Index: /reasoner/mainAlgorithms.tex
===================================================================
--- /reasoner/mainAlgorithms.tex	(revision 189)
+++ /reasoner/mainAlgorithms.tex	(revision 190)
@@ -2,7 +2,8 @@
 \begin{figure}[h]
 \center
-%\frame{...}
-\includegraphics[scale=0.48,trim={5.1cm 6.2cm 26.5cm 0.3cm},clip]{figures/structure.pdf}
-\caption{Structuring blocks, algorithms and sections.}
+%\frame{
+\includegraphics[scale=0.52,trim={5.9cm 7.0cm 27.5cm 0.4cm},clip]{figures/structure.pdf}
+%}
+\caption{Overview of reasoning algorithms and sections.}
 \label{figStructure}
 \end{figure}
@@ -20,5 +21,5 @@
 \newcommand\problemRecords[0]{m}
 
-The reasoner performs forward reasoning, i.e., it identifies relevant constraints according to the reasoning mode, translates the constraints, stores constraint relations, evaluates the translated constraints 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. 
+The reasoner performs forward reasoning, i.e., it identifies relevant constraints according to the reasoning mode, translates the constraints, maintains relations among constraints and model elements, evaluates the translated constraints in a loop until all constraints are processed and adjusts 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 may be involved in a recursion due to the potentially recursive structure of complex IVML types, in particular nested compounds or containers. Algorithms \ref{algComposeExpression} and \ref{algAddConstraint} shown in the lower part of Figure \ref{figStructure} may appear disconnected, but they are called by most of the translation algorithms to populate the constraint base and to compose complex constraints from recursive nestings of complex IVML types. 
 
 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}, and 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 constraints in Section \ref{sectTopLevelConstraintsRescheduling}.
@@ -26,9 +27,11 @@
 \subsection{Main Reasoning Loop}\label{sectTopLevelMainReasoningLoop}
 
-The main reasoning loop implements the overall control for the IVML reasoning process. The reasoning loop receives a configuration $cfg$ as input and utilizes various global data structures.
-
-First, Algorithm \ref{algMainLoop} sets up the global configuration variable $cfg$ and  the expression evaluator\footnote{In the implementation, the listener for changed variables triggering constraint re-scheduling (Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) as well as recording of assigned variables are registered with the expression evaluator. These details are omitted here.} in lines \ref{algMainLoopSetupVar}-\ref{algMainLoopSetupEval} for use with the configuration $cfg$ and the scope assignments $\scopeAssignments$. In line \ref{algMainLoopStartTime} it stores the start time to terminate potentially endless loops induced by ping-pong assignments among constraints within a given maximum time. The remainder of the algorithm is separated into two parts, the full execution (lines \ref{algMainLoopFullStart}-\ref{algMainLoopFullEnd}), and the incremental part (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}) utilizing a constraint base prepared and stored while running the first part.
-
-As shown in Algorithm \ref{algMainLoop}, first structures are created to store constraints for reuse (if $reuse$ is enabled), here for copying the constraint base ($base_c$), the relevant constraints per declaration ($base_{\relevantConstraintsPerDeclaration}$, a mapping of declarations to using constraints) and the relevant constraint variables per decision variable ($base_{\relevantConstraintVariables}$, bidirectional mapping between constraint values assigned to configured decision variables). Then,  the reasoner\footnote{In the implementation, translation and reasoning happen in \class{Resolver.java}.} must take the structure of IVML models into account, which is determined by the top-level IVML project making up $cfg$ and a cycle-free traversal of the imports of the top-level project. $discoverProjects(cfg)$ (line \ref{algMainLoopDiscover}, not further detailed in this document), performs a depth-first traversal of the import structure, ignores already seen cyclic imports and returns the processing sequence of all projects involved in $cfg$, i.e., the imported projects sorted in ascending manner according to their number of import dependencies. The loop processes this project sequence as long as no timeout occurred (global flag $hasTimeout$) or the user requests a stop of the reasoning (global flag $stop$).
+The main reasoning loop implements the overall control for the IVML reasoning process. The reasoning loop illustrated in Algorithm \ref{algMainLoop} receives a configuration $c$ as input and sets up/utilizes various global data structures.
+
+First, Algorithm \ref{algMainLoop} sets up the global configuration variable $cfg$ and  the expression evaluator\footnote{In the implementation, the listener for changed variables triggering constraint re-scheduling (Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) as well as recording of assigned variables are registered with the expression evaluator. These realization details are omitted here.} in lines \ref{algMainLoopSetupVar}-\ref{algMainLoopSetupEval} for use with the given configuration $c$ and the scope assignments $\scopeAssignments$ (the data structure is detailed in Section \ref{sectTopLevelConstraintsTranslation}). In line \ref{algMainLoopStartTime}, the algorithm stores the start time of reasoning to terminate the reasoning loop after a given timeout in order to prevent potentially endless ping-pong assignments among constraints. The remainder of the algorithm is separated into two parts, the full reasoning part (lines \ref{algMainLoopFullStart}-\ref{algMainLoopFullEnd}), and the incremental reasoning part (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}), the latter utilizing a constraint base prepared and stored while initially running the full reasoning part.
+
+In the \textbf{full reasoning part}, data structures are set up to store constraints for reuse in the incremental part (if $reuse$ is enabled), here for storing a copy of the constraint base ($base_c$) as well as $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$ storing specific constraint relations. $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$ are important for efficient access to constraints during constraint re-scheduling, i.e., when variable values change as a side effect of value propagation. $\relevantConstraintsPerDeclaration$ is a mapping that links a variable declaration to the constraints using the variable. $\relevantConstraintVariables$ is a bi-directional mapping between constraint values assigned to configured decision variables. $base_{\relevantConstraintsPerDeclaration}$ and $base_{\relevantConstraintVariables}$ are the respective copies if $reuse$ is enabled. 
+
+The resoning process takes each individual project (as top-level evaluation scope) into account and evaluates the constraints defined by the respective project. However, as projects can depend on each other, the reasoning process must follow the import dependencies of the projects starting at those without imports continuing with the dependent projects up to the top-level project in the given configuration $c$. In general, the imports of IVML projects can form a graph with loops, because imports my be cyclic \cite{IVML-LS} as required in complex topological models. Thus, we determine the project sequence through a cycle-free depth-first traversal of the import graph, i.e., we pretend that the import graph is a tree and ignore imports of already seen projects. The traversal determines the project sequence, a partial ascending order of projects according to their (number of) dependencies. In this sequence, projects with no imports are at the beginning of the sequence and projects with imports are are listed after all their depending projects. line \ref{algMainLoopDiscover}, $discoverProjects(cfg)$\footnote{The algorithm is not further detailed in this document} determines the project sequence of all projects involved in $c$. The loop in lines \ref{algMainLoopStart}-\ref{algMainLoopEnd} processes this project sequence as long as no timeout occurred (global flag $hasTimeout$) or the user stops the reasoning process (global flag $stop$).
 
 \begin{algorithm}[H]
@@ -70,5 +73,5 @@
 
 
-For each project $p$, the main loop (lines \ref{algMainLoopStart} - \ref{algMainLoopEnd}) translates the constraints in $p$ and populates the constraint base as a side effect of the constraint translation called in line \ref{algMainLoopTranslate} (detailed in Section \ref{sectTopLevelConstraintsTranslation}). If enabled through $reuse$, the constraint translation stores the respective population of constraints in $base_c$ and their relations in $base_{\relevantConstraintsPerDeclaration}$ and $base_{\relevantConstraintVariables}$. Then the algorithm performs a forward-chaining evaluation of the constraint base in line \ref{algMainLoopEvaluate} (explained in Section \ref{sectTopLevelConstraintsEvaluation}). If a constraint changes a configuration variable as a side effect, the constraints related to that variable are re-scheduled for evaluation (detailed by Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). As last step for a project $p$, the algorithm freezes the actual values according to the (conditional) freeze-block specifications in $p$ in line \ref{algMainLoopFreeze}. 
+For each project $p$, the main loop translates the constraints in $p$ and populates the constraint base as a side effect of the constraint translation called in line \ref{algMainLoopTranslate} (detailed in Section \ref{sectTopLevelConstraintsTranslation}). If enabled through $reuse$, the constraint translation stores the respective population of constraints in $base_c$ and their relations in $base_{\relevantConstraintsPerDeclaration}$ and $base_{\relevantConstraintVariables}$. Then the algorithm performs a forward-chaining evaluation of the constraint base in line \ref{algMainLoopEvaluate} (explained in Section \ref{sectTopLevelConstraintsEvaluation}). If a constraint changes a configuration variable as a side effect, the constraints related to that variable are re-scheduled for evaluation (detailed by Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). As last step for a project $p$, the algorithm freezes the actual values according to the (conditional) freeze-block specifications in $p$ in line \ref{algMainLoopFreeze}. 
 
 In incremental execution (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}), it is sufficient to reset the constraint relations in lines \ref{algMainLoopResetRelStart}-\ref{algMainLoopResetRelEnd}, i.e., the mapping of constraints per declaration $\relevantConstraintsPerDeclaration$ and the mapping between constraint variables and decision variables $\relevantConstraintVariables$, to iterate over all stored projects in $base_c$. For each project, the algorithm takes over the respective constraints from $base_c$  into the actual constraint base, and, as before, evaluates the constraints and freezes the variables.