Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 63)
+++ /reasoner/reasoner.tex	(revision 64)
@@ -167,5 +167,5 @@
 We define two basic functions for constraints: $isConstraint(t)$ indicates whether type $t$ is a constraint type. $isAssignmentConstraint(c)$ indicates whether constraint $c$ is supposed to change the value of a variable through an assignment, e.g., for an integer variable \IVML{x} in IVML notation \IVML{x = 25;}.
 
-As we will discuss in Section \ref{sectTranslation}, various constraints must be instantiated, complemented and rewritten during the constraint translation process, which is executed per project directly before the reasoning step in order to populate the constraint base. For this purpose, we use a specific notation indicating constraint creation combining algorithm elements carrying actual values/elements (written in mathematical notation) and IVML expression operation (stated in teletype) used to build up the constraint expression. For example, for creating the IVML constraint \IVML{x = 25;}, we denote in algorithms $\createConstraint{\IVML{assign(x, 25)}}$. The angle brackets indicate a constraint creation, the contents of the brackets the expression representing the constraint. Here, \IVML{assing} is the assign operation defined by IVML (actually implementing the equals in \IVML{x = 25;}), which returns a Boolean value indicating whether the execution of the operation succeeded. In an algorithm, we may denote $\createConstraint{\IVML{assign}(x, 25)}$, whereby $x$ is determined by the algorithm and used to generically describe a constraint instantiation. 
+As we will discuss in Section \ref{sectTranslation}, various constraints must be instantiated, complemented and rewritten during the constraint translation process, which is executed per project directly before the reasoning step in order to populate the constraint base. For this purpose, we use a specific notation indicating constraint creation combining algorithm elements carrying actual values/elements (written in mathematical notation) and IVML expression operation (stated in teletype) used to build up the constraint expression. For example, for creating the IVML constraint \IVML{x = 25;}, we denote in algorithms $\createConstraint{\IVML{assign(x, 25)}}$. The angle brackets indicate a constraint creation, the contents of the brackets the expression representing the constraint. Here, \IVML{assing} is the assign operation defined by IVML (actually implementing the equals in \IVML{x = 25;}), which returns a Boolean value indicating whether the execution of the operation succeeded. In an algorithm, we may denote $\createConstraint{\IVML{assign}(x, 25)}$, whereby $x$ is determined by the algorithm and used to generically describe a constraint instantiation. As usual in IVML, we denote the creation of collection operations using the arrow and iterator notation. Let $c$ be an IVML collection of Integers, then \IVML{c->forall(i|i>20);} requires that all values in $c$ are greater than 20. To create such a constraint with $c$ being an algorithm variable, we denote $\createConstraint{c\IVML{->forall(i|i>20)}}$.
 
 As part of the constraint instantiation, variables must be replaced. Let $c=\createConstraint{\IVML{assign(x, 25)}}$ be a constraint and \IVML{y} be some IVML variable. Then $\varSubstitution{c}{x = y}$ leads to the substitution of all variables named \IVML{x} by \IVML{x}, i.e., for the example effectively to \IVML{y = 25}. If such substitutions are stored in a mapping, i.e., a set of $\mapEntry{e_s, e_t}$ with $e_s$ being the expression to be replaced and $e_t$ the replacing expression, we can apply this mapping to a constraint $c$ using $\varSubstitutionVarMapping{c}$. Moreover, we can combine a specific mapping and already stored mappings using $\varSubstitutionOtherVarMapping{c}{x = y}$. Please note that such substitutions are transitive, i.e., if $\mapEntry{y}{z}\in \variableMapping$, $x$ will be replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$.
@@ -245,5 +245,5 @@
 In IVML, a \emph{derived type} creates a new type based on an existing type. A derived type can restrict the base type by specifiying constraints, as well as a type alias if no further constraints are given.
 
-For a derived type $t$, $isDerived(t)$ returns true and $base(t)$ \TBD{only base or most basic base type?} returns the type $t$ is derived from. 
+For a derived type $t$, $isDerived(t)$ returns true and $base(t)$ returns the type $t$ is derived from. 
 
 For specifying constraints, a derived type $t$ implicitly declares a variable $decl(t)$ of type $base(t)$. Of course, derived types can be defined based on already existing derived types. In this case, a chain of base types is created, whereby for reasoning typically the most basic type is relevant. For constraint translation in reasoning it is relevant to iterate over all base types of such a chain, e.g., and to instantiate their declared constraints. Therefore, we define
@@ -469,7 +469,7 @@
 \subsection{Derived types}\label{sectDerivedTypes}
 
-As introduced in Section \ref{sectNotationDerivedTypes}, a derived datatype $d$ is defined based on base type $b$. Type $d$ is a type restriction of $b$, if $d$ defines restrincting constraints over $b$ through the local variable $decl(d)$. 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 as of type $d$, all constraints defined for $d$ over $b$ and, transitively over all base types of $b$ must hold for $v$. Whether these constraints are fullfilled depends on the actual value of $v$. For a given variable $v$, instantiate all constraints defined on $type(v)$ as constraints of $v$. This is achieved by Algorithm \ref{algTranslateDerivedDatatypeConstraints}, which collects for a given declaration $d$ all constraints for all basis types substituting in each constraint the respective local variable $decl(d)$ by the actual variable $decl(v)$. The resulting constraints are stored in $\topLevelConstraints$.
+As introduced in Section \ref{sectNotationDerivedTypes}, a derived datatype $t$ is defined based on 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$. 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
 
 \begin{algorithm}[H]
@@ -477,22 +477,12 @@
   \KwIn{declaration $d$, type $t$}
   \KwData{derived type constraints $\topLevelConstraints$}
-  \TBD{check isDerived(t)}\;
+  $isC \assng isContainer(type(d))$\;
   $cs \assng \bigcup_{t \in allBase(t)} constraints(t)$\;
-  $add(\topLevelConstraints, \setWith{\createConstraint{\varSubstitutionOtherVarMapping{c}{decl(c)=d}}}{c\in cs}, true)$\;
+  $add(\topLevelConstraints, \setWith{\createConstraint{
+    \closedCases{d\rightarrow\IVML{forAll(i}|\text{ }\varSubstitutionOtherVarMapping{c}{decl(t)=\IVML{i}}\IVML{)}, & \text{if } isC \\ 
+                          \varSubstitutionOtherVarMapping{c}{decl(t)=d}, &\text{else}} 
+    }}{c\in cs}, true)$\;
  \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints}
 \end{algorithm}
-
-The translation of derived datatypes for containers can be done similarly, but must consider the nested values/variables of a container. As accessor to the container, Algorithm \ref{algTranslateContainerDerivedDatatypeConstraints} uses either the declaration $d$ or, if given, the accesor $ca$. In contrast to Algorithm \ref{algTranslateDerivedDatatypeConstraints}, Algorithm \ref{algTranslateContainerDerivedDatatypeConstraints} introduces an all-quantor and substitutes the specific variable of a derived datatype definition by the actual declaration $d$ to be processed. 
-
-\begin{algorithm}[H]
-  \SetAlgoLined
-  \KwIn{derived type $t$, declaration $d$, compound access $ca$}
-  \KwData{derived type constraints $\topLevelConstraints$}
-
-  $cs \assng \bigcup_{t \in allBase(t} constraints(t)$\;
-  $add(\topLevelConstraints, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }\varSubstitutionOtherVarMapping{c}{decl(c)=d})}}{c \in cs}, true)$\;
- \caption{Translating constraints for derived container types (\IVML{translateContainerDerivedDatatypeConstraints}).}\label{algTranslateContainerDerivedDatatypeConstraints}
-\end{algorithm}
-
 
 
@@ -650,5 +640,5 @@
       $add(\otherConstraints, translateContainerCompoundConstraints(d, v, \undef), true)$\;
       \If{$isContainer(t) \wedge isDerived(contained(t))$}{
-          $translateContainerDerivedDatatypeConstraints(contained(t), d, \undef)$\;
+          $translateDerivedDatatypeConstraints(contained(t), d)$\;
       }
  \caption{Translating declaration default value expressions to constraints (\IVML{translateContainerDeclaration}).}\label{algTranslateContainerDeclaration}