Index: /reasoner/consRescheduling.tex =================================================================== --- /reasoner/consRescheduling.tex (revision 163) +++ /reasoner/consRescheduling.tex (revision 164) @@ -14,7 +14,8 @@ $rescheduleValueChange(v, v, true)$\; \label{algVarChangeRescheduleConstraintVariables} \If{$isValueTypeChange(v, val_n, val_o)$ } { - $rescheduleValueTypeChange(v, val_n, val_o)$\; \label{algVarChangeRescheduleValueTypeChange} + $translateValueTypeChange(v, val_n, val_o)$\; \label{algVarChangeRescheduleValueTypeChange} } } + \tcp{forward chaining} $base \assng base \addSeqNoDupl \seqWith{\relevantConstraintsPerDeclaration[p]}{p\in allParents(v)}$\; \label{algVarChangeRescheduleParents}%constraintsForParent $base \assng base \addSeqNoDupl \seqWith{\relevantConstraintsPerDeclaration[n]}{n\in allNested(v)}$\; \label{algVarChangeRescheduleNested}%constraintsForParent @@ -73,5 +74,5 @@ \KwData{constraint base $base$, other constraints $\otherConstraints$ and relevant constraints per declaration $\relevantConstraintsPerDeclaration$} - $obtainConstraints(v_p, clear, \undef)$ \MISSING{!}\; \label{algRescheduleConstraintValueClear} + $obtainConstraints(v_p, clear, \undef)$\; \label{algRescheduleConstraintValueClear} $e \assng getConstraintValueExpression(value(v))$\; \If{$e \neq \undef$}{ @@ -137,16 +138,63 @@ %\end{algorithm} -\begin{algorithm}[H] - \SetAlgoLined +\MISSING{Text for Algorithm \ref{algTranslateValueTypeChange}, hint to impl \class{Resolver.java}, also obtainConstraints} + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{variable $v$, new value $val_n$, old value $val_o$} + \KwData{incremental flag $inc$, variable mapping $vm$} + $t_n \assng type(val_n)$; $t_o \assng type(val_o)$\; + \uIf{$val_n = \IVMLnull{}$}{ + $obtainConstraints(v, true, null)$\; + }\uElseIf{$val_o = \IVMLnull{}$} { + $inc_o \assng inc$; $inc \assng true$\; + $translateDeclaration(decl(v), v, null)$\; + $inc \assng inc_o$\; + }\uElseIf{$\subTypeEqOf{t_o}{t_n}$} { + $t_r \assng allRefines^+(t_o) \setminus \set{t_n}$\; + $setTypeExcludes(\variableMapping, t_r)$\; + $inc_o \assng inc$; $inc \assng true$\; + $translateDeclaration(decl(v), v, null)$\; + $inc \assng inc_o$\; + }\Else{ + $t_r \assng allRefines^+(t_o) \setminus \set{t_n}$\; + $obtainConstraints(v, true, r_t)$\; + } + + \caption{Translate a value type change (\IVML{translateValueTypeChange}).}\label{algTranslateValueTypeChange} +\end{algorithm} + +During constraint re-scheduling, old constraints must be processed or even removed from the constraint base and the lookup structures ($\relevantConstraintVariables, \relevantConstraintsPerDeclaration$) as well as the problem records. Sometimes, as for the re-scheduling of type changes in Algorithm \ref{algRescheduleValueTypeChange}, even just a subset of constraints according to given types must be removed. Algorithm \ref{algObtainConstraints} performs these tasks. It receives the changed variable $v$, a $clear$ flag indicating whether the constraints for $v$ shall be removed as well as an optional set $f$ of (compound) types that acts as filter, i.e., only constraints attached to one of the types in that set are removed. First, Algorithm \ref{algObtainConstraints} obtains the relevant variables. Then, if enabled by $clear$, the algorithm removes the (filtered) constraints from the constraint base and the lookup data structures. The algorithm returns the constraints related to $v$ that were not cleared. + +Typically, constraints that are related to $v$ for rescheduling can be identified easily via $\relevantConstraintVariables[v]$. However, if $v$ is nested in a container, i.e., represents some nested container element, the constraints may (for technical reasons) actually be related to (one of) the enclosing container variables. Thus, in lines \ref{algObtainConstraintsFindStart}-\ref{algObtainConstraintsFindEnd}, Algorithm \ref{algObtainConstraints} identifies the constraints $cs$ of the next enclosing variable (starting with $v$). If such a set exists and clearing is enabled (lines \ref{algObtainConstraintsClearStart}-\ref{algObtainConstraintsClearEnd}), the algorithm filters $cs$ if requested and removes then all constraints in $cs$ from the constraint base. If filtering is enabled, only those constraints are futher relevant that are attached\footnote{Types are attached to constraints during the translation of compound types in function $translateCmp$ of Algorithm \ref{algTranslateCompoundContent}.} to one of the types in $f$ (line \ref{algObtainConstraintsFilter}). Then the constraints in $cs$ are removed from the constraint $base$ (line \ref{algObtainConstraintsRemoveFromBase}), from the set of problem constraints indicating reasoning errors (line \ref{algObtainConstraintsRemoveFromProblemConstraints}), from the bi-directional constraint variable mapping $\relevantConstraintVariables$ (lines \ref{algObtainConstraintsRemoveFromConstraintVarsStart}-\ref{algObtainConstraintsRemoveFromConstraintVarsEnd}) and from the dependent constraints $\relevantConstraintsPerDeclaration$ (line \ref{algObtainConstraintsRemoveFromConstraintsPerDecl}). Finally, after clearing all constraints, $cs$ can be cleared as no remainng registered constraints are left over (line \ref{algObtainConstraintsClearResult}). + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{variable $v$, flag $clear$, filter type set $f$} + \KwData{relevant constraints $\relevantConstraintVariables, \relevantConstraintsPerDeclaration$, problem records $m$} + \KwOut{persisting constraints of $v$ (if $\neg clear$)} + $i \assng v$; $cs \assng \undef$\; \label{algObtainConstraintsFindStart} + \Repeat{$cs = \undef \wedge~i \neq \undef$}{ + $cs \assng \relevantConstraintVariables[i]$\; + $i \assng parent(i)$\; + }\label{algObtainConstraintsFindEnd} + \If{$clear \wedge~cs \neq \undef$}{ \label{algObtainConstraintsClearStart} + %filter for attached + \lIf{$f \neq \undef$} {$cs \assng \setWith{c}{c \in cs \wedge attached(c) \in f}$}\label{algObtainConstraintsFilter} + %constraintBase.remove + $base \assng base \setminus cs$\; \label{algObtainConstraintsRemoveFromBase} + %failedElements.remove + $m \assng m \setminus cs$\; \label{algObtainConstraintsRemoveFromProblemConstraints} + %simpleAssignmentsFinder + $\relevantConstraintVariables \assng \relevantConstraintVariables \setminus cs$\;\label{algObtainConstraintsRemoveFromConstraintVarsStart} + $\relevantConstraintVariables \assng \relevantConstraintVariables \setminus \setWithFlat{variables(v)}{c \in cs}$\;\label{algObtainConstraintsRemoveFromConstraintVarsEnd} + %variablesMap + $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \setminus \setWith{\mapEntry{w}{c}}{w\in variables(c)}$\; \label{algObtainConstraintsRemoveFromConstraintsPerDecl} + $cs \assng \emptySet$\label{algObtainConstraintsClearResult} + }\label{algObtainConstraintsClearEnd} + \Return $cs$\; + \caption{Obtaining and clearing constraints (\IVML{obtainConstraints}).}\label{algObtainConstraints} - \MISSING{Algorithm}\\ - -\end{algorithm} - - -\begin{algorithm}[H] - \SetAlgoLined - \caption{Reschedule a value type change (\IVML{rescheduleValueTypeChange}).}\label{algRescheduleValueTypeChange} - \MISSING{Algorithm}\\ - -\end{algorithm} +\end{algorithm} + + Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 163) +++ /reasoner/consTranslation.tex (revision 164) @@ -68,5 +68,5 @@ In line \ref{algTranslateDeclarationRefinedType}, the actual type of the variable is determined, either based actual value (if a variable\footnote{\label{fnVariableNull}When initializing a configuration or creating constraints from a constant complex value expression, variables may not already be in place in all cases.} and a value is given), default value expression (as a type approximation of a missing value) or the declaration. If $t$ is a compound type, we set in line \ref{algTranslateDeclarationTranslateSelf1} the value of self $v$ to the actual variable declaration $d$ and create the variable mapping for all slots in line \ref{algTranslateDeclarationRegisterCompound} by calling Algorithm \ref{algTranslateCompoundDeclaration}. Typically, this creates a new context frame in the variable mapping $\variableMapping$, which must be correctly cleaned up at the end of Algorithm \ref{algTranslateDeclaration}. We indicate this by the compound mode $c_m$, which is adjusted here and considered in the translation call in line \ref{algTranslateDeclarationTranslateCompound}. -A remaining default value expression $e_d$ is turned into an assignment constraint if $d$ is not an attribute used within an assignment block (this may otherwise collide with default values defined by the assignment block). If the $v$ variable is a constraint variable, we also have to add $e_d$ to the constraint base. This is done by calling Algorithm \ref{algCreateConstraintVariableConstraint} (cf. Section \ref{sectConstraintVariables}). Then, we turn the default value expression into an assignment expression. However, the creation of the sub-expression $ac$ representing the variable $v$ technically depends on whether $d$ is a (nested) annotation or 'ordinary' variable (lines \ref{algTranslateDeclarationCreateACStart}-\ref{algTranslateDeclarationCreateACEnd}). Further, we must determine the constraint set for adding the assignment constraint (line \ref{algTranslateDeclarationTranslateSelf3}): We add the constraint to $\deferredDefaultConstraints$ if the assignment may override a previous value assignment through a complex value. This is (potentially) the case if \IVML{self} is used in $e_d$ or if $d$ is an overridden slot that may be overriden accidentally by a complex compound value. Else, we add the constraint to the set of default constraints $\defaultConstraints$. Ultimately, we create an expression assigning $e_d$ to $ac$, substitute \IVML{self} and the actual variable mapping in this assignment expression, turn the result into a default constraint and add it to the respective constraint set in line \ref{algTranslateDeclarationTranslateDefault}. +A remaining default value expression $e_d$ is turned into an assignment constraint if $d$ is not an attribute used within an assignment block (this may otherwise collide with default values defined by the assignment block). If the $v$ variable is a constraint variable, we also have to add $e_d$ to the constraint base. This is done by calling Algorithm \ref{algCreateConstraintVariableConstraint} (cf. Section \ref{sectConstraintVariables}). Then, we turn the default value expression into an assignment expression. However, the creation of the sub-expression $ac$ representing the variable $v$ technically depends on whether $d$ is a (nested) annotation or 'ordinary' variable (lines \ref{algTranslateDeclarationCreateACStart}-\ref{algTranslateDeclarationCreateACEnd}). Further, we must determine the constraint set for adding the assignment constraint (line \ref{algTranslateDeclarationTranslateSelf3}): We add the constraint to $\deferredDefaultConstraints$ if the assignment may override a previous value assignment through a complex value. This is (potentially) the case if \IVMLself{} is used in $e_d$ or if $d$ is an overridden slot that may be overriden accidentally by a complex compound value. Else, we add the constraint to the set of default constraints $\defaultConstraints$. Ultimately, we create an expression assigning $e_d$ to $ac$, substitute \IVMLself{} and the actual variable mapping in this assignment expression, turn the result into a default constraint and add it to the respective constraint set in line \ref{algTranslateDeclarationTranslateDefault}. Akin to default value expressions, orthogonal annotation declarations are only translated in full (non-incremental) reasoning mode in line \ref{algTranslateDeclarationAnnotationDefault} using Algorithm \ref{algTranslateAnnotationDeclarations}. @@ -114,8 +114,8 @@ \grayPara{ \begin{gather*} - \patternDerivation{\IVML{compound } C \IVML{\{} T s = deflt\IVML{;\}; } C\ v \IVML{;}}{\varSubstitution{s = deflt}{\IVML{self}=access(v), s=access(v.s),\variableMapping}}\\ - \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; } c(s)\IVML{\}; } C\ v \IVML{;}}{\varSubstitution{c(s)}{\IVML{self}=access(v), s=access(v.s),\variableMapping}}\\ - \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; eval \{} c(s)\IVML{\}\}; } C\ v \IVML{;}}{\varSubstitution{c(s)}{\IVML{self}=access(v), s=access(v.s),\variableMapping}}\\ - \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; assign (\ldots) to \{} c(s)\IVML{\}\}; } C\ v \IVML{;}}{\\\varSubstitution{c(s)}{\IVML{self}=access(v), s=access(v.s),\variableMapping}}\\ + \patternDerivation{\IVML{compound } C \IVML{\{} T s = deflt\IVML{;\}; } C\ v \IVML{;}}{\varSubstitution{s = deflt}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}\\ + \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; } c(s)\IVML{\}; } C\ v \IVML{;}}{\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}\\ + \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; eval \{} c(s)\IVML{\}\}; } C\ v \IVML{;}}{\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}\\ + \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; assign (\ldots) to \{} c(s)\IVML{\}\}; } C\ v \IVML{;}}{\\\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}\\ \patternDerivation{\IVML{compound } C \IVML{\{} T s \IVML{\}; } C\ v \IVML{; } c(v.s)\IVML{;}}{\varSubstitution{c(v.s)}{\variableMapping}}\\ \end{gather*} @@ -128,5 +128,5 @@ \item \emph{Instantiation of a compound slot with default value expression to an assignment constraint:} As mentioned in Section \ref{sectTranslationDeclarationTypesDefaults}, slot initialization as well as slot annotations are handled by recursive execution of Algorithm \ref{algTranslateDeclaration} with an incrementally created access expression, here starting with $v$. Thus, the translation of compound types must create a respective variable mapping (in an own context frame) and apply the already discussed translation. - \item \emph{IVML compound type $C$ with declared slot $s$ and contained constraint $c(s)$ over slot $s$:} The translation is applied if a variable $v$ of type $C$, i.e., a concrete instance of a compound type is declared. A contained constraint is instantiated by qualifying all compound-scoped variable occurrences, i.e., by replacing \IVML{self} with the actual variable $v$, the slot $s$ with the respective qualified access $v.s$ as well as all other known variable mappings including remaining slots. Thus, the variable mapping for a compound must be created before any slot is translated. Nested compounds are implicitly considered through the $access$ function, i.e., by respective access prefix expressions. Moreover, compound instances and, thus, constraints induced by compound types, may occur in containers. In Section \ref{sectContainerDefaults}, we will discuss the translations of containers, which recursively utilizes the translation of variables, i.e., Algorithm \ref{algTranslateDeclaration} and, thus, of compound types. + \item \emph{IVML compound type $C$ with declared slot $s$ and contained constraint $c(s)$ over slot $s$:} The translation is applied if a variable $v$ of type $C$, i.e., a concrete instance of a compound type is declared. A contained constraint is instantiated by qualifying all compound-scoped variable occurrences, i.e., by replacing \IVMLself{} with the actual variable $v$, the slot $s$ with the respective qualified access $v.s$ as well as all other known variable mappings including remaining slots. Thus, the variable mapping for a compound must be created before any slot is translated. Nested compounds are implicitly considered through the $access$ function, i.e., by respective access prefix expressions. Moreover, compound instances and, thus, constraints induced by compound types, may occur in containers. In Section \ref{sectContainerDefaults}, we will discuss the translations of containers, which recursively utilizes the translation of variables, i.e., Algorithm \ref{algTranslateDeclaration} and, thus, of compound types. \item \emph{Eval blocks:} Here nesting becomes transparent and constraints are translated as if they were defined directly in the containing compound type, i.e., according to the second pattern. However, eval blocks require a higher constraint evaluation priority in the compound scope as we will detail below. @@ -234,10 +234,10 @@ \end{algorithm} -If reasoning is not performed in incremental mode, we translate then the default values specified by nested annotation assignments in $t$ in line \ref{algTranslateCompoundDeclarationCompoundAssignments}. As preparation for the subsequent variable substitutions, we determine in line \ref{algTranslateCompoundDeclarationSelf} the actual expression $e_f$ for \IVML{self}, i.e., we either use the access expression $ca$ if given or the declaration $d$. All constraint translations will be performed on $t_r$, the set of refined but not excluded types determined in line \ref{algTranslateCompoundRefinedNotExcluded}. Let +If reasoning is not performed in incremental mode, we translate then the default values specified by nested annotation assignments in $t$ in line \ref{algTranslateCompoundDeclarationCompoundAssignments}. As preparation for the subsequent variable substitutions, we determine in line \ref{algTranslateCompoundDeclarationSelf} the actual expression $e_f$ for \IVMLself{}, i.e., we either use the access expression $ca$ if given or the declaration $d$. All constraint translations will be performed on $t_r$, the set of refined but not excluded types determined in line \ref{algTranslateCompoundRefinedNotExcluded}. Let % \begin{align*}tr&anslateCmp(c_t, v, e_f, \variableMapping, c_s)=add(c_t, \\ &\setWith{register(v, attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{e_f}}), currentType(\variableMapping))}{c\in c_s}, true, v)\end{align*} % -be a function, which translates a given set of compound constraints $c_s$ and performs additional operations to enable fast re-scheduling, i.e., attaching the resulting constraint to the type in the current stack frame (stored in Algorithm \ref{algTranslateCompoundDeclaration}, line \ref{algTranslateCompoundDeclarationTransfer}) and registering the resulting constraints with $v$ (the $register$ operation returns the passed in constraint, cf. Algorithm \ref{algRegisterConstraint}). In $translateCmp$, the constraint translation substitutes the mappings in $\variableMapping$ as well as \IVML{self} with $e_f$. Then, due to their specific priority, we translate first all eval constraints defined for $t_r$ in line \ref{algTranslateCompoundDeclarationEval} and add them to $\otherConstraints$ before translating the remaining compound constraints. Finally, we translate all remaining compound constraints, i.e., type constraints and constraints in annotation assignments in line \ref{algTranslateCompoundDeclarationAll}. +be a function, which translates a given set of compound constraints $c_s$ and performs additional operations to enable fast re-scheduling, i.e., attaching the resulting constraint to the type in the current stack frame (stored in Algorithm \ref{algTranslateCompoundDeclaration}, line \ref{algTranslateCompoundDeclarationTransfer}) and registering the resulting constraints with $v$ (the $register$ operation returns the passed in constraint, cf. Algorithm \ref{algRegisterConstraint}). In $translateCmp$, the constraint translation substitutes the mappings in $\variableMapping$ as well as \IVMLself{} with $e_f$. Then, due to their specific priority, we translate first all eval constraints defined for $t_r$ in line \ref{algTranslateCompoundDeclarationEval} and add them to $\otherConstraints$ before translating the remaining compound constraints. Finally, we translate all remaining compound constraints, i.e., type constraints and constraints in annotation assignments in line \ref{algTranslateCompoundDeclarationAll}. As stated above, we defer most constraint translation work to a recursive execution of Algorithm \ref{algTranslateDeclaration}. However, correctly initializing compounds can be tricky, as default slot values, slot value assignment constraints, default (partial) compound initializer expressions as well as (partial) compound initializer assignment constraints can be mixed. While re-assignments of the same slot in the same scope is forbidden, partial compound initializers and slot assignments can be mixed as long as no re-assignments occur. This happens behind the scenes in the constraint evaluator: Assigning a value to a compound variable (or a slot) causes the creation of a compound value instance with the desired values for the specified slots. Subsequent assignment constraints are executed if no other value has been assigned and, finally, removed by the main constraint evaluation loop in Algorithm \ref{algEvalLoop}. Dependent default values are deferred until all used variables and slots are defined. @@ -251,5 +251,5 @@ \grayPara{ \begin{gather*} - \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;}}{\\\bigcup_{t~\in~usedTypes(v),~ c~\in~constraints(t)}f(v, t)\rightarrow \IVML{forall(w:}\varSubstitution{c(x)}{x=\IVML{w}, \IVML{self}=\IVML{w}, \variableMapping}\IVML{)}}\\ + \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;}}{\\\bigcup_{t~\in~usedTypes(v),~ c~\in~constraints(t)}f(v, t)\rightarrow \IVML{forall(w:}\varSubstitution{c(x)}{x=\IVML{w}, \IVMLself{}=\IVML{w}, \variableMapping}\IVML{)}}\\ \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;}~c(v)\IVML{;}}{\varSubstitution{c(v)}{\variableMapping}} \end{gather*} @@ -258,5 +258,5 @@ There are two basic translation patterns for containers, the first one for constraints induced by the types used in the container and the second one for top-level constraints over collection variables. We will focus here on the first pattern, as the second pattern comes for free as part of the translation of the top-level constraints in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals}. -For the first pattern, we consider all declared and used element types in the actual container value of the container variable $v$ and create for each constraint implied by these types an all-quantified constraint over $v$. In more details, let $t$ be a declared or used element type in $v$, then we can quantify all container elements (or at least a subset of type $t$) through a quantor iterator variable $x$ of type $t$ and apply all constraints for $t$ by instantiating the constraints for $x$, i.e., qualifying all used slots with respect to $x$ and replacing \IVML{self}. Although indivdual constraints may appear superfluous, they are needed to provide detailed error messages and also to keep the re-evaluation effort low. However, if the container is nested, i.e., $T$ is again a container over a certain type, in IVML we must flatten the container, i.e., remove all nested containers, to apply the constraints to all individual elements. As mentioned above, if $\subTypeOf{t}{T}$, accessing specific properties such as compound slots requires some form of type casting / selection on the elements of the container. These additional container transformations depend on the actual container type and are represented in the schema by the function $f(v, t)$. +For the first pattern, we consider all declared and used element types in the actual container value of the container variable $v$ and create for each constraint implied by these types an all-quantified constraint over $v$. In more details, let $t$ be a declared or used element type in $v$, then we can quantify all container elements (or at least a subset of type $t$) through a quantor iterator variable $x$ of type $t$ and apply all constraints for $t$ by instantiating the constraints for $x$, i.e., qualifying all used slots with respect to $x$ and replacing \IVMLself{}. Although indivdual constraints may appear superfluous, they are needed to provide detailed error messages and also to keep the re-evaluation effort low. However, if the container is nested, i.e., $T$ is again a container over a certain type, in IVML we must flatten the container, i.e., remove all nested containers, to apply the constraints to all individual elements. As mentioned above, if $\subTypeOf{t}{T}$, accessing specific properties such as compound slots requires some form of type casting / selection on the elements of the container. These additional container transformations depend on the actual container type and are represented in the schema by the function $f(v, t)$. Basically, $f(v, t)$ turns a sequence into a set to avoid duplicated constraints, flattens a nested container and applies type selects if needed to enable access to slots defined in refined compounds. Therefore, $f(v, t)$ uses the IMVL container operations \IVML{flatten} and \IVML{selectByKind}. Let $ca$ be a container access expression, e.g., $ca=\createExpression{decl(v)}$. If $ca$ is of a nested container type, we apply the \IVML{flatten} operation to extract all element values from all nested containers into one top-level container, i.e., enable access even to deeply nested container elements. We apply the \IVML{selectByKind} operation if $t$ is a subtype of the element type of the container, as otherwise slots defined on the specific type $t$ are not accessible. Finally, as shown in the transformation pattern, we apply an all-quantor over the elements of the (projected) collection using the temporary iterator variable $x$ to the respective constraint $c$ after appropriate variable substitution, in particular to \IVMLself{} by $x$. @@ -478,12 +478,12 @@ In IVML, the type \IVML{Constraint} allows defining variables that contain a constraint. The value of such a variable shall be considered during reasoning as an usual constraint. As for other variables, the value of such a constraint variable can be changed unless it is frozen, i.e., the configuration process can influence the actual set of constraints to be checked on an IVML model. If the value of a constraint variable changes during reasoning, the reasoner must adjust the constraint base accordingly, i.e., the old constraint must be disabled and the new one enabled (cf. Section \ref{sectTopLevelConstraintsRescheduling}). -The basic idea is to turn the (default) value of a constraint variable, a constraint expression, into a constraint and to add it to the constraint base. For constraint containers, we perform a translation of the individual element values each representing constraint expressions. If either pattern is nested within a compound, the variable substitution must particularly replace \IVML{self} by the actual compound variable. Please note that in addition to the translation patterns for constraint variables also the other patterns discussed in this document apply, i.e., if a default value is given, also a respective assignment constraint as shown in Section \ref{sectTranslationDeclarationTypesDefaults}, \ref{sectCompoundDefaults} or \ref{sectContainerDefaults} is created so that the constraint variable also receives the constraint as value. +The basic idea is to turn the (default) value of a constraint variable, a constraint expression, into a constraint and to add it to the constraint base. For constraint containers, we perform a translation of the individual element values each representing constraint expressions. If either pattern is nested within a compound, the variable substitution must particularly replace \IVMLself{} by the actual compound variable. Please note that in addition to the translation patterns for constraint variables also the other patterns discussed in this document apply, i.e., if a default value is given, also a respective assignment constraint as shown in Section \ref{sectTranslationDeclarationTypesDefaults}, \ref{sectCompoundDefaults} or \ref{sectContainerDefaults} is created so that the constraint variable also receives the constraint as value. \grayPara{ \begin{gather*} \patternDerivation{\IVML{Constraint}~v = ex\IVML{;}}{\varSubstitution{ex}{\variableMapping}}\\ - \patternDerivation{\IVML{Compound}~C =~\IVML{\{Constraint } s = ex\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}}{\varSubstitution{ex}{\IVML{self}=v, \variableMapping}}\\ + \patternDerivation{\IVML{Compound}~C =~\IVML{\{Constraint } s = ex\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}}{\varSubstitution{ex}{\IVMLself{}=v, \variableMapping}}\\ \patternDerivation{\IVML{containerOf(Constraint)}~v = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;}}{\varSubstitution{ex_1}{\variableMapping}, \ldots, \varSubstitution{ex_n}{\variableMapping}}\\ - \patternDerivation{\IVML{Compound}~C =~\IVML{\{containerOf(Constraint) } s = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}\\}{\varSubstitution{ex_1}{\IVML{self}=v, \variableMapping}, \ldots, \varSubstitution{ex_n}{\IVML{self}=v, \variableMapping}}\\ + \patternDerivation{\IVML{Compound}~C =~\IVML{\{containerOf(Constraint) } s = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}\\}{\varSubstitution{ex_1}{\IVMLself{}=v, \variableMapping}, \ldots, \varSubstitution{ex_n}{\IVMLself{}=v, \variableMapping}}\\ \end{gather*} } @@ -528,5 +528,5 @@ } -When assigning a value to a variable, the right side may be a complex initializer expression determining the actual value of a collection or a compound. The algorithms and transformations discussed so far focus on nested variables and types rather than such initializer expressions. Instead of defining a specific translation algorithm that must be called from different algorithms, we opted for integrating the translation with the central functionality of adding constraints to the constraint base. The first translation pattern targets containers and the second one compounds. In both patterns, constraint values may occur as (deeply nested) contained values. The translation applied in Algorithm \ref{algAddConstraint} extracts these constraints, performs a respective variable substitution (\IVML{self} is currently not supported here) and adds the result to the constraint base. +When assigning a value to a variable, the right side may be a complex initializer expression determining the actual value of a collection or a compound. The algorithms and transformations discussed so far focus on nested variables and types rather than such initializer expressions. Instead of defining a specific translation algorithm that must be called from different algorithms, we opted for integrating the translation with the central functionality of adding constraints to the constraint base. The first translation pattern targets containers and the second one compounds. In both patterns, constraint values may occur as (deeply nested) contained values. The translation applied in Algorithm \ref{algAddConstraint} extracts these constraints, performs a respective variable substitution (\IVMLself{} is currently not supported here) and adds the result to the constraint base. Algorithm \ref{algAddConstraint} receives a target constraint sequence $s$, a constraint $c$ that shall be added to $s$, a flag which enables checking for constraint values and an optional variable $v$ the constraint shall be related to. For convenience, in some algorithms we also passed a set of constraints for adding instead of a single constraint. We just assume that then all given constraints are forwarded iteratively to Algorithm \ref{algAddConstraint}. Index: /reasoner/mainAlgorithms.tex =================================================================== --- /reasoner/mainAlgorithms.tex (revision 164) +++ /reasoner/mainAlgorithms.tex (revision 164) @@ -0,0 +1,229 @@ +% trim={ } +\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.} +\label{figStructure} +\end{figure} + +\section{Reasoning algorithm}\label{sectReasoning} + +\newcommand\defaultConstraints[0]{c_d} +\newcommand\deferredDefaultConstraints[0]{c_{dd}} +\newcommand\otherConstraints[0]{c_{o}} +\newcommand\topLevelConstraints[0]{c_{t}} +\newcommand\relevantConstraintsPerDeclaration[0]{r_d} +\newcommand\relevantConstraintVariables[0]{r_c} +\newcommand\scopeAssignments[0]{a} +%\newcommand\usedVariables[0]{u} +\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. + +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}. + +\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$). + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{configuration $c$} + \KwData{configuration $cfg$, evaluator $e$, scope assignments $\scopeAssignments$, problem records $m$, start time $startTime$, $reuse$ flag, constraint relations $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$, constraint base copy $base_c, base_{\relevantConstraintsPerDeclaration}, base_{\relevantConstraintVariables}$, $projects$ sequence, $hasTimeout$ and $stop$ flags}%, problem records $\problemRecords$ + \KwResult{Reasoning result $r$} + + $cfg\assng c$\; \label{algMainLoopSetupVar} + %evaluator.init()\; + %evaluator.setResolutionListener(Algorithm \ref{algVarChange})\; + %evaluator.setScopeAssignments(sAssng)\; + $setup(e, cfg, \scopeAssignments)$\; \label{algMainLoopSetupEval} + $startTime = now()$\;\label{algMainLoopStartTime} + \uIf{$base_c = \undef$}{ \label{algMainLoopFullStart} + \If{$reuse$}{ + $base_c = \emptySeq{}$\; %sequence? + $base_{\relevantConstraintsPerDeclaration} = \emptyMap{}$\; + $base_{\relevantConstraintVariables} = \emptySet{}$\; %map? + } + $projects \assng discoverImports(cfg)$\; \label{algMainLoopDiscover} + \ForAll{$p \iterAssng projects \wedge \neg hasTimeout \wedge \neg stop$}{ \label{algMainLoopStart} + $translateConstraints(p)$\; \label{algMainLoopTranslate} + $evaluateConstraints(p)$\; \label{algMainLoopEvaluate} + $freeze(cfg, p)$\; \label{algMainLoopFreeze} + } \label{algMainLoopEnd}\label{algMainLoopFullEnd} + }\Else {\label{algMainLoopIncStart} + $\relevantConstraintsPerDeclaration \assng base_{\relevantConstraintsPerDeclaration}$\;\label{algMainLoopResetRelStart} + $\relevantConstraintVariables \assng base_{\relevantConstraintVariables}$\;\label{algMainLoopResetRelEnd} + \ForAll{$i \in \set{0, \ldots, |base_c|} \wedge \neg hasTimeout \wedge \neg stop$}{ + $base \assng base_c[i]$\; + $evaluateConstraints(projects[i])$\; + $freeze(cfg, projects[i])$\; + } + }\label{algMainLoopIncEnd} + $r \assng createReasoningResult(m, hasTimeout, stop)$\; \label{algMainLoopResult} + \caption{Main reasoning loop (\IVML{resolve}).}\label{algMainLoop} +\end{algorithm} + + +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}. + +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. + +Finally, after all projects have been considered or the main reasoning loop has been terminated prematurely, the algorithm composes\footnote{In the implementation, this is done in \class{Engine.java}, the actual reasoner instance, which creates and utilizes instances of \class{Resolver.java}.} in line \ref{algMainLoopResult} a detailed reasoning result based on recorded evaluation problems. This reasoning result also indicates a successful or failed execution, in particular whether a timeout occurred or a user-requested cancellation was requested. + +\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 evaluated over involved top-level variables. As already mentioned in Section \ref{sectNotationConstraints}, constraints defined on compound slots or indirectly through use of compound instances in containers must be translated before evaluation. The particular issue here is that these constraints can be defined in an IVML model over types (for which no values can be assigned in a configuration) rather than over top-level variables. A solution is to rewrite these constraints by substituting type-local variables by appropriate accessors starting at 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 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 links all currently relevant variables to the correct accessor expressions, which are created before the respective variable substitutions are applied. + +However, a simple stack is not sufficient for two reasons, namely nested complex types, excluded types and assignment blocks. As we will detail below, nested complex types require constraint rewriting through a prefix composed of nested all-quantifiers. Therefore, the stack frames can store the information needed to create the respective quantifier expression. When adding a constraint to the constraint base, we visit the stack frames and, if such information is available, incrementally qualify the expression by the described quantifier. The constraint rescheduling re-uses the constraint transformation. However, performing a complete transformation of all types related to certain value change is typically not needed, so that excluding types from the translation speeds up the re-scheduling operations. +%Moreover, IVML projects and compounds can contain nested assignment blocks. An assignment block implicitly defines assignment constraints for its contained variable declarations including containers or compounds. If we translate first variable declarations and then the related constraints, these constraints are outside their actual scope and, thus, relevant access expressions are not available, i.e., wrong constraints would be added to the constraint bae. Intermingling compund/container translation with annotation-block translation would be a potential solution, which increases the algorithm / code complexity. Thus, we opted to register a declaration with its context frame (which is then implicitly registered with its parent frame for proper cleanup) and to activate/deactivate such a frame, although it is not on top of the stack, when translating the implicit assignment constraints in an assignment block. Such stack frames are also removed from the stack when popping the respective parent context frame. + +In summary, the variable mapping stack structure $\variableMapping$ of the IVML reasoner provides the following operations: + +\begin{itemize} +% \item $setRegisterContexts(\variableMapping, b)$ enables automatic registration of context frames within the parent frame. The operation returns the previous state of the registration flag. +% \item $isContextsRegistering(\variableMapping)$ returns whether new context frames are automatically registered with the parent frame. + \item $pushContext(\variableMapping, d, r)$ creates and pushes a new context frame for declaration $d$ to the stack. If registration of contexts is enabled, $r$ indicates whether the new frame shall be registered with the parent frame and whether already processed types (for handling nested complex types) shall be recorded by this context. + \item $pushContext(\variableMapping, d, c,v, r)$ works like $pushContext(\variableMapping, d, r)$, but registers also information for creating an all-quantified constraint prefix for all constraints added to the constraint base as long this frame is on the stack. The information includes the container expression $c$ and the typed iterator variable $v$ over the element type of $c$. We will apply this function in Section \ref{sectContainerDefaults}. + \item $popContext(\variableMapping)$ removes the top-most context frame. The initial frame, which is created by default and devoted to the enclosing IVML project, is not removed by this operation. + \item $registerMapping(\variableMapping, d, ca)$ registers the access expression $ca$ with the given variable declaration $d$ in the top-most context frame. Essentially, a context frame contains a mapping $m$ and the operation performs $m \assng m \addMap \mapEntry{d}{ca}$. + \item $getMapping(\variableMapping, d)$ returns the mapping for $d$ (for short $\variableMapping[d]$). If no mapping was registered for the actual context frame, all context frames in stack order are considered. If no mapping is registered, the result is $\undef$. + \item $recordProcessed(\variableMapping, t)$ records a processed type with the closest containing context having processed type registration enabled. If \linebreak[4] $isCompound(t)$, this function registers $allRefined^+(t)$. + \item $alreadyProcessed(\variableMapping, t)$ returns whether $t$ was already registered as a processed type in one of the enclosing context frames. +% \item $activate(\variableMapping, d)$ re-activates, i.e., pushes the registered stack frame for $d$ taken from the current context frame. As long as the current context frame exists, this operation can be called again and again. If no context frame is registered for $d$, the stack is not modified. +% \item $deactivate(\variableMapping, d)$ de-activates the registered context frame for $d$, i.e., pops it from the stack but leaves it registered with its parent context frame so that it is available for further activations as long as the parent context frame exists on the stack. + \item $setTypeExcludes(\variableMapping, s)$ defines a set of types to be marked as excluded from constraint transformations. Excluding types is important for a fast processing of re-scheduled constraints in Section \ref{sectTopLevelConstraintsRescheduling}. + \item $transferTypeExcludes(\variableMapping, t)$ transfers excluded types into this context and stores the causing type $t$ in the current context. Transferring excluded types binds them to the actual (usual top-most) type and avoids applying them some nested type. + \item $currentType(\variableMapping)$ returns the type $t$ stored in the current context by $transferTypeExcludes(\variableMapping, t)$. The result is $\undef$ if no transfer happened for the current context. + \item $isTypeExcluded(\variableMapping, t)$ returns whether $t$ is excluded in the current context. $excludedTypes(\variableMapping)$ returns all excluded types for the current context or an empty set. + \item $size(\variableMapping)$ the number of contexts on the stack. There is always at least one context on the stack representing the enclosing project. + \item $clear(\variableMapping)$ clears the stack and cleans up the default context frame dedicated to the IVML project so that $\variableMapping$ is ready for the translation of the next IVML project. +\end{itemize} + +From a black-box perspective, $\variableMapping$ can be considered as a usual map as discussed in Section \ref{sectGeneralNotation}, but performing some stack-based lookup operations. Thus, we just use $\variableMapping$ in the variable substitution notation as introduced in Section \ref{sectNotationConstraints}, e.g., let $e$ be an expression, then $\varSubstitutionVarMapping{e}$ replaces all variables in $e$ having a mapping (through the $getMapping$ operation) in at least on context frame of $\variableMapping$. + +%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 for a variable has been made cannot be maintained by a simple flat mapping. This requires a data structure, which stores information about assignments per project (scope). This structure is important to detect invalid variable re-assignments, i.e., to figure out whether a variable assigned more than once per scope~\cite{IVML-LS}. + +The scope assignments structure of the IVML reasoner (usually named $\scopeAssignments$ for assignments) 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} + +The core idea of the constraint translation is to collect the constraints following the structure of an IVML model and to replace each type-related variable by the correct accessor expression for a global variable in the current scope. According to the IVML specification~\cite{IVML-LS}, the relevant top-level elements are variable declarations, global constraints, annotation assignment blocks and eval-blocks. Type definitions are considered when when processing variable declarations, as the individual type of a variable indicates the specific constraints to be collected and instantiated. + +As Algorithm \ref{algTranslateConstraints} focuses on top-level constraints and delegates more complex transformations to sub-sequent algorithms, in particular Algorithm \ref{algTranslateDeclaration} for variable declarations, and top-level constraints exclusively use qualified variable access expressions, the translation patterns are rather straightforward. Top-level constraints, constraints in (nested) annotation assignments and constraints in (nested) eval blocks are taken over as specified into the constraint base. However, constraints in eval-blocks must be prioritized over the remaining constraints~\cite{IVML-LS}. + +\grayPara{ +\begin{gather*} + \patternDerivation{T \text{ } v\IVML{;} c(v)\IVML{;}}{c(v)} \\ + \patternDerivation{T \text{ } v\IVML{; assign (\ldots) to \{} c(v)\IVML{\};}}{c(v)} \\ + \patternDerivation{T \text{ } v\IVML{; eval \{} c(v)\IVML{\};}}{c(v)} \\ +\end{gather*} +} + +Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. As a side effect, the constraint translation identifies and translates the constraints in the respective project\footnote{The top-translation steps in this algorithm are realized in the implementation by an IVML model visitor implicitly identifying and handling the types without iterating over the project multiple times as the notation here might suggest.}. To prioritize the constraints correctly, the reasoner uses four global sets, which are populated during the constraint translation and, finally, in Algorithm \ref{algTranslateConstraints} added to the constraint base. In more details, the reasoner maintains the following temporary constraint sets + +\begin{enumerate} + \item \emph{Default constraints $\defaultConstraints$} containing constraints setting the default values of all variables. In particular, this set can contain constraints that assign compound and container initializers, i.e., modify multiple values at once. + \item \emph{Deferred default constraints $\deferredDefaultConstraints$} containing default initialization constraints to be evaluated after all constraints in $\defaultConstraints$, but before the remaining two constraint sets below. $\deferredDefaultConstraints$ is required as setting individual variables may be accidentally overridden by compound and container initializers assigned through constraints in $\defaultConstraints$. + \item \emph{Top level constraints $\topLevelConstraints$}, i.e., constraints directly specified in a project, in top-level eval-blocks, in top-level assignment blocks as well as constraints attached to top-level variables, e.g., through derived types. These constraints originating from the top-level scope shall take precedence over constraints in nested scopes~\cite{IVML-LS}. + \item \emph{Remaining other constraints $\otherConstraints$} in particular in in nested structures, including compound types used in containers, nested assignment blocks or constraint variables. +\end{enumerate} + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{project $p$} + \KwData{configuration $cfg$, constraint $base$, constraint base copy $base_c$, constraint sets $\defaultConstraints,\deferredDefaultConstraints, \topLevelConstraints, \otherConstraints$, eval-blocks flag $inEvals$} + + \tcp{start of model visitor}%>ConstraintTranslationVisitor + \ForAll{$d \iterAssng decls(p)$}{ \label{algTranslateConstraintsTranslationStart} + $translateDeclaration(d, decision(cfg, d), \undef)$\; \label{algTranslateConstraintsTranslationDeclaration} + } + $add(\topLevelConstraints, constraints(p), true, \undef)$\; \label{algTranslateConstraintsAdd} \label{algTranslateConstraintsTopLevelConstraints} + \ForAll{$a \iterAssng assignments(p)$}{ + $add(\topLevelConstraints, allAssignmentConstraints(a), true, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationConstraints} + $translateAnnotationAssignments(a, \undef, \undef, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationAssignments} + } \label{algTranslateConstraintsTranslationEnd} + $inEvals \assng true$\; + $add(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)}, true, \undef)$\;\label{algTranslateConstraintsTopLevelEvals} + $inEvals \assng false$\; + \tcp{end of model visitor}% 0 \wedge \neg hasTimeout \wedge \neg stop$} { \label{algEvalLoopLoopStart} + $c \assng pop(base)$\; \label{algEvalLoopPop} + $setAssignmentScope(\scopeAssignments, c)$\; \label{algEvalLoopSetScope} + %$\usedVariables \assng \emptySet$\; \label{algEvalLoopClear} + $setAssignmentState(e, \isDefaultConstraint{c})$\; \label{algEvalLoopAssngState} + $analyzeEvaluationResult(\problemRecords, evaluate(e, c))$\; \label{algEvalLoopAssngEval} + \If{$constraintFulfilled(e) \wedge \isDefaultConstraint{c}$}{\label{algEvalLoopClearStart} + $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \cap \setWith{\mapEntry{v}{c}}{v\in var(c)}$\; + }\label{algEvalLoopClearEnd} + $hasTimeout \assng checkForTimeout()$\; \label{algEvalLoopTimeout} + } \label{algEvalLoopLoopEnd} + \caption{Constraint evaluation loop (\IVML{evaluateConstraints}).}\label{algEvalLoop} +\end{algorithm} + +Successfully evaluated default constraints must not stay in the constraint base as their initialization work has been done. As the evaluation of individual constraints cleans up the constraint base, we just have to avoid that they are accidentally re-scheduled. Therefore, we remove them from $\relevantConstraintsPerDeclaration$, the mapping between variable declarations and constraints in lines \ref{algEvalLoopClearStart}-\ref{algEvalLoopClearEnd}. Please note that no modification of $\relevantConstraintVariables$, the mapping between decision variables and constraints, is needed, as no change of constraint variables or their values occurred here. + +Finally, Algorithm \ref{algEvalLoop} checks for a potential timeout in line \ref{algEvalLoopTimeout} comparing the global $startTime$ set in Algorithm \ref{algMainLoop} with a configured reasoning timeout. If a timeout occurred (not further detailed in this document), the global $hasTimeout$ flag is set to $true$. This flag is also relevant for creating the overall reasoning report as explained for Algorithm \ref{algMainLoop}. Index: /reasoner/notation.tex =================================================================== --- /reasoner/notation.tex (revision 163) +++ /reasoner/notation.tex (revision 164) @@ -11,5 +11,5 @@ 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. +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. Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 163) +++ /reasoner/reasoner.tex (revision 164) @@ -19,4 +19,5 @@ \newcommand\IVML[1]{\texttt{#1}} \newcommand\IVMLself[0]{\texttt{self}} +\newcommand\IVMLnull[0]{\texttt{null}} \newcommand\IVMLMeta[1]{\texttt{#1}} %\underline{} \newcommand\addSet[0]{\cup} @@ -77,5 +78,5 @@ \input{approach} \input{notation} -\input{reasoningAlg} +\input{mainAlgorithms} \input{consTranslation} \input{consRescheduling} Index: asoner/reasoningAlg.tex =================================================================== --- /reasoner/reasoningAlg.tex (revision 163) +++ (revision ) @@ -1,229 +1,0 @@ -% trim={ } -\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.} -\label{figStructure} -\end{figure} - -\section{Reasoning algorithm}\label{sectReasoning} - -\newcommand\defaultConstraints[0]{c_d} -\newcommand\deferredDefaultConstraints[0]{c_{dd}} -\newcommand\otherConstraints[0]{c_{o}} -\newcommand\topLevelConstraints[0]{c_{t}} -\newcommand\relevantConstraintsPerDeclaration[0]{r_d} -\newcommand\relevantConstraintVariables[0]{r_c} -\newcommand\scopeAssignments[0]{a} -%\newcommand\usedVariables[0]{u} -\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. - -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}. - -\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$). - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{configuration $c$} - \KwData{configuration $cfg$, expression evaluator $e$, scope assignments $\scopeAssignments$, start time $startTime$, $reuse$ flag, constraint relations $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$, constraint base copy $base_c, base_{\relevantConstraintsPerDeclaration}, base_{\relevantConstraintVariables}$, $projects$ sequence, $hasTimeout$ and $stop$ flags}%, problem records $\problemRecords$ - \KwResult{Reasoning result $r$} - - $cfg\assng c$\; \label{algMainLoopSetupVar} - %evaluator.init()\; - %evaluator.setResolutionListener(Algorithm \ref{algVarChange})\; - %evaluator.setScopeAssignments(sAssng)\; - $setup(e, cfg, \scopeAssignments)$\; \label{algMainLoopSetupEval} - $startTime = now()$\;\label{algMainLoopStartTime} - \uIf{$base_c = \undef$}{ \label{algMainLoopFullStart} - \If{$reuse$}{ - $base_c = \emptySeq{}$\; %sequence? - $base_{\relevantConstraintsPerDeclaration} = \emptyMap{}$\; - $base_{\relevantConstraintVariables} = \emptySet{}$\; %map? - } - $projects \assng discoverImports(cfg)$\; \label{algMainLoopDiscover} - \ForAll{$p \iterAssng projects \wedge \neg hasTimeout \wedge \neg stop$}{ \label{algMainLoopStart} - $translateConstraints(p)$\; \label{algMainLoopTranslate} - $evaluateConstraints(p)$\; \label{algMainLoopEvaluate} - $freeze(cfg, p)$\; \label{algMainLoopFreeze} - } \label{algMainLoopEnd}\label{algMainLoopFullEnd} - }\Else {\label{algMainLoopIncStart} - $\relevantConstraintsPerDeclaration \assng base_{\relevantConstraintsPerDeclaration}$\;\label{algMainLoopResetRelStart} - $\relevantConstraintVariables \assng base_{\relevantConstraintVariables}$\;\label{algMainLoopResetRelEnd} - \ForAll{$i \in \set{0, \ldots, |base_c|} \wedge \neg hasTimeout \wedge \neg stop$}{ - $base \assng base_c[i]$\; - $evaluateConstraints(projects[i])$\; - $freeze(cfg, projects[i])$\; - } - }\label{algMainLoopIncEnd} - $r \assng createReasoningResult(m, hasTimeout, stop)$\; \label{algMainLoopResult} - \caption{Main reasoning loop (\IVML{resolve}).}\label{algMainLoop} -\end{algorithm} - - -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}. - -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. - -Finally, after all projects have been considered or the main reasoning loop has been terminated prematurely, the algorithm composes\footnote{In the implementation, this is done in \class{Engine.java}, the actual reasoner instance, which creates and utilizes instances of \class{Resolver.java}.} in line \ref{algMainLoopResult} a detailed reasoning result based on recorded evaluation problems. This reasoning result also indicates a successful or failed execution, in particular whether a timeout occurred or a user-requested cancellation was requested. - -\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 evaluated over involved top-level variables. As already mentioned in Section \ref{sectNotationConstraints}, constraints defined on compound slots or indirectly through use of compound instances in containers must be translated before evaluation. The particular issue here is that these constraints can be defined in an IVML model over types (for which no values can be assigned in a configuration) rather than over top-level variables. A solution is to rewrite these constraints by substituting type-local variables by appropriate accessors starting at 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 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 links all currently relevant variables to the correct accessor expressions, which are created before the respective variable substitutions are applied. - -However, a simple stack is not sufficient for two reasons, namely nested complex types, excluded types and assignment blocks. As we will detail below, nested complex types require constraint rewriting through a prefix composed of nested all-quantifiers. Therefore, the stack frames can store the information needed to create the respective quantifier expression. When adding a constraint to the constraint base, we visit the stack frames and, if such information is available, incrementally qualify the expression by the described quantifier. The constraint rescheduling re-uses the constraint transformation. However, performing a complete transformation of all types related to certain value change is typically not needed, so that excluding types from the translation speeds up the re-scheduling operations. -%Moreover, IVML projects and compounds can contain nested assignment blocks. An assignment block implicitly defines assignment constraints for its contained variable declarations including containers or compounds. If we translate first variable declarations and then the related constraints, these constraints are outside their actual scope and, thus, relevant access expressions are not available, i.e., wrong constraints would be added to the constraint bae. Intermingling compund/container translation with annotation-block translation would be a potential solution, which increases the algorithm / code complexity. Thus, we opted to register a declaration with its context frame (which is then implicitly registered with its parent frame for proper cleanup) and to activate/deactivate such a frame, although it is not on top of the stack, when translating the implicit assignment constraints in an assignment block. Such stack frames are also removed from the stack when popping the respective parent context frame. - -In summary, the variable mapping stack structure $\variableMapping$ of the IVML reasoner provides the following operations: - -\begin{itemize} -% \item $setRegisterContexts(\variableMapping, b)$ enables automatic registration of context frames within the parent frame. The operation returns the previous state of the registration flag. -% \item $isContextsRegistering(\variableMapping)$ returns whether new context frames are automatically registered with the parent frame. - \item $pushContext(\variableMapping, d, r)$ creates and pushes a new context frame for declaration $d$ to the stack. If registration of contexts is enabled, $r$ indicates whether the new frame shall be registered with the parent frame and whether already processed types (for handling nested complex types) shall be recorded by this context. - \item $pushContext(\variableMapping, d, c,v, r)$ works like $pushContext(\variableMapping, d, r)$, but registers also information for creating an all-quantified constraint prefix for all constraints added to the constraint base as long this frame is on the stack. The information includes the container expression $c$ and the typed iterator variable $v$ over the element type of $c$. We will apply this function in Section \ref{sectContainerDefaults}. - \item $popContext(\variableMapping)$ removes the top-most context frame. The initial frame, which is created by default and devoted to the enclosing IVML project, is not removed by this operation. - \item $registerMapping(\variableMapping, d, ca)$ registers the access expression $ca$ with the given variable declaration $d$ in the top-most context frame. Essentially, a context frame contains a mapping $m$ and the operation performs $m \assng m \addMap \mapEntry{d}{ca}$. - \item $getMapping(\variableMapping, d)$ returns the mapping for $d$ (for short $\variableMapping[d]$). If no mapping was registered for the actual context frame, all context frames in stack order are considered. If no mapping is registered, the result is $\undef$. - \item $recordProcessed(\variableMapping, t)$ records a processed type with the closest containing context having processed type registration enabled. If \linebreak[4] $isCompound(t)$, this function registers $allRefined^+(t)$. - \item $alreadyProcessed(\variableMapping, t)$ returns whether $t$ was already registered as a processed type in one of the enclosing context frames. -% \item $activate(\variableMapping, d)$ re-activates, i.e., pushes the registered stack frame for $d$ taken from the current context frame. As long as the current context frame exists, this operation can be called again and again. If no context frame is registered for $d$, the stack is not modified. -% \item $deactivate(\variableMapping, d)$ de-activates the registered context frame for $d$, i.e., pops it from the stack but leaves it registered with its parent context frame so that it is available for further activations as long as the parent context frame exists on the stack. - \item $setTypeExcludes(\variableMapping, s)$ defines a set of types to be marked as excluded from constraint transformations. Excluding types is important for a fast processing of re-scheduled constraints in Section \ref{sectTopLevelConstraintsRescheduling}. - \item $transferTypeExcludes(\variableMapping, t)$ transfers excluded types into this context and stores the causing type $t$ in the current context. Transferring excluded types binds them to the actual (usual top-most) type and avoids applying them some nested type. - \item $currentType(\variableMapping)$ returns the type $t$ stored in the current context by $transferTypeExcludes(\variableMapping, t)$. The result is $\undef$ if no transfer happened for the current context. - \item $isTypeExcluded(\variableMapping, t)$ returns whether $t$ is excluded in the current context. $excludedTypes(\variableMapping)$ returns all excluded types for the current context or an empty set. - \item $size(\variableMapping)$ the number of contexts on the stack. There is always at least one context on the stack representing the enclosing project. - \item $clear(\variableMapping)$ clears the stack and cleans up the default context frame dedicated to the IVML project so that $\variableMapping$ is ready for the translation of the next IVML project. -\end{itemize} - -From a black-box perspective, $\variableMapping$ can be considered as a usual map as discussed in Section \ref{sectGeneralNotation}, but performing some stack-based lookup operations. Thus, we just use $\variableMapping$ in the variable substitution notation as introduced in Section \ref{sectNotationConstraints}, e.g., let $e$ be an expression, then $\varSubstitutionVarMapping{e}$ replaces all variables in $e$ having a mapping (through the $getMapping$ operation) in at least on context frame of $\variableMapping$. - -%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 for a variable has been made cannot be maintained by a simple flat mapping. This requires a data structure, which stores information about assignments per project (scope). This structure is important to detect invalid variable re-assignments, i.e., to figure out whether a variable assigned more than once per scope~\cite{IVML-LS}. - -The scope assignments structure of the IVML reasoner (usually named $\scopeAssignments$ for assignments) 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} - -The core idea of the constraint translation is to collect the constraints following the structure of an IVML model and to replace each type-related variable by the correct accessor expression for a global variable in the current scope. According to the IVML specification~\cite{IVML-LS}, the relevant top-level elements are variable declarations, global constraints, annotation assignment blocks and eval-blocks. Type definitions are considered when when processing variable declarations, as the individual type of a variable indicates the specific constraints to be collected and instantiated. - -As Algorithm \ref{algTranslateConstraints} focuses on top-level constraints and delegates more complex transformations to sub-sequent algorithms, in particular Algorithm \ref{algTranslateDeclaration} for variable declarations, and top-level constraints exclusively use qualified variable access expressions, the translation patterns are rather straightforward. Top-level constraints, constraints in (nested) annotation assignments and constraints in (nested) eval blocks are taken over as specified into the constraint base. However, constraints in eval-blocks must be prioritized over the remaining constraints~\cite{IVML-LS}. - -\grayPara{ -\begin{gather*} - \patternDerivation{T \text{ } v\IVML{;} c(v)\IVML{;}}{c(v)} \\ - \patternDerivation{T \text{ } v\IVML{; assign (\ldots) to \{} c(v)\IVML{\};}}{c(v)} \\ - \patternDerivation{T \text{ } v\IVML{; eval \{} c(v)\IVML{\};}}{c(v)} \\ -\end{gather*} -} - -Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. As a side effect, the constraint translation identifies and translates the constraints in the respective project\footnote{The top-translation steps in this algorithm are realized in the implementation by an IVML model visitor implicitly identifying and handling the types without iterating over the project multiple times as the notation here might suggest.}. To prioritize the constraints correctly, the reasoner uses four global sets, which are populated during the constraint translation and, finally, in Algorithm \ref{algTranslateConstraints} added to the constraint base. In more details, the reasoner maintains the following temporary constraint sets - -\begin{enumerate} - \item \emph{Default constraints $\defaultConstraints$} containing constraints setting the default values of all variables. In particular, this set can contain constraints that assign compound and container initializers, i.e., modify multiple values at once. - \item \emph{Deferred default constraints $\deferredDefaultConstraints$} containing default initialization constraints to be evaluated after all constraints in $\defaultConstraints$, but before the remaining two constraint sets below. $\deferredDefaultConstraints$ is required as setting individual variables may be accidentally overridden by compound and container initializers assigned through constraints in $\defaultConstraints$. - \item \emph{Top level constraints $\topLevelConstraints$}, i.e., constraints directly specified in a project, in top-level eval-blocks, in top-level assignment blocks as well as constraints attached to top-level variables, e.g., through derived types. These constraints originating from the top-level scope shall take precedence over constraints in nested scopes~\cite{IVML-LS}. - \item \emph{Remaining other constraints $\otherConstraints$} in particular in in nested structures, including compound types used in containers, nested assignment blocks or constraint variables. -\end{enumerate} - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{project $p$} - \KwData{configuration $cfg$, constraint $base$, constraint base copy $base_c$, constraint sets $\defaultConstraints,\deferredDefaultConstraints, \topLevelConstraints, \otherConstraints$, eval-blocks flag $inEvals$} - - \tcp{start of model visitor}%>ConstraintTranslationVisitor - \ForAll{$d \iterAssng decls(p)$}{ \label{algTranslateConstraintsTranslationStart} - $translateDeclaration(d, decision(cfg, d), \undef)$\; \label{algTranslateConstraintsTranslationDeclaration} - } - $add(\topLevelConstraints, constraints(p), true, \undef)$\; \label{algTranslateConstraintsAdd} \label{algTranslateConstraintsTopLevelConstraints} - \ForAll{$a \iterAssng assignments(p)$}{ - $add(\topLevelConstraints, allAssignmentConstraints(a), true, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationConstraints} - $translateAnnotationAssignments(a, \undef, \undef, \undef)$\; \label{algTranslateConstraintsTopLevelAnnotationAssignments} - } \label{algTranslateConstraintsTranslationEnd} - $inEvals \assng true$\; - $add(\topLevelConstraints,\seqWith{constraints(e)}{e\in evals(p)}, true, \undef)$\;\label{algTranslateConstraintsTopLevelEvals} - $inEvals \assng false$\; - \tcp{end of model visitor}% 0 \wedge \neg hasTimeout \wedge \neg stop$} { \label{algEvalLoopLoopStart} - $c \assng pop(base)$\; \label{algEvalLoopPop} - $setAssignmentScope(\scopeAssignments, c)$\; \label{algEvalLoopSetScope} - %$\usedVariables \assng \emptySet$\; \label{algEvalLoopClear} - $setAssignmentState(e, \isDefaultConstraint{c})$\; \label{algEvalLoopAssngState} - $analyzeEvaluationResult(\problemRecords, evaluate(e, c))$\; \label{algEvalLoopAssngEval} - \If{$constraintFulfilled(e) \wedge \isDefaultConstraint{c}$}{\label{algEvalLoopClearStart} - $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \cap \setWith{\mapEntry{v}{c}}{v\in var(c)}$\; - }\label{algEvalLoopClearEnd} - $hasTimeout \assng checkForTimeout()$\; \label{algEvalLoopTimeout} - } \label{algEvalLoopLoopEnd} - \caption{Constraint evaluation loop (\IVML{evaluateConstraints}).}\label{algEvalLoop} -\end{algorithm} - -Successfully evaluated default constraints must not stay in the constraint base as their initialization work has been done. As the evaluation of individual constraints cleans up the constraint base, we just have to avoid that they are accidentally re-scheduled. Therefore, we remove them from $\relevantConstraintsPerDeclaration$, the mapping between variable declarations and constraints in lines \ref{algEvalLoopClearStart}-\ref{algEvalLoopClearEnd}. Please note that no modification of $\relevantConstraintVariables$, the mapping between decision variables and constraints, is needed, as no change of constraint variables or their values occurred here. - -Finally, Algorithm \ref{algEvalLoop} checks for a potential timeout in line \ref{algEvalLoopTimeout} comparing the global $startTime$ set in Algorithm \ref{algMainLoop} with a configured reasoning timeout. If a timeout occurred (not further detailed in this document), the global $hasTimeout$ flag is set to $true$. This flag is also relevant for creating the overall reasoning report as explained for Algorithm \ref{algMainLoop}.