Index: /reasoner/mainAlgorithms.tex
===================================================================
--- /reasoner/mainAlgorithms.tex	(revision 190)
+++ /reasoner/mainAlgorithms.tex	(revision 191)
@@ -17,9 +17,10 @@
 \newcommand\relevantConstraintsPerDeclaration[0]{r_d}
 \newcommand\relevantConstraintVariables[0]{r_c}
-\newcommand\scopeAssignments[0]{a}
+\newcommand\scopeAssignments[0]{asngs}
 %\newcommand\usedVariables[0]{u}
-\newcommand\problemRecords[0]{m}
-
-The reasoner performs forward reasoning, i.e., it identifies relevant constraints according to the reasoning mode, translates the constraints, maintains relations among constraints and model elements, evaluates the translated constraints in a loop until all constraints are processed and adjusts the constraint set upon variable value changes.  Figure \ref{figStructure} shows the call graph of the reasoner algorithms and the sections where we will discuss them in more detail. Some algorithms may be involved in a recursion due to the potentially recursive structure of complex IVML types, in particular nested compounds or containers. Algorithms \ref{algComposeExpression} and \ref{algAddConstraint} shown in the lower part of Figure \ref{figStructure} may appear disconnected, but they are called by most of the translation algorithms to populate the constraint base and to compose complex constraints from recursive nestings of complex IVML types. 
+\newcommand\problemRecords[0]{plm}
+\newcommand\evaluator[0]{eval}
+
+The reasoner performs forward reasoning, i.e., it identifies relevant constraints according to the reasoning mode, translates the constraints, maintains relations among constraints and model elements, evaluates the translated constraints in a loop until all constraints are processed and adjusts the constraint set upon variable value changes.  Figure \ref{figStructure} shows the call graph of the reasoner algorithms and the sections where we will discuss them in more detail. Some algorithms may be involved in a recursion due to the potentially recursive structure of complex IVML types, in particular nested compounds or containers. Algorithms \ref{algComposeExpression} and \ref{algAddConstraint} shown in the lower part of Figure \ref{figStructure} may appear disconnected, but they are called by most of the translation algorithms to populate the constraint base and to compose complex constraints from recursive nesting of complex IVML types. 
 
 This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the reasoner data structures in Section \ref{sectDataStructures}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, and the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation}. The algorithms for constraint translation will be discussed in detailed in Section \ref{sectTranslation} and the algorithms for re-scheduling constraints in Section \ref{sectTopLevelConstraintsRescheduling}.
@@ -38,6 +39,6 @@
   \SetAlgoLined
   \KwIn{configuration $c$}
-  \KwData{configuration $cfg$, evaluator $e$, scope assignments $\scopeAssignments$, problem records $m$, start time $startTime$, $reuse$ flag, constraint relations $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$, constraint base copy $base_c, base_{\relevantConstraintsPerDeclaration}, base_{\relevantConstraintVariables}$, $projects$ sequence, $hasTimeout$ and $stop$ flags}%, problem records $\problemRecords$
-  \KwResult{Reasoning result $r$}
+  \KwData{configuration $cfg$, evaluator $\evaluator$, scope assignments $\scopeAssignments$, problem records $\problemRecords$, $startTime$, $reuse$ flag, constraint relations $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$, constraint base copy $base_c, base_{\relevantConstraintsPerDeclaration}, base_{\relevantConstraintVariables}$, $hasTimeout$ flag and $stop$ flag}
+  \KwResult{Reasoning result}
   
   $cfg\assng c$\; \label{algMainLoopSetupVar}
@@ -45,5 +46,5 @@
   %evaluator.setResolutionListener(Algorithm \ref{algVarChange})\;
   %evaluator.setScopeAssignments(sAssng)\;
-  $setup(e, cfg, \scopeAssignments)$\; \label{algMainLoopSetupEval}
+  $setup(\evaluator, cfg, \scopeAssignments)$\; \label{algMainLoopSetupEval}
   $startTime = now()$\;\label{algMainLoopStartTime}
   \uIf{$base_c = \undef$}{ \label{algMainLoopFullStart}
@@ -53,6 +54,6 @@
          $base_{\relevantConstraintVariables} = \emptySet{}$\; %map?
      }
-    $projects \assng discoverImports(cfg)$\; \label{algMainLoopDiscover}
-    \ForAll{$p \iterAssng projects \wedge \neg hasTimeout \wedge \neg stop$}{ \label{algMainLoopStart}
+    $prjs \assng discoverImports(cfg)$\; \label{algMainLoopDiscover}
+    \ForAll{$p \iterAssng prjs \wedge \neg hasTimeout \wedge \neg stop$}{ \label{algMainLoopStart}
       $translateConstraints(p)$\; \label{algMainLoopTranslate}
       $evaluateConstraints(p)$\; \label{algMainLoopEvaluate}
@@ -63,29 +64,32 @@
     $\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]$\; 
+       $base \assng base \cup base_c[i]$\; \label{algMainLoopTakeOverConstraints}
        $evaluateConstraints(projects[i])$\;
        $freeze(cfg, projects[i])$\;
      }
   }\label{algMainLoopIncEnd}
-  $r \assng createReasoningResult(m, hasTimeout, stop)$\; \label{algMainLoopResult}
+  \Return $createReasoningResult(\problemRecords, hasTimeout, stop)$\; \label{algMainLoopResult}
   \caption{Main reasoning loop (\IVML{resolve}).}\label{algMainLoop}
 \end{algorithm}
 
-
-For each project $p$, the main loop 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_{\relevantConstraintsPerDeclaration}$ 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}, i.e., the mapping of constraints per declaration $\relevantConstraintsPerDeclaration$ and the mapping between constraint variables and decision variables $\relevantConstraintVariables$, 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.
+For each project $p$, the full reasoning loop translates the constraints in $p$ and populates the global constraint base as a side effect of the constraint translation (line \ref{algMainLoopTranslate}, detailed in Section \ref{sectTopLevelConstraintsTranslation}). If enabled by $reuse$, the constraint translation stores the respective population of constraints in $base_c$ and their relations in $base_{\relevantConstraintsPerDeclaration}$ 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 as side effect a configuration variable, the constraints related to that variable are identified via $\relevantConstraintsPerDeclaration$ or $\relevantConstraintVariables$ for re-scheduling (detailed by Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). As last step for project $p$, the algorithm freezes the actual values according to the (conditional) freeze-block specifications given in $p$ (line \ref{algMainLoopFreeze}). 
+
+In \textbf{incremental reasoning} (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}), it is sufficient to start with known constraint relations for $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$ (lines \ref{algMainLoopResetRelStart}-\ref{algMainLoopResetRelEnd}) and to iterate over all projects stored in $base_c$. For each project in the sequence previously determined in line \ref{algMainLoopDiscover}, the algorithm takes over the respective constraints from $base_c$ into the actual constraint base (keeping so far failing constraints, line \ref{algMainLoopTakeOverConstraints}), and, akin to full reasoning, performs the evaluation of the constraints and the freezing of 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}.} a detailed reasoning result based on recorded evaluation problems (line \ref{algMainLoopResult}). This reasoning result also indicates successful or failed reasoning, i.e., whether the configuration is valid as all constraints are fulfilled, or, in case of failing, whether this is due to timeout or a user-requested cancellation.
 
 \subsection{Data Structures}\label{sectDataStructures}
 
-This section introduces the most important data structures needed to describe the operations of the IVML reasoner, namely the variable mapping structure (Section \ref{sectVarMapping}) and the scope assignments structure (Section \ref{sectScopeAssignments}).
+This section introduces the most important data structures maintained to efficiently realize the operations of the IVML reasoner, namely the variable mapping structure (Section \ref{sectVarMapping}) and the scope assignments structure (Section \ref{sectScopeAssignments}).
 
 \subsubsection{Variable Mapping}\label{sectVarMapping}
 
-During the constraint translation, top-level constraints can directly be evaluated over involved top-level variables. As already mentioned in Section \ref{sectNotationConstraints}, constraints defined on compound slots or indirectly through use of compound instances in containers must be translated before evaluation. The particular issue here is that these constraints can be defined in an IVML model over types (for which no values can be assigned in a configuration) rather than over top-level variables. A solution is to rewrite these constraints by substituting type-local variables by appropriate accessors starting at top-level variables. To manage the various lots and access expressions, the translation utilizes a stack-based data structure, onto which we push/pop a context frame for each IVML project and each contained compound type, container type or combinations of both used in variables of a project. A context frame links all currently relevant variables to the correct accessor expressions, which are created before the respective variable substitutions are applied.
-
-However, a simple stack is not sufficient for two reasons, namely nested complex types, excluded types and assignment blocks. As we will detail below, nested complex types require constraint rewriting through a prefix composed of nested all-quantifiers. Therefore, the stack frames can store the information needed to create the respective quantifier expression. When adding a constraint to the constraint base, we visit the stack frames and, if such information is available, incrementally qualify the expression by the described quantifier. The constraint rescheduling re-uses the constraint transformation. However, performing a complete transformation of all types related to certain value change is typically not needed, so that excluding types from the translation speeds up the re-scheduling operations. 
+During the constraint translation, top-level constraints can directly be evaluated base on involved top-level variables. However, as already mentioned in Section \ref{sectNotationConstraints}, constraints defined on compound slots or indirectly through use of compound instances in containers must be translated before evaluation. The task here is that these constraints can be defined in an IVML model on (complex) types, i.e., on all instances of that type, rather than (top-level) variables. A solution is to rewrite these constraints before reasoning by substituting nested variables through appropriate accessor (path) expressions starting at respective top-level variables. 
+
+We utilize a stack-based data structure, the \textbf{variable mapping} $\variableMapping$, to manage slots and their related access expressions. $\variableMapping$ contains a context frame for each IVML project and each contained complex type (compound type, container type or combination of both) used for declaring variables in the project. A context frame links all relevant variables to their respective accessor expressions. The accessor expressions are created and related to the variables in one step before the respective variable substitutions are applied.
+
+However, a simple stack is not sufficient due to nested complex types and structures such as assignment blocks. As we will detail below, nested complex types require constraint rewriting through a prefix composed of nested all-quantifiers. Therefore, the stack frames stores the information needed to create the respective quantifier expression. When adding a constraint to the constraint base, we visit the stack frames and, if such information is available, incrementally qualify the expression by the described quantifier. 
+
+Moreover, the constraint rescheduling also applies the constraint transformation, in particular if values or constraint variables change in a way that additional constraints become relevant during reasoning. Then, performing a complete transformation of all types related to certain value change is inefficient, so that excluding certain types from the translation speeds up the re-scheduling. Therefore, the context frames can also manage excluded types used for constraint transformation during re-scheduling.
 %Moreover, IVML projects and compounds can contain nested assignment blocks. An assignment block implicitly defines assignment constraints for its contained variable declarations including containers or compounds. If we translate first variable declarations and then the related constraints, these constraints are outside their actual scope and, thus, relevant access expressions are not available, i.e., wrong constraints would be added to the constraint bae. Intermingling compund/container translation with annotation-block translation would be a potential solution, which increases the algorithm / code complexity. Thus, we opted to register a declaration with its context frame (which is then implicitly registered with its parent frame for proper cleanup) and to activate/deactivate such a frame, although it is not on top of the stack, when translating the implicit assignment constraints in an assignment block. Such stack frames are also removed from the stack when popping the respective parent context frame.
 
@@ -95,23 +99,24 @@
 %    \item $setRegisterContexts(\variableMapping, b)$ enables automatic registration of context frames within the parent frame. The operation returns the previous state of the registration flag.
 %    \item $isContextsRegistering(\variableMapping)$ returns whether new context frames are automatically registered with the parent frame.
-    \item $pushContext(\variableMapping, d, r)$ creates and pushes a new context frame for declaration $d$ to the stack. If registration of contexts is enabled, $r$ indicates whether the new frame shall be registered with the parent frame and whether already processed types (for handling nested complex types) shall be recorded by this context.
-    \item $pushContext(\variableMapping, d, c,v, r)$ works like $pushContext(\variableMapping, d, r)$, but registers also information for creating an all-quantified constraint prefix for all constraints added to the constraint base as long this frame is on the stack. The information includes the container expression $c$ and the typed iterator variable $v$ over the element type of $c$. We will apply this function in Section \ref{sectContainerDefaults}.
-    \item $popContext(\variableMapping)$ removes the top-most context frame. The initial frame, which is created by default and devoted to the enclosing IVML project, is not removed by this operation.
-    \item $registerMapping(\variableMapping, d, ca)$ registers the access expression $ca$ with the given variable declaration $d$ in the top-most context frame. Essentially, a context frame contains a mapping $m$ and the operation performs $m \assng m \addMap \mapEntry{d}{ca}$.
-    \item $getMapping(\variableMapping, d)$ returns the mapping for $d$ (for short $\variableMapping[d]$). If no mapping was registered for the actual context frame, all context frames in stack order are considered. If no mapping is registered, the result is $\undef$.
-    \item $getLocalMapping(\variableMapping, n)$ returns the mapping for variable / slot name $n$ within the actual context frame. If there is no registration, the result is $\undef$.
-    \item $recordProcessed(\variableMapping, t)$ records a processed type with the closest containing context having processed type registration enabled. If \linebreak[4] $isCompound(t)$, this function registers $allRefined^+(t)$.
-    \item $alreadyProcessed(\variableMapping, t)$ returns whether $t$ was already registered as a processed type in one of the enclosing context frames.
+    \item $size(\variableMapping)$ returns the number of context frames on the stack. There is always at least one frame on the stack representing the actual IVML project. This frame is pushed automatically when creating $\variableMapping$.
+    \item $clear(\variableMapping)$ clears the stack and cleans up the context frame dedicated to the actual IVML project so that $\variableMapping$ can be re-used for translating the next project.
+    \item $pushContext(\variableMapping, d, r)$ creates and pushes a new context frame for declaration $d$ onto the stack. For handling nested complex types, $r$ indicates whether the new frame shall be registered with the parent frame so that information about already processed types is not recorded in the top context rather than its parent context.
+    \item $pushContext(\variableMapping, d, c,v, r)$ works like $pushContext(\variableMapping, d, r)$, but supports creating constraints for nested container types. As long as the created frame is on the stack, all constraints added to the constraint base are automatically quantified by an all-quantor for the typed iterator variable $v$ over the container expression $c$. %We will apply this function in Section \ref{sectContainerDefaults}.
+    \item $popContext(\variableMapping)$ removes the top frame from the stack. The frame representing the actual IVML project is not removed by this operation.
+    \item $registerMapping(\variableMapping, d, e)$ relates access expression $e$ to variable declaration $d$ in the top context frame. Essentially, a context frame contains a mapping $m$ and the operation performs $m \assng m \addMap \mapEntry{d}{e}$.
+    \item $getMapping(\variableMapping, d)$ returns the mapping for $d$ (for short $\variableMapping[d]$), by first considering the top frame and, if there is no mapping, also the other frames in stack order. Returns $\undef$ if no mapping was found.
+    \item $getLocalMapping(\variableMapping, n)$ returns the mapping for variable/slot name $n$ from the top context frame. Returns $\undef$ if there is no such mapping.
+    \item $recordProcessed(\variableMapping, t)$ records a processed type in the closest containing context in stack order for which the registration of processed types is enabled. If  $isCompound(t)$, all types in $allRefined^+(t)$ are registered implicitly.
+    \item $alreadyProcessed(\variableMapping, t)$ returns whether $t$ was already registered as a processed type in one of the context frames.
 %    \item $activate(\variableMapping, d)$ re-activates, i.e., pushes the registered stack frame for $d$ taken from the current context frame. As long as the current context frame exists, this operation can be called again and again. If no context frame is registered for $d$, the stack is not modified.
 %    \item $deactivate(\variableMapping, d)$ de-activates the registered context frame for $d$, i.e., pops it from the stack but leaves it registered with its parent context frame so that it is available for further activations as long as the parent context frame exists on the stack. 
-    \item $setTypeExcludes(\variableMapping, s)$ defines a set of types to be marked as excluded from constraint transformations. Excluding types is important for a fast processing of re-scheduled constraints in Section \ref{sectTopLevelConstraintsRescheduling}.
-    \item $transferTypeExcludes(\variableMapping, t)$ transfers excluded types into this context and stores the causing type $t$ in the current context. Transferring excluded types binds them to the actual (usual top-most) type and avoids applying them some nested type.
-    \item $currentType(\variableMapping)$ returns the type $t$ stored in the current context by $transferTypeExcludes(\variableMapping, t)$. The result is $\undef$ if no transfer happened for the current context.
-    \item $isTypeExcluded(\variableMapping, t)$ returns whether $t$ is excluded in the current context. $excludedTypes(\variableMapping)$ returns all excluded types for the current context or an empty set.
-    \item $size(\variableMapping)$ the number of contexts on the stack. There is always at least one context on the stack representing the enclosing project.
-    \item $clear(\variableMapping)$ clears the stack and cleans up the default context frame dedicated to the IVML project so that $\variableMapping$ is ready for the translation of the next IVML project.
+    \item $setTypeExcludes(\variableMapping, s)$ marks the set $s$ of types as excluded from constraint transformations. Excluding types is important for efficient constraint re-scheduling as discussed in Section \ref{sectTopLevelConstraintsRescheduling}.
+    \item $isTypeExcluded(\variableMapping, t)$ returns whether $t$ is marked as excluded in the top context frame. 
+    \item $excludedTypes(\variableMapping)$ returns all types marked in the top context frame. The result may be an empty set.
+    \item $transferTypeExcludes(\variableMapping, t)$ moves excluded types from enclosing context frames to the top frame. Also stores the current (causing) type $t$ in the top frame. Transferring excluded types binds them to the top-most type and prevents applying them to a nested type.
+    \item $currentType(\variableMapping)$ returns the current type $t$ from the top frame. The result is either $\undef$ or was set before by $transferTypeExcludes(\variableMapping, t)$.
 \end{itemize}
 
-From a black-box perspective, $\variableMapping$ can be considered as a usual map as discussed in Section \ref{sectGeneralNotation}, but performing some stack-based lookup operations. Thus, we just use $\variableMapping$ in the variable substitution notation as introduced in Section \ref{sectNotationConstraints}, e.g., let $e$ be an expression, then $\varSubstitutionVarMapping{e}$ replaces all variables in $e$ having a mapping (through the $getMapping$ operation) in at least on context frame of $\variableMapping$. 
+In the $\variableMapping$ data structure, there are visible mappings (accessible through the $getMapping$ operation), but there may also be hidden mapping entries in context frames on lower stack positions. Thus, from a black-box perspective, $\variableMapping$ can be considered as a mapping of variable declarations to access expressions. Consequently, based on only visible entries, we can use $\variableMapping$ to specify variable substitutions (as defined for ordinary mappings in Section \ref{sectNotationConstraints}). For example, let $e$ be an expression, then $\varSubstitutionVarMapping{e}$ replaces all variables in $e$ having a visible mapping entry in at least one context frame of $\variableMapping$. 
 
 %For translating containers, context frames can store additional information. We will provide details along with the translation of containers in Section \ref{sectContainerDefaults}.