Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 9)
+++ /reasoner/reasoner.tex	(revision 9)
@@ -0,0 +1,140 @@
+\documentclass[12pt]{article}
+\usepackage{amsmath}
+\usepackage{multirow}
+\usepackage{color}
+\usepackage[ruled, vlined]{algorithm2e}
+
+\newcommand\TBD[1]{{\color{red}TBD: #1}}
+\newcommand\IVML[1]{\texttt{TBD: #1}}
+
+
+\begin{document}
+
+\title{SSE reasoner}
+\date{}
+\maketitle
+
+This is a summary of the implemented reasoning algorithm of the SSE reasoner as a basis for checking completeness against the IVML specification and correctness of the reasoning. Changes to the implementation shall be reflected here and vice versa.
+
+\section{Notation/Terminology}
+
+
+\begin{itemize}
+  \item An access expression specifies slots (within compounds or behind references) or elements (within a collection) to be accessed. Examples: \IVML{cmp.slot}, \IVML{cmp.slot1.slot2}, \IVML{coll[1]}, \IVML{coll[1].slot}.
+  \item $\perp$ is the undefined constraint
+  \item $name(s)$ is the default value expression of slot $s$
+  \item $default(s)$ is the default value expression of slot $s$
+  \item $elements(c)$ is the set of all element values in a collection
+  \item $isNested(c)$ whether a collection is a nested collection
+  \item $refines(c)$ is the set of all compounds refining $c$ (excluding $c$), $refines^+(c)=refines(c) \cup \{c\}$ i; both empty if not compound
+  \item $dfltSlots(v) = \{s|s\in slots(v) \wedge default(s) \neq \perp\}$, empty for all non-compound types
+\end{itemize}
+
+\section{Reasoning algorithm}
+
+The reasoner performs forward reasoning, i.e., it identifies all constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes. 
+
+For IVML, the reasoner must take the structure of IVML models into account, i.e., in particular IVML projects. An IVML projects constitutes a reasoning scopes, i.e., no duplicated variable assignment must occur within a project. Moreover, a project acts as search space for dynamic dispatch of user-defined operations. The main reasoning loop over the involved IVML projects for a given configuration $cfg$ is shown in Algorithm \ref{algMainLoop}. 
+
+Relevant IVML projects are identified throgh the (potentially cyclic) import structure performing a depth-first search starting with the top-level project of a configuration. $discoverProjects(cfg)$ returns a sequence of IVML projects for $cfg$ listing the projects with less import dependencies first. Following this sequence, Algorithm \ref{algMainLoop} first identifies the constraints determining default values, then the remaining constraints and registers the constraints with the respective variables. The constraints are added to the constraint $base$ in this sequence to ensure that variables are properly initialized before other constraints are considered. We will discuss the relevant expressions, constraints and their transformations in detail in Section \ref{sectConstraintTranslation}. 
+
+Following this sequence, the $evaluate(base)$ functions (cf. Algorithm \ref{algEvalLoop}) evaluates each constraint in $base$ in sequence until no more (failing) constraints are available. If a constraint changes a configuration variable as a side effect, the constraints related to that variable are re-scheduled for evaluation by Algorithm \ref{algVarChange}.
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwData{configuration $cfg$, boolean $incremental$ \TBD{inc?}}
+  \KwResult{Reasoning result $r$}
+  $projects \leftarrow$ discoverImports(cfg)\;
+  \For{$p \leftarrow projects$}{
+      $base \leftarrow collectDefaults(p)$\;
+      $base \leftarrow base \uplus collectConstraints(p)$\;
+      $evaluate(base)$\;
+      $freeze(p)$\;
+  }
+ \caption{Main reasoning loop.}\label{algMainLoop}
+\end{algorithm}
+
+\TBD{Evaluation loop}
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwData{decision variable $v$, constraint $base$}
+  \KwResult{Changed constraint $base$}
+  \If{$\neg isLocal(v)$}{
+      \TBD{fill}\;
+  }
+ \caption{Constraint evaluation loop.}\label{algEvalLoop}
+\end{algorithm}
+
+\TBD{Variable change}
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwData{decision variable $v$, constraint $base$}
+  \KwResult{Changed constraint $base$}
+  \If{$\neg isLocal(v)$}{
+      \TBD{fill}\;
+  }
+ \caption{Modification of constraint base upon variable change.}\label{algVarChange}
+\end{algorithm}
+
+\section{Constraint translation}\label{sectConstraintTranslation}
+
+\subsection{Default constraints}
+
+IVML allows defining default value expressions for all variables including top-level project variables as well as compound slots. From the perspective of IVML and its object model, a default value is part of a variable declaration, i.e., per se not a constraint, i.e., the syntax
+
+\texttt{Type variable = expression;}
+
+must be translated into a constraint $variable = expression$. Expressions may be simple variables, calculations or operation calls, in compounds also using the predefined variable \texttt{self} indicating the actual instance of the respective compound. These constraints must be evaluated upon each variable instantiation, i.e., for top-level basic variables, top-level compound variables, compound values within compounds as well as compound values within container initialiers, each potentially with a different access expression to make the variable unique. 
+
+\subsubsection{Compound default constraints}
+
+\subsubsection{Collection default constraints}\label{deflt_collections}
+
+Constraints defined on types that are implicitly instantiated within a collection must be turned into individual constraints and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables.
+
+\TBD{What about typedefs/derived?}
+
+\begin{itemize}
+\item \textbf{Parameter:} collection $c$ 
+
+\item \textbf{Elements:} $elts = \bigcup_{v\in\{refines^+(c)|c \in elements(c) \}} : dfltSlots(v)$
+
+\item \textbf{Transformation ($s\in elts$):} $\langle flatten(c)\rightarrow forAll(i|assng(i.\bf{name(s)}, \bf{default(s)}|_{self=i}\rangle$
+
+\item \textbf{Optimization:} Replace $flatten(c)$ by $\left.\begin{cases}flatten(c), & \text{if } isNested(c) \\ c, &\text{else}\end{cases}\right\}$ to save an unneeded operation in case of non-nested collections.
+\end{itemize}
+
+\subsection{Other constraints}
+
+\section{Completeness}
+
+\begin{table*}[t]
+\centering
+\begin{tabular}{|l|c||l|c|}
+\hline
+\textbf{IVML concept} & \textbf{Spec} & \textbf{Reasoner transformation} & \textbf{Section}\\
+\hline
+ \multicolumn{4}{|c|}{Default expressions}\\
+\hline
+Basic variable & & & \\
+Derived type variable & & & \\
+Enum variable & & & \\
+Compound variable & & & \\
+Container variable & & & \ref{deflt_collections} \\
+Reference variable & & & \\
+Constraint variable & & & \\
+\hline
+ \multicolumn{4}{|c|}{Constraints}\\
+\hline
+Top-Level constraint & & & \\
+Compound constraint & & & \\
+\hline
+\end{tabular}
+\caption{IVML concepts vs. reasoning constraint transformations.}
+\label{tab:IVMLReasoner}
+\end{table*}
+
+
+\end{document}