Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 158) +++ /reasoner/consTranslation.tex (revision 159) @@ -478,31 +478,30 @@ 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}). -There are four basic translation patterns, three are shown below. The basic idea is to translate the (default) value, a constraint expression, directly into a constraint performing appropriate variable substitutions. For constraint containers, we translate the element values, which represent constraint expressions. If either pattern is nested within a compound (not shown for constraint containers below), the translation substitution must particularly replace \IVML{self} by the actual compound variable. - -\grayPara{ -\begin{gather*} - \patternDerivation{\IVML{Constraint } v = ex\IVML{;}}{\varSubstitution{ex}{\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{ \{Constraint } s = ex \IVML{\}}\IVML{; } C v\IVML{;}}{\varSubstitution{ex}{\IVML{self}=v, \variableMapping}} -\end{gather*} -} - -In more details, Algorithm \ref{algCreateConstraintVariableConstraint} translates a constraint (if not undefined, including the IVML \IVML{null} case, i.e., a de-configured constraint variable). Algorithm \ref{algCreateConstraintVariableConstraint} creates constraints through variable substitution with $\variableMapping$ and, if available, a respective value for \IVMLself (here $f$), turning the resulting expression into a constraint and adding it to the set of other constraints $\otherConstraints$. Moreover, the relationship between the underlying variable $v$ and the constraint must be recorded for efficient update of the constraint base upon value change (cf. Algorithm \ref{algVarChange}). - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{constraint expression $c$, actual value for \IVMLself{} $f$, variable $v$} - \KwData{other constraints $\otherConstraints$} - \If {$c \neq \undef$} { - $c \assng \createConstraintConstraint{\varSubstitutionSelfVarMapping{c}{f}}$\; - $add(\otherConstraints, \set{c}, \neg isConst(c), v)$\; - $register(v, c)$\; - } +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. + +\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{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}}\\ +\end{gather*} +} + +In more details, Algorithm \ref{algCreateConstraintVariableConstraint} 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}). + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{constraint expression $c$, expression for \IVMLself{} $e_f$, variable $v$} + \KwData{other constraints $\otherConstraints$, variable mapping $\variableMapping$} + $c \assng \createConstraintConstraint{\varSubstitutionSelfVarMapping{c}{e_f}}$\;\label{algCreateConstraintVariableConstraintCreate} + $add(\otherConstraints, c, \neg isConst(c), v)$\;\label{algCreateConstraintVariableConstraintAdd} + $register(v, c)$\;\label{algCreateConstraintVariableConstraintRegister} \caption{Creating constraints for constraint variables (\IVML{createConstraintVariableConstraint}).}\label{algCreateConstraintVariableConstraint} \end{algorithm} -It is important to note that the constraint translation for collection leads to quantor expressions for initializing constraint variables. This is per se dangerous, as due to the variable substitutions, a constraint acting as a value may then relate to the quantor iterator variable(s). Evaluating such a constraint leads to undefined expressions, as the iterator variables are unbound and shall be substituted by appropriate variables (in most cases \IVMLself{}). When utilizing quantor expressions, defining individual substitutions based on the involved instances does not work (as this is the purpose of the quantor). So one solution is to unfold the implicit loop as discussed in Section \ref{sectContainerDefaults}. However, as quantor expressions over variable assignments are valid IVML and may be utilized in a model, the reasoner and the constraint evaluation must be able to work with them anyway. - -As solution, we perform the variable replacement when changing the constraint value, i.e., during constraint re-scheduling (Section \ref{sectTopLevelConstraintsRescheduling}). For short, we utilize the quantor expressions as discussed in this section, during quantor evaluation we register also the temporary iterator variables in the actual context, let the quantor evaluation assign the constraints to the variables, and consider this dynamically modified context during constraint re-scheduling. Constraint re-scheduling is anyway notified about the variable change and utilized to replace the old constraint by the new one in the constraint base. Thereby, we perform a variable substitution to bind the constraint to the actual variable taking into account the actual context including the iterator variables, i.e., we accept a temporary inconsistent constraint with unbound variables for the short time between assigning the constraint variable value and the directly subsequent constraint re-scheduling for this value change. However, this finally corrected constraint must be stored in the configuration so that saving the configuration can happen with the actual (consistent) constraint. +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. \subsection{Constraint base operations}\label{sectContainerBase}