Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 24)
+++ /reasoner/reasoner.tex	(revision 25)
@@ -14,9 +14,11 @@
 \newcommand\addSeqNoDupl[0]{\uplus}
 \newcommand\assng[0]{\leftarrow}
-\newcommand\iterAssng[0]{:} % <<-
+\newcommand\iterAssng[0]{:} % use <<- instead?
 \newcommand\undef[0]{\perp}
+\newcommand\mapEntry[2]{(#1, #2)}
 \newcommand\emptySet[0]{\{\}}
 \newcommand\set[1]{\{#1\}}
 \newcommand\setWith[2]{\{#1:#2\}}
+\newcommand\seqWith[2]{\bigoplus_{#2}#1}
 \newcommand\createConstraint[1]{\langle #1 \rangle}
 \newcommand\createDefaultConstraint[1]{\langle_d\text{ } #1 \rangle}
@@ -52,7 +54,7 @@
   \item usually, if not used otherwise, $v$ is variable, $d$ is declaration, $t$ is type, $val$ is value
   \item $\undef$ is the undefined value, e.g., an undfined constraint, type or declaration. \TBD{what is a constraint, how to denote a constraint creation in contrast to mathematical/algorithmic notation}
-  \item $decision(cfg, d)$ the variable from the configuration $cfg$. In contrast to a declaration, a (decision) variable is linked to a respective configuration, has an assignment state and holds the actually configured value. $decision(v, s)$ returns the decision variable related to the nested slot $s$ of a compound variable $v$.
+  \item $decision(cfg, d)$ the variable from the configuration $cfg$. In contrast to a declaration, a (decision) variable is linked to a respective configuration, has an assignment state and holds the actually configured value. $decision(v, s)$ returns the decision variable related to the nested slot $s$ of a compound variable $v$, $nested(v)$ all nested variables in $v$ (may be empty), $allNested(v) = \begin{cases}\set{}, & \text{if } |nested(v)| = 0 \\  \set{nested(v)} \cup \setWith{allNested(w)}{w\in vars(v)}, & \text{else}\\ \end{cases}$.
   \item $declaration(v)$ the declaration of variable $v$
-  \item $parent(d)$ the model element the declaration $d$ is nested within
+  \item $parent(d)$ the model element the declaration $d$ is nested within, $allParents(v) = \begin{cases}\set{}, & \text{if } \neg isVariable(parent(v)) \\  \set{parent(v)} \cup allParents(parent(v)), & \text{else}\\ \end{cases}$
   \item $type(d)$ the type of the declaration $d$, similarly $type(v) = type(declaration(v))$ and $type(val)$ the (potentially sub-)type of the value $val$
   \item $annotations(d)$ returns the set of orthogonal IVML annotations declarations for declaration $d$. Similarly, $annotations(v)$ returns the set of actual annotations for the variable $v$. There is a significant difference between $annotations(d)$ and $annotations(decision(cfg,d))$, as a declaration can only holds the specifically declared attributes for $d$, while a variable is instantiated with all annotations applied to the containing project or variables (in case of compounds or collections). 
@@ -76,4 +78,5 @@
   \item $parentCompound(d) = \begin{cases} parent(d), & \text{if } parent(d) \neq \undef \wedge{} isCompound(parent(d)) \\ parentCompound(parent(d)), & \text{if } parent(d) \neq \undef \\ \undef, & \text{else}\end{cases}$
   \item $isOverridden(d) = d \in \setWith{slots(r)}{r\in allRefines(parentCompound(d))}$
+  \item $isAssignmentConstraint(c)$ whether constraint $c$ is of form \IVML{assign(v, e)} with $v$ variable and $e$ expression
 \end{itemize}
 \TBD{Algorithms + implementation name, for simplicity we ignore here that variable values can be \IVML{null}, would lead to $\undef$ on some operations and shall be filtered out/considered properly by an implementation.}
@@ -120,5 +123,5 @@
 \begin{algorithm}[H]
   \SetAlgoLined
-  \KwIn{configuration $cfg$, incremental $inc$}
+  \KwIn{configuration $cfg$, incremental $inc$, \TBD{consider frozen}}
   \KwData{problem records $m$, relevant constraints $t$ \TBD{$t$??}}
   \KwResult{Reasoning result $r$}
@@ -177,6 +180,6 @@
       $registerScopeAssignment(a, v)$\;
       \MISSING{change constraints if dynamic value type changes}\;
-      $base \assng base \addSeqNoDupl constraintsForParent(v)$\;
-      $base \assng base \addSeqNoDupl constraintsForChilds(v)$\;
+      $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
   }
  \caption{Adjusting the constraint base (\IVML{notifyChanged}).}\label{algVarChange}
@@ -347,5 +350,5 @@
 
   \ForAll{s \iterAssng slots(v)} { %actual slots
-      $c \assng (s, \createExpression{\closedCases{\IVMLMeta{acc}(d,s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, type(value(v))), s), &\text{else}}})$\;
+      $c \assng \mapEntry{s}{\createExpression{\closedCases{\IVMLMeta{acc}(d,s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, type(value(v))), s), &\text{else}}}}$\;
       $\variableMapping \assng \variableMapping \cup \set{c}$\;
       $translateDeclarationDefaults(s, decision(v, s), c)$\;
@@ -454,7 +457,7 @@
   $v \assng \createExpression{\IVML{\IVMLMeta{var}(t)}}$
   \ForAll{s \iterAssng slots(t)} {
-      $\variableMapping \assng \variableMapping \cup (s, \createExpression{\IVMLMeta{acc}(v,s)})$\;
-  }
-  \ForAll{$e \iterAssng getAllCompoundConstraints(t)$} {
+      $\variableMapping \assng \variableMapping \cup \mapEntry{s}{\createExpression{\IVMLMeta{acc}(v,s)}}$\;
+  }
+  \ForAll{$e \iterAssng allCompoundConstraints(t)$} {
     $coll \assng\createExpression{\closedCases{ca, & \text{if } ca = \undef \\ d, &\text{else}}}$\;
     $coll \assng\createExpression{coll.\closedCases{\IVML{selectByKind}(a, t), & \text{if } t \neq dt \\  &\text{else}}}$\;
@@ -468,31 +471,44 @@
 \section{Constraint translation}\label{sectConstraintTranslation}
 
-\TBD{Text}
-
-\begin{algorithm}[H]
-  \SetAlgoLined
-  \KwIn{project $p$, relevant constraints $t$ \TBD{??}, incremental $inc$}
-  \KwData{constraint $base$ \TBD{join, reorder, beautify}}
+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.
+
+\begin{align*}
+retrieve&CollectionConstraints(c, m) =\\ 
+             &\closedCases{checkContainerInitializer(c, \undef), & \text{if } isContainerInitializer(c) \\ checkCompoundInitializer(c, m) &\text{if } isCompoundInitializer(c)\\ \set{}, & \text{else}}
+\end{align*}
+\begin{align*}
+checkContainerInitializer(c, m) = \seqWith{\closedCases{e|_m, & \text{if } m \ne \undef \\ e &\text{else}}}{e\in expr(c)}
+\end{align*}
+\begin{align*}
+check&CompoundInitializer(c, m) =\\ 
+         &\seqWith{\closedCases{checkContainerInitializer(e, m), & \text{if } isContainerInitializer(e) \\ checkCompoundInitializer(e, m) &\text{if } isCompoundInitializer(e)\\ \set{}, & \text{else}}}{e\in expr(c)}
+\end{align*}
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{project $p$, relevant constraints $t$ \TBD{??}, incremental $inc$, \TBD{consider frozen}}
+  \KwData{constraint $base$ , variable mapping $\variableMapping$ \TBD{join, reorder, beautify, leave out non-incremental on-the-fly}}
 
    $c_s \assng \set{}$\;  
-   \If{$\neg incremental$} {
-       $\defaultConstraints \assng \defaultConstraints \addSeq \deferredDefaultConstraints$\;
-       $c_s \assng c_s \addSeq \TBD{transformContraints(\defaultConstraints, true)}$\;
-  }
-  $c_s \assng c_s \addSeq transformContraints(\derivedTypeConstraints, true)$\;
-  $c_s \assng c_s \addSeq \setWith{constraints(e)}{e\in evals(p)}$\;
+   \If{$\neg inc$} {
+       $c_s \assng c_s \addSeq \seqWith{\createDefaultConstraint{c|_{\variableMapping}}}{c\in \defaultConstraints \addSeq \deferredDefaultConstraints}$\;
+  }
+  $c_s \assng c_s \addSeq \seqWith{\createConstraint{c|_{\variableMapping}}}{c \in \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 incremental$} {
-    $c_s \assng c_s \addSeq \setWith{\TBD{translateAnnotationAssignments(a, \undef, \undef)}}{a\in assignments(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$\;
   \ForAll{$c \iterAssng c_s$} {
-      \TBD{retrieveCollectionConstraints(c)}\;
+      $retrieveCollectionConstraints(c, \variableMapping)$\;
   }
   $c_s \assng c_s \addSeq \collectionConstraints$\;
-  \TBD{$fillVariableConstraintPool(c_s)$}\;
-  \If{$incremental$} {
-      $c_s \assng \TBD{validationConstraints(c_s)}$\;
+  $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$\;