Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 125)
+++ /reasoner/reasoner.tex	(revision 126)
@@ -137,19 +137,25 @@
 As a convention to ease reading the algorithms presented later, we use $d$ for variable declarations, $v$ for configuration variables, $t$ for types, $val$ for a values, $c$ for constraints and $cfg$ for configurations consting of decision variables and their assigned values. For temporary/local variables, we typically use a name close by, e.g., $w$ for an iterator variable (instead of $v$) etc. If not indicated otherwise, all operations introduced below that are bound to a certain type, e.g., an IVML compound, return $\undef$ if the operation is used with another type, e.g., an IVML basic type.
 
-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}$. 
+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}
 
-An IVML \emph{variable declaration} $d$ specifies a variable with $name(d)$ and $type(d)$.~$default(d)$ is an expression specifying the default value of $d$, whereby $default(d)$ must evaluate to a type compatible with $type(d)$. $isDeclaration(d)$ is true for a variable declaration $d$. Further, $parent(d)$ is the model element the declaration $d$ is nested within, typically, a compound or a project. Moreover, $annotations(d)$ denotes the set of (orthogonal) IVML annotation (variable) declarations for $d$ and $isAnnotation(d)$ returns whether a variable declaration is an annotation. Let $annotation(d, n) = a$ if $a\in annotations(d) \wedge name(a)=m$, else $annotation(d, n) = \undef$. 
-%
-For an arbitrary model element $e$ (including type definitions, projects and variable declarations), $parent(e)$ returns the parent model element and $isAssngBlock(e)$ returns whether $e$ is an assignment block. Moreover, 
+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$. 
+
+$annotations(d)$ denotes the set of (orthogonal) IVML annotation (variable) declarations for $d$ and $isAnnotation(d)$ returns whether a variable declaration is an annotation. $annotations(d)=\emptySet$ if $d$ does not define any annotations. Further, $annotation(d, n)$ indicates whether for declaration $d$ an annotation $a$ with name $n$ is defined. 
 %
 $$
+  annotation(d, n) = \begin{cases}a & \text{if }annotations(d) \wedge name(a)=n\\
+                                                       \undef & \text{else}\end{cases}
+$$
+To ease the definition of actual annotation values, IVML defines so called assignment blocks. An assignment block is a block that indicate the actual value of at least on annotation variable and applies the related value assignment to all variable declarations stated within the block. For the variable declarations appear as if they are directly defined within the containing element. For an arbitrary model element $e$, $isAssngBlock(e)$ returns whether $e$ is an assignment block. Moreover, 
+%
+\begin{multline*}
     annotations^+(e) = \begin{cases}
-      annotations(e), &\text{if } parent(e) = \undef \\
-      annotations(e) \cup annotations(parent(e)), &\text{else}
+      annotations(e) &\text{if } parent(e) = \undef \\
+      annotations(e)\text{ } \cup\\\text{ }annotations(parent(e)) &\text{else}
 \end{cases}
-$$
-returns all declared annotations for an arbutrary model element $e$, in particular a variable declaration or a slot, assuming that $annotations(e)=\emptySet$ for model elements that do not declare annotations. 
+\end{multline*}
+returns all declared annotations for an arbitrary model element $e$. 
 
 \subsubsection{Configuration Variables}\label{sectNotationConfigVars}