Index: /reasoner/approach.tex
===================================================================
--- /reasoner/approach.tex	(revision 184)
+++ /reasoner/approach.tex	(revision 185)
@@ -19,7 +19,7 @@
 Often, reasoning over all variables of a project including all defined constraints, i.e., \emph{full reasoning}, is needed. This may differ for use cases in which considering all constraints is neither required nor efficient in terms of reasoning time. The first use case is \emph{incremental reasoning}, i.e., starting with a given configuration and performing reasoning just for those variables that have been changed between two subsequent reasoner runs, e.g., by the user. The idea is to provide immediate reasoning results, so that reasoning can happen upon every change made by the user even on complex and large models. It is important to note that in incremental reasoning the underlying model structures may change, so that from time to time also a full reasoning run may be required. The second use case is \emph{runtime reasoning}, e.g., reasoning for validity of a configuration at runtime of a system to identify validations and to trigger re-configuration or adaptation~\cite{Eichelberger16, Eichelberger18}. In contrast to incremental reasoning, in this case we assume that the underlying IVML model is not changed, so that initially translated constraints can always be re-used. For supporting these two cases, we will relay on the following two techniques:
 \begin{itemize}
-  \item \emph{Creation of a partial constraint base} due to changed variables, in particular non-frozen variables\footnote{In EASy-Producer, this technique can be enabled through the reasoner configuration.}. In more detail, constraints assigning already processed default values or constraints over variables that cannot change anymore (frozen variables) are not added to the constraint base. The remaining configuration variables are assumed to be properly initialized (initial full reasoning) or shall be determined during the actual run by the reasoner if possible.  
-  \item \emph{Re-using a previously created constraint base:} The initial constraint base created by the constraint translation is stored in memory and re-stored when applying the reasoner again to the same (structurally unchanged) model, i.e., we require that no new types or variables are added between two reasoning runs. This technique\footnote{This technique can be applied by requesting a re-usable reasoner instance from the EASy-Producer reasoner core and by using that instance instead of the default interface provided by the static reasoning fronted.} trades off reasoning time for memory consumption and can even be combined with creating a partial constraint base, saving up to further 75\% reasoning time.
+  \item \emph{Creation of a partial constraint base}\footnote{In EASy-Producer, this technique can be enabled through the reasoner configuration.} due to changed variables, in particular non-frozen variables. In this mode, constraints assigning already processed default values or constraints over variables that cannot change anymore (frozen variables) are not added to the constraint base. The remaining configuration variables are assumed to be properly initialized (initial full reasoning) or are determined during the actual run by the reasoner if possible.  
+  \item \emph{Re-using a previously created constraint base:}\footnote{This technique can be applied by requesting a re-usable reasoner instance from the EASy-Producer reasoner core.} The constraint base created by the constraint translation during an initial run is stored in memory and re-stored when applying the reasoner again to the same (structurally unchanged) model. Here, we require that no structural changes happen to the model between two subsequent reasoning runs, e.g., no new types or variables are added . This technique trades off reasoning time for memory consumption and can even be combined with creating a partial constraint base.
 \end{itemize}
 
-To implement the IVML reasoner, we first designed and realized an \emph{expression evaluation mechanism}, which is able to evaluate individual IVML expressions. The evaluation mechanisms covers constraint expressions (expressions evaluating to a Boolean value) as well as general default value expressions. The reasoner relies on that mechanism, i.e., in the algorithms described in this document, we just refer to the evaluation mechanism without further detailing it. We assume that the mechanism either returns the correctly evaluated value of an expression with respect to a given model / configuration or that it indicates that the evaluation result is undefined, e.g., as configuration variables used in the evaluated expression are undefined.
+To implement the IVML reasoner, we first designed and realized an \emph{expression evaluation mechanism}, which is able to evaluate individual IVML expressions. The evaluation mechanisms covers constraint expressions (expressions evaluating to a Boolean value) as well as general default value expressions. In the algorithms described in this document, we just refer to the evaluation mechanism without further detailing it. We assume that the mechanism either returns the correctly evaluated value of an expression with respect to a given model / configuration or that it indicates that the evaluation result is undefined, e.g., as configuration variables used in the evaluated expression are undefined.
Index: /reasoner/notation.tex
===================================================================
--- /reasoner/notation.tex	(revision 184)
+++ /reasoner/notation.tex	(revision 185)
@@ -7,29 +7,30 @@
 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. \emptySet{} 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 \emptySeq{} 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. We denote removing elements from a map by set differences, either mentioning the pairs, e.g., for one entry $m \setminus \mapEntry{k}{v}$ or just the keys, e.g., $m \setminus \set{k_1, k_2, \ldots}$.
-
-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 $\emptySet$ or $\emptySeq$, respectively. 
+As usual, we denote a \emph{set} of elements by $s=\set{1, 2, ...}$ with no duplicates allowed. \emptySet{} 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$. 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 that $s_1\text{ } \cup \undef = s_1$.
+
+For some parts of the reasoning algorithm, in particular to prioritize the evaluation of different constraint types and \IVML{eval}-blocks, we need \emph{sequences}, i.e., structures that hold elements in a given sequence potentially including duplicates. The the order is defined when adding / inserting elements to a sequence. We denote a sequence by $q=\seq{2, 1, ...}$ and \emptySeq{} 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 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 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$ (accessible by $m[k]$) is overridden by the new entry. If there is no mapping for a certain key, $m[k]$ is $\undef$. We denote removing elements from a map by set differences, either mentioning the pairs, e.g., for one entry $m \setminus \mapEntry{k}{v}$ or just the keys, e.g., $m \setminus \set{k_1, k_2, \ldots}$. Iterating over a map, e.g., in an algorithm, means iterating over the entries of a map in an arbitrary sequence. 
+
+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. 
 
 \subsection{IVML elements}
 In this section, we discuss the IVML elements and types that are relevant for IVML reasoning. 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 that are defined in the IVML object model. 
 
-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 consisting 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}$. Further, for a model element $e$, $parent(e)$ denotes the model element $e$ is nested within, typically, a compound or a project.
+As a convention to ease reading the algorithms presented later, we use $d$ for a variable declaration, $v$ for a configuration variable, $t$ for a type, $val$ for a value, $c$ for a constraint and $cfg$ for a configuration consisting 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 defined for element $e$ by $constraints(e)$. Let $s$ be a set of elements, then $constraints(s) = \setWithFlat{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}\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$. 
-
-$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\\
+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)$ returns $true$, if $d$ is a variable declaration. A variable declaration defines a decision as usual in decision modeling~\cite{CzarneckiGruenbacherRabiser+12, SchmidJohn04}.
+
+$annotations(d)$ denotes the set of (orthogonal) IVML annotation (variable) declarations for $d$. $annotations(d)=\emptySet$ if $d$ does not define any annotations. In particular, $annotations(e)$ is empty for an arbitrary model element $e$ that does not define any annotations. $isAnnotation(e)$ returns whether $e$ is an annotation. Further, $annotation(e, n)$ indicates whether an annotation $a$ with name $n$ is defined for model element $e$, in particular a variable declaration: 
+%
+$$
+  annotation(e, n) = \begin{cases}a & \text{if }a \in annotations(e) \wedge name(a)=n\\
                                                        \undef & \text{else}\end{cases}
 $$
+Moreover, let
 %
 \begin{multline*}
@@ -39,42 +40,53 @@
 \end{cases}
 \end{multline*}
-returns all declared annotations for an arbitrary model element $e$. 
+return all declared annotations for an arbitrary model element $e$ including those defined by all parents $e$ is nested within. 
 
 \subsubsection{Configuration Variables}\label{sectNotationConfigVars}
 
-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 configuration variable with declaration $d$ as part of a certain \emph{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$. A configuration $cfg$ returns all contained variables in terms of $vars(cfg)$.
-
-$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). We will detail some relevant properties of values below in Section \ref{sectNotationValues}.
-
-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)=\emptySet$ 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
+While variable declarations as introduced in Section \ref{sectNotationVarDecls} as well as types as introduced below allow defining (a meta-model of) configuration options, configuration variables make up the configuration of a specific product. A \emph{configuration variable} holds the actual configured value for a variable declaration. A configuration variable $v$  is defined through a variable declaration $d$. For a single variable declaration $d$ in a model, multiple configuration variables can exist in different configurations. 
+
+Let $v$ be a configuration variable for declaration $d$ as part of a certain \emph{configuration} $cfg$, i.e., $decision(cfg, d)=v$, $parent(v)=cfg$, $declaration(v) = d$, and $type(v) = type(declaration(v))$. For a configuration variable $v$, $isVariable(v)$ returns $true$, for any other IVML element/type $false$. A configuration $cfg$ returns all contained variables in terms of $vars(cfg)$.
+
+$value(v)$ denotes the actual value of $v$ and $type(value(v))$ is the type of the value of $v$, which must be 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 (cf. Section \ref{sectNotationCompounds}). We will detail some relevant properties of values below in Section \ref{sectNotationValues}.
+
+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)=\emptySet$ if no nested variables are defined for $v$, i.e., $type(v)$. For a variable $v$, $\forall_{w\in nested(v)}\text{ } parent(w)=v$ must hold. Let
+%
+$$
+nested(v, n) = \begin{cases}
+  w & \text{if } w\in nested(v) \wedge name(w) = n\\ 
+  \undef & \text{else}
+\end{cases}
+$$ be the nested variable in $v$ with name $n$. Moreover, we define
 %
 \begin{multline*}
 allNested(v) = \begin{cases}
-  \emptySet, & \text{if } |nested(v)| = 0 \\  
+  \emptySet, & \text{if } nested(v) = \emptySet \\  
   \begin{aligned}\set{&nested(v)}~\cup\\ &\setWith{allNested(w)}{w\in nested(v)},\end{aligned} & \text{else}\\ \end{cases}
 \end{multline*}
+%
+to obtain all variables nested in a given variable $v$ as well as
 %
 \begin{multline*}
 allParents(v) = \begin{cases}
   \emptySet, & \text{if } \neg isVariable(parent(v)) \\  
-  \begin{aligned}\set{&parent(v)} \cup\\ &allParents(parent(v)),\end{aligned} & \text{else}\\ \end{cases}
+  \begin{aligned}\set{&parent(v)}~\cup\\ &allParents(parent(v)),\end{aligned} & \text{else}\\ \end{cases}
 \end{multline*}
 %
-Akin to variable declarations, $annotations(v)$ returns the set of actual annotation variables for variable $v$. Please note that there is a significant difference between $annotations(d)$ for a variable declaration $d$ and\linebreak[4]$annotations(decision(cfg,d))$, as a declaration only holds the specifically declared attributes for $d$, while a variable is instantiated with all annotations potentially inherited from containing project or variables (in case of compounds or containers). 
-
-Due to the specific semantics of default or frozen variables, IVML variables have an \emph{assignment state} that be accessed via $state(v)$. The state of individual variables is changes (indirectly) when values are assigned, e.g., as as a side effect of constraint evaluation. The following states are defined:
+to obtain all variable parents $v$ is nested into.
+
+Akin to variable declarations, $annotations(v)$ returns the set of actual annotation variables for variable $v$. Please note that there is a significant difference between $annotations(d)$ for a variable declaration $d$ and\linebreak[4]$annotations(decision(cfg,d))$, as a declaration only holds the specifically declared attributes for $d$, while a variable is instantiated with all annotations also inherited from containing project or variables. 
+
+Due to the specific semantics of default or frozen variables, IVML variables have an \emph{assignment state} that can be accessed via $state(v)$. The state of individual variables is changes when values are assigned, e.g., as as a side effect of constraint evaluation. The following states are defined:
 
 \begin{itemize}
-      \item \IVML{UNDEFINED}: No value has been assigned so far or the value was cleared intentionally through assigning the IVML constant value \IVML{null}.
-      \item \IVML{DEFAULT}: A type compatible default value has been assigned by evaluating the default value expression of the underlying variable declaration. Default values can be changed unless frozen, but not more than once within the same project scope. 
-      \item \IVML{ASSIGNED}: A type compatible value has been assigned (by some EASy-Producer component). The value can still be changed, but not more than once within the same project scope.
-      \item \IVML{USER\_ASSIGNED}: A type compatible value has been assigned by the user and shall not be overridden, e.g., by the reasoner.
+      \item \IVML{UNDEFINED}: No value has been assigned so far or the value was cleared intentionally through assigning the IVML constant value \IVMLnull{}.
+      \item \IVML{DEFAULT}: A type compatible default value has been assigned by evaluating the default value expression of the underlying variable declaration. Default values can be changed unless frozen, but not more than once within the same evaluation scope. 
+      \item \IVML{ASSIGNED}: A type compatible value has been assigned by the running program. The value can still be changed, but not more than once within the same evaluation scope~\cite{IVML-LS}.
+      \item \IVML{USER\_ASSIGNED}: A type compatible value has been assigned by the user and shall not be overridden by the program, e.g., by the reasoner.
       \item \IVML{DERIVED}: A type compatible value has been assigned as a side effect of reasoning and constraint evaluation.
-      \item \IVML{FROZEN}: The variable was frozen through the IVML \IVML{freeze} statement to avoid further changes of the actual value (including no value in state \IVML{UNDEFINED}). Further assignments are not allowed and cause an assignment error irrespective of the actual scope.
+      \item \IVML{FROZEN}: The variable was frozen through the IVML \IVML{freeze} statement to avoid further changes of the actual value (including no value in state \IVML{UNDEFINED}). Further assignments are not allowed and cause an assignment error irrespective of the evaluation scope.
 \end{itemize}
 
-Variables can be \emph{local}, e.g., as they are used in the IVML model as parameters of a user-defined constraint function, as variable in a let let-expression or as an iterator of a collection function. Such variables have the same properties as usual configuration variables, but they just hold a temporary value, may be re-assigned within a certain scope, e.g., iterator variables, typically have the state \IVML{ASSIGNED} and cannot be frozen. Local variables can be identified using $isLocal(v)$, which returns $true$ if $v$ is a local variable.
+Variables can be \emph{local}, e.g., as they are used in the IVML model as parameters of a user-defined constraint function, as variable in a \IVML{let}-expression or as an iterator of a collection function. Such variables have the same properties as usual configuration variables, but they hold a temporary value, may be re-assigned within their local scope, e.g., iterator variables, typically have the state \IVML{ASSIGNED} and cannot be frozen. $isLocal(v)$ returns $true$ if $v$ is a local variable.
 
 %For simplifying the descriptions of algorithms, we ignore here the fact that IVML variables can have the IVML value \IVML{null}, i.e., explicitly undefined (and different from a null pointer). While the underlying implementation must contain explicit checks, we just assume here that the functions lead to $\undef$, \emptySet or \seq{\text{}}, respectively.
@@ -82,7 +94,9 @@
 \subsubsection{Project}\label{sectNotationProject}
 
-A \emph{project} is a named scope, which can contain variable declarations, type declarations, assignment-blocks and eval-blocks. $decls(p)$ denotes the set of all variable declarations introduced in project $p$. $isProject(p)$ returns $true$ for a project $p$. 
-
-$evals(p)$ is the set of (potentially nested) \emph{eval-blocks} in project $p$. If $e\in evals(p)$ then $constraints(e)$ returns the constraints listed in $e$, whereby $constraints(e)$ may be empty, in particular if $e$ is an arbitrary model element. Similarly, $evals(e)$ returns the nested eval-blocks. Subsequently, the function $allEvalConstraints(e)$ returns all constraints in eval-block $e$ including all nested eval-blocks.
+A \emph{project} is a named scope, which can contain variable declarations, type declarations, annotation assignment blocks and \IVML{eval}-blocks. $decls(p)$ denotes the set of all variable declarations introduced in project $p$. $isProject(p)$ returns $true$ for a project $p$. 
+
+A project constitutes the evaluation scope for all contained constraints, i.e., during the evaluation of a project, a variable must not be assigned more than once~\cite{IVML-LS}. As stated above, local variables are evaluated within their containing local scope and can be re-assigned.
+
+$evals(p)$ is the set of (potentially nested) \emph{eval-blocks} in project $p$. If $e\in evals(p)$ then $constraints(e)$ returns the constraints listed in $e$, whereby $constraints(e)$ may be empty, in particular if $e$ is an arbitrary model element. Similarly, $evals(e)$ returns the nested eval-blocks. Subsequently, the function $allEvalConstraints(e)$ returns all constraints in eval-block $e$ including all nested eval-blocks:
 %
 \begin{align*}
@@ -91,5 +105,5 @@
 \end{align*}
 %
-In IVML, an \emph{annotation assignment} is a kind of block, which allows assigning annotation values to the variables defined within the block, i.e., the specified annotation values shall be applied to all contained variable declarations. The declared variables shall behave as if they are defined in the innermost containing element that is not an annotation assignment. For convenience, also constraints relating to the contained variable declarations can be stated within an annotation assignment. To indicate orthogonal combinations of annotation assignments in IVML models, annotation assignments can be nested referring to different annotations. For convenience, only the innermost annotation value assignment shall be applied in nested assignment blocks in order to avoid accidental multiple assignments to the same annotation within the same project scope.
+In IVML, an \emph{annotation assignment} is a kind of block, which allows assigning annotation values to the variables declared within the block, i.e., the specified annotation values shall be applied to all contained variable declarations. The declared variables shall behave as if they are defined in the innermost containing element that is not an annotation assignment. For convenience, also constraints relating to the contained variable declarations can be stated within an annotation assignment. To indicate orthogonal combinations of annotation assignments in IVML models, annotation assignment blocks can be nested. For convenience, only the innermost annotation value assignment shall be applied in nested assignment blocks in order to avoid accidental multiple assignments to the same annotation within the same project scope~\cite{IVML-LS}.
 
 $assignments(p)$ is the set of (potentially nested) annotation assignments of project $p$. If $a\in assignments(p)$ then $decls(a)$ returns the variables declared in $a$ and $constraints(a)$ the constraints declared within $a$. Further, $assignments(a)$ returns the annotation assignments nested within $a$. All three results may be empty. Further, $assignmentData(a)$ provides access to the intended value assignment, i.e., if $f \in assignmentData(a)$ then $name(f)$ is the name of the affected attribute and $default(f)$ the intended default value expression that shall be assigned to all attributes with name $name(f)$ for all declarations within the containing attribute assignment. $isAnnotationAssng(a)$ returns whether $e$ is an annotation assignment.
