Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 33)
+++ /reasoner/reasoner.tex	(revision 34)
@@ -88,7 +88,6 @@
 \newcommand\defaultConstraints[0]{c_d}
 \newcommand\deferredDefaultConstraints[0]{c_{dd}}
-\newcommand\usualConstraintsStageThree[0]{c_{u3}}
-\newcommand\usualConstraintsStageTwo[0]{c_{u2}}
-\newcommand\usualConstraintsStageOne[0]{c_{u1}}
+\newcommand\otherConstraints[0]{c_{o}}
+\newcommand\topLevelConstraints[0]{c_{t}}
 \newcommand\variableMapping[0]{vm}
 \newcommand\relevantConstraints[0]{r_t}
@@ -100,11 +99,10 @@
 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}
+\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$ \TBD{also $\usualConstraintsStageThree$?}.
-  \item Default annotation constraints and assigned annotation constraints $\usualConstraintsStageThree$.
-  \item Usual constraints such as compound types used in collections, constraint variables, compound type constraints, compound eval constraints, constraintVariableConstraints $\usualConstraintsStageTwo$.
-  \item Usual constraints such as top-level project, derived type constraints$\usualConstraintsStageOne$
-\end{itemize}
+  \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 collections, constraint variables, compound type constraints, compound eval constraints, constraintVariableConstraints, default annotation constraints and assigned annotation constraints $\otherConstraints$.
+\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.
 
@@ -193,5 +191,5 @@
 \begin{algorithm}[H]
   \SetAlgoLined
-  \KwIn{project $p$, relevant constraints $\relevantConstraints$ \TBD{??}, incremental $inc$, \TBD{consider frozen}}
+  \KwIn{project $p$, relevant constraints $\relevantConstraints$ \TBD{??}, incremental $inc$}
   \KwData{constraint $base$ , variable mapping $\variableMapping$}
 
@@ -201,17 +199,14 @@
         $translateDeclarationDefaults(d, decision(cfg, d), \undef, inc)$\;
     }
-   $add(\usualConstraintsStageOne,\seqWith{constraints(e)}{e\in evals(p)} \addSeq constraints(p), true)$\;
+   $add(\topLevelConstraints,\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$\;
+  $base \assng \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \topLevelConstraints \addSeq \otherConstraints$\;
    $\defaultConstraints \assng \set{}$\;
    $\deferredDefaultConstraints \assng \set{}$\;
-   $\usualConstraintsStageOne \assng \set{}$\;
-   $\usualConstraintsStageTwo \assng \set{}$\;
-   $\usualConstraintsStageThree \assng \set{}$\;
+   $\topLevelConstraints \assng \set{}$\;
+   $\otherConstraints \assng \set{}$\;
 
  \caption{Translating constraints (\IVML{translateConstraints}).}\label{algTranslateConstraints}
@@ -221,18 +216,18 @@
 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
 \begin{itemize}
-  \item Translates the constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) and stores them into the global set of derived type constraints $\usualConstraintsStageOne$.
-  \item Constructs the default value assignment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $\usualConstraintsStageThree$
+  \item Translates the constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) and stores them into the global set of derived type constraints $\topLevelConstraints$.
+  \item Constructs the default value assignment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $\otherConstraints$
   \item Translates the default value expression and the constraints for all nested compound slots if $d$ is a compound. Therefore, the algorithm uses the type of $d$ or, if available, or the actual type of the default value expression, which may be a refined type of $d$. The translation of the nested compound slots contributes to the variable-accessor mapping $c$. Then the algorithm  substitutes all occurrences of \IVMLself{} by the actual declaration as well as all mapped variables from $m$ in the default value expression. It is important that the constraints for the nested compound slots must be translated regardless wether a default value expression for $d$ is specified.
   \item Collects all transformed collection compounds based on the actual used types if $d$ is a collection. If $d$ is a collection over compounds, here all potentially refined compound types and their specific constraints are considered (cf. Section \ref{deflt_collections}).
   \item Translates remaining (slot) default value expression by replacing potential \IVMLself{} usages with the compound access. In case that \IVMLself{} is used in the default value expression or the declaration is an overriding slot, the expression shall be turned into a deferred default value constraint ($\deferredDefaultConstraints$), i.e., a constraint that is evaluated later than all usual default value constraints. Deferring these constraints ensures that individual slots are assigned after values for entire compounds or containers on top-level are assigned, i.e., the individual slot value is not accidentally overridden by a more global value for the entire structure. 
-  \item Translates usual collection compound constraints independent of any default value expression and stores them into $\usualConstraintsStageTwo$. \TBD{check}
-  \item Translates collection constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) independent of any default value expression filling $\usualConstraintsStageTwo$. \TBD{check, also section ref}
+  \item Translates usual collection compound constraints independent of any default value expression and stores them into $\otherConstraints$. \TBD{check}
+  \item Translates collection constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) independent of any default value expression filling $\otherConstraints$. \TBD{check, also section ref}
 \end{itemize}
-Finally, the default value expression is turned into a constraint. If the declaration is a constraint variable, i.e., a variable that contains an overridable constraint, \TBD{check ca not present} then the default value expression already represents the constraint and can be added to the constraint set of constraint variables $\usualConstraintsStageTwo$. Else, an assign constraint for the declaration $d$ (or the compound access in case of default constraints \TBD{check why}) is constructed and added either to $\defaultConstraints$ or $\deferredDefaultConstraints$ as determined before. 
+Finally, the default value expression is turned into a constraint. If the declaration is a constraint variable, i.e., a variable that contains an overridable constraint, \TBD{check ca not present} then the default value expression already represents the constraint and can be added to the constraint set of constraint variables $\otherConstraints$. Else, an assign constraint for the declaration $d$ (or the compound access in case of default constraints \TBD{check why}) is constructed and added either to $\defaultConstraints$ or $\deferredDefaultConstraints$ as determined before. 
 
 \begin{algorithm}[H]
   \SetAlgoLined
   \KwIn{declaration $d$, variable $v$, access $ca$, incremental $inc$}
-  \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\usualConstraintsStageTwo$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$}
+  \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$}
   
       $translateDerivedDatatypeConstraints(d)$\;
@@ -256,5 +251,5 @@
            }
       } \uElse{$ dflt \assng \undef $\;}
-      $add(\usualConstraintsStageTwo, translateCollectionCompoundConstraints(d, v, \undef), true)$\;
+      $add(\otherConstraints, translateCollectionCompoundConstraints(d, v, \undef), true)$\;
       \If{$isContainer(t) \wedge isDerived(contained(t))$}{
           $translateCollectionDerivedDatatypeConstraints(d, \undef)$\;
@@ -263,5 +258,5 @@
           \uIf{$isConstraint(t)$}{
               \lIf{$ ca == \undef $}{
-                  $add(\usualConstraintsStageTwo, \createConstraint{dflt}, true)$\;
+                  $add(\otherConstraints, \createConstraint{dflt}, true)$\;
                   $\relevantConstraints \assng \relevantConstraints \cup (\createConstraint{dflt}, v)$}
           }\Else{
@@ -275,13 +270,13 @@
 \subsection{Derived types}\label{sectDerivedTypes}
 
-In IVML, a derived datatype $d$ is defined based on a known base type $b$. Type $d$ is a type restriction of $b$, if $d$ defines restrincting constraints over $b$ using a local variable $decl(d)$ to express the constraints. \TBD{decl(d) is not introduced above. Needed?}. Type $d$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(d) = \emptySet$. If a variable $v$ is declared of type $d$, all constraints defined for $d$ over $b$ and, transitively over the base types of $b$ apply. Whether these constraints are fullfilled depends on the actual value of $v$. Therefore, we translate all constraints defined on type $d$ (of $v$) to constraints of $v$. This is achieved by Algorithm \ref{algTranslateDerivedDatatypeConstraints}, which collects for a given declaration $d$ all constraints for basis types substituting in each constraint the respective local variable by the actual variable $d$. The resulting constraints are stored in $\usualConstraintsStageOne$.
+In IVML, a derived datatype $d$ is defined based on a known base type $b$. Type $d$ is a type restriction of $b$, if $d$ defines restrincting constraints over $b$ using a local variable $decl(d)$ to express the constraints. \TBD{decl(d) is not introduced above. Needed?}. Type $d$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(d) = \emptySet$. If a variable $v$ is declared of type $d$, all constraints defined for $d$ over $b$ and, transitively over the base types of $b$ apply. Whether these constraints are fullfilled depends on the actual value of $v$. Therefore, we translate all constraints defined on type $d$ (of $v$) to constraints of $v$. This is achieved by Algorithm \ref{algTranslateDerivedDatatypeConstraints}, which collects for a given declaration $d$ all constraints for basis types substituting in each constraint the respective local variable by the actual variable $d$. The resulting constraints are stored in $\topLevelConstraints$.
 
 \begin{algorithm}[H]
   \SetAlgoLined
   \KwIn{declaration $d$}
-  \KwData{derived type constraints $\usualConstraintsStageOne$}
+  \KwData{derived type constraints $\topLevelConstraints$}
 
   $cs \assng \bigcup_{t \in allBase(type(d))} constraints(t)$\;
-  $add(\usualConstraintsStageOne, \setWith{\createInternalConstraint{c|_{decl(c)=d}}}{c\in cs}, true)$\;
+  $add(\topLevelConstraints, \setWith{\createInternalConstraint{c|_{decl(c)=d}}}{c\in cs}, true)$\;
  \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints}
 \end{algorithm}
@@ -292,8 +287,8 @@
   \SetAlgoLined
   \KwIn{derived type $t$, declaration $d$, compound access $ca$}
-  \KwData{derived type constraints $\usualConstraintsStageOne$}
+  \KwData{derived type constraints $\topLevelConstraints$}
 
   $cs \assng \bigcup_{t \in allBase(t} constraints(t)$\;
-  $add(\usualConstraintsStageOne, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }c|_{decl(c)=d})}}{c \in cs}, true)$\;
+  $add(\topLevelConstraints, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }c|_{decl(c)=d})}}{c \in cs}, true)$\;
  \caption{Translating constraints for derived collection types (\IVML{translateCollectionDerivedDatatypeConstraints}).}\label{algTranslateCollectionDerivedDatatypeConstraints}
 \end{algorithm}
@@ -307,8 +302,8 @@
   \SetAlgoLined
   \KwIn{configuration $cfg$, declaration $d$, compound access $ca$}
-  \KwData{constraints $\usualConstraintsStageThree$}
+  \KwData{constraints $\otherConstraints$}
 
   $a \assng annotations(decision(cfg, d))$\;
-  $add(\usualConstraintsStageThree, \setWith{\createDefaultConstraint{\IVML{assign}(\closedCases{\IVMLMeta{acc}(d,r), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,r), &\text{else}}, default(r))}}{r\in a}, false)$\; 
+  $add(\otherConstraints, \setWith{\createDefaultConstraint{\IVML{assign}(\closedCases{\IVMLMeta{acc}(d,r), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,r), &\text{else}}, default(r))}}{r\in a}, false)$\; 
  \caption{Translating annotation defaults (\IVML{translateAnnotationDefaults}).}\label{algTranslateAnnotationDefaults}
 \end{algorithm}
@@ -355,5 +350,5 @@
 First, Algorithm \ref{algTranslateCompoundDefaults} creates all accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. While the first case creates a static accessor based on the declared type, the second case mitigates the problem that on slots known for specific value types may not be accessed through simple accessor expression as the compound access may be created for a refined type. Therefore, it creates a compound accessor for the most specific type obtained from an IVML type cast of the compound accessor to the actual value type (can be omitted if $t=type(value(v))$, not shown here). Then, it performs a transitive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclarationDefaults}.
 
-Second, Algorithm \ref{algTranslateCompoundDefaults} considers all slots, in particular if one slot is a container of constraints, it translates all (constraint) values into instantiated constraints by substituting \IVMLself{} with the actual declaration (including matching mappings in $\variableMapping$) adding the translated constraint to the set of constraint variables ($\usualConstraintsStageTwo$). If the slot directly represents a constraint (variable), the algorithm performs a similar translation on the respective default value expression. If the slot is a compound collection, it translates all (\TBD{defaults?}) the contained constraints using Algorithm \ref{algTranslateCollectionCompoundConstraints}. 
+Second, Algorithm \ref{algTranslateCompoundDefaults} considers all slots, in particular if one slot is a container of constraints, it translates all (constraint) values into instantiated constraints by substituting \IVMLself{} with the actual declaration (including matching mappings in $\variableMapping$) adding the translated constraint to the set of constraint variables ($\otherConstraints$). If the slot directly represents a constraint (variable), the algorithm performs a similar translation on the respective default value expression. If the slot is a compound collection, it translates all (\TBD{defaults?}) the contained constraints using Algorithm \ref{algTranslateCollectionCompoundConstraints}. 
 
 Finally, the algorithm translates all attribute assignments using Algorithm \ref{algTranslateAnnotationAssignments}, all direct compound constraints (substituting \IVMLself{} and registered variables), and translates and collects all eval constraints (\TBD{no self??}).
@@ -362,5 +357,5 @@
   \SetAlgoLined
   \KwIn{declaration $d$, variable $v$, compound access $ca$, default value type $t$}
-  \KwData{constraints $\usualConstraintsStageTwo$, variable mapping $\variableMapping$}
+  \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$}
 
   \ForAll{s \iterAssng slots(v)} { %actual slots
@@ -373,10 +368,10 @@
   \ForAll{s \iterAssng slots(v)} { %actual slots
       \If{$isConstraintContainer(type(s))$} {
-          $add(\usualConstraintsStageTwo, \setWith{\createConstraint{value(e)|_{\IVMLself =d, \variableMapping}}}{e \in elements(value(s))}, true)$\;
+          $add(\otherConstraints, \setWith{\createConstraint{value(e)|_{\IVMLself =d, \variableMapping}}}{e \in elements(value(s))}, true)$\;
       }
       \If{$isConstraint(type(s)) \wedge default(s) \neq \undef$}{
-          $add(\usualConstraintsStageTwo, \set{\createConstraint{default(s)|_{\IVMLself =d, \variableMapping}}}, true)$\;
-      }
-     $add(\usualConstraintsStageTwo, translateCollectionCompoundConstraints(s, v, \variableMapping[s]), true)$\;
+          $add(\otherConstraints, \set{\createConstraint{default(s)|_{\IVMLself =d, \variableMapping}}}, true)$\;
+      }
+     $add(\otherConstraints, translateCollectionCompoundConstraints(s, v, \variableMapping[s]), true)$\;
   }
   \If{$\neg inc$} {
@@ -385,6 +380,6 @@
       }
   }
-  $add(\usualConstraintsStageTwo, \setWith{\createConstraint{c|_{\IVMLself =d, \variableMapping}}}{c\in allCompoundConstraints(t, false)}, true)$\;
-  $add(\usualConstraintsStageTwo, \setWith{\createConstraint{c|_{vm}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\;
+  $add(\otherConstraints, \setWith{\createConstraint{c|_{\IVMLself =d, \variableMapping}}}{c\in allCompoundConstraints(t, false)}, true)$\;
+  $add(\otherConstraints, \setWith{\createConstraint{c|_{vm}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\;
 
  \caption{Translating annotation defaults (\IVML{translateCompoundDefaults}).}\label{algTranslateCompoundDefaults}
@@ -401,15 +396,15 @@
 If a compound accessor $ca$ is given, it takes precedence and the annotation is accessed through $ca$ and the respective annotation defined for the given variable declaration $d$ through ($annotation(d, name(a))$. If no accessor is given and the declaration $d$ is not in the variable mapping $\variableMapping$ (\TBD{are variables or declarations mapped}), $d$ is taken as accessor, else the actual accessor in $\variableMapping$. The accessor is used as the left side of an IVML assignment, the right side (value) is made up of the default value expression given by the assignment data $a$.
 
-Algorithm \ref{algTranslateAnnotationAssignments} uses the translation of an individual assignment data to process an entire assignment block. In IVML, an assignment block is used to declare compound slots with an implicit assignment of annotations for each delcared variable. Further, assignment blocks can be nested an the assignments defined for the outer blocks must be applied also to the inner blocks. Therefore, Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the effective assignments $ea$. Then, for all assignment data and all declared slots, it creates the variable mapping. When the mapping is complete, it performs the transformation defined above and collects the created constraints in $\usualConstraintsStageThree$. If the type \TBD{this is the static type} of the slot is a comound, it performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given).
+Algorithm \ref{algTranslateAnnotationAssignments} uses the translation of an individual assignment data to process an entire assignment block. In IVML, an assignment block is used to declare compound slots with an implicit assignment of annotations for each delcared variable. Further, assignment blocks can be nested an the assignments defined for the outer blocks must be applied also to the inner blocks. Therefore, Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the effective assignments $ea$. Then, for all assignment data and all declared slots, it creates the variable mapping. When the mapping is complete, it performs the transformation defined above and collects the created constraints in $\otherConstraints$. If the type \TBD{this is the static type} of the slot is a comound, it performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given).
 
 \begin{algorithm}[H]
   \SetAlgoLined
   \KwIn{assignment block $a$, effective assignment data $ea$, compound access $ca$}
-  \KwData{constraints $\usualConstraintsStageThree$}
+  \KwData{constraints $\otherConstraints$}
   
   $ea \assng ea \cup assignmentData(a)$\;
   \ForAll{$e \iterAssng ea$}{
       \ForAll{$d \iterAssng slots(a)$} {
-          $add(\usualConstraintsStageThree, \set{translateAnnotationAssignment(e, d, ca)}, false)$\;
+          $add(\otherConstraints, \set{translateAnnotationAssignment(e, d, ca)}, false)$\;
           \If{$isCompound(type(d))$} {
               \ForAll{$s \iterAssng slots(d)$} {
@@ -419,5 +414,5 @@
               \ForAll{$s \iterAssng slots(d)$} {
                   $b \assng translateAnnotationAssignment(e, s, c)$\;
-                  $add(\usualConstraintsStageThree, \set{b})$\;
+                  $add(\otherConstraints, \set{b})$\;
               }
           }
@@ -498,7 +493,7 @@
     \If{$check$}{
       \If{$isContainerInitializer(c)$} {
-          $\usualConstraintsStageTwo \assng \usualConstraintsStageTwo \addSeq checkCompoundInitializer(c, m)$\;
+          $\otherConstraints \assng \otherConstraints \addSeq checkCompoundInitializer(c, m)$\;
       }\ElseIf{$isCompoundInitializer(c)$}{
-          $\usualConstraintsStageTwo \assng \usualConstraintsStageTwo \addSeq checkCompoundInitializer(c, m)$\;
+          $\otherConstraints \assng \otherConstraints \addSeq checkCompoundInitializer(c, m)$\;
       }
     }