Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 15)
+++ /reasoner/reasoner.tex	(revision 16)
@@ -59,10 +59,12 @@
   \item $isDerived(t)$ whether $t$ is a derived type. In this case, $basis(t)$ is the basis type $t$ is derived from, else $basis(t) =\undef$
   \item $refines(t)$ is the set of compounds directly refining compound $t$, if there are none or $t$ is not a compound $refines(t)=\emptySet$
+  \item $base(t)$ the type $t$ is derived from if $isDerived(t)$, $contained(t)$ the type contained in $t$ if $isCollection(t)$ or $t$
   \item $constraints(t)$ is the set of constraints defined for type $t$, similarly for a declaration $d$. Let $s$ be a set of types or declarations, then $constraints(s) = \setWith{constraints(t)}{t\in s}$.
   \item $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
-  \item $alBase(t) = \begin{cases}\set{t}, & \text{if } isDerived(t) \wedge  base(t) = \undef \\  \set{t} \cup allBase(base(t)), & \text{if } isDerived(t) \wedge base(t) \neq \undef \\ \emptySet, & \text{else}\\ \end{cases}$
+  \item $allBase(t) = \begin{cases}\set{t}, & \text{if } isDerived(t) \wedge  base(t) = \undef \\  \set{t} \cup allBase(base(t)), & \text{if } isDerived(t) \wedge base(t) \neq \undef \\ \emptySet, & \text{else}\\ \end{cases}$
   \item $allRefines(t) = \begin{cases}\emptySet, & \text{if } refines(t) = \emptySet \\  allRefines(t) \cup \bigcup_{u\in refines(t)} allRefines(u), & \text{else}\\ \end{cases}$
   \item $allRefines^+(t) = \begin{cases}allRefines(t) \cup \set{t}, & \text{if } isCompound(t) \\ \emptySet, & \text{else} \\  \end{cases}$
   \item Creating a constraint through OCL function call notation in angle brackets, e.g., $\createConstraint{\IVML{assign}(x, 25)}$ represents the IVML constraint \IVML{x = 25;}. If the constraint is marked as a default constraint, then we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$, if it is an internal \TBD{clarify semantics }constraint for reasoning we use $\createInternalConstraint{\IVML{assign}(x, 25)}$. We indicate IVML operations in teletype font.
+  \item $usedTypes(c) = \setWith{contained(type(e))}{e\in elements(c)}$ the set of (contained) types used in collection $c$
 \end{itemize}
 \TBD{Algorithms + implementation name}
@@ -154,10 +156,5 @@
 must be translated into a constraint $variable = expression$. Thereby, constraints defined over the type of the variable, e.g., in case of a derived type must be instantiated for the respective variable. 
 
-The top-level transformation is defined by Algorithm \ref{algTranslateDefaults}. It considers all variable declarations in the given project and 
-\begin{itemize}
-  \item translates the constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) and stores them into the global set of internal constraints $c_i$
-  \item constructs the default value assingment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $c_i$
-  \item \TBD{fill}
-\end{itemize}
+The top-level transformation is defined by Algorithm \ref{algTranslateDefaults}. It considers all variable declarations in the given project and runs Algorithm \ref{translateDeclarationDefaults} on them.
 
 \begin{algorithm}[H]
@@ -171,4 +168,14 @@
  \caption{Translating project default value expressions to constraints (\IVML{translateDefaults}).}\label{algTranslateDefaults}
 \end{algorithm}
+
+Algorithm \ref{translateDeclarationDefaults} translates the default value expression according to the actual type of the declation $d$ or, if applicable, the value represented by the default value expression. The algorithm
+\begin{itemize}
+  \item Translates the constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) and stores them into the global set of internal constraints $c_i$
+  \item Constructs the default value assignment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $c_i$
+  \item Translates the default value expression and the constraints for all nested compound slots if $d$ is a compound. Therefore, the algorithm uses the type of $d$ or, if available, or the actual type of the default value expression, which may be a refined type of $d$. The translation of the nested compound slots contributes to the variable-accessor mapping $c$. Then the algorithm  substitutes all occurrences of \IVML{self} by the actual declaration as well as all mapped variables from $m$ in the default value expression. It is important that the constraints for the nested compound slots must be translated regardless wether a default value expression for $d$ is specified.
+  \item Collects all transformed collection compounds based on the actual used types if $d$ is a collection. If $d$ is a collection over compounds, here all potentially refined compound types and their specific constraints are considered.
+  \item Translates remaining (slot) default value expression by replacing potential self usages with the compound access. In case that self is used in the default value expression or the declaration is an overriding slot, the expression shall be turned into a deferred default value constraint ($c_{dd}$), i.e., a constraint that is evaluated later than all usual default value constraints. Deferring these constraints ensures that individual slots are assigned after values for entire compounds or containers on top-level are assigned, i.e., the individual slot value is not accidentally overridden by a more global value for the entire structure. 
+\end{itemize}
+\TBD{Check - why here: Then, usual collection compound constraints as well as internal collection constraints stemming from derived types (cf. Section \ref{sectDerivedTypes}) are collected}. Finally, the default value expression is turned into a constraint. If the declaration is a constraint variable, i.e., a variable that contains an overridable constraint, \TBD{check ca not present} then the default value expression already represents the constraint and can be added to the constraint set of constraint variables $c_v$. Else, an assign constraint for the declaration $d$ (or the compound access in case of default constraints \TBD{check why}) is constructed and added either to $c_d$ or $c_{dd}$ as determined before. 
 
 \begin{algorithm}[H]
@@ -186,5 +193,5 @@
         } \ElseIf{$ dflt \neq \undef $}{
           \uIf{$ isContainer(type(d)) $}{
-              \ForAll{$u \iterAssng \TBD{usedTypes(dflt)}$}{
+              \ForAll{$u \iterAssng usedTypes(dflt)$}{
                    \TBD{$collectCompoundsCollection(d, u)$}\;
               }
@@ -198,10 +205,10 @@
       \If{$ deflt \neq \undef $}{
           \uIf{$isConstraint(t)$}{
-              \lIf{$ ca \neq \undef $}{$c_v \assng c_v \cup (\createConstraint{dflt}, v)$}
+              \lIf{$ ca == \undef $}{$c_v \assng c_v \cup (\createConstraint{dflt}, v)$}
           }\Else{
               $dfltS \assng dfltS \cup \createDefaultConstraint{\IVML{assign}(\left.\begin{cases}ca, & \text{if } dfltS == c_d \\ d, &\text{else}\end{cases}\right\}, deflt)}$\;
           }
       }
- \caption{Translating default value expressions to constraints (\IVML{translateDeclarationDefaults}).}\label{algTranslateDefaults}
+ \caption{Translating default value expressions to constraints (\IVML{translateDeclarationDefaults}).}\label{translateDeclarationDefaults}
 \end{algorithm}