Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 77)
+++ /reasoner/reasoner.tex	(revision 78)
@@ -26,4 +26,5 @@
 \newcommand\setEmpty[0]{\set{}} % or \emptyset
 \newcommand\setWith[2]{\{#1:#2\}}
+\newcommand\setWithFlat[2]{\bigcup_{#2}\text{} #1}
 \newcommand\setSepText[0]{colon }
 \newcommand\seq[1]{[#1]}
@@ -92,5 +93,5 @@
 In this section, we clarify the notation and terminology that we use for explaining the reasoning process and the constraint translation.
 
-\subsection{General notation}
+\subsection{General notation}\label{sectGeneralNotation}
 
 As usual, we denote a \emph{set} of elements by $s=\set{1, 2, ...}$ with no duplicates allowed (and \setEmpty as the empty set). We write the derivation of a set based on another set by $s_1=\setWith{i+1}{i\in s}$, i.e., $s_1$ is derived from $s$ by iterating over all elements $i$ in $s$ and deriving new values for each $i$ through $i+1$. We use the part after the \setSepText  to indicate the set to take the elements from (possibly including conditions), while the part before the \setSepText indicates how to derive new set elements from the existing ones. $s_2 = s \cup s_1$ denotes the union of the two sets $s$ and $s_1$, i.e., $s_2$ contains all elements from $s_1$ and $s_2$ without duplicates (and the sequence of elements does not matter).
@@ -186,5 +187,5 @@
 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 $\variableMapping=\set{\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}$.
+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 $\variableMapping=\set{\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}$. 
 
 For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate this information as a `$d$' in the constraint creation notation, i.e., for creating a default constraint, we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$
@@ -198,4 +199,6 @@
 $$dfltSlots(v) = \setWith{s}{s\in slots(v) \wedge default(s) \neq \undef}$$ %, compound slots of $v$ having default value expressions, empty for all non-compound types
 %
+Compounds can define own nested constraints, i.e., the constaints of compound type $t$ are then $constraints(t)$.
+
 Compounds can form an inheritance hierarchy through multiple inheritance. Individual slots from parent compounds can thereby shadowed / redefined by slots of the same or more specific type. $refines(t)$ represents the set of compound types directly refined by compound $t$, returning an empty set if there are no such compounds or if $t$ is not a compound type. We define
 %
@@ -223,5 +226,5 @@
 \begin{align*}
 all&CompoundConstraints(t) = \\
-   &\setWith{constraints(s) \cup allAssignmentConstraints(s)}{t \in allRefines^+(t)}
+   &\setWith{constraints(s) \cup allAssignmentConstraints(s)}{s \in allRefines^+(t)}
 \end{align*}
 %
@@ -322,9 +325,9 @@
 \newcommand\problemRecords[0]{m}
 
-The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), translates the constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes.  Figure \ref{figStructure} shows the call graph of the reasoner algorithms and the sections where we will discuss them in more detail. This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation} and the re-scheduling of constraints while evaluation in Section \ref{sectTopLevelConstraintsRescheduling}. The constraint translation will be discussed in detailed in Section \ref{sectTranslation}.
+The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), translates the constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes.  Figure \ref{figStructure} shows the call graph of the reasoner algorithms and the sections where we will discuss them in more detail. This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the global variable mapping structure used during the translation in Section \ref{sectVarMapping}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation} and the re-scheduling of constraints while evaluation in Section \ref{sectTopLevelConstraintsRescheduling}. The constraint translation will be discussed in detailed in Section \ref{sectTranslation}.
 
 \begin{figure}[ht]
 \center
-\includegraphics[scale=0.41]{figures/structure.eps}
+\includegraphics[scale=0.50]{figures/structure.eps}
 \caption{Structuring blocks, algorithms and sections.}
 \label{figStructure}
@@ -360,4 +363,28 @@
 For each project $p$, the main loop (lines \ref{algMainLoopStart} - \ref{algMainLoopEnd}) translates the constraints in $p$ (and populates the constraint base as a side effect, line \ref{algMainLoopTranslate} discussed / Section \ref{sectTopLevelConstraintsTranslation}) and performs the forward-chaining evaluation of the constraint base, i.e., for $p$, in line \ref{algMainLoopEvaluate} / Section \ref{sectTopLevelConstraintsEvaluation}. If a constraint changes a configuration variable as a side effect, the constraints related to that variable are re-scheduled for evaluation by Algorithm \ref{algVarChange}. As last step for a project $p$, the algorithm freezes the actual values according to the (conditional) freeze-block specifications in $p$ in line \ref{algMainLoopFreeze}. Finally, after all projects have been considered or the main reasoning loop has been terminated prematurely, the main reasoning algorithm composes\footnote{In the implementation, this step happens in the class \class{Engine.java}, the actual reasoner instance, which utilizes and calls instances of \class{Resolver.java}.} a detailed reasoning result based on persisting recorded evaluation problems in line \ref{algMainLoopResult}. This reasoning result also includes whether a timeout or a user-requested cancellation of the reasoning occurred.
 
+\subsection{Variable Mapping}\label{sectVarMapping}
+
+During the constraint translation, top-level constraints can directly be applied to the involved top-level variables. As mentioned above, constraints defined on compound slots or indirectly through use of compound instances in containers must be treated differently. The particular issue here is that these constraints can be defined on types rather than top-level variables, which is possible but valid only for individual top-level variables, and for evaluating the related constraints, the must be rewritten to utilize through accessors based on top-level variables. To manage the various lots and access expressions, the translation utilizes a stack-based data structure, onto which we push/pop a stack (context) frame for each IVML project and each contained compound type, container type or combinations of both used in variables of a project. A context frame linkes all currently relevant variables to the respective accessor expressions, which are created before the respective translation.
+
+However, a simple stack is not sufficient, as IVML projects may contain assignment-blocks. An assignment-block implicitly defines constraints for its contained variable declarations including containers or compounds. If we translate first the variable declarations and then the constraints, these constraints are outside their actual scope and, thus, relevant access expressions are not available, leading to wrong constraint translations and erroneous reasoner failures. While changing the translation sequence would be one option, it would also intermingle compund/container translation with annotation-block translation. Thus, we opted to extend the notion of a context stack, allowing to register a declaration with its context frame, to store this registration in the parent context frame and to activate/deactivate such a frame upon translating the implicit assignment-block constraints for a given variable declaration. Registered stack frames are removed from the stack structure when the parent context frame is popped from the stack.
+
+The variable mapping stack structure $\variableMapping$ of the IVML reasoner provides the following operations:
+
+\begin{itemize}
+    \item $setRegisterContexts(\variableMapping, bool)$ enabling automatic registration of context frames within the parent frame. The operation returns the previous state of the registration flag.
+    \item $pushContext(\variableMapping, d)$ creates and pushes a new context frame for declaration $d$ to the stack. If registration is enabled, the new frame will be registered with the parent frame for $var$ (unless $var=\undef$).
+    \item $popContext(\variableMapping)$ removes the top-most context frame. The initial frame, which is created by default and devoted to the containing IVML project, is not removed by this operation.
+    \item $registerMapping(\variableMapping, d, ca)$ registers the access expression $ca$ with the given variabe declaration $d$ in the top-most context frame. Essentially, a context frame contains a mapping $m$ and the operation performs $m \assng m \addMap \mapEntry{d}{ca}$.
+    \item $getMapping(\variableMapping, d)=\variableMapping[d]$ returns the mapping for $d$. If no mapping was registered for the actual context frame, all context frames in stack order are considered. If no mapping was registered at all, the result is $\undef$.
+    \item $activate(\variableMapping, d)$ re-activates, i.e., pushes the registered stack frame for $d$ from the current context frame. As long as the current context frame exists, this operation can be called over and over. If no context frame is registered for $d$, the stack is not modified.
+    \item $deactivate(\variableMapping, d)$ de-activates the registered context frame for $d$, i.e., pops it from the stack but leaves it registered with its parent context frame so that it is available for further activations as long as the parent context frame exists. 
+    \item $clear(\variableMapping)$ clears the stack and cleans up the default context frame dedicated to the IVML project so that $\variableMapping$ is ready for the translation of the next IVML project.
+\end{itemize}
+
+From a black-box perspective, $\variableMapping$ can be considered as a usual map as discussed in Section \ref{sectGeneralNotation}. Thus, we just use $\variableMapping$ in the variable substitution notation as introduced in Section \ref{sectNotationConstraints}, e.g., let $e$ be an expression, then $\varSubstitutionVarMapping{e}$ replaces all variables in $e$ with definition $d$ by $\variableMapping[d]$, respectively. 
+
+For translating containers, context frames can store additional information. We will provide details along with the translation of containers in Section \ref{sectContainerDefaults}.
+
+
 \subsection{Top-level Constraints Translation}\label{sectTopLevelConstraintsTranslation}
 
@@ -365,6 +392,4 @@
 
 Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. In full reasoning mode ($base_c = \undef$), Algorithm \ref{algTranslateConstraints} shall always be executed. If incremental reasoning based on a re-used constraint base is enabled, then this algorithm shall run only if there is no constraint base copy ($|base_c| = 0$), which is then created at the end of the algorithm. 
-
-In line \ref{algTranslateConstraintsClearMapping}, algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$, i.e., a dictionary linking each actually relevant variable, compound slot or annotation to its access expression based on a top-level IVML variable. The variable mapping is a global core data structure of the constraint translation and specific for the project under translation, i.e., mappings for other already processed projects are not needed and can safely be cleared. As $\variableMapping$ is global (also for performance reasons) and cleared only after processing an IVML project, it can temporarily contain outdated or  superfluous entries, e.g., from the a previous compound of the same type being currently processed. However, the mapping is anyway correct as long as the IVML model was correctly created, e.g., through the IVML parser, as then all model elements and their types are properly resolved, no dangling references do exist and the relevant entires in $\variableMapping$ are overridden by the translation algorithm before use, i.e., the  remaining superfluous entries are just ignored.
 
 \begin{algorithm}[H]
@@ -374,5 +399,4 @@
 
    \If{$base_c = \undef \vee |base_c| = 0$} {
-     $\variableMapping \assng \setEmpty$\; \label{algTranslateConstraintsClearMapping} 
      \tcp{start of model visitor}%>ConstraintTranslationVisitor
      \ForAll{$d \iterAssng varDeclarations(p)$}{ \label{algTranslateConstraintsTranslationStart}
@@ -380,9 +404,9 @@
       }
      $add(\topLevelConstraints, constraints(p), true)$\; \label{algTranslateConstraintsAdd} \label{algTranslateConstraintsTopLevelConstraints}
-     \ForAll{a \iterAssng assignments(p)}{
+     \ForAll{$a \iterAssng assignments(p)$}{
         $translateAnnotationAssignments(a, \undef, \undef, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationAssignments}
      } \label{algTranslateConstraintsTranslationEnd}
      $inEvals \assng true$\;
-     $add(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)}\TBD{Priority?}$\;\label{algTranslateConstraintsTopLevelEvals}
+     $add(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)}$\;\label{algTranslateConstraintsTopLevelEvals}
      $inEvals \assng false$\;
      \tcp{end of model visitor}%<ConstraintTranslationVisitor
@@ -392,14 +416,13 @@
      $\topLevelConstraints \assng \setEmpty$\;
      $\otherConstraints \assng \setEmpty$\; \label{algTranslateConstraintsClearSetsEnd}
-     \If{$base_c \neq \undef$}{ \label{algTranslateConstraintsBaseCopyStart}
+     \uIf{$base_c \neq \undef$}{ \label{algTranslateConstraintsBaseCopyStart}
          $base_c \assng \setWith{c}{c \in base}$\tcp*[l]{copy contents}
      }\label{algTranslateConstraintsBaseCopyEnd}
+     $clear(\variableMapping)$\; \label{algTranslateConstraintsClearMapping} 
    }
  \caption{Translating constraints (\IVML{translateConstraints}).}\label{algTranslateConstraints}
 \end{algorithm}
 
-From a technical point of view, the variability mapping consists of mapping entries relating a variable declaration with an access expression if needed. For directly accessible variables such as top-level variables directly defined within a project, no such mapping is needed ($\undef$).  For variables used in constraints within compounds or containers, an appropriate accessor is needed, created and registered when starting to translate the respective type. The respective constraints for that type are then enumerated, copied and while copying the variables registered in the variable mapping are replaced by the accessor expressions in the mapping. It is important to ensure that the mapping for the respective type is complete before constraint translation, so that all variables including cross references within the same type can be replaced properly. References to other variables are already given as accessor expressions and do not need to be considered here.
-
-Then, the algorithm identifies and translates the constraints in the respective project\footnote{The top-translation steps in this algorithm are realized in the implementation by an IVML model visitor implicitly identifying and handling the types without iterating over the project multiple times as the notation here might suggest.}. To separate and prioritize the constraints, the reasoner uses several global sets, which are populated independently during the constraint translation and, in Algorithm \ref{algTranslateConstraints} added to the constraint base. In more details, the reasoner maintains the following temporary constraint sets 
+The algorithm identifies and translates the constraints in the respective project\footnote{The top-translation steps in this algorithm are realized in the implementation by an IVML model visitor implicitly identifying and handling the types without iterating over the project multiple times as the notation here might suggest.}. To separate and prioritize the constraints, the reasoner uses several global sets, which are populated independently during the constraint translation and, in Algorithm \ref{algTranslateConstraints} added to the constraint base. In more details, the reasoner maintains the following temporary constraint sets 
 
 \begin{enumerate}
@@ -413,4 +436,6 @@
 
 Adding constraints or sets of constraints to the constraint base involves constraint filtering in order to respect the incremental reasoning mode as well as constraints that initialize compounds and containers through respective initializer expressions. This is done by a specific operation, which we will discuss in Section \ref{sectContainerBase}. During algorithm discussion, we ill just use the respective function $add(s, c, b)$, which adds constraint $c$ to constraint set $s$, considering compound and container initialization expressions if $b = true$. Compound and container initialization expressions are a specific and relevant case here, as they represent complex compound or container values containing (interrelating) expressions that can only be evaluated during reasoning in contrast to constant values, which are already resolved by the IVML parser (or by a simple configuration initialization mechanism). These expressions are particularly important to correctly consider constraints stemming from constraint variables. While most translation algorithms rely on default values or actual values (e.g., through the $relevantValue$ function defined in Section \ref{sectNotationValues}, compound and container initializers can only be obtained from assignment constraints, i.e., completed and instantiated constraints, which are only available when adding constraints to a constraint set or the constraint base. Thus, We will skip container and compound initializers in the translation algorithms, focus on actual or constant default values, and finally consider these specific cases in Section \ref{sectContainerBase}.
+
+Finally, in line \ref{algTranslateConstraintsClearMapping}, algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$ so that it can be re-used for translating the next IVML project.
 
 \subsection{Top-level Constraints Evaluation}\label{sectTopLevelConstraintsEvaluation}
@@ -498,12 +523,13 @@
   \KwData{variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$, incremental $inc$}
   
-      $t \assng type(d)$; $dflt \assng default(d)$; $s \assng \undef$\; \label{algTranslateDeclarationDecl}
+      $t \assng type(d)$; $dflt \assng default(d)$; $f \assng \undef$\; \label{algTranslateDeclarationDecl}
       \lIf{$isDerived(t)$} {$translateDerivedDatatypeConstraints(d, t)$} \label{algTranslateDeclarationDerivedDatatype}
       \lIf{$\neg inc$} {
           $translateAnnotationDeclarations(d, v, \undef)$ \label{algTranslateDeclarationAnnotationDefault}
       }
-      \lIf{$dflt \neq \undef$}{$t \assng type(d)$ \MISSING{relevantValue}}
+      %\lIf{$value(v) \neq \undef$}{$t \assng type(value(v))$}
+      \lIf{$dflt \neq \undef$}{$t \assng type(d)$}
       \uIf{$isCompound(t)$}{
-            $s \assng d$\;
+            $f \assng d$\;
             $translateCompoundDeclaration(d, v, ca, t)$\; \label{algTranslateDeclarationTranslateCompound}
        } \uElseIf{$ isContainer(type(d)) $}{ \label{algTranslateDeclarationHasDefault}
@@ -519,8 +545,8 @@
                   $ac\assng \closedCases{\IVMLMeta{acc}(d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,a), &\text{else}}$\;\label{algTranslateDeclarationTranslateAnnotationAccess}
               }\uElse{
-                  $ac \assng \closedCases{ca, & \text{if } s = ca \\ d, &\text{else}}$\; \label{algTranslateDeclarationTranslateUsualAccess}
+                  $ac \assng \closedCases{ca, & \text{if } f = ca \\ d, &\text{else}}$\; \label{algTranslateDeclarationTranslateUsualAccess}
               }
              \lIf{$\IVMLself{} \in dflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$}\lElse{$dfltS \assng \defaultConstraints$}
-              $add(dfltS, \createDefaultConstraint{\varSubstitutionSelfVarMapping{\IVML{assign}(ac, dflt)}{s}})$\; \label{algTranslateDeclarationTranslateDefault}
+              $add(dfltS, \createDefaultConstraint{\varSubstitutionSelfVarMapping{\IVML{assign}(ac, dflt)}{f}})$\; \label{algTranslateDeclarationTranslateDefault}
           }
       }
@@ -555,15 +581,5 @@
 A compound can define constraints in several places, namely through types and defaults of its slots and annotations (including constraint variables as well as refined slots and annotations), as constraints listed directly within a compound, within assignment-blocks or within eval-blocks. For slots and annotations we can resort to Algorithm \ref{algTranslateDeclaration}, i.e., compound types, derived types, constraint variables and collections, while for the remaining constraints, we must visit these structures, instantiate and collect the respective constraints. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. In particular, if the IVML keyword \IVMLself{} is used within a constraint, it must be substituted by the actual variable of the respective compound type. Moreover, it is important to recall that a variable $v$ of type $type(v)$ can contain instances of any refined type $allRefines^+(t)$, and in this case the translation must consider the default values of the potentially larger slot, additional constraints and nested structures.
 
-Algorithm \ref{algTranslateCompoundDeclaration} translates the default constraints for a compound variable $v$ with declaration $d$, potential compound accessor $ca$ and (default value) type (or $type(d)$ if no default expression is defined for $d$). The types are related by $type(d) = type(v) \in allRefines^+(t)$. Algorithm \ref{algTranslateCompoundDeclaration} consists of three parts:
-%
-\begin{enumerate} 
-\item Creation and registration of access expressions to all slots and attributes so that cross references can be implicitly resolved during variable substitution applied to all default value expressions and constraints.
-\item Translating all slot declarations and attributes using Algorithm \ref{algTranslateDeclaration}.
-\item Translating all nested annotation assignment-blocks $\otherConstraints$ as value assignment constraints (if not in incremental mode).
-\item Translating all nested eval blocks to $\otherConstraints$.
-\item Translating all compound related constraints to $\otherConstraints$.
-\end{enumerate} 
-
-In lines \ref{algTranslateCompoundDeclarationVarMappingStart}-\ref{algTranslateCompoundDeclarationVarMappingEnd}, Algorithm \ref{algTranslateCompoundDeclaration} creates accessors for all slots of the compound and registers them in the variable mapping $\variableMapping$. The first case creates a static accessor based on the declared type. The second case handles values of sub-types of $type(d)=type(v)$. Therefore, it creates a compound accessor for the most specific type given by $type(value(v))$. However, due to static type checking of the expression, we need a type cast to $type(value(v))$ as otherwise slots defined on the more specific type are not accessible. In fact, as an optimization, the type cast can be omitted if $t=type(value(v))$, but this is not shown in Algorithm \ref{algTranslateCompoundDeclaration}. Now, as the mapping is completed for $v$, the algorithm performs a transitive / recursive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclaration} in line \ref{algTranslateCompoundDeclarationTranslateSlots}. Please note that $slots(v)$ also includes the actual annotations for $v$, i.e., at this point the variable mapping contains also accessors to annotations and processing their declarations through Algorithm \ref{algTranslateDeclaration} anyway considers annotations.
+Algorithm \ref{algTranslateCompoundDeclaration} translates the default constraints for a compound variable $v$ with declaration $d$, potential compound accessor $ca$ and (default value) type (or $type(d)$ if no default expression is defined for $d$). The types are related by $type(d) = type(v) \in allRefines^+(t)$. Algorithm \ref{algTranslateCompoundDeclaration} creates a context frame and pushes it onto the variable mapping stack $\variableMapping$. The main two steps are detailed in Algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent} as both Algorithms are reused with different arguments during the translation of compounds in Section \ref{sectCompoundDefaults}. Algorithms \ref{algRegisterCompoundMapping} registers all compound slots and annotations in the variable mapping, using $ca$ or $d$ as basis for access expressions for slots and annotations and casts to the type of the actual value in $v$ if available (else $\undef$ is passed in as argument). Now Algorithm \ref{algTranslateCompoundContent} can translate the entire compound content including slots, annotations, constraints, annotation-blocks and eval-blocks. Finally, Algorithm \ref{algTranslateCompoundDeclaration} pops the context frame for this compound from $\variableMapping$.
 
 \begin{algorithm}[H]
@@ -572,30 +588,69 @@
   \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$}
 
-  \ForAll{$s \iterAssng slots(v)$} { \label{algTranslateCompoundDeclarationVarMappingStart} %actual slots
-      $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(d,s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, type(value(v))), s), &\text{else}}}$\;
-      $\variableMapping \assng \variableMapping \addMap \set{\mapEntry{s}{x}}$\;
-  }\label{algTranslateCompoundDeclarationVarMappingEnd}
-  \ForAll{$s \iterAssng slots(v)$ } { %actual slots
-      $translateDeclaration(s, decision(v, s), c)$\; \label{algTranslateCompoundDeclarationTranslateSlots}
+  $pushContext(\variableMapping, d)$\;
+  $e \assng \createExpression{d}$\;
+  $registerCompoundMapping(t, ca, e, type(value(v)))$\;
+  $translateCompoundContent(d, v, t, ca)$\;
+  $popContext(\variableMapping)$;
+
+ \caption{Translating compound declarations (\IVML{translateCompoundDeclaration}).}\label{algTranslateCompoundDeclaration}
+\end{algorithm}
+
+Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The compound type $t_c$ indicates the type to be processed, i.e., where to take slot and annotation definitions from. The access expressions $ca$ is optional as usual and, if given, utilized as prefix to create access expressions for slots and annotations. Finally, a target type $t_t$ is given if the access via $ca_s$ or $ca_t$ requires a type cast so that specific slots of $t_t$ can be accessed. Type casts are required if if the actual value is of a refined type of $t_c$, as otherwise slots defined on the more specific type are not accessible and access is rejected by static type checking of IVML expressions.
+
+Algorithm \ref{algRegisterCompoundMapping} iterates over all slots accessible for the given compound type $t_c$ and creates for each slot a respective accessor. If a preceding compound access expression for the slots $ca_s$ is not given, it creates a static accessor based on $v$. If an accessor is given, we create an accessor based on $ca_s$ and include a type cast to $t_t$\footnote{In fact, the type cast can be omitted if $t=type(value(v))$. This is done by the implementation, but not detailed here as a type cast to the actual type does not have an effect.}. The created accessor is then registered with $\variableMapping$. Similarly, we iterate over all annotations for the current slot, create an accessor expression based on $ca_a$ and register the result with $\variableMapping$.
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{compound type $t_c$, acccess $ca$, variable $v$, target type $t_t$}
+  \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$}
+
+  \ForAll{$s \iterAssng \setWithFlat{slots(t)}{t\in allRefines^+(t_c)}$} { \label{algRegisterCompoundMappingVarMappingStart} %actual slots
+      $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), s), &\text{else}}}$\;
+      $registerMapping(\variableMapping, s, x)$\;
+      \ForAll{$a \iterAssng annotations(s)$}{
+        $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(v,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t, a), &\text{else}}}$\;
+        $registerMapping(\variableMapping, a, x)$\;
+      }
+  }\label{algRegisterCompoundMappingVarMappingEnd}
+
+ \caption{Registering the compound mapping (\IVML{registerCompoundMapping}).}\label{algRegisterCompoundMapping}
+\end{algorithm}
+
+Given a complete mapping for a compound type, we can apply Algorithm \ref{algTranslateCompoundContent}. The algorithm performs a transitive / recursive translation of the default values of all slots using the respective accessor calling Algorithm \ref{algTranslateDeclaration} in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} if $v$ is defined ($slots(v)$ also includes all slots for $v$) or all slots for type$t$. It is important to note that in both cases, the second occurs in container translations, we call Algorithm \ref{algTranslateDeclaration}, which dispatches for all types and also considers annotations. 
+
+In line \ref{algTranslateCompoundDeclarationSelf}, we determine the actual expression for self, i.e., the access expression $ca$ if given or the declaration $d$. Then, due to their specific priorities, we first translate all eval constraints defined along the type hierarchy for $t$ in lines \ref{algTranslateCompoundDeclarationEvalStart}-\ref{algTranslateCompoundDeclarationEvalEnd}. Afterwards, we include all remaining compound constraints, i.e., type constraints and annotation constraints in lines \ref{algTranslateCompoundDeclarationAllStart}-\ref{algTranslateCompoundDeclarationAllEnd}.
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{declaration $d$, variable $v$, compound type $t$, access $ca$}
+  \KwData{constraints $\otherConstraints$, variable mapping $\variableMapping$}
+
+  \uIf{$v\neq\undef$}{
+    \ForAll{$s \iterAssng slots(v)$ } {
+      $translateDeclaration(s, decision(v, s), \variableMapping[s]))$\; \label{algTranslateCompoundDeclarationTranslateSlotsV}
+    }
+  } \Else {
+    \ForAll{$s \iterAssng \setWithFlat{slots(u)}{u\in allRefines^+(t)}$ } {
+      $translateDeclaration(s, \undef, \variableMapping[s]))$\; \label{algTranslateCompoundDeclarationTranslateSlotsT}
+    }
   }
   \If{$\neg inc$} {
       \ForAll{$a \iterAssng assignments(t)$}{
-          $translateAnnotationAssignments(a, v, \undef, ca)$\; \label{algTranslateCompoundDeclarationCompoundAssignments}
+          $translateAnnotationAssignments(a, \undef, \undef, ca)$\; \label{algTranslateCompoundDeclarationCompoundAssignments}
       }
   }
-  \leIf{$ca \neq \undef$}{$f\assng ca$}{$f\assng d$}
-  $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{f}{c}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\;
-  $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}}{c\in allCompoundConstraints(t)}, true)$\;
-
- \caption{Translating compound declarations (\IVML{translateCompoundDeclaration}).}\label{algTranslateCompoundDeclaration}
-\end{algorithm}
-
-Now, we can translate further nested values / structures or contained constraints involving the mapping. First, Algorithm \ref{algTranslateCompoundDeclaration} inspects all slots / attributes. If one slot is a container of constraints, it translates all (constraint) values into instantiated constraints by substituting \IVMLself{} with the actual declaration (including matching mappings in $\variableMapping$) adding the translated constraint to the set of other constraints $\otherConstraints$. 
-
-Finally, the algorithm translates the nested structures. Then it translates all annotation value assignments using Algorithm \ref{algTranslateAnnotationAssignments}. For the last two translations, we need the actual value of \IVMLself{}, to be determined for the recent compound, either based on the given accessor $ca$ or the declaration $d$. Then, to keep the priority of eval-blocks, it collects all constraints of all nested eval-blocks, replaces \IVMLself{} and variable mappings $\variableMapping$ and adds them to $\otherConstraints$. Finally, we take over and translate all constraints of all transitively declared constraints refined compounds and assignment constraints.
+  \leIf{$ca \neq \undef$}{$f\assng ca$}{$f\assng d$}\label{algTranslateCompoundDeclarationSelf}
+  $eval \assng \setWithFlat{allEvalConstraints(r)}{r\in allRefines^+(t)}$\;\label{algTranslateCompoundDeclarationEvalStart}
+  $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}}{c\in eval}, true)$\;\label{algTranslateCompoundDeclarationEvalEnd}
+  $cmp \assng \setWithFlat{allCompoundConstraints(r)}{r\in allRefines^+(t)}$\;\label{algTranslateCompoundDeclarationAllStart}
+  $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}}{c\in cmp}, true)$\;\label{algTranslateCompoundDeclarationAllEnd}
+
+ \caption{Translating compound content (\IVML{translateCompoundContent}).}\label{algTranslateCompoundContent}
+\end{algorithm}
 
 \subsection{Container constraints}\label{sectContainerDefaults}
 
-Per se, a container variable can only declare the contained type and the respective element values through its default, i.e., there is no direct opportunity to define constraints for a container. However, constraints are indirectly defined through the contained type and the types used for the individual elements. Here, compounds, derived types, constraint types and, transitively, nested containers can introduce constraints further characterizing a container variable. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. Due to refinement, all relevant types may be more specific than the (generic) container type given for the initial container variable. 
+Per se, a container variable can only declare the contained type and the respective element values through its default, i.e., there is no direct opportunity to define constraints for a container. However, constraints are indirectly defined through the contained type and the types used for the individual elements. Here, compounds, derived types, constraint types and, transitively, nested containers can introduce constraints further characterizing (the contents of) a container variable. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. Due to refinement, all relevant types may be more specific than the (generic) container type given for the initial container variable. 
 
 \begin{algorithm}[H]
@@ -609,14 +664,18 @@
           $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{e}{ca}}}{e \in allElements(val)}, true)$\; \label{algTranslateContainerDeclarationConstraintContainer}
       } \ElseIf{$isCompound(t_b)$} {
-              $used \assng \setWith{base(u)}{u \in usedTypes(val) \wedge isContainer(base(u))}$\; \label{algTranslateContainerDeclarationUsedTypesDefault}
+           \If{$val \neq \undef$} {
+              $used \assng \setWithFlat{base(u)}{u \in usedTypes(val) \wedge isContainer(base(u))}$\; \label{algTranslateContainerDeclarationUsedTypesDefault}
+              $used \assng used \setminus \setWithFlat{allRefines(u)}{u \in used}$\; \label{algTranslateContainerDeclarationUsedTypesPrune}
+              } \Else {
+                $used \assng \set{t_b}$\; \label{algTranslateContainerDeclarationUsedTypesFallback}
+              }
               \ForAll{$u \iterAssng used$}{\label{algTranslateContainerDeclarationCompoundContainerDefaultsStart}
-                   $translateDefaultsCompoundsContainer(d, u)$\;
+                   $translateCompoundContainer(d, u, t_n, ca)$\;
                }\label{algTranslateContainerDeclarationCompoundContainerDefaultsEnd}
-               $used \assng used \setminus \setWith{allRefines(u)}{u \in used}$\;
-               \lIf{$|used| = 0$}{$used \assng \set{base(contained(d))}$}
-               \ForAll{$u \iterAssng used$} {\label{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart}
-                   $add(\otherConstraints, translateCompoundContainer(u, t_n, d, ca), true)$\;
-               }\label{algTranslateContainerDeclarationCompoundContainerUsedCompoundsEnd}
-          %$add(\otherConstraints, translateCompoundContainer(d, v, ca, used), true)$\;\label{algTranslateContainerDeclarationCompoundContainerCompounds}
+    %           $used \assng used \setminus \setWith{allRefines(u)}{u \in used}$\;
+     %          \lIf{$|used| = 0$}{$used \assng \set{base(contained(d))}$}
+      %         \ForAll{$u \iterAssng used$} {\label{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart}
+      %             $add(\otherConstraints, translateCompoundContainer(u, t_n, d, ca), true)$\;
+      %         }\label{algTranslateContainerDeclarationCompoundContainerUsedCompoundsEnd}
       }
       \uIf{$isDerived(t_n)$}{
@@ -628,79 +687,38 @@
 However, containers are different than usual variables as the may contain an arbitrary number of elements. Thus, for specifying a constraint over a container, we must apply all-quantification (the IVML \IVML{forAll} operation) for all constraints defined on contained types. Moreover, for nested collections we must apply the IMVL \IVML{flatten} operation to gain access to the individual elements, and for refined types even explicit IVML type casts using the \IVML{asType} operation to have access to specific operations, slots or annotations.
 
-Algorithm \ref{algTranslateContainerDeclaration} performs the transformation for a container variable declaration $d$ of variable $v$, if nested with given access expression $ca$ and specific type $t$ (due to a known default value). First, we determine the innermost nested type $t_n$ and its base type $t_b$ (taking derived types into account) as well as the relevant value $val$. If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we collect and translate all constraints constituted by all (flattened) element values in line \ref{algTranslateContainerDeclarationConstraintContainer}. If $v$ is a compound container, i.e., the innermost nested base type is a compound, we try to derive as many relevant constraints as possible. Therefore, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault}. For all these types, we determine all default value constraints using Algorithm \ref{algTranslateDefaultsCompoundContainer} in lines \ref{algTranslateContainerDeclarationCompoundContainerDefaultsStart}-\ref{algTranslateContainerDeclarationCompoundContainerDefaultsEnd}. Moreover, for all used most specific compound types (if there are none, we take the contained type of $d$ instead), we collect and instantiate all compound-related constraints using Algorithm \ref{algTranslateCompoundContainer2} in lines \ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart}-\ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsEnd}. As Algorithm \ref{algTranslateCompoundContainer2} takes all refined compounds into account, we leave out the refined types from the used containers in line \ref{algTranslateContainerDeclarationCompoundContainerUsedCompoundsStart}. 
-%For the remaining, not already translated compound types, we also apply Algorithm \ref{algTranslateCompoundContainer2}, here through Algorithm \ref{algTranslateCompoundContainer} (based on the configured value) in line \ref{algTranslateContainerDeclarationCompoundContainerCompounds}. 
-Independently of constraint or compound container, we finally translate and collect all constraints stemming from derived type definitions in line \ref{algTranslateContainerDeclaration}.
-
-We turn now to the algorithms that were used by Algorithm \ref{algTranslateContainerDeclaration}. 
-
-Algorithm \ref{algTranslateDefaultsCompoundContainer} creates constraints for default value instantiation of compound values directly created in container initializers, e.g., in IVML something like \IVML{seq = \{\{i=1\}, \{i=2\}\}}, assuming that \IVML{seq} is a sequence of compounds, which have an integer slot \IVML{i}. As these compounds are created implicitly within a container initializer, so far no default value constraints are created and scheduled to the constraint base, i.e., these compounds would remain uninitialized. Algorithm \ref{algTranslateDefaultsCompoundContainer} solves this by creating all-quantized constraints over all elements of the container applying the default value expressions to the elements. Utilizing quantor constraints here implies that default initializations, which remain undefined if some dependent variables have not been determined so far, cause a re-evaluation for all elements of the container. Here, unfolding the implicit loop of such a quantor may be a solution, as then only individual constraints are triggered. However, this only works for sequences, as sets do not provide element-wise/index-based access and unfolding the constraint for a large container also may create a huge number of constraints. Currently, we stay with the compromise of creating a single quantized constraint for all slots with default values.
-
-Algorithm \ref{algTranslateDefaultsCompoundContainer} creates the constraint in incremental fashion, considering several special cases but also allowing for optimization. Here, $d$ is a container variable declaration, $t$ the compound type to be processed, i.e., the innermost basic type of $type(d)$ or one of its refining compound types. For each constraint with default values of a given type, we create in line \ref{algTranslateDefaultsCompoundContainerInitE} an expression just holding the variable of the container $d$. 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$ to be processed is not the same as the type of the declaration $type(d)$, we must consider that the slot $s$ only exists for the specific refined type $t$, i.e., the instantiation applies only to container elements of type $t$ (or of refined types), i.e., we insert in line \ref{algTranslateDefaultsCompoundContainerCast} an element selection by type kind projecting the container to all elements of type $t$ (and refined types). As preparation for creating the quantor constraint, we create in line \ref{algTranslateDefaultsCompoundContainerTemporary} the temporary iterator $i$ variable of type $t$ and substitute in line \ref{algTranslateDefaultsCompoundContainerSubst} the variables of the default value expression for $u$ according to the actual variable mapping, replacing also \IVMLself{} by $i$ (not slot $s$, which may be of any other type). Finally, we create in line \ref{algTranslateDefaultsCompoundContainerQuantor} the all-quantor for all typed elements $i$ assigning slot $s$ on $i$ the value defined by the substituted default value expression.
-
-\begin{algorithm}[H]
-  \SetAlgoLined
-  \KwIn{declaration $d$, (specific) type $t$}
+Thus, the core idea of this algorithm is to consider all elements over all used types. If no value is available, we resort to the static type of the declaration of the containser variable. We create all-quantized constraints for all used types and distinguish between constraint containers, where the values directly turn into constraints, compound containers, where slots, constraints and annotations lead to further constraints, and derived types.
+
+Algorithm \ref{algTranslateContainerDeclaration} performs the transformation for a container variable declaration $d$ of variable $v$, if nested with given access expression $ca$ and specific type $t$ (due to a known default value). First, we determine the innermost nested type $t_n$ and its base type $t_b$ (i.e., ignoring intermediate derived types) as well as the relevant value $val$. If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we collect and translate all constraints constituted by all (flattened) element values in line \ref{algTranslateContainerDeclarationConstraintContainer}. If $v$ is a compound container, i.e., the innermost nested base type is a compound, we consider the used types. If there is a value, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault} and prune more general refined types in line \ref{algTranslateContainerDeclarationUsedTypesPrune}, as the following algorithm must anyway iterate over the refinement hierarchy. If there is no value, the only used type is the innermost nested base type $t_b$, actually a compound (line \ref{algTranslateContainerDeclarationUsedTypesFallback}). The, we iterate over all (pruned) used types and apply Algorithm \ref{algTranslateCompoundContainer}.  Independently of constraint or compound container, we finally translate and collect all constraints stemming from derived type definitions in line \ref{algTranslateContainerDeclaration}.
+
+Algorithm \ref{algTranslateCompoundContainer} creates constraints for compound values utilized in compounds, e.g., through a container initialize, in IVML like \IVML{seq = \{\{i=1\}, \{i=2\}\}}, assuming that \IVML{seq} is a sequence of compounds, which have an integer slot \IVML{i}. As these compounds are created implicitly within a container initializer, so far no default value constraints, nested constraints, annotation assignments etc. are scheduled to the constraint base, i.e., these compounds would remain uninitialized and their constraints not considered. 
+
+Algorithm \ref{algTranslateCompoundContainer} solves 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 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). 
+
+Now we create a context for the container on the stack of $\variableMapping$. In contrast to compound translations, we also register the prefix expression $e$ and the iterator variable $l$. As for compounds, we create now the compound mapping using Algorithm \ref{algTranslateCompoundContent}. Please note that slot access now happens via the iterator variable $l$, while annotation access happens through $ca$. Specifying $t$ also as target type avoids unnecessary type casts here. Then, we call Algorithm \ref{algTranslateCompoundContent} to translate the compound slots, implying translation of annotations as well as recursion over further compounds and containers.
+
+
+
+\TBD{Recursive case.}
+
+Utilizing quantor constraints here implies that default initializations, which remain undefined if some dependent variables have not been determined so far, cause a re-evaluation for all elements of the container. Here, unfolding the implicit loop of such a quantor may be a solution, as then only individual constraints are triggered. However, this only works for sequences, as sets do not provide element-wise/index-based access and unfolding the constraint for a large container also may create a huge number of constraints. Currently, we stay with the compromise of creating a single quantized constraint for all slots with default values.
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{declaration $d$, (specific) type $t$, declared type $u$, access $ca$}
   \KwData{deferred default constraints $\deferredDefaultConstraints$}
-  \ForAll{$s \iterAssng \setWith{dfltSlots(u)}{u \in allRefines^+(t)}$}{
-      $e\assng\createExpression{d}$\; \label{algTranslateDefaultsCompoundContainerInitE}
+  $l\assng \createExpression{\IVMLMeta{var}(t)}$\;
+
+  $e\assng\closedCases{ca, & \text{if } ca \neq \undef\\\createExpression{d}, &\text{else}}$\; \label{algTranslateDefaultsCompoundContainerInitE}
       \uIf{$isNested(type(d))$} {
         $e\assng\createExpression{\IVML{flatten}(d)}$\; \label{algTranslateDefaultsCompoundContainerFlatten}
       }
-      \uIf{$type(d)\neq t$} {
+      \uIf{$u\neq t$} {
             $e\assng\createExpression{\IVML{selectByKind}(e, t)}$\; \label{algTranslateDefaultsCompoundContainerCast}
       }
-      $i\assng\createExpression{\IVMLMeta{var}(t)}$\; \label{algTranslateDefaultsCompoundContainerTemporary}
-      $f\assng\varSubstitutionSelfVarMapping{default(s)}{i}$\; \label{algTranslateDefaultsCompoundContainerSubst}
-      $add(\deferredDefaultConstraints, \createDefaultConstraint{e\rightarrow \IVML{forAll}(i|\IVML{assign}(\IVML{acc}(i,name(s)), f)})$\; \label{algTranslateDefaultsCompoundContainerQuantor}
-   }
- \caption{Translating defaults in compound containers (\IVML{translateDefaultsCompoundContainer}).}\label{algTranslateDefaultsCompoundContainer}
-\end{algorithm}
-
-\MISSING{---HERE---}
-%-----------------------------------------------------------------------------------------------------------------
-
-In addition to the default value expression, we must also consider all constraints for a compound type used in a container. 
-
-%Algorithm \ref{algTranslateCompoundContainer} is called in Algorithm \ref{algTranslateContainerDeclaration} line \ref{algTranslateContainerDeclarationCompoundContainerCompounds} as a fallback even if no relevant value for can be determined. 
-
-%As Algorithm \ref{algTranslateCompoundContainer} is used within different algorithms, we return the collected constraints here.
-%The relevant types to be considered includes the contained type of $d$ and the types of all elements. If the respective type is a compound, we perform the actual translation (cf. Algorithm \ref{algTranslateCompoundContainer2}).
-
-%\begin{algorithm}[H]
-%  \SetAlgoLined
-%  \KwIn{declaration $d$, variable $v$, compound access $ca$, compound set $done$}
-%  \KwOut{resulting constraints $c$}
-%
-%      $c \assng \set$\;
-%      $tc \assng contained(type(d))$\;
-%      \ForAll{$t \iterAssng \set{tc} \cup \setWith{type(value(e))}{e\in allElements(v)}$}{
-%          \lIf{$isDerived(t)$}{$t \assng base(t)$}
-%          \uIf{$isCompound(t) \wedge (done = \undef \vee done[t]=\undef)$}{
-%              $c \assng c \cup translateCompoundContainer(t, tc, d, ca)$\;
-%          }
-%   }
-% \caption{Translating compound constraints from a container (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer}
-%\end{algorithm}
-
-
-\begin{algorithm}[H]
-  \SetAlgoLined
-  \KwIn{compound type $t$, declared compound type $dt$, declaration $d$, compound access $ca$}
-  \KwData{variable mapping $\variableMapping$}
-  \KwOut{resulting constraints $c$}
-
-  $c \assng \set$\;
-  $v \assng \createExpression{\IVML{\IVMLMeta{var}(t)}}$\;
-  \ForAll{s \iterAssng slots(t)} {
-      $\variableMapping \assng \variableMapping \addMap \mapEntry{s}{\createExpression{\IVMLMeta{acc}(v,s)}}$\;
-  }
-  \ForAll{$e \iterAssng allCompoundConstraints(t) \cup allVariableConstraints(t)$} {
-    $coll \assng\createExpression{\closedCases{ca, & \text{if } ca = \undef \\ d, &\text{else}}}$\;
-    \lIf{$nested(d)$}{$coll \assng\createExpression{\IVML{flatten}(coll)}$}
-    $coll \assng\createExpression{coll.\closedCases{\IVML{selectByKind}(a, t), & \text{if } t \neq dt \\  &\text{else}}}$\;
-    $c\assng c \cup \createConstraint{coll\rightarrow\IVML{forAll}(i|\text{ }\varSubstitutionVarMapping{e})}$\;
-  }
-
- \caption{Translating compound constraints from a container (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer2}
+    $pushContext(\variableMapping, \undef, e, l)$\;
+    $registerCompoundMapping(t, l, d, t)$\;
+    $translateCompoundContent(l, \undef, t, ca)$\;
+    $popContext()$\;
+ \caption{Translating constraints for compound containers (\IVML{translateCompoundContainer}).}\label{algTranslateCompoundContainer}
 \end{algorithm}
 
@@ -728,5 +746,5 @@
 
 Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the set of effective assignments data $ea$ that is relevant for the actual assignment-block $a$ (initially $ea=\emptySet$ for a top-level assignment-block). 
-For a given assignment-block $a$, the algorithm performs then the transformation of each individual assignment and collects the created constraints in $\otherConstraints$. 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.
+For a given assignment-block $a$, the algorithm performs then the transformation of each individual assignment and collects the created constraints in $\otherConstraints$. 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). It is important to note that we temporarily activate a context frame of $\variableMapping$ for each declaration $d$ if a context has been created/registered before during compound translation. This is required as the constraints are actually created after the translation of the types and otherwise we would still use the original variables specified in the model rather than the instantiated ones needed for reasoning. Finally, the algorithm recursively processes contained assignment-blocks.
 
 \begin{algorithm}[H]
@@ -738,4 +756,5 @@
   \ForAll{$e \iterAssng ea$}{
       \ForAll{$d \iterAssng slots(a)$} {
+          $activate(\variableMapping, d)$\;
           $add(\otherConstraints, \set{translateAnnotationAssignment(e, d, ca)}, false)$\;
           $t \assng type(d)$\;
@@ -751,4 +770,5 @@
               }
           }
+          $deactivate(\variableMapping, d)$\;
       }
   }
@@ -771,27 +791,17 @@
 \subsection{Constraint variables}\label{sectConstraintVariables}
 
-Constraint variables can be created by taking the respective default/actual variable, performing the variable substitution with $\variableMapping$ and, if available, a respective value for \IVMLself, turning the resulting expression into a constraint and adding it to the set of other constraints $\otherConstraints$. Moreover, the relationship between the underlying variable $v$ and the constraint must be recorded for efficient update of the constraint base upon value change (cf. Algorithm \ref{algVarChange}).
-
-\begin{algorithm}[H]
-  \SetAlgoLined
-  \KwIn{constraint expression $c$, actual value for \IVMLself $s$, variable $v$}
+Constraint variables can be created by taking the respective default/actual variable, performing the variable substitution with $\variableMapping$ and, if available, a respective value for \IVMLself, turning the resulting expression into a constraint and adding it to the set of other constraints $\otherConstraints$. Moreover, the relationship between the underlying variable $v$ and the constraint must be recorded for efficient update of the constraint base upon value change (cf. Algorithm \ref{algVarChange}). Recording happens only if $v$ is defined, which may not be the case if this algorithm is called while processing container values.
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{constraint expression $c$, actual value for \IVMLself{} $f$, variable $v$}
   \KwData{other constraints $\otherConstraints$, relevant constraints $\relevantConstraints$}
 
-      $c \assng \createConstraint{\varSubstitutionSelfVarMapping{c}{s}}$\;
+      $c \assng \createConstraint{\varSubstitutionSelfVarMapping{c}{f}}$\;
       $add(\otherConstraints, \set{c}, true)$\;
-      \MISSING{map v to c for dynamic value type change}\;
-      $\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{c}{v}$
-      
-      
-      %    $add(\otherConstraints, \set{\createConstraint{\varSubstitutionSelfVarMapping{default(s)}{d}}}, true)$\;
-                  %$add(\otherConstraints, \createConstraint{dflt}, true)$\;
-                  %$\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{\createConstraint{dflt}}{v}$
-
-
-      %\If{$isConstraint(type(s)) \wedge default(s) \neq \undef$}{
-      %}
-
-%  $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{ }\varSubstitution{c}{decl(c)=d})}}{c \in cs}, true)$\;
+      \If{$v \neq \undef$}{
+         \MISSING{map v to c for dynamic value type change}\;
+          $\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{c}{v}$
+      } 
  \caption{Creating constraints for constraint variables (\IVML{createConstraintVariableConstraint}).}\label{algCreateConstraintVariableConstraint}
 \end{algorithm}
@@ -804,4 +814,5 @@
   \KwIn{constraint sequence $s$, constraint $c$, perform initializers $check$}
   \KwData{top level and other constraints $\topLevelConstraints, \otherConstraints$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraints$ , incremental flag $inc$, evals flag $inEvals$}
+  $c = composeExpression(\variableMapping, c)$\;
   \If{$\neg inc \vee (inc \wedge \neg isAssignment(c))$} {
     \If{$check$}{