Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 46)
+++ /reasoner/reasoner.tex	(revision 47)
@@ -107,5 +107,5 @@
 An IVML \emph{variable declaration} $d$ specifies a variable with $name(d)$ and $type(d)$.~$default(d)$ is an expression specifying the default value of $d$, whereby $default(d)$ must evaluate to a type compatible with $type(d)$. Further, $parent(d)$ is the model element the declaration $d$ is nested within, typically, a compound or a project. Moreover, $annotations(d)$ denotes the set of (orthogonal) IVML annotation (variable) declarations for $d$. 
 
-\subsubsection{Configuration Variables}
+\subsubsection{Configuration Variables}\label{sectNotationConfigVars}
 
 An IVML \emph{configuration variable} $v$ is an instance of a variable declaration $d$ as part of a certain configuration $cfg$, i.e., $decision(cfg, d)=v$. For such a combination of declaration $d$ and variable $v$, we define $declaration(v) = d$ as well as $type(v) = type(declaration(v))$. For a variable $v$, the function $isVariable(v)$ returns $true$, for any other IVML element/type $false$.
@@ -131,5 +131,5 @@
 Variables can be \emph{local}, e.g., as specified in the IVML model used as parameters of a user-defined constraint function, within let-expression or as collection iterator. Such variables have the same properties as usual configuration variables and can be identified using $isLocal(v)$, which then returns $true$.
 
-Due to the specific semantics of default or frozen variables, IVML variables have an internal state. The state of individual variables is actually changed (indirectly) by the expression evaluator as side effect of constraint evaluation. The following states are defined:
+Due to the specific semantics of default or frozen variables, IVML variables have an internal \emph{assignment state}. The state of individual variables is actually changed (indirectly) by the expression evaluator as side effect of constraint evaluation. The following states are defined:
 
 \begin{itemize}
@@ -259,13 +259,18 @@
 \newcommand\relevantConstraints[0]{r_t}
 
-The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), translates the constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes.  This section introduces the top-level reasoning algorithms, while the constraint translation will be discussed in detailed in Section \ref{sectTranslation}.
+The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), translates the constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes.  This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation} and the re-scheduling of constraints while evaluation in Section \ref{sectTopLevelConstraintsRescheduling}. The constraint translation will be discussed in detailed in Section \ref{sectTranslation}.
+
+\subsection{Main Reasoning Loop}\label{sectTopLevelMainReasoningLoop}
+
+The main reasoning loop implements the overall control for the IVML reasoning process. For IVML, the reasoner\footnote{In the implementation, constraint translation and reasoning happens in the class \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 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. 
 
 \begin{algorithm}[H]
   \SetAlgoLined
   \KwIn{configuration $cfg$}
-  \KwData{problem records $m$, global flags $hasTimeout$ and $stop$}
+  \KwData{problem records $m$, reasoning start time $startTime$, global flags $hasTimeout$ and $stop$}
   \KwResult{Reasoning result $r$}
   
   $projects \assng discoverImports(cfg)$\; \label{algMainLoopDiscover}
+  $startTime = now()$\;\label{algMainLoopStartTime}
   \ForAll{$p \iterAssng projects \wedge \neg hasTimeout \wedge \neg stop$}{ \label{algMainLoopStart}
       %evaluator.init()\;
@@ -276,10 +281,13 @@
       $freeze(p)$\; \label{algMainLoopFreeze}
   } \label{algMainLoopEnd}
-  $r \assng createReasoningResult(m)$\; \label{algMainLoopResult}
+  $r \assng createReasoningResult(m, hasTimeout, stop)$\; \label{algMainLoopResult}
   \caption{Main reasoning loop (\IVML{resolve}).}\label{algMainLoop}
 \end{algorithm}
 
-
-For IVML, the reasoner\footnote{In the implementation, constraint translation and reasoning happens in the class \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 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$). 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}) and performs the forward-chaining evaluation of the constraint base, i.e., for $p$, in line \ref{algMainLoopEvaluate}. 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 step happens in the class \class{Engine.java}, the actual reasoner instance, which utilizes and calls instances of \class{Resolver.java}.} a detailed reasoning result based on persisting recorded evaluation problems in line \ref{algMainLoopResult}.
+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 step happens in the class \class{Engine.java}, the actual reasoner instance, which utilizes and calls 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.
+
+\subsection{Top-level Constraints Translation}\label{sectTopLevelConstraintsTranslation}
 
 Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. In line \ref{algTranslateConstraintsClearMapping}, algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$. The variable mapping is a core data structure of the constraint translation and specific for the project under translation, i.e., mappings for other already processed projects are not needed.  
@@ -289,80 +297,80 @@
 \begin{algorithm}[H]
   \SetAlgoLined
-  \KwIn{project $p$, relevant constraints $\relevantConstraints$ \TBD{??}, incremental $inc$}
-  \KwData{constraint $base$ , variable mapping $\variableMapping$}
+  \KwIn{project $p$}
+  \KwData{constraint $base$ , variable mapping $\variableMapping$, relevant constraints $\relevantConstraints$, incremental mode flag $inc$}
 
    $\variableMapping \assng \setEmpty$\; \label{algTranslateConstraintsClearMapping} 
    %>ConstraintTranslationVisitor
-   \ForAll{$d \iterAssng varDeclarations(p)$}{ %translateDeclarationDefaults
+   \ForAll{$d \iterAssng varDeclarations(p)$}{ \label{algTranslateConstraintsTranslationStart} %translateDeclarationDefaults
         $translateDeclarationDefaults(d, decision(cfg, d), \undef, inc)$\;
     }
-   $add(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)} \addSeq constraints(p), true)$\;
+   $add(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)} \addSeq constraints(p), true)$\; \label{algTranslateConstraintsAdd} 
    \ForAll{a \iterAssng assignments(p)}{
       $translateAnnotationAssignments(a, \undef, \undef)$\;
-   }
+   } \label{algTranslateConstraintsTranslationEnd}
    %<ConstraintTranslationVisitor
-  $base \assng \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \topLevelConstraints \addSeq \otherConstraints$\;
-   $\defaultConstraints \assng \setEmpty$\;
+  $base \assng base \addSeq \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \topLevelConstraints \addSeq \otherConstraints$\; \label{algTranslateConstraintsCompose}
+   $\defaultConstraints \assng \setEmpty$\; \label{algTranslateConstraintsClearSetsStart}
    $\deferredDefaultConstraints \assng \setEmpty$\;
    $\topLevelConstraints \assng \setEmpty$\;
-   $\otherConstraints \assng \setEmpty$\;
+   $\otherConstraints \assng \setEmpty$\; \label{algTranslateConstraintsClearSetsEnd}
 
  \caption{Translating constraints (\IVML{translateConstraints}).}\label{algTranslateConstraints}
 \end{algorithm}
 
-
-Then, the algorithm identifies and translates the constraints in the respective project\footnote{The top-translation steps in this algorithm are realized in the implementation by an IVML model visitor implicitly identifying and handling the types without iterating over the project multiple times as the notation here might suggest.}. To separate and prioritize the constraints, the reasoner uses several global sets, which are populated independently during the constraint translation and, in Algorithm ref \ref{algTranslateConstraints} added to the constraint base. In more details, the reasoner maintains the following constraint sets 
-
-\TBD{Here}
-
+Then, the algorithm identifies and translates the constraints in the respective project\footnote{The top-translation steps in this algorithm are realized in the implementation by an IVML model visitor implicitly identifying and handling the types without iterating over the project multiple times as the notation here might suggest.}. To separate and prioritize the constraints, the reasoner uses several global sets, which are populated independently during the constraint translation and, in Algorithm ref \ref{algTranslateConstraints} added to the constraint base. In more details, the reasoner maintains the following temporary constraint sets 
 
 \begin{enumerate}
-  \item Default constraints $\defaultConstraints$ containing constraints setting the default values.
-  \item Deferred default constraints $\deferredDefaultConstraints$ containing default initialization constraints to be evaluated after all constraints in $\defaultConstraints$  but before the other usual constraints in $\topLevelConstraints$ and $\otherConstraints$.
-  \item Top level constraints and derived type constraints $\topLevelConstraints$
-  \item Remaining usual constraints including compound types used in containers, constraint variables, compound type constraints, compound eval constraints, constraintVariableConstraints, default annotation constraints and assigned annotation constraints $\otherConstraints$.
+  \item \emph{Default constraints $\defaultConstraints$} containing constraints setting the default values of all variables. In particular, this set can contain constraints that assign compound and container initializer, i.e., modify multiple values at once.
+  \item \emph{Deferred default constraints $\deferredDefaultConstraints$} containing default initialization constraints to be evaluated after all constraints in $\defaultConstraints$, but before the other usual constraints in $\topLevelConstraints$ and $\otherConstraints$. $\deferredDefaultConstraints$ is required as setting individual variables may be accidentally overridden by compound and container initializers assigned through constraints in $\defaultConstraints$.
+  \item \emph{Top level constraints $\topLevelConstraints$}, i.e., constraints directly specified in a project, constraints in top-level eval-blocks and their derived type constraints. These constraints, in particular top-level eval-block constraints, shall take precedence over nested constraints.
+  \item \emph{Remaining usual constraints $\otherConstraints$} in nested structures, including compound types used in containers, constraint variables, or annotation constraints.
 \end{enumerate}
-Further, the algorithm maintains a global variable mapping $\variableMapping$, a map of already processed variables to accessors so that later processed complex expressions can be substituted with the correct accessors.
-
-The constraints are appended 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}. 
-
-
- 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 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. 
+
+These constraint sets are filled through the top-level calls in line \ref{algTranslateConstraintsTranslationStart}-\ref{algTranslateConstraintsTranslationEnd} including subsequent calls. Please note that adding constraints to a constraint set (currently) requires filtering out unneeded constraints as well as indexing used variables. This is done by the $add$ function in line \ref{algTranslateConstraintsAdd}, which we will detail below in Section \ref{sectTranslation}. According to the priority of the constraint sets introduced above, Algorithm \ref{algTranslateConstraints} composes the constraint base (keeping remaining constraints from prior project evaluations of the same configuration) in line \ref{algTranslateConstraintsCompose}. Finally, Algorithm \ref{algTranslateConstraints} clears the temporary constraint sets in lines \ref{algTranslateConstraintsClearSetsStart}-\ref{algTranslateConstraintsClearSetsEnd}.
+
+\subsection{Top-level Constraints Evaluation}\label{sectTopLevelConstraintsEvaluation}
+
+When the constraint base is filled for a given project, the constraint evaluation for that project (including potentially left over constraints from previous project evaluations) can start. Algorithm \ref{algEvalLoop} implements the constraint evaluation for a project. As mentioned above, this part heavily relies on the IVML constraint evaluation mechanism, i.e., the evaluator for IVML expressions.
+
+An IVML projects constitutes a reasoning scope, i.e., no duplicated variable assignment must occur within a project. To prepare validating this rule, Algorithm \ref{algEvalLoop} clears in line \ref{algEvalLoopClearScope} the (global) scope assignments. Further, it sets $p$ as search space for the dynamic dispatch of user-defined operations on the expression evaluator (line \ref{algEvalLoopDispatchScope}). 
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{project $p$}
+  \KwData{constraint $base$, scope assignments $a$, problem records $m$, used variables $u$, constraint evaluator $e$, flags $hasTimeout$ and $stop$}
+  
+    $clearScopeAssignments(a)$\; \label{algEvalLoopClearScope}
+    $setDispatchScope(e, p)$\; \label{algEvalLoopDispatchScope}%evaluator.setDispatchScope
+    \While {$|base| > 0 \wedge \neg hasTimeout \wedge \neg stop$} { \label{algEvalLoopLoopStart}
+        $c \assng pop(base)$\; \label{algEvalLoopPop}
+        $clear(u)$\; \label{algEvalLoopClear}
+        $setAssignmentState(e, isDefault(c))$\; \label{algEvalLoopAssngState}
+        $m \assng m \addSeq analyzeEvaluationResult(evaluate(e, c), u)$\; \label{algEvalLoopAssngEval}
+        $hasTimeout \assng checkForTimeout()$\; \label{algEvalLoopTimeout}
+    } \label{algEvalLoopLoopEnd}
+ \caption{Constraint evaluation loop (\IVML{evaluateConstraints}).}\label{algEvalLoop}
+\end{algorithm}
+
+The main loop (lines \ref{algEvalLoopLoopStart}-\ref{algEvalLoopLoopEnd}) runs as long as there are constraints in the constraint $base$, assuming that the evaluation either terminates when all constraints are successfully evaluated (and value changes may add new constraints, cf. Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) or constraints fail and do not induce further constraints. The main loop also stops if reasoning runs into a timeout or is canceled by the user through the $stop$ flag.
+
+In each iteration of the main loop, the algorithm pops a constraint for evaluation from $base$ (line \ref{algEvalLoopPop}) and clears the records about used variables (line \ref{algEvalLoopClear}). Recording used variables is required as detailed information for recording reasoning problems and later for creating the detailed reasoning report (last step of Algorithm \ref{algMainLoop}).
+
+In order to assign values with the correct assignment state (cf. Section \ref{sectNotationConfigVars}), Algorithm \ref{algEvalLoop} registers the actual assignment state for the current constraint $c$ (line \ref{algEvalLoopAssngState}).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}. Next, constraint $c$ is evaluated (line \ref{algEvalLoopAssngEval}) through the constraint evaluator. If configuration variables are changed as part of the constraint evaluation, the variables are recorded in $u$ (not shown in Algorithm \ref{algVarChange}) and their constraints are re-scheduled for reasoning (cf. Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). Then, the evaluation result is analyzed (still line \ref{algEvalLoopAssngEval}) and, if needed, problem records are created, e.g., due to duplicate variable assignments in the same project scope 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 Constraint $c$ is evaluated successfully so that existing problem records for $c$ can be removed from $m$. 
+  \item Constraint $c$ is evaluated as undefined. As specified by IVML \ref{IVML-LS}, a constraint for which at least one variables or expressions is evaluated to undefined, is also considered undefined. This situation does not lead to the creation of a problem record, as the constraint can either be ignored or will be re-scheduled if one of the (currently undefined) variables is changed through the evaluation of 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
-  \KwIn{project $p$, constraint $base$}
-  \KwData{scope assignments $a$, problem records $m$, used variables $u$, constraint evaluator $e$, flags $hasTimeout$ $stop$}
-  
-    $clearScopeAssignments(a)$\;
-    $setDispatchScope(e, p)$\; %evaluator.setDispatchScope
-    \While {$|base| > 0 \wedge \neg hasTimeout \wedge \neg stop$} {
-        $c \assng pop(base)$\;
-        $clear(u)$\;
-        $setAssignmentState(e, isDefault(c))$\; 
-        $m \assng m \addSeq analyzeEvaluationResult(evaluate(e, c), u)$\;
-        $checkForTimeout()$\;
-    }
- \caption{Constraint evaluation loop (\IVML{evaluateConstraints}).}\label{algEvalLoop}
-\end{algorithm}
-
-When variable $v$ is changed as side effect of a constraint evaluation during reasoning, Algorithm \ref{algVarChange} is called. If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a container operation nor a local variable defined in a let-expression, the change is registered within the actual scope. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then all known constraints (\MISSING{dynamic value changes}) for both, parent and client variables of $v$ are identified. Both, parents and children must be considered, as value in compounds may have impact on both kinds of siblings. These constraints are appended to the constraint $base$, not adding an individual constraint if it is already scheduled in the constraint base.
-
-\begin{algorithm}[H]
-  \SetAlgoLined
-  \KwIn{decision variable $v$}
+Finally, Algorithm \ref{algEvalLoop} checks for a potential timeout in line \ref{algEvalLoopTimeout} comparing the global $startTime$ set in Algorithm \ref{algMainLoop} with a configured reasoning timeout. If a timeout occurred (not further detailed in this document), the global $hasTimeout$ flag is set to $true$. This information is particularly relevant for creating the overall reasoning report as explained for Algorithm \ref{algMainLoop}.
+
+\subsection{Constraint Re-scheduling}\label{sectTopLevelConstraintsRescheduling}
+
+When variable $v$ is changed as side effect of a constraint evaluation during reasoning, Algorithm \ref{algVarChange} is called. If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a container operation nor a local variable defined in a let-expression, the change is registered within the actual project scope. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then all known constraints (\MISSING{dynamic value type changes}) for a variable are identified and become subject to re-scheduling. The identification includes both, parent and nested variables, which is in particular relevant to capture all relevant constraints for variables in compound and container values. These constraints are appended to the constraint $base$, not adding an individual constraint if it is already scheduled in the constraint $base$.
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{decision variable $v$, old value $val$}
   \KwData{scope assignments $a$, relevant constraints $\relevantConstraints$}
   
@@ -370,6 +378,6 @@
       $registerScopeAssignment(a, v)$\;
       \MISSING{change constraints if dynamic value type changes}\;
-      $base \assng base \addSeqNoDupl \bigcup_{p\in allParents(v)}t[v]$\; %constraintsForParent
-      $base \assng base \addSeqNoDupl \bigcup_{c\in alNested(v)}t[v]$\; %constraintsForChilds, nested geht für alle variablen
+      $base \assng base \addSeqNoDupl \bigcup_{p\in allParents(v)}t[p]$\; %constraintsForParent
+      $base \assng base \addSeqNoDupl \bigcup_{c\in alNested(v)}t[c]$\; %constraintsForChilds, nested geht für alle variablen
   }
  \caption{Adjusting the constraint base (\IVML{notifyChanged}).}\label{algVarChange}