Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 9)
+++ /reasoner/reasoner.tex	(revision 10)
@@ -6,5 +6,5 @@
 
 \newcommand\TBD[1]{{\color{red}TBD: #1}}
-\newcommand\IVML[1]{\texttt{TBD: #1}}
+\newcommand\IVML[1]{\texttt{#1}}
 
 
@@ -29,4 +29,5 @@
   \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
+  \item assignment states
 \end{itemize}
 
@@ -39,28 +40,49 @@
 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}.
+Following this sequence, the $evaluateConstraints$ function (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}. Finally, the main reasoning algorithm composes a structured reasoning result based on persisting recorded evaluation problems.
 
 \begin{algorithm}[H]
   \SetAlgoLined
-  \KwData{configuration $cfg$, boolean $incremental$ \TBD{inc?}}
+  \KwIn{configuration $cfg$, boolean $incremental$ \TBD{inc?}}
+  \KwData{problem records $m$}
   \KwResult{Reasoning result $r$}
   $projects \leftarrow$ discoverImports(cfg)\;
   \For{$p \leftarrow projects$}{
+      %evaluator.init()\;
+      %evaluator.setResolutionListener(Algorithm \ref{algVarChange})\;
+      %evaluator.setScopeAssignments(sAssng)\;
       $base \leftarrow collectDefaults(p)$\;
       $base \leftarrow base \uplus collectConstraints(p)$\;
-      $evaluate(base)$\;
+      $evaluateConstraints(p, base)$\;
       $freeze(p)$\;
+      %evaluator.clear()\;
   }
- \caption{Main reasoning loop.}\label{algMainLoop}
+  $r \leftarrow createReasoningResult(m)$
+  \caption{Main reasoning loop.}\label{algMainLoop}
 \end{algorithm}
 
-\TBD{Evaluation loop}
+The main constraint evaluation loop ($evaluate(p, base)$) is summarized in Algorithm \ref{algEvalLoop}. It heavily relies on the IVML constraint evaluation mechanism, an expression evaluator for IVML expressions based on a given IVML configuration. 
+
+First, the main constraint evaluation loop clears recorded information about the assignments done so far so that the actual scope $p$ is clear. Then it sets the scope for dynamic dispatch of user-defined IVML operations. The algorithm runs as long as there are constraints in the constraint $base$, assuming that the evaluation either terminates as all constraints are successfully evaluated (and value changes may add new constraints, cf. Algorithm \ref{algVarChange}) or constraints fail and do not add further constraints. For each iteration, the algorithm pops a constraint for evaluation from $base$ and clears the records about used variables. Then it sets the actual assignment state of the constraint evaluator. If $c$ is a default constraint, this causes that the subsequent value assignments during the evaluation of $c$ 
+are done with state \IVML{DEFAULT}, else state \IVML{DERIVED}. 
+
+Finally, each constraint is evaluated. If configuration variables are changed as part of the constraint evaluation, the changed variables are recorded in $u$ (not shown in Algorithm \ref{algVarChange}). Finally, the evaluation result is analyzed and may lead to further problem records, e.g., duplicate variable assignments etc. Here, we distinguish three cases. 
+\begin{enumerate}
+  \item The constraint is evaluated successfully so that existing problem records can be removed from $m$. 
+  \item The constraint is evaluated as undefined. As defined by IVML, a constraint for which not all variables or expressions can be evaluated, is considered undefined, but evaluated. This does not lead to a problem record, as the constraint can either be ignored or will be re-scheduled if one of the (undefined) variables is changed through another constraint. 
+  \item The constraint evaluation fails and a problem record is created including the used variables $u$ for detailed error reporting or further (external) analysis. 
+\end{enumerate}
 
 \begin{algorithm}[H]
   \SetAlgoLined
-  \KwData{decision variable $v$, constraint $base$}
-  \KwResult{Changed constraint $base$}
-  \If{$\neg isLocal(v)$}{
-      \TBD{fill}\;
+  \KwIn{project $p$, constraint $base$}
+  \KwData{problem records $m$, used variables $u$, constraint evaluator $e$}
+    $clearScopeAssignments(p)$\;
+    $setDispatchScope(p)$\; %evaluator.setDispatchScope
+    \While {$|base| > 0$} {
+        $c \leftarrow pop(base)$\;
+        $clear(u)$\;
+        $setAssignmentState(e, isDefault(c))$\; 
+        $m \leftarrow m \uplus analyzeEvaluationResult(evaluate(e, c), u)$\;
   }
  \caption{Constraint evaluation loop.}\label{algEvalLoop}
@@ -71,5 +93,5 @@
 \begin{algorithm}[H]
   \SetAlgoLined
-  \KwData{decision variable $v$, constraint $base$}
+  \KwIn{decision variable $v$, constraint $base$}
   \KwResult{Changed constraint $base$}
   \If{$\neg isLocal(v)$}{