Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 208) +++ /reasoner/consTranslation.tex (revision 209) @@ -216,12 +216,15 @@ \subsubsection{Translating Compound Constraints}\label{sectionTransComp} -Given a complete mapping for compound type $t$, we can transform the constraints, i.e., apply Algorithm \ref{algTranslateCompoundContent}. As mentioned above, the algorithm first translates all default value expressions of slots, then the default values from annotation assignments, and, finally, the constraints in eval blocks with higher evaluation priority as well as the remaining nested constraints. When translating the default value expression for slots, Algorithm \ref{algTranslateCompoundContent} calls Algorithm \ref{algTranslateDeclaration}, and, thus, triggers a potentially recursive translation along the respective slot types, in particular in case of compound or container slots. - -Let -% -$$slots^-(t) = \setWith{s}{s \in slots(t) \wedge \neg isTypeExcluded(\variableMapping, type(parent(s)))} $$ -% -be the slots of compound type $t$ for which the containing parent type is not excluded in the actual context of $\variableMapping$, e.g., due to constraint re-scheduling. In lines \ref{algTranslateCompoundDeclarationTranslateSlotsStart}-\ref{algTranslateCompoundDeclarationTranslateSlotsEnd}, Algorithm \ref{algTranslateCompoundContent} performs the translation of the default value expressions. We must distinguish two cases here, namely whether the configuration variable $v$ is available or not\footref{fnVariableNull}. -In the first case (lines \ref{algTranslateCompoundDeclarationTranslateSlotsStart}-\ref{algTranslateCompoundDeclarationTranslateSlotsMid}), we can rely on the compound variable $v$ and its nested variables representing all slots even refined ones\footnote{This also holds for $slots^-(v)$ if the parent type of $v$ is not excluded.} (cf. Section \ref{sectNotationCompounds}). Thus, in line \ref{algTranslateCompoundDeclarationTranslateSlotsV}, we call Algorithm \ref{algTranslateDeclaration} for slot $s$ and its annotations with the variable corresponding to $s$ and the access expression for $s$ recorded in $\variableMapping$. In the second case (lines \ref{algTranslateCompoundDeclarationTranslateSlotsMid}-\ref{algTranslateCompoundDeclarationTranslateSlotsEnd}), we use the type structure as fallback, i.e., we translate constraints without knowledge about the actual type of the variables. In line \ref{algTranslateCompoundDeclarationTranslateSlotsT}, we call Algorithm \ref{algTranslateDeclaration} for a type-based transformation of the slot declaration $d$ and its annotations, i.e., without slot variable but with accessor expression for $s$ recorded in $\variableMapping$. +Given a complete mapping for compound type $t$, we can transform the constraints declared in $t$ and its sub-structures such as assignment or eval blocks. Algorithm \ref{algTranslateCompoundContent} first translates all default value expressions of all relevant slots and annotations (in annotation blocks), so that default values can be assigned before any further constraint of $t$ is evaluated. Then, for all refined but not excluded compound types, the algorithm first translates the constraints in the eval blocks meething the higher evaluation priority and, finally, the remaining constraints via recursion. + +% When translating the default value expression for slots, Algorithm \ref{algTranslateCompoundContent} calls Algorithm \ref{algTranslateDeclaration}, and, thus, triggers a potentially recursive translation along the respective slot types. Then, the algorithm translates all + +In Algorithm \ref{algTranslateCompoundContent}, the relevant slots are declared in $t$ and for which the containing type is not excluded. This is denoted by +% +$$slots^-(u) = \setWith{s}{s \in slots(u) \wedge \neg isTypeExcluded(\variableMapping, type(parent(s)))} $$ +% +In lines \ref{algTranslateCompoundDeclarationTranslateSlotsStart}-\ref{algTranslateCompoundDeclarationTranslateSlotsEnd}, Algorithm \ref{algTranslateCompoundContent} performs the translation of the default value expressions of all slots in $slots^-$. Here, we must distinguish two cases, namely whether the configuration variable $v$ is available or not\footref{fnVariableNull}. If $v$ is available (lines \ref{algTranslateCompoundDeclarationTranslateSlotsStart}-\ref{algTranslateCompoundDeclarationTranslateSlotsMid}), $slots^-(v)$ returns all slots in terms of nested (refined) variables, which are applied to Algorithm \ref{algTranslateDeclaration} in line \ref{algTranslateCompoundDeclarationTranslateSlotsV}. If $v$ is not available (lines \ref{algTranslateCompoundDeclarationTranslateSlotsMid}-\ref{algTranslateCompoundDeclarationTranslateSlotsEnd}), we use the type hierarchy as fallback, i.e., we translate constraints without knowledge about the actual type of the variables. In line \ref{algTranslateCompoundDeclarationTranslateSlotsT}, we call Algorithm \ref{algTranslateDeclaration} for a type-based transformation of the slot declaration $d$, i.e., without slot variable but with accessor expression for $s$ recorded in $\variableMapping$. + +Then we translate then the default values specified by nested annotation assignments in $t$ in line \ref{algTranslateCompoundDeclarationCompoundAssignments}. Akin to Algorithm \ref{algTranslateDeclaration}, translating these default values is not needed in incremental reasoning mode. \begin{algorithm}[H] @@ -232,5 +235,5 @@ \uIf{$v\neq\undef$}{\label{algTranslateCompoundDeclarationTranslateSlotsStart} \ForAll{$s \iterAssng slots^-(v)$} { - $translateDeclaration(s, decision(v, s), \variableMapping[s]))$\; \label{algTranslateCompoundDeclarationTranslateSlotsV} + $translateDeclaration(decl(s), s, \variableMapping[s]))$\; \label{algTranslateCompoundDeclarationTranslateSlotsV} } } \Else {\label{algTranslateCompoundDeclarationTranslateSlotsMid} @@ -244,24 +247,26 @@ } } - \leIf{$ca \neq \undef$}{$e_f\assng ca$}{$e_f\assng d$}\label{algTranslateCompoundDeclarationSelf} + \leIf{$ca \neq \undef$}{$f\assng ca$}{$f\assng \createExpression{d}$}\label{algTranslateCompoundDeclarationSelf} $t_r \assng allRefines^+(t) \text{ } \setminus \text{ } excludedTypes(t)$\;\label{algTranslateCompoundRefinedNotExcluded} % $t_c \assng currentType(\variableMapping)$\;\label{algTranslateCompoundCurrentType} % $eval \assng \setWithFlat{allEvalConstraints(r)}{r\in t_r}$\;\label{algTranslateCompoundDeclarationEvalStart} -% $add(\otherConstraints, \setWith{register(v, attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{e_f}}, t_c))}{c\in eval}, true, v)$\;\label{algTranslateCompoundDeclarationEvalEnd} - $translateCmp(\otherConstraints, v, e_f, \variableMapping, \setWithFlat{allEvalConstraints(r)}{r\in t_r})$\;\label{algTranslateCompoundDeclarationEval} +% $add(\otherConstraints, \setWith{register(v, attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}, t_c))}{c\in eval}, true, v)$\;\label{algTranslateCompoundDeclarationEvalEnd} + $translateCmp(\otherConstraints, v, f, \variableMapping, \setWithFlat{allEvalConstraints(r)}{r\in t_r})$\;\label{algTranslateCompoundDeclarationEval} % $cmp \assng \setWithFlat{allCmpConstraints(r)}{r\in t_r}$\;\label{algTranslateCompoundDeclarationAllStart} -% $add(\otherConstraints, \setWith{register(v, attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{e_f}}), t_c)}{c\in cmp}, true, v)$\;\label{algTranslateCompoundDeclarationAllEnd} - $translateCmp(\otherConstraints, v, e_f, \variableMapping, \setWithFlat{allCmpConstraints(r)}{r\in t_r})$\;\label{algTranslateCompoundDeclarationAll} +% $add(\otherConstraints, \setWith{register(v, attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}), t_c)}{c\in cmp}, true, v)$\;\label{algTranslateCompoundDeclarationAllEnd} + $translateCmp(\otherConstraints, v, f, \variableMapping, \setWithFlat{allCmpConstraints(r)}{r\in t_r})$\;\label{algTranslateCompoundDeclarationAll} \caption{Translating compound content (\IVML{translateCompoundContent}).}\label{algTranslateCompoundContent} \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 \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 +As preparation for subsequent variable substitutions, we determine in line \ref{algTranslateCompoundDeclarationSelf} the expression $f$ for \IVMLself{}, which is either the access expression $ca$ if given or the declaration $d$. The remaining translations are 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 \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. +be a function, which translates a given set of compound constraints $c_s$. At its core, $translateCmp$ substitutes the mappings in $\variableMapping$ as well as \IVMLself{} with $f$ for all given constraints and adds the substitution results to the given constraint sequence $c_t$. In addition, $translateCmp$ performs additional operations supporting fast re-scheduling, i.e., it attaches the resulting constraints to the type in the current stack frame and registers the resulting constraints with $v$ in $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$ (cf. Section \ref{sectConstraintBase}). + +Due to their specific evauation priority, we apply $translateCmp$ first to all eval constraints defined for $t_r$ in line \ref{algTranslateCompoundDeclarationEval} and add them to the other constraints sequence $\otherConstraints$. Finally, we translate all remaining compound constraints including 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 occur in mixed sequence and may accidentally overwrite each other. 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. These situations are implicitly handled by the main evaluation loop and 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. Otherwise the evaluation fails due to assignment conflicts, which is considered by the main evaluation loop in Algorithm \ref{algMainLoop}. Dependent default values are deferred by the constraint evaluation until all used variables and slots are defined. \subsection{Container types}\label{sectContainerDefaults} @@ -521,5 +526,5 @@ 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} +\subsection{Constraint base operations}\label{sectContainerBase}\label{sectConstraintBase} In this section, we discuss the support operations to create and maintain the constraint based, in particular the $add$ function\footnote{\IVML{addConstraint} in the implementation, in this document $add$ due to layout reasons.} and the $register$\footnote{\label{fnRegisterConstraint}\IVML{registerConstraint} in the implementation, akin to $add$ due to layout reasons.} function. We start with the $add$ function and continue with the $register$ function.