Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 60)
+++ /reasoner/reasoner.tex	(revision 61)
@@ -1,7 +1,9 @@
 \documentclass[12pt]{article}
+\usepackage[utf8]{inputenc}
 \usepackage{amsmath}
 \usepackage{multirow}
 \usepackage{color}
 \usepackage[ruled, vlined]{algorithm2e}
+\usepackage{graphicx}
 
 \newcommand\TBD[1]{{\color{blue}TBD: #1}}
@@ -173,5 +175,5 @@
 In some cases, expressions used to build up a constraint are created before the actual constraint and stored in structures for lookup. We denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for calculating the sum of $x$ and 25. Thereby, sometimes the creation of temporary (local) variables, e.g., for an IVML let-expression or a container iterator is required. We state this by $\IVMLMeta{var}(i, t)$, i.e., create the temporary variable $i$ of type $t$. For a variable $v$ created by \IVMLMeta{var} holds $isLocal(v) = true$.
 
-\subsubsection{Compounds}
+\subsubsection{Compounds}\label{sectNotationCompounds}
 
 A \emph{compound} is an IVML type, which consists of variable declarations, called slots. Let $t$ be a compound type, then $isCompound(t)$ returns $true$, else for all other types $false$. The slots of a compound $t$ can be accessed through $slots(t)$. Akin to a variable declaration, for slot $s$ $name(s)$, $default(s)$ and $type(s)$ are defined. Moreover, let $v$ be a compound variable, i.e., a variable of a compound type, then $decision(v, s)$ returns the variable related to slot $s$ in the configuration $v$ is a member of. For convenience, we introduce
@@ -219,5 +221,5 @@
 The value of a compound variable defined, e.g., as a default value expression or as an assignment constraint, using complex value expressions, so called \emph{compound initializers}, essentially a name-value mapping. As slots can be of a complex type, e.g., a compound, a compound initializer can also contain complex values, e.g., further compound initializers.
 
-\subsubsection{Containers}
+\subsubsection{Containers}\label{sectNotationContainers}
 
 A \emph{container} is a parameterized structure that holds an arbitrary number of variables / values. IVML ships with two default container types, namely sequence (duplicates allowed, order important) and set (no duplicates allowed, order irrelevant). 
@@ -239,5 +241,5 @@
 Akin to compounds, containers can be initialized by complex values, so called \emph{container initializers}, here as a listing of possible complex values. If the container is a sequence, the given order of values in the container initializer used as (initial) order of the sequence elements.
 
-\subsubsection{Derived types}
+\subsubsection{Derived types}\label{sectNotationDerivedTypes}
 
 In IVML, a \emph{derived type} creates a new type based on an existing type. A derived type can restrict the base type by specifiying constraints, as well as a type alias if no further constraints are given.
@@ -268,5 +270,11 @@
 \newcommand\problemRecords[0]{m}
 
-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.  This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation} and the re-scheduling of constraints while evaluation in Section \ref{sectTopLevelConstraintsRescheduling}. The constraint translation will be discussed in detailed in Section \ref{sectTranslation}.
+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. This section introduces the top-level reasoning algorithms, in particular the main reasoning loop in Section \ref{sectTopLevelMainReasoningLoop}, the top-level constraint translation in Section \ref{sectTopLevelConstraintsTranslation}, the top-level constraint evaluation in Section \ref{sectTopLevelConstraintsEvaluation} and the re-scheduling of constraints while evaluation in Section \ref{sectTopLevelConstraintsRescheduling}. The constraint translation will be discussed in detailed in Section \ref{sectTranslation}.
+
+\begin{figure}[ht]
+\includegraphics[scale=0.6]{figures/structure.eps}
+\caption{Structuring blocks, algorithms and sections.}
+\label{figStructure}
+\end{figure}
 
 \subsection{Main Reasoning Loop}\label{sectTopLevelMainReasoningLoop}
@@ -320,5 +328,5 @@
         $translateAnnotationAssignments(a, \undef, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationAssignments}
      } \label{algTranslateConstraintsTranslationEnd}
-     $add(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)}$\;\label{algTranslateConstraintsTopLevelEvals}
+     $add(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)}\TBD{Priority?}$\;\label{algTranslateConstraintsTopLevelEvals}
      \tcp{end of model visitor}%<ConstraintTranslationVisitor
     $base \assng base \addSeq \defaultConstraints \addSeq \deferredDefaultConstraints \addSeq \topLevelConstraints \addSeq \otherConstraints$\; \label{algTranslateConstraintsCompose}
@@ -414,5 +422,5 @@
 \end{enumerate}
 
-We start with the algorithm for translating declaration types and defaults in Section \ref{sectTranslationDeclarationTypesDefaults}. Then we will discuss more specific algorithms used within the translatation of declaration types and defaults, including derived types in Section \ref{sectDerivedTypes}, annotation assignments in Section \ref{sectAnnotationDefaults} (as already used in (Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}), compound defaults in Section \ref{sectCompoundDefaults}, and, finally, container defaults in Section \ref{sectContainerDefaults}.
+We start with the main algorithm, Algorithm \ref{algTranslateDeclaration}, for translating variable declarations and related default value expressions in Section \ref{sectTranslationDeclarationTypesDefaults}. Algorithm \ref{algTranslateDeclaration} decides about the translations needed in detail and delegates the translation to further algorithms. Thus, we structure the further sections along the structure of Algorithm \ref{algTranslateDeclaration} and detail the translatation of derived types in Section \ref{sectDerivedTypes}, annotation assignments in Section \ref{sectAnnotationDefaults} (as already used in (Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}), compound defaults in Section \ref{sectCompoundDefaults}, container defaults in Section \ref{sectContainerDefaults}, and, constraint variables in Section \ref{sectConstraintVariables}.
 
 \subsection{Translate Variable Declarations}\label{sectTranslationDeclarationTypesDefaults}
@@ -458,25 +466,10 @@
 \end{algorithm}
 
-\begin{algorithm}[H]
-  \SetAlgoLined
-  \KwIn{declaration $d$, variable $v$, access $ca$, type $t$}
-  \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$, incremental flag $inc$}
-  
-      \uIf{$ dflt \neq \undef \wedge \neg inc $}{
-              \ForAll{$u \iterAssng usedTypes(default(d))$}{
-                 \MISSING{derived types?}
-                   $translateDefaultsCompoundsContainer(d, u)$\;
-               }
-           }
-      $add(\otherConstraints, translateContainerCompoundConstraints(d, v, \undef), true)$\;
-      \If{$isContainer(t) \wedge isDerived(contained(t))$}{
-          $translateContainerDerivedDatatypeConstraints(contained(t), d, \undef)$\;
-      }
- \caption{Translating declaration default value expressions to constraints (\IVML{translateContainerDeclaration}).}\label{algTranslateContainerDeclaration}
-\end{algorithm}
 
 \subsection{Derived types}\label{sectDerivedTypes}
 
-In IVML, a derived datatype $d$ is defined based on a known base type $b$. Type $d$ is a type restriction of $b$, if $d$ defines restrincting constraints over $b$ using a local variable $decl(d)$ to express the constraints. \TBD{decl(d) is not introduced above. Needed?}. Type $d$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(d) = \emptySet$. If a variable $v$ is declared of type $d$, all constraints defined for $d$ over $b$ and, transitively over the base types of $b$ apply. Whether these constraints are fullfilled depends on the actual value of $v$. Therefore, we translate all constraints defined on type $d$ (of $v$) to constraints of $v$. This is achieved by Algorithm \ref{algTranslateDerivedDatatypeConstraints}, which collects for a given declaration $d$ all constraints for basis types substituting in each constraint the respective local variable by the actual variable $d$. The resulting constraints are stored in $\topLevelConstraints$.
+As introduced in Section \ref{sectNotationDerivedTypes}, a derived datatype $d$ is defined based on base type $b$. Type $d$ is a type restriction of $b$, if $d$ defines restrincting constraints over $b$ through the local variable $decl(d)$. Type $d$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(d) = \emptySet$. 
+
+If a variable $v$ is declared as of type $d$, all constraints defined for $d$ over $b$ and, transitively over all base types of $b$ must hold for $v$. Whether these constraints are fullfilled depends on the actual value of $v$. For a given variable $v$, instantiate all constraints defined on $type(v)$ as constraints of $v$. This is achieved by Algorithm \ref{algTranslateDerivedDatatypeConstraints}, which collects for a given declaration $d$ all constraints for all basis types substituting in each constraint the respective local variable $decl(d)$ by the actual variable $decl(v)$. The resulting constraints are stored in $\topLevelConstraints$.
 
 \begin{algorithm}[H]
@@ -502,31 +495,5 @@
 \end{algorithm}
 
-\subsection{Constraint variables}\label{sectConstraintVariables}
-
-Constraint variables can be created by taking the respective default/actual variable, performing the variable substitution with $\variableMapping$ and, if available, a respective value for \IVMLself, turning the resulting expression into a constraint and adding it to the set of other constraints $\otherConstraints$. Moreover, the relationship between the underlying variable $v$ and the constraint must be recorded for efficient update of the constraint base upon value change (cf. Algorithm \ref{algVarChange}).
-
-\begin{algorithm}[H]
-  \SetAlgoLined
-  \KwIn{constraint expression $c$, actual value for \IVMLself $s$, variable $v$}
-  \KwData{other constraints $\otherConstraints$, relevant constraints $\relevantConstraints$}
-
-      $c \assng \createConstraint{\varSubstitutionSelfVarMapping{c}{s}}$\;
-      $add(\otherConstraints, \set{c}, true)$\;
-      \MISSING{map v to c for dynamic value type change}\;
-      $\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{c}{v}$
-      
-      
-      %    $add(\otherConstraints, \set{\createConstraint{\varSubstitutionSelfVarMapping{default(s)}{d}}}, true)$\;
-                  %$add(\otherConstraints, \createConstraint{dflt}, true)$\;
-                  %$\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{\createConstraint{dflt}}{v}$
-
-
-      %\If{$isConstraint(type(s)) \wedge default(s) \neq \undef$}{
-      %}
-
-%  $cs \assng \bigcup_{t \in allBase(t} constraints(t)$\;
-%  $add(\topLevelConstraints, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }\varSubstitution{c}{decl(c)=d})}}{c \in cs}, true)$\;
- \caption{Creating constraints for constraint variables (\IVML{createConstraintVariableConstraint}).}\label{algCreateConstraintVariableConstraint}
-\end{algorithm}
+
 
 \subsection{Annotation default expressions}\label{sectAnnotationDefaults}
@@ -545,6 +512,5 @@
 
 
-
-\subsection{Compound default constraints}\label{sectCompoundDefaults}
+\subsection{Compound constraints}\label{sectCompoundDefaults}
 
 Translating a compound into all its constraints requires considering all slots, all constraints defined within a compound, as well as all supported nested structures, such as eval blocks or attribute value assignment blocks. In particular, if the IVML keyword \IVMLself{} is used, it must be replaced by the actual variable of the respective compound type. First, we define some helper functions, then the translation algorithms.
@@ -671,4 +637,22 @@
 Constraints defined on types that are implicitly instantiated within a container must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algTranslateDefaultsCompoundContainer} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested container). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the container using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVMLself{} substituted by the iterator variable $i$.
 
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{declaration $d$, variable $v$, access $ca$, type $t$}
+  \KwData{configuration $cfg$, constraint $base$, variable mapping $\variableMapping$, constraint variables $\otherConstraints$, default (deferred) constraints $\defaultConstraints$ and $\deferredDefaultConstraints$, relevant constraints $\relevantConstraints$, incremental flag $inc$}
+  
+      \uIf{$ dflt \neq \undef \wedge \neg inc $}{
+              \ForAll{$u \iterAssng usedTypes(default(d))$}{
+                 \MISSING{derived types?}
+                   $translateDefaultsCompoundsContainer(d, u)$\;
+               }
+           }
+      $add(\otherConstraints, translateContainerCompoundConstraints(d, v, \undef), true)$\;
+      \If{$isContainer(t) \wedge isDerived(contained(t))$}{
+          $translateContainerDerivedDatatypeConstraints(contained(t), d, \undef)$\;
+      }
+ \caption{Translating declaration default value expressions to constraints (\IVML{translateContainerDeclaration}).}\label{algTranslateContainerDeclaration}
+\end{algorithm}
+
 
 \begin{algorithm}[H]
@@ -700,4 +684,5 @@
  \caption{Translating compound constraints from a container (\IVML{translateContainerCompoundConstraints}).}\label{algTranslateContainerCompoundConstraints}
 \end{algorithm}
+
 
 \begin{algorithm}[H]
@@ -763,4 +748,33 @@
  \caption{Records and analyzes a constraint sequence.}\label{algAddConstraints}
 \end{algorithm}
+
+\subsection{Constraint variables}\label{sectConstraintVariables}
+
+Constraint variables can be created by taking the respective default/actual variable, performing the variable substitution with $\variableMapping$ and, if available, a respective value for \IVMLself, turning the resulting expression into a constraint and adding it to the set of other constraints $\otherConstraints$. Moreover, the relationship between the underlying variable $v$ and the constraint must be recorded for efficient update of the constraint base upon value change (cf. Algorithm \ref{algVarChange}).
+
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{constraint expression $c$, actual value for \IVMLself $s$, variable $v$}
+  \KwData{other constraints $\otherConstraints$, relevant constraints $\relevantConstraints$}
+
+      $c \assng \createConstraint{\varSubstitutionSelfVarMapping{c}{s}}$\;
+      $add(\otherConstraints, \set{c}, true)$\;
+      \MISSING{map v to c for dynamic value type change}\;
+      $\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{c}{v}$
+      
+      
+      %    $add(\otherConstraints, \set{\createConstraint{\varSubstitutionSelfVarMapping{default(s)}{d}}}, true)$\;
+                  %$add(\otherConstraints, \createConstraint{dflt}, true)$\;
+                  %$\relevantConstraints \assng \relevantConstraints \addMap \mapEntry{\createConstraint{dflt}}{v}$
+
+
+      %\If{$isConstraint(type(s)) \wedge default(s) \neq \undef$}{
+      %}
+
+%  $cs \assng \bigcup_{t \in allBase(t} constraints(t)$\;
+%  $add(\topLevelConstraints, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }\varSubstitution{c}{decl(c)=d})}}{c \in cs}, true)$\;
+ \caption{Creating constraints for constraint variables (\IVML{createConstraintVariableConstraint}).}\label{algCreateConstraintVariableConstraint}
+\end{algorithm}
+
 
 \section{IVML-Completeness}\label{sectCompleteness}