Index: /reasoner/consTranslation.tex
===================================================================
--- /reasoner/consTranslation.tex	(revision 153)
+++ /reasoner/consTranslation.tex	(revision 154)
@@ -272,6 +272,6 @@
 \begin{algorithm}[H]
   \SetAlgoLined
-  \KwIn{declaration $d$, variable $v$, access $ca$, type $t$}
-  \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, incremental flag $inc$}
+  \KwIn{declaration $d$, variable $v$, container access $ca$, actual type $t$}
+  \KwData{variable mapping $\variableMapping$, constraints $\otherConstraints$, incremental flag $inc$}
   
       $pushContext(\variableMapping, false)$\;\label{algTranslateContainerDeclarationPushContext}
@@ -303,14 +303,15 @@
 \end{algorithm}
 
-\MISSING{No pattern for this!}
-
-Algorithm \ref{algTranslateCompoundContainer} creates constraints for compound values in containers, e.g., through a container initializer, in IVML like \IVML{setOf(C) s; s = \{\{i=1\}, \{i=2\}\}}, assuming that \IVML{s} is a set of compounds of type \IVML{C} declaring an integer slot \IVML{i}. As these compounds are created implicitly within a container initializer, so far no constraint was added to the constraint base, neither through default value assignments, nested constraints, annotation assignments etc. In consequence, these compounds would remain uninitialized and their implicit constraints would not even be evaluated. 
-
-\begin{algorithm}[H]
-  \SetAlgoLined
-  \KwIn{declaration $d$, (specific) type $t$, declared type $u$, access $ca$, mode $m$}
-  \KwData{deferred default constraints $\deferredDefaultConstraints$}
-
-    \If{$\neg alreadyProcessed(\variableMapping, t)$}{
+Algorithm \ref{algTranslateCompoundContainer} translates a compound container declaration $d$ with access expression $ca$ based on a given actual element type $t$ and the declared elemnt type $t_d$. The idea of Algorithm \ref{algTranslateCompoundContainer} is to $f(v, t)$ in order to quantify the constraints in $t$ over all container elements in $d$ and to translate the individual constraints using the compound translation algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent}. As several constraints may need to be translated for $t$, Algorithm \ref{algTranslateCompoundContainer} creates the quantification prefix expression including $f(v, t)$ once and applies it for all constraints defined by $t$. As containers and compounds may be nested, Algorithm \ref{algTranslateCompoundContainer} stores the relevant information for the quantification prefix in the actual context frame of $\variableMapping$ and composes the complete quantification prefix when adding a translated constraint to the constraint base. Adding constraints happens by calling Algorithm \ref{algTranslateCompoundContent}, i.e., dependent on the type structure, this may cause a recursion involving also the general translation of declarations in Algorithm \ref{algTranslateDeclaration}.
+
+Algorithm \ref{algTranslateCompoundContainer} first checks  in line \ref{algTranslateCompoundContainerAlreadyProcessed} whether type $t$ has already been translated within this container, i.e., in the scope of the actual context frame pushed in line \ref{algTranslateContainerDeclarationPushContext} of Algorithm \ref{algTranslateContainerDeclaration}. Translating the same type for the same container elements multiple times leads to a repeated evaluation of the constraints of that type, i.e., an increased reasoning time and, if the evaluation fails, to (accidentally) repeated error messages, e.g., for unintended variable re-assignments. Moreover, checking whether $t$ has already been processed in the same container also solves the problem that if $t$ is used as a slot type of a nested compound / as an element type in a nested container, processing it by a recursion of Algorithms \ref{algTranslateCompoundContainer}, \ref{algTranslateContainerDeclaration}, \ref{algTranslateCompoundContent} and \ref{algTranslateDeclaration} may cause an endless cycle. 
+
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{declaration $d$, actual element type $t$, declared element type $t_d$, container access $ca$}
+  \KwData{variable mapping $\variableMapping$}
+
+    \If{$\neg alreadyProcessed(\variableMapping, t)$}{\label{algTranslateCompoundContainerAlreadyProcessed}
         $recordProcessed(\variableMapping, t)$\;
 
@@ -324,5 +325,5 @@
           $e\assng\createExpression{\IVML{flatten}(e)}$\; \label{algTranslateDefaultsCompoundContainerFlatten}
         }
-        \uIf{$u\neq t$} {
+        \uIf{$t \neq t_d$} {
             $e\assng\createExpression{\IVML{selectByKind}(e, t)}$\; \label{algTranslateDefaultsCompoundContainerCast}
         }
@@ -337,8 +338,7 @@
 \end{algorithm}
 
-Algorithm \ref{algTranslateCompoundContainer} targets this by creating all-quantized constraints over all elements of the container, mostly be reusing Algorithm \ref{algRegisterCompoundMapping} to create a compound mapping and Algorithm \ref{algTranslateCompoundContent} to translate the compound content. Initially, we a local variable $l$ as later iterator variable for the quantifier expressions. Then, we create a prefix expression $e$ of the quantor constraint expression, i.e., we determine in line \ref{algTranslateDefaultsCompoundContainerInitE} the access expression to the collection either using $ca$ or just holding the variable of the container $d$. If the container is a sequence that may contain duplicates, we first turn it into a set to avoid accidentally duplicated constraints (line \ref{algTranslateDefaultsCompoundContainerFlatten}). If the container is nested, we flatten it in line \ref{algTranslateDefaultsCompoundContainerFlatten} as constraints only need to be created for the elements (no specific constraints can be attached to a container type except for derived values, which are handled by Algorithm \ref{algTranslateDeclaration}). If the actual type $t$ is not the same as the type of the declaration $u)$, we must consider that the slot $s$ only exists for the specific refined type $t$. Then, the instantiation shall apply only to container elements of type $t$ (or of refined types), i.e., we insert in line \ref{algTranslateDefaultsCompoundContainerCast} an element selection by projecting the container to all elements of type $t$ (and refined types). 
+Initially, we a local variable $l$ as later iterator variable for the quantifier expressions. Then, we create a prefix expression $e$ of the quantor constraint expression, i.e., we determine in line \ref{algTranslateDefaultsCompoundContainerInitE} the access expression to the collection either using $ca$ or just holding the variable of the container $d$. If the container is a sequence that may contain duplicates, we first turn it into a set to avoid accidentally duplicated constraints (line \ref{algTranslateDefaultsCompoundContainerFlatten}). If the container is nested, we flatten it in line \ref{algTranslateDefaultsCompoundContainerFlatten} as constraints only need to be created for the elements (no specific constraints can be attached to a container type except for derived values, which are handled by Algorithm \ref{algTranslateDeclaration}). If the actual type $t$ is not the same as the type of the declaration $u)$, we must consider that the slot $s$ only exists for the specific refined type $t$. Then, the instantiation shall apply only to container elements of type $t$ (or of refined types), i.e., we insert in line \ref{algTranslateDefaultsCompoundContainerCast} an element selection by projecting the container to all elements of type $t$ (and refined types). 
 
 %from above
-As it is sufficient to process an actually contained type $t$ once per container, we translate constraints for $t$ only if $t$ was not already processed (in \ref{}). This also solves the potential problem that if $t$ is also used as a slot type within a nested compound type and no further measure is taken, Algorithm \ref{algTranslateContainerDeclaration} may run into an endless recursion.