Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 123)
+++ /reasoner/reasoner.tex	(revision 124)
@@ -33,5 +33,5 @@
 \newcommand\setSepText[0]{colon }
 \newcommand\seq[1]{[#1]}
-\newcommand\seqEmpty[0]{\set{\text{}}}
+\newcommand\seqEmpty[0]{\seq{\text{ }}}
 \newcommand\seqWith[2]{[#1:#2]}
 \newcommand\subTypeOf[2]{t \succ s}
@@ -118,20 +118,20 @@
 \section{Notation and Terminology}\label{sectNotation}
 
-In this section, we clarify the notation and terminology that we use for explaining the reasoning process and the constraint translation.
+In this section, we define the notation and terminology that we use for explaining the reasoning process and the constraint translation.
 
 \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). For convenience, we assume for a set $s_3$, $s_3 \cup \undef = s_3$.
-
-For some parts of the reasoning algorithm, in particular to prioritize constraint types, we need \emph{sequences}, i.e., structures that contain elements in the order given by inserting the elements and potentially containing duplicates. We denote a sequence by $q=\seq{2, 1, ...}$ and \seqEmpty{} as the empty sequence. Akin to sets, the derivation of a sequence from another sequence preserving the order of elements in the originating sequence by $q_1=\seqWith{i+1}{i \in q}$. Accessing the $i$-th element in sequence $q$ is expressed by $q[i]$. We denote adding an element to an existing sequence / the sequence concatenation as $q_2=q \addSeq q_1$, i.e., $q_2$ contains all elements in $q$ and $q_1$ including duplicates with the elements of $q$ preceding the elements of $q_1$ in the original sequences as given in $q$ and $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ as a sequence concatenation that omits duplicates.
-
-We also want to express that a \emph{mapping} from a certain key to a value is recorded, retrieved and used in some algorithms. We simply denote such a map as a set of entries $\mapEntry{k}{v}$ relating a key $k$ to a value $v$. As key-value pairs are unique within a mapping, in particular there is only one mapping for a certain key, using a set of such entries is reasonable. We denote adding an entry to a map by $m \assng m \addMap \mapEntry{k}{v}$, assuming that an existing entry for $k$ (accessed by $m[k]$) is overridden by the new entry. If there is no mapping for a certain key, $m[k]$ will return undefined denoted by $\undef$. Iterating over a map means iterating over the entries of a map.
-
-In general, we use $\undef$ to denote an \emph{undefined result/value}. 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 individual \emph{algorithms}, we indicate and use the actual name as used in the implementation to ease mapping from code to algorithms and back. Further, we use parameters and return values in the fashion the implementation does and indicate access to class or instance attributes in the`data' section of the algorithm descriptions. For ease of reading, we ignore here that elements or results of functions in the actual implementation may be a null pointer implying respective checks. Thus, we simply assume here that unless stated otherwise functions either return $\undef$ or, in case of set or sets or sequences $\setEmpty$ or $\seqEmpty$, respectively. 
+In general, we use $\undef$ to denote an \emph{undefined result/value}. Unless stated otherwise, we assume, that operations return a meaningful result even if $\undef$ is passed in as parameter.
+
+As usual, we denote a \emph{set} of elements by $s=\set{1, 2, ...}$ with no duplicates allowed. \setEmpty{} is the empty set. We denote the derivation of set $s_1$ from another set $s$ by $s_1=\setWith{i+1}{i\in s}$, i.e., $s_1$ is derived from $s$ by iterating over and determining a new value for all elements $i$ in $s$, here through $i+1$. In this notation, conditions / projections may apply to the source set $s_1$. Further, $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. For convenience, we assume for a set $s_3$ that $s_3\text{ } \cup \undef = s_3$.
+
+For some parts of the reasoning algorithm, in particular to prioritize the evaluation of different constraint types and eval-blocks, we need \emph{sequences}, i.e., structures that hold elements in a given sequence as well as potentially duplicates of the elements. The the order is defined when adding / inserting elements to a sequence. We denote a sequence by $q=\seq{2, 1, ...}$ and \seqEmpty{} as the empty sequence. Akin to sets, we denote the derivation of a sequence $q_1$ from another sequence $q$ preserving the order of elements in $q$ by $q_1=\seqWith{i+1}{i \in q}$. Accessing the $i$-th element in sequence $q$ is expressed by $q[i]$. Further, we denote the sequence concatenation by $q_2=q \addSeq q_1$, i.e., $q_2$ contains all elements (including duplicates) from $q$ and $q_1$, first the elements from $q$ in the sequence of $q$, then the elements from $q_1$ in their sequence of $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ to denote a sequence concatenation of $q$ and $q_d$ omitting all occurring duplicates.
+
+In some cases, we also need to express a \emph{mapping} between key elements and associated value elements. We denote such a mapping as a set of pairs $\mapEntry{k}{v}$ relating a key $k$ to a value $v$. Within a mapping, key-value pairs are unique with respect to the key. We denote adding a key-value pair to a map by $m \addMap \mapEntry{k}{v}$, assuming that an existing entry for $k$ (accessed by $m[k]$) is overridden by the new entry. If there is no mapping for a certain key, $m[k]$ is $\undef$. Iterating over a map means iterating over the entries of a map.
+
+As this document is intended to detail the actual implementation and to ease mapping from code to algorithms and back, we use for the \emph{algorithms} (where feasible from the space / layout point of view) the actual name from the implementation. Further, we use parameters and return values as done in the implementation. If global, static or instance data is used, we indicate this in `data' section of the respective algorithm description. For simplifying the reading, we treat null values that may occur in the implementation either through $\undef$ or just omit null pointers and the respective checks needed in the code, i.e., unless stated otherwise, functions return then $\undef$ or, in case of set or sets or sequences $\setEmpty$ or $\seqEmpty$, respectively. 
 
 \subsection{IVML elements}
-In this section, we recapitulate the IVML elements and types that are relevant to reasoning for IVML. For these elements and types we introduce functions to access their respective properties. We focus here on functions that are used for specifying the reasoning algorithm rather than all functions defined in the IVML object model. 
+In this section, we recapitulate the IVML elements and types that are relevant to reasoning for IVML. For these elements and types we introduce functions to access their respective properties. We focus here on functions that are used for specifying the reasoning algorithm rather than all functions defined in the IVML object model. 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.
 
 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 associated values. For temporary/local variables, we typically use a name close by, e.g., $w$ for an iterator variable (instead of $v$) etc.