Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 141)
+++ /reasoner/reasoner.tex	(revision 142)
@@ -705,25 +705,9 @@
 
 
-%set in line \ref{algTranslateDeclarationTranslateSelf1} the value of self $v$ to the actual variable declaration $d$ and create the variable mapping for all slots in line \ref{algTranslateDeclarationRegisterCompound}. As for container types, the actual translation happens at the end of Algorithm \ref{algTranslateDeclaration} as expressions for slots or elements may refer to each other.
-
-
-%the reasoner is not operating incremental mode as there no default value assignments are needed. Then we process the default value for the actual declaration. In particular for a correct compound initialization, which may mix default and provided values, it is important that the potentially overriding value expression of the variable is scheduled to the constraint base before the default values of the compounds slots. If there is a default value and $d$ is not an attribute used within an assignment block (this may otherwise collide with default values defined by the assignment block), we have to check whether the actual variable is a constraint variable or an usual variable. 
-
-.
-
-
-
-
-
-%If there is a default value expression and reasoning is not in incremental mode, i.e., we shall translate default value expressions to assignment constraints, and if there is a compound accessor, we just have to schedule a replacement of \IVML{self} by the compound accessor. 
-
-
-%Finally, if $t$ is a compound type, we execute the specific translations for compound types using Algorithm \ref{algTranslateCompoundDeclaration}. If $t$ is a container type, we call \ref{algTranslateContainerDeclaration} instead. 
-
 \subsection{Derived types}\label{sectDerivedTypes}
 
-As introduced in Section \ref{sectNotationDerivedTypes}, a derived datatype $t$ is defined through its base type $base(t)$. A derived type $t$ is a type restriction of $base(t)$, if $t$ defines restricting constraints over $base(t)$ through the local variable $decl(t)$. Type $t$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(t) = \emptySet$. 
-
-If a variable $v$ is declared as of a derived type $t$, all constraints defined for $t$ over $base(t)$ and, transitively all constraints over all base types $allBase(t)$ must hold for $v$. Whether these constraints are fullfilled depends on the actual value of $v$. The constraint translation follows this nested type structure and instantiates all constraints defined along the nesting as shown in the following translation pattern. 
+As introduced in Section \ref{sectNotationDerivedTypes}, a derived datatype $t$ is defined as a restriction or an alias of its base type $base(t)$. A derived type $t$ is a type restriction of $base(t)$, if $t$ defines restricting constraints over $base(t)$ using the local variable $decl(t)$ representing $t$. Type $t$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(t) = \emptySet$. The base type of a derived type can in particular be another derived type, but, of course, also any other IVML type. If a variable $v$ is declared to be of a derived type $t$, all constraints defined for $t$ over $base(t)$ must hold for $v$. In particular, if $base(t)$ is a derived type, all constraints over all base types $allBase(t)$ of $t$ must hold transitively. Whether these constraints are fullfilled depends on the actual value of $v$. 
+
+The constraint translation follows this chained type structure and instantiates all constraints defined along the nesting as shown in the following translation pattern. 
 
 \grayPara{
@@ -733,7 +717,7 @@
 }
 
-The constraint defined for all constraints induced by derived types are turned into constraints applying a substitution, which replaces the declaration variable and any cross-referenced variables in the resulting constraint. It is important to mention that reference types may be used in combination with derived types and then appropriate de-referencing on $v$ must apply (indicated by $deref(v)$, which leads to $v$ if no de-referencing is needed.
-
-For a given variable $v$ (in terms of declaration $d$ and specific type $t$), Algorithm \ref{algTranslateDerivedDatatypeConstraints} instantiates\footnote{The actual implementation receives the iterator variable causing the creation of the quantifier constraint and the parent model element for creating the constraint.} all constraints defined for $dref(allBase(t))$, i.e., for all base types also through references types, as constraints of $d$. Thereby, we must consider whether we perform this instantiation for a container variable. If it is a container variable, we create an all-quantifying constraint over all container values, whereby the iterator variable substitutes $decl(t)$. If it is not a container variable, we substitute $decl(t)$ by the actual variable $d$. It is important to note that this substitution is transitive if $d$ is a compound slot, i.e., if $d$ is also mentioned in $\variableMapping$, the previously collected compound accessor for $d$ (in Algorithm \ref{algTranslateCompoundDeclaration}) is used to substitute $decl(t)$. Moreover, if the type $t$ consists of reference types, we need to de-reference $i$ by the number of reference types (through the internal IVML \IVML{refBy} operation). The respective composite expression for $i$ is created through the function $deref(t, ex)$ shown below. The resulting constraints are stored in the set of top-level constraints $\topLevelConstraints$. % shall not make a difference for nested variables as they are already initialized
+Given a variable $v$ of derived type $T$, all constraints induced by the derived type and all its base types are turned into instantiated constraints. During instantiation, we appy a substitution, which replaces the respective local variable by $v$ or an accessor expression to $v$ and, if applicable, any cross-referenced variables in $\variableMapping$. It is important to mention that just substituting the respective local variable by $v$ is not sufficient, as also reference types can be used as base type. A reference type requires then de-referencing of $v$, e.g., to permit access to the slots of a compound variable. This is indicated in the translation pattern by the function $deref(t, v)$, which either dereferences $v$ with respect to $t$ or returns $v$ if no de-referencing is needed.
+
+For a given variable $v$ (in terms of declaration $d$ and for technical reasons its type $t$), Algorithm \ref{algTranslateDerivedDatatypeConstraints} instantiates all constraints defined for all dereferenced transitive base types. However, we must consider whether we perform this instantiation for a container variable\footnote{The actual implementation receives the iterator variable causing the creation of the quantifier constraint and the parent model element for creating the constraints.}. If $v$ is a container variable, we create an all-quantifying constraint over all container elements, whereby the iterator variable $i$ of the quantifier substitutes $decl(t)$. If the derived type $t$ is defined based on some reference type, we must dereference the iterator variable $i$ appropriately. If $v$ is not a container variable, we substitute $decl(t)$ by the actual variable $d$. It is important to note that this substitution is transitive if $d$ is a compound slot, i.e., if $d$ is also mentioned in $\variableMapping$, the previously collected compound accessor for $d$ (in Algorithm \ref{algTranslateCompoundDeclaration}) is used to substitute $decl(t)$. The respective composite expression for $i$ is created through the function $deref(t, ex)$ shown below. The resulting constraints are stored in the set of top-level constraints $\topLevelConstraints$ as the variables in the resulting constraints are then fully qualified and in IVML derived types can only be defined on top level. % shall not make a difference for nested variables as they are already initialized
 
 \begin{algorithm}[H]
@@ -741,14 +725,17 @@
   \KwIn{declaration $d$, type $t$}
   \KwData{derived type constraints $\topLevelConstraints$}
-  $isC \assng isContainer(type(d))$\;
   $cs \assng \bigcup_{t \in deref(allBase(t))} constraints(t)$\;
-  $add(\topLevelConstraints, \setWith{\createConstraint{
-    \varSubstitutionOtherVarMapping{\closedCases{\IVML{forAll(i:}c\IVML{)}, & \text{if } isC \\ 
-                          c, &\text{else}}}{decl(t)=deref(t, i)} 
-    }}{c\in cs}, true, \undef)$\;
+  \If{$isContainer(t)$}{
+      $cs \assng \setWith{\createConstraint{\varSubstitutionOtherVarMapping{\IVML{forAll(i:}c\IVML{)}}{decl(t)=deref(t, i)}}}{c\in cs}$\;
+  }\Else{
+      $cs \assng \setWith{\createConstraint{\varSubstitutionOtherVarMapping{c}{decl(t)=deref(t, v)}}}{c\in cs}$\;
+  }
+  $add(\topLevelConstraints, cs, true, \undef)$\;
  \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints}
 \end{algorithm}
 %
-$$deref(t, ex)=\begin{cases} deref(base(t), ex), & \text{if } isDerived(t) \wedge \neg isDerived(base(t)) \\ \IVML{refBy}(deref(base(base(t)), ex)), & \text{if } isDerived(t) \wedge isDerived(base(t))\\ ex, & \text{else}\\\end{cases}$$
+The dereferencing operation\footnote{The actual implementation performs the dereferencing when explicitly adding a variable mapping in addition to $\variableMapping$ to the expression substitution visitor.} for Algorithm \ref{algTranslateDerivedDatatypeConstraints} takes a type $t$ and a basis expression $ex$. For each reference base type in the chain of base types, it adds a call of the (internal) IVML dereferencing operation \IVML{refBy} around $ex$ or the recursively built up expression to $ex$. Other types than derived types immediately lead to $ex$ as result.
+%
+$$deref(t, ex)=\begin{cases} deref(base(t), ex), & \text{if } isDerived(t) \wedge \neg isReference(base(t)) \\ \IVML{refBy}(deref(base(base(t)), ex)), & \text{if } isDerived(t) \wedge isReference(base(t))\\ ex, & \text{else}\\\end{cases}$$
 %
 \subsection{Compound types}\label{sectCompoundDefaults}