Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 28)
+++ /reasoner/reasoner.tex	(revision 29)
@@ -98,4 +98,5 @@
 \newcommand\assignedAttributeConstraints[0]{c_{aa}}
 \newcommand\unresolvedConstraints[0]{c_{u}}
+\newcommand\topLevelConstraints[0]{c_{t}}
 \newcommand\variableMapping[0]{vm}
 
@@ -104,5 +105,5 @@
 For IVML, the reasoner must take the structure of IVML models into account, i.e., in particular IVML projects. 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 reasoning loop over the involved IVML projects for a given configuration $cfg$ is shown in Algorithm \ref{algMainLoop}. 
 
-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 clears the actual variable mapping $\variableMapping$ as its scope is for a single project. Then, it identifies the constraints determining default values, then the remaining constraints and registers the constraints with the respective variables. To separate and prioritize the constraints, the reasoner uses several global sets, which are composed into the constraint based before constraint evaluation, namely the set of
+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 clears the actual variable mapping $\variableMapping$ as its scope is for a single project. Then, it identifies and translates the constraints in the respective project\footnote{Most of the translation commands in this algorithm can be executed through a single loop, more specifically an IVML model visitor.}. To separate and prioritize the constraints, the reasoner uses several global sets, which are composed into the constraint based before constraint evaluation, namely the set of
 
 \begin{itemize}
@@ -114,4 +115,5 @@
   \item Constraints related to compound types and their slots $\compoundConstraints$.
   \item Constraints related to compound types used in collections $\collectionCompoundConstraints$.
+  \item Top-level constraints $\topLevelConstraints$
   \item TBD{check: $\assignedAttributeConstraints, \unresolvedConstraints$}
 \end{itemize}
@@ -134,6 +136,14 @@
       %evaluator.setScopeAssignments(sAssng)\;
       $\variableMapping \assng \set{}$\; % clear
-      $base \assng translateDefaults(p, cfg, t, inc)$\;
-      $base \assng base \addSeq translateConstraints(p, t, inc)$\;
+      %>ConstraintTranslationVisitor
+     \ForAll{$d \iterAssng varDeclarations(p)$}{ %translateDeclarationDefaults
+          $translateDeclarationDefaults(d, decision(cfg, d), \undef, inc)$\;
+      }
+      $\topLevelConstraints \assng\seqWith{constraints(e)}{e\in evals(p)} \addSeq constraints(p)$\;
+      \ForAll{a \iterAssng assignments(p)}{
+          $translateAnnotationAssignments(a, \undef, \undef)$\;
+      }
+      %<ConstraintTranslationVisitor
+      $translateConstraints(p, t, inc)$\;
       $evaluateConstraints(p, base)$\;
       $freeze(p)$\;
@@ -196,16 +206,5 @@
 must be translated into a constraint $variable = expression$. Thereby, constraints defined over the type of the variable, e.g., in case of a derived type must be instantiated for the respective variable. 
 
-The top-level transformation is defined by Algorithm \ref{algTranslateDefaults}. It considers all variable declarations in the given project and runs Algorithm \ref{algTranslateDeclarationDefaults} on them.
-
-\begin{algorithm}[H]
-  \SetAlgoLined
-  \KwIn{project $p$, configuration $cfg$, incremental $inc$}
-  \KwData{constraint $base$, derived type constraints $\derivedTypeConstraints$, attribute constraints $\defaultAnnotationConstraints$}
-  
-  \ForAll{$d \iterAssng varDeclarations(p)$}{ %translateDeclarationDefaults
-      $translateDeclarationDefaults(d, decision(cfg, d), \undef, inc)$\;
-  }
- \caption{Translating project default value expressions to constraints (\IVML{translateDefaults}).}\label{algTranslateDefaults}
-\end{algorithm}
+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.
 
 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
@@ -227,5 +226,7 @@
   
       $translateDerivedDatatypeConstraints(d)$\;
-      $translateAnnotationDefaults(cfg, d, \undef)$\;
+      \If{$\neg inc$} {
+          $translateAnnotationDefaults(cfg, d, \undef)$\;
+      }
       $t \assng type(d)$; $dflt \assng default(d)$; $dfltS \assng \defaultConstraints$\;
       \uIf{$isCompound(t)$}{
@@ -366,6 +367,8 @@
      $\compoundConstraints \assng \compoundConstraints \cup translateCollectionCompoundConstraints(s, v, \variableMapping[s])$\;
   }
-  \ForAll{$a \iterAssng assignments(t)$}{
-      $translateAnnotationAssignments(a, \undef, ca)$\;
+  \If{$\neg inc$} {
+      \ForAll{$a \iterAssng assignments(t)$}{
+          $translateAnnotationAssignments(a, \undef, ca)$\;
+      }
   }
   $\compoundConstraints \assng \compoundConstraints \cup \setWith{\createConstraint{c|_{\IVMLself =d, \variableMapping}}}{c\in allCompoundConstraints(t, false)}$\;
@@ -480,5 +483,5 @@
 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.
 
-If no incremental reasoning is needed, default constraints ($\defaultConstraints$) and deferred default constraints ($\deferredDefaultConstraints$) are translated in this sequence by replacing the variables in the variable mapping $\variableMapping$ collected in the previous translations. \TBD{check whether this late substitution can be avoided}. Independent of incremental reasoning, constraints stemming from derived types are translated and added to the temporary set of constraints $c_s$. Then, eval constraints \TBD{including nested??}, from compound eval blocks as well as from top-level constraints (using the correct variables through their specification) are added to $c_s$. If reasoning is not done in incremental fashion, next the constraints from top-level project assignment blocks are translated and added using Algorithm \ref{algTranslateAnnotationAssignments}. After that, already complete compound constraints ($\compoundConstraints$), constraint variable constraints ($\constraintVariablesConstraints$) and collection compound constraints ($\collectionCompoundConstraints$) are added.
+First, the various constraint sets are composed starting with default constraints ($\defaultConstraints$) adding then the remaining constraints. After transferring the 
 
 \begin{align*}
@@ -499,12 +502,5 @@
   \KwData{constraint $base$ , variable mapping $\variableMapping$ \TBD{join, reorder, beautify, leave out non-incremental on-the-fly}}
 
-  $c_s \assng c_s \addSeq \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \derivedTypeConstraints$\;
-  $c_s \assng c_s \addSeq \seqWith{constraints(e)}{e\in evals(p)}$\;
-  $c_s \assng c_s \addSeq \compoundEvalConstraints$\;
-  $c_s \assng c_s \addSeq constraints(p)$\;
-  \If{$\neg inc$} {
-    $c_s \assng c_s \addSeq \seqWith{translateAnnotationAssignments(a, \undef, \undef)}{a\in assignments(p)}$\;
-  }
-  $c_s \assng c_s \addSeq \compoundConstraints \addSeq \constraintVariablesConstraints \addSeq \collectionCompoundConstraints$\;
+  $c_s \assng c_s \addSeq \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \derivedTypeConstraints \addSeq\topLevelConstraints \addSeq \compoundEvalConstraints \addSeq \compoundConstraints \addSeq \constraintVariablesConstraints \addSeq \collectionCompoundConstraints$\;
   \ForAll{$c \iterAssng c_s$} {
       $retrieveCollectionConstraints(c, \variableMapping)$\;
@@ -512,13 +508,9 @@
   $c_s \assng c_s \addSeq \collectionConstraints$\;
   $t \assng t \cup \setWith{\mapEntry{v}{c}}{v\in variables(c) \wedge c\in c_s}$\; % assignConstraintsToVariables
-  \If{$inc$} {
-      $c_s \assng \setWith{c}{c\in c_s \wedge isAssignmentConstraint(c)}$\;
-  }
-  $base \assng \addSeq c_s$\;
-  \If{$\neg inc$} {
-      $base \assng \addSeq \defaultAnnotationConstraints \addSeq \assignedAttributeConstraints$\;
-   }
+  $c_s \assng \setWith{c}{c\in c_s \wedge (\neg inc \vee (inc \wedge \neg isAssignmentConstraint(c)))}$\;
+  $base \assng c_s  \addSeq \defaultAnnotationConstraints \addSeq \assignedAttributeConstraints$\;
    $\defaultConstraints \assng \set{}$\;
    $\deferredDefaultConstraints \assng \set{}$\;
+   $\topLevelConstraints \assng \set{}$\;
    $\derivedTypeConstraints \assng \set{}$\;
    $\compoundConstraints \assng \set{}$\;