Index: /reasoner/consTranslation.tex
===================================================================
--- /reasoner/consTranslation.tex	(revision 207)
+++ /reasoner/consTranslation.tex	(revision 208)
@@ -180,7 +180,11 @@
 \subsubsection{Registering Compound Accessor Expressions}\label{sectionRegCompAcc}
 
-We detail now the variable mapping for compound types. Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations of a given compound type $t$, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The access expressions $ca$ is optional and, if given, utilized as prefix to create access expressions for slots and annotations. If $ca$ is not given, $e_d$ is used instead, usually containing an expression to the variable declaration using $t$. Algorithm \ref{algRegisterCompoundMapping} iterates over all slots defined for the given compound type $t$ including shadowed ones along the refinement hierarchy starting at $t$. If a slot already has a local access expression mapping (line \ref{algRegisterCompoundMappingExMapping}), it is shadowed and we just use the already registered more specific expression. If no mapping exists, Algorithm \ref{algRegisterCompoundMapping} a respective accessor for slot $s$. If the compound access expression $ca$ is not given, Algorithm \ref{algRegisterCompoundMapping} creates a static accessor based on $e_d$. The created accessor $x$ is then registered with $\variableMapping$. Similarly, we register accessors for annotations of the current slot $s$ based on the accessor $x$ for $s$. Finally, the algorithm creates accessors for all annotations declared for the underlying compound variable (through $e_d$).
-
-Given a complete mapping for compound type $t$, we can transform the constraints, i.e., apply Algorithm \ref{algTranslateCompoundContent}. As mentioned above, the algorithm first translates all default value expressions of slots, then the default values from annotation assignments, and, finally, the constraints in eval blocks with higher evaluation priority as well as the remaining nested constraints. When translating the default value expression for slots, Algorithm \ref{algTranslateCompoundContent} calls Algorithm \ref{algTranslateDeclaration}, and, thus, triggers a potentially recursive translation along the respective slot types, in particular in case of compound or container slots.
+We detail now the variable mapping for compound types. Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations of a given compound type $t$, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The access expressions $ca$ is optional and, if given, used as qualifying access expression for contained slots and annotations. If $ca$ is not given, $e_d$ is used instead\footnote{In the implementation, defining a "joint" accessor expression for $d$ in terms of an extra parameter enables instance reuse of the accessor.}, usually containing an expression to the variable declaration of type $t$. In Algorithm \ref{algRegisterCompoundMapping} we create for $t$ a context frame that contains accessor expressions for all slots declared in $t$ including all visible slot declarations for all types in $refines(t)$. Thereby,  we must consider inherited as well as refined/shadowed slots. Slot $s$
+
+\begin{itemize}
+  \item is declared in $t$ and no further slot with $name(s)$ is defined in any $u\in refines(t)$. Then an accessor expression for $s$ shall be registered in the context frame.
+  \item is inherited from a refined component $u\in refines(t)$. $u$ declares $s$ and $t$ does not declare a slot with $name(s)$, but $s$ is accessible in $t$ through compound refinement. Then the context frame shall contain an accessor for $s$ as if it would be declared in $t$.
+  \item shadows all slots with $name(s)$ that may be available through inheritance from $refines(t)$, if $t$ declares $s$ and at least one of its refined types also declare a slot with $name(s)$. In this case, the context frame shall contain an accessor expression for $s$ as defined in $t$.
+\end{itemize}
 
 \begin{algorithm}[H]
@@ -191,7 +195,7 @@
   \ForAll{$s \iterAssng slots^+(t)$} { \label{algRegisterCompoundMappingVarMappingStart} %actual slots
         $x \assng getLocalMapping(\variableMapping, name(s))$\; \label{algRegisterCompoundMappingExMapping}
-        \If{$x = \undef$} {
+        \If{$x = \undef$} {\label{algRegisterCompoundMappingAccStart}
             $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d, s), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca, s), &\text{else}}}$\; \label{algRegisterCompoundMappingVarMapping}
-        }
+        }\label{algRegisterCompoundMappingAccEnd}
         $registerMapping(\variableMapping, s, x)$\;
         \ForAll{$a \iterAssng annotations(s)$}{
@@ -199,13 +203,18 @@
         }
   }\label{algRegisterCompoundMappingVarMappingEnd}
-  \ForAll{$a \iterAssng annotations^+(decl(e_d))$}{
+  \ForAll{$a \iterAssng annotations^+(decl(e_d))$}{\label{algRegisterCompoundMappingEdStart}
      $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca, a), &\text{else}}}$\; \label{algRegisterCompoundMappingCreateExpression}
       $registerMapping(\variableMapping, a, x)$\; % left out origins
-    }
-
+    }\label{algRegisterCompoundMappingEdEnd}
  \caption{Registering the compound mapping (\IVML{registerCompoundMapping}).}\label{algRegisterCompoundMapping}
 \end{algorithm}
 
+Algorithm \ref{algRegisterCompoundMapping} iterates over all slots of $t$ and its refined compounds using $slots^+(t)$, which contains all potentially visible slots for $t$ along the refinement hierarchy starting with the slots of $t$. Due to this processing sequence, the decision whether we must create a new accessor for slot $s$ just depends on if there is already an access expression defined for $name(s)$ in the actual (local) context frame (line \ref{algRegisterCompoundMappingExMapping}). Lines \ref{algRegisterCompoundMappingAccStart}-\ref{algRegisterCompoundMappingAccEnd} create such an accessor expression if none was found in the actual context frame. The accessor is either based on $ca$ (if given) or on $e_d$. The created accessor $x$ is then registered in the actual context frame of $\variableMapping$.  Similarly, we create accessors for all declared annotations of $s$ based on the accessor $x$ for $s$. 
+
+Finally, in lines \ref{algRegisterCompoundMappingEdStart}-\ref{algRegisterCompoundMappingEdEnd}, the algorithm creates accessors for all annotations directly declared for the underlying compound variable (through $e_d$).
+
 \subsubsection{Translating Compound Constraints}\label{sectionTransComp}
+
+Given a complete mapping for compound type $t$, we can transform the constraints, i.e., apply Algorithm \ref{algTranslateCompoundContent}. As mentioned above, the algorithm first translates all default value expressions of slots, then the default values from annotation assignments, and, finally, the constraints in eval blocks with higher evaluation priority as well as the remaining nested constraints. When translating the default value expression for slots, Algorithm \ref{algTranslateCompoundContent} calls Algorithm \ref{algTranslateDeclaration}, and, thus, triggers a potentially recursive translation along the respective slot types, in particular in case of compound or container slots.
 
 Let