Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 134)
+++ /reasoner/reasoner.tex	(revision 135)
@@ -434,5 +434,5 @@
   \SetAlgoLined
   \KwIn{configuration $cfg$}
-  \KwData{problem records $\problemRecords$, scope assignments $\scopeAssignments$, expression evaluator $e$, reasoning start time $startTime$, flags $hasTimeout$ and $stop$, $resue$ instance flag, $projects$ sequence, relevant constraints $\relevantConstraintsPerType$ and $\relevantConstraintVariables$, constraint base copy $base_c, base_{\relevantConstraintsPerType}, base_{\relevantConstraintVariables}$}
+  \KwData{expression evaluator $e$, scope assignments $\scopeAssignments$, start time $startTime$, $reuse$ flag, constraint base copy $base_c, base_{\relevantConstraintsPerType}, base_{\relevantConstraintVariables}$, $projects$ sequence, $hasTimeout$ and $stop$ flags, constraints relations $\relevantConstraintsPerType$ and $\relevantConstraintVariables$, problem records $\problemRecords$}
   \KwResult{Reasoning result $r$}
   
@@ -455,11 +455,10 @@
     } \label{algMainLoopEnd}\label{algMainLoopFullEnd}
   }\Else {\label{algMainLoopIncStart}
-    $\relevantConstraintsPerType \assng base_{\relevantConstraintsPerType}$\;
-    $\relevantConstraintVariables \assng base_{\relevantConstraintVariables}$\;
+    $\relevantConstraintsPerType \assng base_{\relevantConstraintsPerType}$\;\label{algMainLoopResetRelStart}
+    $\relevantConstraintVariables \assng base_{\relevantConstraintVariables}$\;\label{algMainLoopResetRelEnd}
     \ForAll{$i \in \set{0, \ldots, |base_c|} \wedge \neg hasTimeout \wedge \neg stop$}{
        $base \assng base_c[i]$\; 
-       $p \assng projects[i]$\;
-       $evaluateConstraints(p)$\;
-       $freeze(cfg, p)$\;
+       $evaluateConstraints(projects[i])$\;
+       $freeze(cfg, projects[i])$\;
      }
   }\label{algMainLoopIncEnd}
@@ -468,13 +467,13 @@
 \end{algorithm}
 
-First, Algorithm \ref{algMainLoop} sets up\footnote{In the implementation, the listener for changed variables triggering constraint re-scheduling (Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) as well as recording of assigned variables are registered with the expression evaluator. These details are omitted here.} the expression evaluator in line \ref{algMainLoopSetupEval} for use with the configuration $cfg$ and the scope assignments $\scopeAssignments$. The remainder of the algorithm is separated into two parts, the full execution (lines \ref{algMainLoopFullStart}-\ref{algMainLoopFullEnd}), and the incremental part (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}) utilizing a constraint base prepared and stored while running the first part.
-
-For IVML, the full execution of the reasoner\footnote{In the implementation, translation and reasoning happen in \class{Resolver.java}.} must take the structure of IVML models into account, i.e., in particular IVML projects and their imports. As shown in Algorithm \ref{algMainLoop}, first structures are created to store constraints for reuse (if $reuse$ is enabled), here for copying the constraint base ($base_c$), the relevant constraints per type ($base_{\relevantConstraintsPerType}$) and the relevant constraint variables per decision variable ($base_{\relevantConstraintVariables}$). Then, the relevant IVML projects and their sequence are identified. Therefore, $discoverProjects(cfg)$ (line \ref{algMainLoopDiscover}, not further detailed in this document), performs a depth-first traversal of the import structure, ignores already seen cyclic imports and returns a sequence of all projects involved in $cfg$ according to the increasing number of import dependencies. 
-
-Following this sequence, the main reasoning loop considers all IVML projects for a given configuration $cfg$, as long as no timeout occurred (global flag $hasTimeout$) or the user requested a stop of the reasoning operations (global flag $stop$). Further, the algorithm records the start time in line \ref{algMainLoopStartTime} in order to be able to detect timeouts. 
-
-For each project $p$, the main loop (lines \ref{algMainLoopStart} - \ref{algMainLoopEnd}) translates the constraints in $p$ (and populates the constraint base as a side effect, line \ref{algMainLoopTranslate} discussed / Section \ref{sectTopLevelConstraintsTranslation}) and performs the forward-chaining evaluation of the constraint base, i.e., for $p$, in line \ref{algMainLoopEvaluate} / Section \ref{sectTopLevelConstraintsEvaluation}. 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}. As last step for a project $p$, the algorithm freezes the actual values according to the (conditional) freeze-block specifications in $p$ in line \ref{algMainLoopFreeze}. Finally, after all projects have been considered or the main reasoning loop has been terminated prematurely, the main reasoning algorithm composes\footnote{In the implementation, this is done in \class{Engine.java}, the actual reasoner instance, which creates and utilizes instances of \class{Resolver.java}.} a detailed reasoning result based on persisting recorded evaluation problems in line \ref{algMainLoopResult}. This reasoning result also includes whether a timeout or a user-requested cancellation of the reasoning occurred.
-
-In incremental execution (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}), it is sufficient to take over the constraints for the respective project into the constraint base, and, as before, to evaluate the constraints and to freeze the variables. Before starting an incremental execution, it is necessary to clear global storages required by the implementation (but not detailed here), such as error data structures, counters, etc.
+First, Algorithm \ref{algMainLoop} sets up\footnote{In the implementation, the listener for changed variables triggering constraint re-scheduling (Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) as well as recording of assigned variables are registered with the expression evaluator. These details are omitted here.} the expression evaluator in line \ref{algMainLoopSetupEval} for use with the configuration $cfg$ and the scope assignments $\scopeAssignments$. In line \ref{algMainLoopStartTime} it stores the start time to terminate potentially endless loops induced by ping-pong assignments among constraints within a given maximum time. The remainder of the algorithm is separated into two parts, the full execution (lines \ref{algMainLoopFullStart}-\ref{algMainLoopFullEnd}), and the incremental part (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}) utilizing a constraint base prepared and stored while running the first part.
+
+As shown in Algorithm \ref{algMainLoop}, first structures are created to store constraints for reuse (if $reuse$ is enabled), here for copying the constraint base ($base_c$), the relevant constraints per type ($base_{\relevantConstraintsPerType}$) and the relevant constraint variables per decision variable ($base_{\relevantConstraintVariables}$). Then,  the reasoner\footnote{In the implementation, translation and reasoning happen in \class{Resolver.java}.} must take the structure of IVML models into account, which is determined by the top-level IVML project making up $cfg$ and a cycle-free traversal of the imports of the top-level project. $discoverProjects(cfg)$ (line \ref{algMainLoopDiscover}, not further detailed in this document), performs a depth-first traversal of the import structure, ignores already seen cyclic imports and returns the processing sequence of all projects involved in $cfg$, i.e., the imported projects sorted in ascending manner according to their number of import dependencies. The main reasoning loop processes this project sequence as long as no timeout occurred (global flag $hasTimeout$) or the user requests a stop of the reasoning (global flag $stop$).
+
+For each project $p$, the main loop (lines \ref{algMainLoopStart} - \ref{algMainLoopEnd}) translates the constraints in $p$ and populates the constraint base as a side effect of the constraint translation called in line \ref{algMainLoopTranslate} (detailed in Section \ref{sectTopLevelConstraintsTranslation}). If enabled through $reuse$, the constraint translation stores the respective population of constraints in $base_c$ and their relations in $base_{\relevantConstraintsPerType}$ and $base_{\relevantConstraintVariables}$. Then the algorithm performs a forward-chaining evaluation of the constraint base in line \ref{algMainLoopEvaluate} (explained in Section \ref{sectTopLevelConstraintsEvaluation}). If a constraint changes a configuration variable as a side effect, the constraints related to that variable are re-scheduled for evaluation (detailed by Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). As last step for a project $p$, the algorithm freezes the actual values according to the (conditional) freeze-block specifications in $p$ in line \ref{algMainLoopFreeze}. 
+
+In incremental execution (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}), it is sufficient to reset the constraint relations in lines \ref{algMainLoopResetRelStart}-\ref{algMainLoopResetRelEnd}, to iterate over all stored projects in $base_c$. For each project, the algorithm takes over the respective constraints from $base_c$  into the actual constraint base, and, as before, evaluates the constraints and freezes the variables.
+
+Finally, after all projects have been considered or the main reasoning loop has been terminated prematurely, the algorithm composes\footnote{In the implementation, this is done in \class{Engine.java}, the actual reasoner instance, which creates and utilizes instances of \class{Resolver.java}.} in line \ref{algMainLoopResult} a detailed reasoning result based on recorded evaluation problems. This reasoning result also indicates a successful or failed execution, in particular whether a timeout occurred or a user-requested cancellation was requested.
 
 \subsection{Data Structures}\label{sectDataStructures}