Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 112)
+++ /reasoner/reasoner.tex	(revision 113)
@@ -386,5 +386,5 @@
 The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), translates the constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes.  Figure \ref{figStructure} shows the call graph of the reasoner algorithms and the sections where we will discuss them in more detail. Some algorithms call others recursively due to the potentially recursive structure of some IVML types, in particular compounds and containers. Algorithm \ref{algAddConstraint} and \ref{algComposeExpression} appear disconnected, but are called by most of the translation algorithms to populate the constraint base and to compose complex constraints from recursive nesting of containers and compounds. 
 
-This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the global variable mapping structure used during the translation in Section \ref{sectVarMapping}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation}. The algorithms for constraint translation will be discussed in detailed in Section \ref{sectTranslation} and the algorithms for re-scheduling of constraints during evaluation in Section \ref{sectTopLevelConstraintsRescheduling}.
+This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the reasoner data structures in Section \ref{sectDataStructures}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation}. The algorithms for constraint translation will be discussed in detailed in Section \ref{sectTranslation} and the algorithms for re-scheduling of constraints during evaluation in Section \ref{sectTopLevelConstraintsRescheduling}.
 
 \begin{figure}[ht]
@@ -440,5 +440,9 @@
 In incremental execution (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}), it is sufficient to take over the constraints for the respective project into the constraint base, and, as before, to evaluate the constraints and to freeze the variables. Before starting an incremental execution, it is necessary to clear global storages required by the implementation (but not detailed here), such as error data structures, counters, etc.
 
-\subsection{Variable Mapping}\label{sectVarMapping}
+\subsection{Data Structures}\label{sectDataStructures}
+
+This section introduces the most important data structures needed to describe the operations of the IVML reasoner, namely the variable mapping structure (Section \ref{sectVarMapping}) and the scope assignments structure (Section \ref{sectScopeAssignments}).
+
+\subsubsection{Variable Mapping}\label{sectVarMapping}
 
 During the constraint translation, top-level constraints can directly be applied to the involved top-level variables. As mentioned above, constraints defined on compound slots or indirectly through use of compound instances in containers must be treated differently. The particular issue here is that these constraints can be defined on types rather than top-level variables, which is possible but valid only for individual top-level variables, and for evaluating the related constraints, the must be rewritten to utilize through accessors based on top-level variables. To manage the various lots and access expressions, the translation utilizes a stack-based data structure, onto which we push/pop a stack (context) frame for each IVML project and each contained compound type, container type or combinations of both used in variables of a project. A context frame linkes all currently relevant variables to the respective accessor expressions, which are created before the respective translation.
@@ -472,4 +476,16 @@
 For translating containers, context frames can store additional information. We will provide details along with the translation of containers in Section \ref{sectContainerDefaults}.
 
+\subsubsection{Scope Assignments}\label{sectScopeAssignments}
+
+Due to the potentially nested nature of IVML projects, the knowledge about when an assignment to a variable has been made cannot be maintained by a flat mapping, rather than a data structure which stores information about assignments per project (scope). This information is important to detect invalid variable re-assignments, i.e., a variable is not allowed to be assigned more than once per scope \cite{IVML-LS}. 
+
+The scope assignments structure of the IVML reasoner (usually named $\scopeAssignments$) provides the following operations:
+
+\begin{itemize}
+    \item $setAssignmentScope(\scopeAssignments, c)$ defines the scope of constraint $c$ as the actual assignment scope. Adding and checking assignments rely on the actual scope. Here, the scope of $c$ is the top-level parent of $c$, i.e., the containing project.
+    \item $addAssignment(\scopeAssignments, v)$ indicates that variable $v$ was changed through an assignment within the actual scope.
+    \item $wasAssigned(\scopeAssignments, v)$ returns whether variable $v$ was assigned in the actual scope. This operation is used to validate an assignment before it is performed out by the expression evaluator.
+    \item $clearAssignments$ clears all assignments in all scopes.
+\end{itemize}
 
 \subsection{Top-level Constraints Translation}\label{sectTopLevelConstraintsTranslation}
@@ -535,8 +551,9 @@
   \KwData{constraint $base$, scope assignments $\scopeAssignments$, problem records $\problemRecords$, used variables $\usedVariables$, relevant constraints $\relevantConstraints$, expression evaluator $e$, flags $hasTimeout$ and $stop$}
   
-    $\scopeAssignments \assng \setEmpty{}$\; \label{algEvalLoopClearScope}%clearScopeAssignment
+    $clearAssignments(\scopeAssignments)$\; \label{algEvalLoopClearScope}%clearScopeAssignment
     $setDispatchScope(e, p)$\; \label{algEvalLoopDispatchScope}%evaluator.setDispatchScope
     \While {$|base| > 0 \wedge \neg hasTimeout \wedge \neg stop$} { \label{algEvalLoopLoopStart}
         $c \assng pop(base)$\; \label{algEvalLoopPop}
+        $setCurrentScope(\scopeAssignments, c)$\;
         $\usedVariables \assng \setEmpty$\; \label{algEvalLoopClear}
         $setAssignmentState(e, \isDefaultConstraint{c})$\; \label{algEvalLoopAssngState}
@@ -1122,5 +1139,5 @@
   
   \If{$\neg isLocal(v)$}{
-      $\scopeAssignments \assng \scopeAssignments \cup \set{v}$\; \label{algVarChangeScope} %addScopeAssignment
+      $addAssignment(\scopeAssignments, v)$\; \label{algVarChangeScope} %addScopeAssignment
       \MISSING{change constraints if dynamic value type changes}\;
       $base \assng base \addSeqNoDupl \seqWith{\relevantConstraints[p]}{p\in allParents(v)}$\; \label{algVarChangeRescheduleParents}%constraintsForParent