Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 31)
+++ /reasoner/reasoner.tex	(revision 32)
@@ -120,18 +120,8 @@
   
   $projects \assng discoverImports(cfg)$\;
-  \ForAll{$p \iterAssng projects$}{
+  \ForAll{$p \iterAssng projects \wedge \neg hasTimeout \wedge \neg stop$}{
       %evaluator.init()\;
       %evaluator.setResolutionListener(Algorithm \ref{algVarChange})\;
       %evaluator.setScopeAssignments(sAssng)\;
-      $\variableMapping \assng \set{}$\; % clear
-      %>ConstraintTranslationVisitor
-     \ForAll{$d \iterAssng varDeclarations(p)$}{ %translateDeclarationDefaults
-          $translateDeclarationDefaults(d, decision(cfg, d), \undef, inc)$\;
-      }
-      $add(\usualConstraintsStageOne,\seqWith{constraints(e)}{e\in evals(p)} \addSeq constraints(p), true)$\;
-      \ForAll{a \iterAssng assignments(p)}{
-          $translateAnnotationAssignments(a, \undef, \undef)$\;
-      }
-      %<ConstraintTranslationVisitor
       $translateConstraints(p, t, inc)$\;
       $evaluateConstraints(p, base)$\;
@@ -157,14 +147,15 @@
   \SetAlgoLined
   \KwIn{project $p$, constraint $base$}
-  \KwData{scope assignments $a$, problem records $m$, used variables $u$, constraint evaluator $e$}
+  \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$} {
+    \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}
@@ -186,6 +177,5 @@
 \end{algorithm}
 
-
-\section{Default value translation}\label{sectDefltTranslation}
+\section{Constraint translation}\label{sectDefltTranslation}
 
 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
@@ -196,4 +186,36 @@
 
 The top-level transformation is called by Algorithm \ref{algMainLoop}. It considers all variable declarations and constraints in the given project and executes the following algorithms.
+
+The constraint translation composes the individual constraint sets into the constraint base and translates missing non-default constraints. This is summarized in Algorithm \ref{algTranslateConstraints}. Here, also the incremental reasoning mode is realized assuming that for incremental reasoning first a full reasoning on the same configuration took place, i.e., possible and propagated values are assigned and variables are frozen. Then, in incremental (runtime) reasoning, just changes on the remaining variables can be validated and respective propagations can be performed.
+
+First, the various constraint sets are composed starting with default constraints ($\defaultConstraints$) adding then the remaining constraints. After transferring the 
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{project $p$, relevant constraints $\relevantConstraints$ \TBD{??}, incremental $inc$, \TBD{consider frozen}}
+  \KwData{constraint $base$ , variable mapping $\variableMapping$}
+
+   $\variableMapping \assng \set{}$\; % clear
+   %>ConstraintTranslationVisitor
+   \ForAll{$d \iterAssng varDeclarations(p)$}{ %translateDeclarationDefaults
+        $translateDeclarationDefaults(d, decision(cfg, d), \undef, inc)$\;
+    }
+   $add(\usualConstraintsStageOne,\seqWith{constraints(e)}{e\in evals(p)} \addSeq constraints(p), true)$\;
+   \ForAll{a \iterAssng assignments(p)}{
+      $translateAnnotationAssignments(a, \undef, \undef)$\;
+   }
+   %<ConstraintTranslationVisitor
+  $c_s \assng c_s \addSeq \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \usualConstraintsStageOne \addSeq \usualConstraintsStageTwo$ \TBD{add with flag}\;
+ % $c_s \assng \setWith{c}{c\in c_s \wedge (\neg inc \vee (inc \wedge \neg isAssignmentConstraint(c)))}$\;
+  $base \assng c_s  \addSeq \usualConstraintsStageThree$\;
+   $\defaultConstraints \assng \set{}$\;
+   $\deferredDefaultConstraints \assng \set{}$\;
+   $\usualConstraintsStageOne \assng \set{}$\;
+   $\usualConstraintsStageTwo \assng \set{}$\;
+   $\usualConstraintsStageThree \assng \set{}$\;
+
+ \caption{Translating constraints (\IVML{translateConstraints}).}\label{algTranslateConstraints}
+\end{algorithm}
+
 
 Algorithm \ref{algTranslateDeclarationDefaults} translates the default value expression according to the actual type of the declation $d$ or, if applicable, the value represented by the default value expression. The algorithm
@@ -470,10 +492,4 @@
 
 
-\section{Constraint translation}\label{sectConstraintTranslation}
-
-The constraint translation composes the individual constraint sets into the constraint base and translates missing non-default constraints. This is summarized in Algorithm \ref{algTranslateConstraints}. Here, also the incremental reasoning mode is realized assuming that for incremental reasoning first a full reasoning on the same configuration took place, i.e., possible and propagated values are assigned and variables are frozen. Then, in incremental (runtime) reasoning, just changes on the remaining variables can be validated and respective propagations can be performed.
-
-First, the various constraint sets are composed starting with default constraints ($\defaultConstraints$) adding then the remaining constraints. After transferring the 
-
 \begin{algorithm}[H]
   \KwIn{constraint sequence $s$, constraint $c$, perform initializers $check$}
@@ -516,21 +532,11 @@
 
 
-\begin{algorithm}[H]
-  \SetAlgoLined
-  \KwIn{project $p$, relevant constraints $\relevantConstraints$ \TBD{??}, incremental $inc$, \TBD{consider frozen}}
-  \KwData{constraint $base$ , variable mapping $\variableMapping$}
-
-  $c_s \assng c_s \addSeq \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \usualConstraintsStageOne \addSeq \usualConstraintsStageTwo$ \TBD{add with flag}\;
- % $c_s \assng \setWith{c}{c\in c_s \wedge (\neg inc \vee (inc \wedge \neg isAssignmentConstraint(c)))}$\;
-  $base \assng c_s  \addSeq \usualConstraintsStageThree$\;
-   $\defaultConstraints \assng \set{}$\;
-   $\deferredDefaultConstraints \assng \set{}$\;
-   $\usualConstraintsStageOne \assng \set{}$\;
-   $\usualConstraintsStageTwo \assng \set{}$\;
-   $\usualConstraintsStageThree \assng \set{}$\;
-
- \caption{Translating constraints (\IVML{translateConstraints}).}\label{algTranslateConstraints}
-\end{algorithm}
-
+\section{Incremental and runtime reasoning}
+
+In some use cases, reasoning over all variables of a project including all dependencies is needed and even not efficient with respect to reasoning time. These cases are incremental and runtime reasoning, i.e., reasoning for constraint checking at runtime of the system, e.g., to support adaptation. We distinguish between incremental reasoning
+\begin{itemize}
+  \item with creation of a partial constraint base (see flag $inc$ above). In this mode, certain constraint types such as default-values (\TBD{or constraints for frozen values}) are not added to the constraint base and the related variables are assumed to be properly instantiated through an initial reasoning run. Thus, reasoning focuses on the non-frozen variables, in particular changed variables. In our experiments, this mode can save up to 65\% reasoning time. This mode can be activated through the reasoner configuration.
+  \item re-using the constraint base. Trading off less reasoning time (\TBD{measure effect}) with memory for storing a copy of the constraint base, we require that the underlying project does not change structurally, i.e., no new types or variables are declared between two reasoning steps. This mode can be activated by requesting a re-usable reasoner instance from the EASy reasoner core and using that instance instead of the default interface (the static reasoning frontend).
+\end{itemize}
 
 \section{Completeness}