Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 97)
+++ /reasoner/reasoner.tex	(revision 98)
@@ -305,5 +305,13 @@
 No specific constraint translation is needed for \emph{basic types} (Boolean, Integer, Real String), the constraint type as well as for enums as IVML does not support modifying these types  or does not allow attaching constraints directly to these types. Constraints can be attached indirectly through variable declarations / compound slots or derived types. The available functions for these types, such as adding two integer values, are subject to the creation of the IVML model, e.g., through a parser, and are, therefore, if specified, already part of constraint expressions before reasoning.
 
-In IVML, a \emph{configuration reference} points to a variable defined in the same or another project (if made available through imports). As the actual IVML specification~\cite{IVML-LS} does not define specific properties or operations for reference types, we can safely assume that variables of reference types are transparent and just provide access to the referenced variable. In particular, this holds even if constraints are defined on that variable, as they are translated for / evaluated on the referenced variable.
+In IVML, a \emph{configuration reference} points to a variable defined in the same or another project (if made available through imports). A reference is a type $t$ defined for a base type $base(t)$ the reference points to. If $t$ is a reference, $isReference(t)$ returns true. In some cases, we must dereference a set $s$ of reference types through
+%
+$$deref(t)=\begin{cases} base(t), & \text{if } isDerived(t) \wedge \neg isDerived(base(t))\\ dereference(base(t)), & \text{if } isDerived(t) \wedge isDerived(base(t))\\ t, & \text{else}\\\end{cases}$$
+%
+and
+%
+$$deref(s)=\setWith{s\in t}{deref(t)}$$
+%
+As the actual IVML specification~\cite{IVML-LS} does not define specific properties or operations for reference types, we can safely assume that variables of reference types are transparent and just provide access to the referenced variable. In particular, this holds even if constraints are defined on that variable, as they are translated for / evaluated on the referenced variable. 
 
 \subsubsection{Values}\label{sectNotationValues}
@@ -539,5 +547,5 @@
   
       $t \assng type(d)$; $dflt \assng default(d)$; $f \assng \undef$\; \label{algTranslateDeclarationDecl}
-      \lIf{$isDerived(t)$} {$translateDerivedDatatypeConstraints(d, t)$} \label{algTranslateDeclarationDerivedDatatype}
+      $translateDerivedDatatypeConstraints(d, t)$\; \label{algTranslateDeclarationDerivedDatatype}
       \lIf{$\neg inc$} {
           $translateAnnotationDeclarations(d, v, \undef)$ \label{algTranslateDeclarationAnnotationDefault}
@@ -575,5 +583,5 @@
 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.
 
-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 $allBase(t)$ 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)$. 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
+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)$. 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
 
 \begin{algorithm}[H]
@@ -582,5 +590,5 @@
   \KwData{derived type constraints $\topLevelConstraints$}
   $isC \assng isContainer(type(d))$\;
-  $cs \assng \bigcup_{t \in allBase(t)} constraints(t)$\;
+  $cs \assng \bigcup_{t \in deref(allBase(t))} constraints(t)$\;
   $add(\topLevelConstraints, \setWith{\createConstraint{
     \closedCases{d\rightarrow\IVML{forAll(i}|\text{ }\varSubstitutionOtherVarMapping{c}{decl(t)=\IVML{i}}\IVML{)}, & \text{if } isC \\