Index: /reasoner/consTranslation.tex
===================================================================
--- /reasoner/consTranslation.tex	(revision 156)
+++ /reasoner/consTranslation.tex	(revision 157)
@@ -433,45 +433,44 @@
       \ForAll{$d \iterAssng decls(a)$} {\label{algTranslateAnnotationAssignmentsLoopStart}
           $a_d\assng ea[name(d)]$\; \label{algTranslateAnnotationAssignmentsObtainEA}
-          $add(\otherConstraints, \set{translateAnnotationAssignment(a_d, d, ca)}, false, \undef)$\; \label{algTranslateAnnotationAssignmentsTranslateBasic}
-          $t \assng type(d)$\;
-          \If{$v \neq \undef$}{
+          $add(\otherConstraints, \set{translateAnnotationAssignment(a_d, d, ca, \variableMapping)}, false, \undef)$\; \label{algTranslateAnnotationAssignmentsTranslateBasic}
+          $t \assng type(d)$\; 
+          \If{$isCompound(t)$} {\label{algTranslateAnnotationAssignmentsIsCompoundStart}
+           \If{$v \neq \undef$}{ \label{algTranslateAnnotationAssignmentsActTypeStart}
               $w \assng nested^*(v, name(d))$\;
               \uIf{$n \neq \undef \wedge\text{ } value(w) \neq \undef$} {
                   $t \assng type(value(w))$\;
               }
-          }
-          \If{$isCompound(t)$} {
+             } \label{algTranslateAnnotationAssignmentsActTypeEnd}
               $ac \assng \closedCases{
                 \createExpression{\IVMLMeta{acc}(ca, d)}, & \text{if } ca \neq \undef \\
-                \createExpression{\IVMLMeta{acc}(\IVMLMeta{var}(decl(v)), d)}, & \text{if } var \neq \undef \\
-                \createExpression{\IVMLMeta{var}(s)}, & \text{else}
-              }$\;
-              \ForAll{$s \iterAssng slots(t)$} {
-                  $x \assng \createExpression{\IVMLMeta{acc}(ac, s)}$\;
-                  $x \assng translateAnnotationAssignment(a_d, s, v, x)$\;
-                  $add(\otherConstraints, x, false, \undef)$\;
-              }
-          }\label{algTranslateAnnotationAssignmentsLoopEnd}
-  }
+                \createExpression{\IVMLMeta{acc}(\IVMLMeta{var}(decl(v)), d)}, & \text{if } v \neq \undef \\
+                \createExpression{\IVMLMeta{var}(d)}, & \text{else}
+              }$\; \label{algTranslateAnnotationAssignmentsAccess}
+              \ForAll{$s \iterAssng slots(t)$} {\label{algTranslateAnnotationAssignmentsSlotsStart}
+                  $x \assng \createExpression{\IVMLMeta{acc}(ac, s)}$\; \label{algTranslateAnnotationAssignmentsSlotAccess}
+                  $x \assng translateAnnotationAssignment(a_d, s, x, \variableMapping)$\; \label{algTranslateAnnotationAssignmentsSlotConstraint}
+                  $add(\otherConstraints, x, false, \undef)$\; \label{algTranslateAnnotationAssignmentsSlotConstraintAdd}
+              }\label{algTranslateAnnotationAssignmentsSlotsEnd}
+          }\label{algTranslateAnnotationAssignmentsIsCompoundEnd}
+  }\label{algTranslateAnnotationAssignmentsLoopEnd}
     
-  \ForAll{$b \iterAssng assignments(a)$} {
+  \ForAll{$b \iterAssng assignments(a)$} {\label{algTranslateAnnotationAssignmentsNestedStart}
       $translateAnnotationAssignments(b, ea, ca)$\;
-  }
+  }\label{algTranslateAnnotationAssignmentsNestedEnd}
 
  \caption{Translating annotation assignments (\IVML{translateAnnotationAssignments}).}\label{algTranslateAnnotationAssignments}
 \end{algorithm}
 
-For a given annotation assignment $a$, the algorithm processes all declared variables (lines \ref{algTranslateAnnotationAssignmentsLoopStart}-\ref{algTranslateAnnotationAssignmentsLoopEnd}). For each variable, the algorithm obtains the effective assignment data $a_d$ in line \ref{algTranslateAnnotationAssignmentsObtainEA}, creates then default value assignment constraint and adds it to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsTranslateBasic}.
-
-
- If the type of the slot (if available the dynamic type of the value)  is a compound, the algorithm performs the same transformation on all compound slots with respective accessors (either using the slot variable $d$ or the compound accessor $ca$ if given).  Finally, the algorithm recursively processes contained assignment-blocks.
-
-Algorithm \ref{algTranslateAnnotationAssignments} relies on the translation of an individual assignment data object. The translation of a single assignment from an assignment data $a$ leads to the creation of an assignment constraint as shown below. If a compound accessor $ca$ is given, 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$, $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$.
+For a given annotation assignment $a$, the algorithm processes all declared variables (lines \ref{algTranslateAnnotationAssignmentsLoopStart}-\ref{algTranslateAnnotationAssignmentsLoopEnd}). For each variable, the algorithm obtains the effective assignment data $a_d$ in line \ref{algTranslateAnnotationAssignmentsObtainEA}, creates the default value assignment constraint and adds it to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsTranslateBasic}. If the declared variable is of compound type (lines \ref{algTranslateAnnotationAssignmentsIsCompoundStart}-\ref{algTranslateAnnotationAssignmentsIsCompoundEnd}), we also must consider the compound slots. Therefore, the algorithm determines in lines \ref{algTranslateAnnotationAssignmentsActTypeStart}-\ref{algTranslateAnnotationAssignmentsActTypeEnd} the actual type of the declared variable $d$, which may differ from the declared type for annotations of compound type due to type refinement. In line \ref{algTranslateAnnotationAssignmentsAccess}, the algorithm determines the access expression $ac$ to the declared compound variable $d$, which may either be $ca.d$ if $ca$ is given, $v.d$ if $v$ is given or, as fallback, just $d$. Now, the algorithm can iterate over all slots of the compound annotation (lines \ref{algTranslateAnnotationAssignmentsSlotsStart}-\ref{algTranslateAnnotationAssignmentsSlotsEnd}), create an access expression for each slot in line \ref{algTranslateAnnotationAssignmentsSlotAccess}, i.e., $ac.s$, create the assignment constraint in line \ref{algTranslateAnnotationAssignmentsSlotConstraint} and add the resulting constraint to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsSlotConstraintAdd}. Finally, the algorithm recursively processes the nested annotation assignments in lines \ref{algTranslateAnnotationAssignmentsNestedStart}-\ref{algTranslateAnnotationAssignmentsNestedEnd} by calling Algorithm \ref{algTranslateAnnotationAssignments} recursively.
+
+In lines \ref{algTranslateAnnotationAssignmentsTranslateBasic} and \ref{algTranslateAnnotationAssignmentsSlotConstraint}, Algorithm \ref{algTranslateAnnotationAssignments} relies on the translation of an individual assignment data object. The translation of a single assignment from an assignment data object $a$ leads to the creation of an assignment constraint as shown below. 
 
 \begin{align*}
-  translate&AnnotationAssignment(a, d, ca) = \\
+  translate&AnnotationAssignment(a, d, ca, \variableMapping) = \\
      \createConstraint{\varSubstitutionSelfVarMapping{\IVML{assign}&(\IVMLMeta{ann}(\closedCases{ca, & \text{if } ca \neq \undef\\ d, & \text{if } ca = \undef \wedge \text{ }vm[d] = \undef \\ vm[d] &\text{else}}, \\
      &findAnnotation(d, name(a))), default(a))}{ca}}
 \end{align*}
+
+If a compound accessor $ca$ is given, the annotation is accessed through $ca$. If no accessor is given and the declaration $d$ is not in the variable mapping $\variableMapping$, $d$ is taken as basic accessor expression, else the actual expression in $\variableMapping$. The access expression is completed by, the annotation declaration retrieved from the underlying variable declaration $d$. Ultimately, the accessor is used as left side of an IVML assignment operation, the right side (value) is made up of the default value expression given by the assignment data $a$ after an appropriate variable substitution.
 
 \subsection{Constraint variables}\label{sectConstraintVariables}