Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 126)
+++ /reasoner/reasoner.tex	(revision 127)
@@ -139,5 +139,5 @@
 For all IVML elements introduced in the following subsections, we denote the set of constraints\footnote{Duplicates do not matter in this document as constraints are usually rather unique structures. The only effects of duplicates could be unintended re-evaluations or unintended multiple error messages for the duplicated constraints.} defined for element $e$ by $constraints(e)$. Let $s$ be a set of elements, then $constraints(s) = \setWith{constraints(t)}{t\in s}$. Further, for a model element $e$, $parent(e)$ denotes the model element $e$ is nested within, typically, a compound or a project.
 
-\subsubsection{Variable Declarations}
+\subsubsection{Variable Declarations}\label{sectNotationVarDecls}
 
 An IVML \emph{variable declaration} $d$ is defined through a $name(d)$ and a $type(d)$.~$default(d)$ is an optional expression specifying the default value of $d$, whereby $default(d)$ must evaluate to a value of a type compatible with $type(d)$. $isDeclaration(d)$ is true for a variable declaration $d$. 
@@ -161,9 +161,11 @@
 \subsubsection{Configuration Variables}\label{sectNotationConfigVars}
 
-An IVML \emph{configuration variable} $v$ is an instance of a variable declaration $d$ as part of a certain configuration $cfg$, i.e., $decision(cfg, d)=v$. For such a combination of declaration $d$ and variable $v$, we define $declaration(v) = d$ as well as $type(v) = type(declaration(v))$. For a variable $v$, the function $isVariable(v)$ returns $true$, for any other IVML element/type $false$.
-
-$value(v)$ denotes the actual value of $v$, with $type(value(v))$ compliant with $type(v)$. Please note, that $type(value(v))$ can be a subtype of $type(v)$ (cf.~\cite{IVML-LS} for details on the IVML type compliance rules and the IVML type hierarchy).
-
-As types like container or compound require a nesting of configuration variables, we generically define $nested(v)$ as the set of all variables nested in $v$ and $nested(v, n)$ the nested variable with name $n$ in $v$ ($nested(v, n)$ may be undefined). Of course, $nested(v)=\setEmpty$ if no nested variables are defined on $v$, $type(v)$ or $type(value(v))$. We define $parent(v)$ as the object $v$ is nested within, which is either the containing configuration if $v$ is a top-level variable or the parent variable, i.e., $\forall_{n\in nested(v)}:parent(n)=v$. For convenience, we also define
+While variable declarations as introduced in Section \ref{sectNotationVarDecls} as well as types as introduced below allow defining (a meta-model of) configuration options, \emph{configuration variables} are part of the configuration of a specific product and hold the actual configured value for a variable declaration. A configuration variable $v$ (representing a decision, inspired by decision modeling~\cite{CzarneckiGruenbacherRabiser+12, SchmidJohn04}) is defined through a variable declaration $d$, but for a single variable declaration $d$ in a model, multiple configuration variables can exist in different configurations. 
+
+Let $v$ be a (top-level) configuration variable of variable declaration $d$ as part of a certain configuration $cfg$, i.e., $decision(cfg, d)=v$ and $parent(v)=cfg$. For such a combination of declaration $d$ and variable $v$, we define $declaration(v) = d$ as well as $type(v) = type(declaration(v))$. For a variable $v$, the function $isVariable(v)$ returns $true$, for any other IVML element/type $false$.
+
+$value(v)$ denotes the actual value of $v$ and $type(value(v))$ compliant with $type(v)$. Please note, that $type(value(v))$ can be a subtype of $type(v)$, in particular if $type(v)$ is a refined type through inheritance (cf.~\cite{IVML-LS} for details on the IVML type compliance rules and the IVML type hierarchy).
+
+As some IVML types allow a nesting of configuration variables, we generically define $nested(v)$ as the set of all variables nested in $v$. Of course, $nested(v)=\setEmpty$ if no nested variables are defined on $v$, $type(v)$ or $type(value(v))$. For a variable $v$, $\forall_{w\in nested(v)}\text{ } parent(w)=v$ must hold. Moreover, let $nested(v, n)$ be the nested variable in $v$ with name $n$, while $nested(v, n)=\undef$ if no such variable is defined. For convenience, we also define
 %
 \begin{multline*}
@@ -592,5 +594,5 @@
 \begin{enumerate}
   \item Constraint $c$ is evaluated successfully so that existing problem records for $c$ can be removed from $\problemRecords$. 
-  \item Constraint $c$ is evaluated as undefined. As specified by IVML \ref{IVML-LS}, a constraint for which at least one variables or expressions is evaluated to undefined, is also considered undefined. This situation does not lead to the creation of a problem record, as the constraint can either be ignored or will be re-scheduled if one of the (currently undefined) variables is changed through the evaluation of another constraint. 
+  \item Constraint $c$ is evaluated as undefined. As specified by IVML \cite{IVML-LS}, a constraint for which at least one variables or expressions is evaluated to undefined, is also considered undefined. This situation does not lead to the creation of a problem record, as the constraint can either be ignored or will be re-scheduled if one of the (currently undefined) variables is changed through the evaluation of another constraint. 
   \item The constraint evaluation fails and a problem record is created including the used variables $\usedVariables$ for detailed error reporting or further (external) analysis. 
 \end{enumerate}
@@ -727,5 +729,6 @@
 Algorithm \ref{algTranslateCompoundDeclaration} collects and translates the 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$). No translation happens if type $t$ was already processed, e.g., in case of recursive compound types. 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$\footnote{For optimizing constraint rescheduling (see Section \ref{sectTopLevelConstraintsRescheduling}), the algorithm applies type exclusions to the actual context by transferring them and storing the causing type $t$ in the current context}. Used types are registered only if there is no variable $v$ given, e.g., we process constraints according to a potentially recursive type structure. If a variable $v$ is given, the nested variables are initialized correctly, in particular recursively nested variables terminate correctly based on configured values, i.e., we do not have to take care of recursion in this case. 
 
-The main two steps are detailed in Algorithm \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent} as both Algorithms are reused with different arguments during the translation of compounds in Section \ref{sectCompoundDefaults}. Algorithm \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. As the context with the compound mapping is only valid during Algorithm \ref{algRegisterCompoundMapping}, default value expressions must be translated within the actual context, i.e., if $deflt$ has been passed in, lines \ref{algTranslateCompoundSubstStart}-\ref{algTranslateCompoundSubstEnd} perform the respective substitution, which will be returned as result of Algorithm \ref{algRegisterCompoundMapping}. Finally, Algorithm \ref{algTranslateCompoundDeclaration} removes the actual context frame for this compound from $\variableMapping$.
+The main two steps are detailed in Algorithm \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent} as both Algorithms are reused with different arguments during the translation of compounds in Section \ref{sectCompoundDefaults}. Algorithm \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. 
+%As the context with the compound mapping is only valid during Algorithm \ref{algRegisterCompoundMapping}, default value expressions must be translated within the actual context, i.e., if $deflt$ has been passed in, lines \ref{algTranslateCompoundSubstStart}-\ref{algTranslateCompoundSubstEnd} perform the respective substitution, which will be returned as result of Algorithm \ref{algRegisterCompoundMapping}. Finally, Algorithm \ref{algTranslateCompoundDeclaration} removes the actual context frame for this compound from $\variableMapping$.
 
 \begin{algorithm}[H]
@@ -775,5 +778,5 @@
   }\label{algRegisterCompoundMappingVarMappingEnd}
   \ForAll{$a \iterAssng annotations^+(decl(e_d))$}{
-     $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), a), &\text{else}}}$\; \label{algRegisterCompoundMappingAnnotationMapping}
+     $x \assng \createExpression{\closedCases{\IVMLMeta{acc}(e_d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(\IVML{asType}(ca, t_t), a), &\text{else}}}$\; \label{algRegisterCompoundMappingCreateExpression}
       $registerMapping(\variableMapping, a, x)$\; % left out origins
     }
@@ -1208,5 +1211,5 @@
          }
 
-  \caption{Reschedule a value change (\IVML{rescheduleValueChange}).}\label{algContainerValue}
+  \caption{Reschedule a value change (\IVML{rescheduleValueChange}).}\label{algRescheduleContainerValue}
 \end{algorithm}
 
@@ -1271,5 +1274,5 @@
 In this section, we discuss the completeness of the reasoner with respect to IVML concepts. Reasoning completeness, e.g., involving advanced reasoning capabilities such as narrowing down value instances by limiting constraints or instance creation, is not topic of this section and may be targeted by future work.
 
-\begin{table*}[h]
+\begin{table*}[ht]
 %\begin{adjustbox}{angle=90}
 \centering
@@ -1332,5 +1335,5 @@
 \TBD{Check quantized instance constraints.}
 
-\begin{table*}[h]
+\begin{table*}[ht]
 %\begin{adjustbox}{angle=90}
 \centering
@@ -1385,5 +1388,5 @@
 \TBD{No annotation, assignment blocks and partial evaluation possible from IVML syntax. Accessor-based access handled by \tabAlg{algTranslateDeclaration}.} 
 
-\begin{table*}[h]
+\begin{table*}[ht]
 %\begin{adjustbox}{angle=90}
 \centering
@@ -1437,5 +1440,5 @@
 \TBD{Recursive annotations are not supported by IVML, add section number below. A*1 means all annotation-related tests, which focus on one specifc type used in the annotation, e.g., ACn1 for a compound used in an annotation, but always applied to all relvant types.} 
 
-\begin{table*}[h]
+\begin{table*}[ht]
 %\begin{adjustbox}{angle=90}
 \centering
@@ -1546,5 +1549,5 @@
 For referencing the test cases, we use identifiers composed for the main concepts to be validated. We use the abbreviations shown in Table \ref{tab:testCaseIdSchema} to compose identifiers. For example, test case nuber one on Integer (I) variables used as compound (Co) slots is identified by 'ICo1'. Table \ref{tab:reasonerTestCasesBasics} and Table \ref{tab:reasonerTestCasesAdvanced} list the test cases referenced in this document. Test case names ending with 'Valid' indicate that there is an associate test case testing also the failing of the constraint under test.
 
-\begin{table*}[h]
+\begin{table*}[ht]
 %\begin{adjustbox}{angle=90}
 \centering
@@ -1578,5 +1581,5 @@
 
 
-\begin{table*}[h]
+\begin{table*}[ht]
 %\begin{adjustbox}{angle=90}
 \centering
@@ -1627,5 +1630,5 @@
 \footnotetext{A similar test is defined for all basic types.}
 
-\begin{table*}[h]
+\begin{table*}[ht]
 %\begin{adjustbox}{angle=90}
 \centering
@@ -1682,5 +1685,5 @@
 \footnotetext{This test aims at recursive compound types.}
 
-\begin{table*}[h]
+\begin{table*}[ht]
 %\begin{adjustbox}{angle=90}
 \centering