Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 218) +++ /reasoner/consTranslation.tex (revision 219) @@ -81,6 +81,6 @@ \grayPara{ - \patternDerivationLabel{\IVML{typedef } T \IVML{ with }(c); T\ v\IVML{;}}{\nonumber\\\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{c}{decl(u)=deref(u, v), \variableMapping}}{formDerivedDatatypeConstraints} - \patternDerivationLabel{\IVML{typedef } \IVMLcontainer{T} \IVML{ with }(c); T\ v\IVML{;}}{\nonumber\\\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{\IVMLforall{v}{i}{c}}{decl(u)=deref(u, i), \variableMapping}}{formDerivedDatatypeConstraintsContainer} + \patternDerivationLabel{\IVML{typedef } T \IVML{ with }(c); T\ v\IVML{;}}{\oatternDerivationLinebreak\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{c}{decl(u)=deref(u, v), \variableMapping}}{formDerivedDatatypeConstraints} + \patternDerivationLabel{\IVML{typedef } \IVMLcontainer{T} \IVML{ with }(c); T\ v\IVML{;}}{\oatternDerivationLinebreak\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{\IVMLforall{v}{i}{c}}{decl(u)=deref(u, i), \variableMapping}}{formDerivedDatatypeConstraintsContainer} } @@ -119,8 +119,8 @@ \grayPara{ - \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s = deflt\IVML{;\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{s = deflt}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundDefault} - \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s\IVML{; } \constraintWith{c}{s}\IVML{\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundSlot} - \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s\IVML{; eval \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundEval} - \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s\IVML{; assign (\ldots) to \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundAssign} + \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s = deflt\IVML{;\}; } C\ v \IVML{;}}{\oatternDerivationLinebreak\varSubstitution{s = deflt}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundDefault} + \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s\IVML{; } \constraintWith{c}{s}\IVML{\}; } C\ v \IVML{;}}{\oatternDerivationLinebreak\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundSlot} + \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s\IVML{; eval \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\oatternDerivationLinebreak\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundEval} + \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s\IVML{; assign (\ldots) to \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\oatternDerivationLinebreak\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundAssign} \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s \IVML{\}; } C\ v \IVML{; } \constraintWith{c}{v.s}\IVML{;}}{\varSubstitution{\constraintWith{c}{v.s}}{\variableMapping}}{forCompoundConstraint} } @@ -276,7 +276,7 @@ \grayPara{ - \patternDerivationLabel{\IVMLcontainer{T}\ v\IVML{;}}{\nonumber\\\bigcup_{t~\in~usedTypes(v),~ c~\in~constraints(t)}\IVMLforall{f(v, t)}{\IVML{i}}{\varSubstitution{\constraintWith{c}{x}}{x=\IVML{i}, \IVMLself{}=\IVML{i}, \variableMapping}}}{forContainerQuant} - \patternDerivationLabel{\IVMLcontainer{\IVML{Constraint}}~v = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;}}{\nonumber\\\varSubstitution{ex_1}{\variableMapping}, \ldots, \varSubstitution{ex_n}{\variableMapping}}{forConstraintContainer} - \patternDerivationLabel{\IVMLcontainer{T}\ v\IVML{;}~\constraintWith{c}{v}\IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{v}}{\variableMapping}}{forContainerTop} + \patternDerivationLabel{\IVMLcontainer{T}\ v\IVML{;}}{\oatternDerivationLinebreak\bigcup_{t~\in~usedTypes(v),~ c~\in~constraints(t)}\IVMLforall{f(v, t)}{\IVML{i}}{\varSubstitution{\constraintWith{c}{x}}{x=\IVML{i}, \IVMLself{}=\IVML{i}, \variableMapping}}}{forContainerQuant} + \patternDerivationLabel{\IVMLcontainer{\IVML{Constraint}}~v = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;}}{\oatternDerivationLinebreak\varSubstitution{ex_1}{\variableMapping}, \ldots, \varSubstitution{ex_n}{\variableMapping}}{forConstraintContainer} + \patternDerivationLabel{\IVMLcontainer{T}\ v\IVML{;}~\constraintWith{c}{v}\IVML{;}}{\oatternDerivationLinebreak\varSubstitution{\constraintWith{c}{v}}{\variableMapping}}{forContainerTop} } @@ -562,18 +562,20 @@ \subsection{Constraint variables}\label{sectConstraintVariables} -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 \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. +In IVML, the type \IVML{Constraint} allows defining variables that contain a constraint. The value of a constraint variable shall be considered during reasoning as an usual constraint~\cite{IVML-LS}. As for other variables, the value of a constraint variable can be changed by assigning new constraints (including \IVML{true}, \IVML{false}, or even \IVML{null}) unless it is frozen. If the value of a constraint variable changes during reasoning, the reasoner must adjust the constraint base accordingly, i.e., the old constraint (value) must be removed and the new one added (cf. Section \ref{sectTopLevelConstraintsRescheduling}). + +As shown below, the translation of constraint variables must consider constraint variables (Pattern \ref{forConstraintVariable}), containers containing constraints (Pattern \ref{forConstraintContainer2}, already mentioned as Pattern \ref{forConstraintContainer} in Section \ref{sectContainerDefaults}) as well as combinations of both patterns with compounds (Patterns \ref{forConstraintVariableCompound} and \ref{forConstraintContainerCompound}): \grayPara{ - \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}{\IVMLself{}=v, \variableMapping}} - \patternDerivation{\IVMLcontainer{\IVML{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{;}\nonumber\\}{\varSubstitution{ex_1}{\IVMLself{}=v, \variableMapping}, \ldots, \varSubstitution{ex_n}{\IVMLself{}=v, \variableMapping}} + \patternDerivationLabel{\IVML{Constraint}~v = ex\IVML{;}}{\oatternDerivationLinebreak\varSubstitution{ex}{\variableMapping}}{forConstraintVariable} + \patternDerivationLabel{\IVMLcontainer{\IVML{Constraint}}~v = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;}}{\oatternDerivationLinebreak\varSubstitution{ex_1}{\variableMapping}, \ldots, \varSubstitution{ex_n}{\variableMapping}}{forConstraintContainer2} + \patternDerivationLabel{\IVML{Compound}~C =~\IVML{\{Constraint } s = ex\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}}{\oatternDerivationLinebreak\varSubstitution{ex}{\IVMLself{}=v, \variableMapping}}{forConstraintVariableCompound} + \patternDerivationLabel{\IVML{Compound }C =\ \IVML{\{containerOf(Constraint) } s = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}\oatternDerivationLinebreak}{\varSubstitution{ex_1}{\IVMLself{}=v, \variableMapping}, \ldots, \varSubstitution{ex_n}{\IVMLself{}=v, \variableMapping}}{forConstraintContainerCompound} } -% CONSTRAINT CONTAINER REPEATED!!! - -In more details, Algorithm \ref{algCreateConstraintVariableConstraint}\footnote{Here we abstract two implementation parameters for the self value/expression into one parameter and omit the parameter indicating the parent instance of the constraint to be created.} takes a constraint expression (e.g., the default value of a variable or a nested variable through Algorithm \ref{algTranslateDeclaration}), an optional expression $e_f$ representing \IVMLself{} and the variable $v$ the translation is applied to. Algorithm \ref{algCreateConstraintVariableConstraint} performs in line \ref{algCreateConstraintVariableConstraintCreate} a variable substitution with $\variableMapping$ and, if given, $e_f$, and turns the resulting expression into a (constraint variable) constraint. In line \ref{algCreateConstraintVariableConstraintAdd}, the algorithm adds the created constraint to the set of other constraints $\otherConstraints$. The third parameter of the $add$ function (will be discussed in Section \ref{sectContainerBase}) indicates whether the constraint be analyzed for complex value assignments that contain constraints as values for constraint variables. This is not required (and may sometimes lead to endless recursions) if the constraint here is a constant value. Finally, in line \ref{algCreateConstraintVariableConstraintRegister}, the relationship between the underlying variable $v$ and the constraint is recorded to enable efficient updates of the constraint base upon value change (cf. Algorithm \ref{algVarChange}). +The basic idea for translating constrainat variables is to turn the (default) value, a constraint expression, into a constraint and to add the expression to the constraint base (Pattern \ref{forConstraintVariable}). For constraint containers, i.e., containers containing constraints, we perform a translation of the individual element values each representing constraint expressions (Pattern \ref{forConstraintContainer2}). As discussed in Section \ref{sectCompoundContainer}, this will ultimately lead to an all-quantization over the constraint values in the container. If either is nested in a compound, the variable substitution must particularly replace \IVMLself{} by the actual compound variable (Pattern \ref{forConstraintVariableCompound} or Pattern \ref{forConstraintContainerCompound}). Please note that in addition to the translation patterns for constraint variables also the other translation patterns apply, i.e., if a default value is given, also a respective assignment constraint according to Pattern \ref{forVarDecl} from Section \ref{sectTranslationDeclarationTypesDefaults}, Pattern \ref{forCompoundDefault} from Section \ref{sectCompoundDefaults} or Pattern \ref{forContainerQuant} from Section \ref{sectContainerDefaults} is created so that the constraint variable also receives the constraint as value. + +In more details\footnote{In contrast to the implementation, we represent here two parameters for self value/expression by a single parameter and omit a parameter for the constraint parent.}, Algorithm \ref{algCreateConstraintVariableConstraint} takes a constraint expression (e.g., the default value of a constraint variable or a nested variable through Algorithm \ref{algTranslateDeclaration}), an optional expression $e_f$ representing \IVMLself{} and the constraint variable $v$ if available\footref{fnVariableNull}. Algorithm \ref{algCreateConstraintVariableConstraint} performs in line \ref{algCreateConstraintVariableConstraintCreate} a variable substitution with $\variableMapping$ and, if given, $e_f$, and turns the resulting expression into a (constraint variable) constraint. In line \ref{algCreateConstraintVariableConstraintAdd}, the algorithm adds the created constraint to the set of other constraints $\otherConstraints$ (disabling the analysis for complex values in case of constant constraints such as \IVML{true}). +%The third parameter of the $add$ function (will be discussed in Section \ref{sectContainerBase}) indicates whether the constraint be analyzed for complex value assignments that contain constraints as values for constraint variables. This is not required (and may sometimes lead to endless recursions) if the constraint here is a constant value. +In line \ref{algCreateConstraintVariableConstraintRegister}, the algorithm registers the relation between $v$ and the created constraint in $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$. %is recorded to enable efficient updates of the constraint base upon value changes (cf. Algorithm \ref{algVarChange}). \begin{algorithm}[H] @@ -587,7 +589,21 @@ \end{algorithm} -It is important to note that the constraint translation for collections in Section \ref{sectContainerDefaults} creates quantor expressions also for collections over constraint variables. Per se this is problematic, as due to the applied variable substitutions, a constraint acting as a value may accidentally be bound to quantor iterator variable(s). During constraint translation, the constraint is passed by Algorithm \ref{algTranslateDeclaration} to Algorithm \ref{algCreateConstraintVariableConstraint} and added to the constraint base without the surrounding quantor, i.e., an evaluation is always undefined as the iterator variables remain unbound. As a heuristic, in most cases one could bind the iterator variables by variable substitution in Algorithm \ref{algCreateConstraintVariableConstraint} by the actual value for \IVMLself{}, i.e., $e_f$ or $v$. - -A precise solution is to defer the substitution until the iterator variables are defined, i.e., during quantor evaluation. Thus, we track changes of the (local) iterator variables and perform their replacement during constraint re-scheduling (cf. Section \ref{sectTopLevelConstraintsRescheduling}), which is also executed when the initial values of variables are set. For short, during quantor evaluation, we we track the value changes of temporary iterator variables in terms of an extended dynamic variable mapping in $\variableMapping$. When the quantor evaluation assigns the new constraint value, the value change triggers the replacement of the old constraint by the new one in the constraint base. For the new constraint, constraint translation must be performed, i.e., the variable substitution applied in all constraint translations utilizes the dynamically modified $\variableMapping$ and implicitly binds the iterator variables in the constraint to the correct values. In other words, we accept specific temporarily inconsistent constraints with unbound variables for the short time between assigning the constraint value and the subsequent constraint re-scheduling. Ultimately, the corrected constraint must also be assigned to the configuration variable so that further model operations such as saving the configuration uses the actual (consistent) constraint. Obviously, this final assignment shall avoid triggering the constraint re-scheduling again. +It is important to mention that the constraint translation for collections as discussed in Section \ref{sectContainerDefaults}, in particular the all-quantization can lead to erroneous default value expressions for constraint variables. Given the following IVML fragment + +\begin{verbatim} +compound C { + Integer j; + Constraint c = j > 0; +} +setOf(C) s = {...}; +\end{verbatim} + +The constraint translation applies Pattern \ref{forContainerQuant} to container \IVML{s} and, subsequently, Pattern \ref{forConstraintVariableCompound} to constraint slot \IVML{c}. This leads to the creation of the constraint \IVML{\IVMLforall{s}{i}{i.j > 0}} that correctly restricts all compound values in set \IVML{s} by the constraint given in the constraint variable \IVML{c}. + +In the same step, the constraint translation applies Pattern \ref{forCompoundDefault} to handle the default value of \IVML{c} within container \IVML{s} (Pattern \ref{forContainerQuant}). This leads to \IVML{\IVMLforall{s}{i}{i.c = i.j > 0}}, i.e., a quantification of assignment constraints. At a glance, the expression seems to be correct, but without further consideration, the expression evaluator may turn the assigned constraint value into an unbound expression. If the usual evaluation rules are applied, the right side \IVML{i.j > 0} becomes a constraint expression value and is assigned to slot \IVML{c} without the enclosing quantor. Without the quantor, which indeed must not be part of the value of \IVML{c} according to the fragment above, the assigned constraint value contains the unbound iterator variable \IVML{i}, i.e., the value is a wrong expression that cannot (further) be evaluated. + +As a heuristic, in most cases it would be correct to bind the unbound iterator variables with the actual value for \IVMLself{}, i.e., in Algorithm \ref{algCreateConstraintVariableConstraint} $e_f$ or $v$. This heuristic may fail, in particular if multiple unbound iterator variables occur, e.g., for nested compound containers. A precise solution is to defer the substitution from translation time until the iterator variables are defined, i.e., until quantor evaluation. To achieve this, we track changes of the iterator variables during evaluation and consider them for variable substitution before the constraint value is (finally) assigned. + +In more details, we use $\variableMapping$ also during expression evaluation to track the actual values of (local) iterator variables within an additional stack frame created during the evaluation. We may apply the tracked values when assigning the new constraint value to the respective variable, but this would lead to unwanted dependencies between expression evaluator and reasoning. A second point in time when we can perform the variable substitution is the constraint re-scheduling, i.e., when the reasoner is informed that the value (including the initial default value) of a variable was changed. When the evaluation of the quantor assigns the new constraint value, the value change triggers the replacement of the old constraint by the new one in the constraint base. For the new constraint, the constraint translation must executed anyway, i.e., a variable substitution is performed. The variable substitution utilizes $\variableMapping$, i.e., also the stack frame for iterator variables added during the evaluation, and, thus, implicitly binds the iterator variables in the constraint to the correct values. Finally, the corrected constraint is assigned to the configuration variable so that further model operations such as saving the configuration use the actual (correct) constraint. For the time between triggering the assignment of a constraint value and the subsequent constraint re-scheduling, which effectively corrects the value and performs the final assignment, we accept constraints with unbound variables. This is not a problem per se, as no further constraint (sub-)expressions happen in this time span. \subsection{Constraint base operations}\label{sectContainerBase}\label{sectConstraintBase} Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 218) +++ /reasoner/reasoner.tex (revision 219) @@ -69,4 +69,5 @@ \newcommand\patternDerivation[2]{#1 \patternDerivationSymbol #2\\} \newcommand\patternDerivationLabel[3]{#1 \patternDerivationSymbol #2\label{#3}\\} +\newcommand\oatternDerivationLinebreak[0]{\nonumber\\} \let\emph\relax % there's no \RedeclareTextFontCommand