Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 217) +++ /reasoner/consTranslation.tex (revision 218) @@ -24,5 +24,5 @@ In Algorithm \ref{algTranslateDeclaration}, we apply the translation patterns above: Let $v$ be a variable with default value expression $deflt$. Pattern \ref{forVarDecl} turns $deflt$ into an assignment constraint. If $v$ is nested in a compound or a sequence, a qualified access expression for $v$ is required in the resulting constraint. We indicate this in terms of the $access(e)$ function on the right side. $access(e)$ returns $e$ if $e$ is already (an accessor expression based on) a top-level variable. $access(e)$ turns $e$ into an accessor (path) expression based on a respective top-level variable. Pattern \ref{forVarDeclAnnotation} targets annotations. As introduced in Section \ref{sectNotationVarDecls}, annotations are variables denoting an orthogonal configuration dimension of 'ordinary' variables. Thus, an annotation $a$ is translated in the context of the underlying 'ordinary' variable named $v$ in the pattern, i.e., requires a qualification based on $v$. In Algorithm \ref{algTranslateDeclaration}, we will focus on the first transformation pattern. As stated above, we will defer more complex translations to later sections, e.g., annotations to Section \ref{sectAnnotationDefaults}, as these algorithms can then re-use the more generic translation of variables discussed here. -Algorithm \ref{algTranslateDeclaration} translates all constraints related to a given variable declaration $d$ and its configuration variable $v$, which may be $\undef$ for type-only translations\footnote{\label{fnVariableNull}When initializing a configuration or creating constraints from a complex constant value expression, variables may not already be in place in all cases.}. Default value assignment constraints created in Algorithm \ref{algTranslateDeclaration} are stored either in the global set for default constraints $\defaultConstraints$ or the set for deferred default constraints $\deferredDefaultConstraints$. As the type of $v$ may be a complex type such as a compound, Algorithm \ref{algTranslateDeclaration} delegates these translations to more specialized algorithms, which use Algorithm \ref{algTranslateDeclaration} recursively. As thereby the translation context changes, the involved algorithms incrementally adjust the access expression $ca$ and the variable mapping $\variableMapping$. +Algorithm \ref{algTranslateDeclaration} translates all constraints related to a given variable declaration $d$ and its configuration variable $v$, which may be $\undef$ for type-based translations\footnote{\label{fnVariableNull}When initializing a configuration or creating constraints from a complex constant value expression, variables may not already be in place in all cases.}. Default value assignment constraints created in Algorithm \ref{algTranslateDeclaration} are stored either in the global set for default constraints $\defaultConstraints$ or the set for deferred default constraints $\deferredDefaultConstraints$. As the type of $v$ may be a complex type such as a compound, Algorithm \ref{algTranslateDeclaration} delegates these translations to more specialized algorithms, which use Algorithm \ref{algTranslateDeclaration} recursively. As thereby the translation context changes, the involved algorithms incrementally adjust the access expression $ca$ and the variable mapping $\variableMapping$. \begin{algorithm}[H] @@ -172,5 +172,5 @@ Algorithm \ref{algTranslateCompoundDeclaration} is the main entry point into the constraint translation for compound types. The algorithm supports the two phases mentioned above, namely 1) the creation the variable mapping for a compound as well as 2) translating the constraints in the compound based on the variable mapping. Typically, these two phases are executed in immediate sequence, i.e., no distinct phases would be needed. However, in some situations, such as in Algorithm \ref{algTranslateDeclaration}, further translations must be performed in between. The compound mode indicates the phase to be executed, i.e., $REGISTER$ for the first phase and $TRANSLATE$ for the second phase. Further, in constraint re-scheduling, some compound types may be excluded from translation to speed up reasoning, i.e., for a certain type, no context frame is created in the first phase and also no context frame shall be released in the second phase. For convenience, Algorithm \ref{algTranslateCompoundDeclaration} integrates the two phases with the type exclusion and the conditional cleanup. The phases are realized by subsequent algorithms (Algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent}, respectively) to enable their re-use for the translation of compound containers (cf. Section \ref{sectCompoundDefaults}). -In more details, Algorithm \ref{algTranslateCompoundDeclaration} takes a compound variable $v$ of declaration $d$ ($v$ may be $\undef$ for type-only translations\footref{fnVariableNull}), an optional compound accessor $ca$, the actual (compound) type $t$ as well as the desired compound translation $mode$. The algorithm returns the follow-up compound mode for the second phase. In both phases, compound type $t$ is processed only if $t$ was not marked before as processed or excluded. If $t$ shall not be processed, the resulting follow-up compound mode is $NONE$, indicating that $TRANSLATE$ shall not be executed, i.e., also no context frame cleanup shall happen. +In more details, Algorithm \ref{algTranslateCompoundDeclaration} takes a compound variable $v$ of declaration $d$ ($v$ may be $\undef$ for type-based translations\footref{fnVariableNull}), an optional compound accessor $ca$, the actual (compound) type $t$ as well as the desired compound translation $mode$. The algorithm returns the follow-up compound mode for the second phase. In both phases, compound type $t$ is processed only if $t$ was not marked before as processed or excluded. If $t$ shall not be processed, the resulting follow-up compound mode is $NONE$, indicating that $TRANSLATE$ shall not be executed, i.e., also no context frame cleanup shall happen. In $REGISTER$ mode, i.e., the variable mapping shall be created for compound type $t$, Algorithm \ref{algTranslateCompoundDeclaration} pushes a new context frame onto the variable mapping stack $\variableMapping$ (line \ref{algTranslateCompoundDeclarationPushContext}). In line \ref{algTranslateCompoundDeclarationTransfer}, the algorithm transferring excluded types into the actual context frame (cf. Section \ref{sectVarMapping}). Then the algorithm registers all required compound mappings by calling Algorithm \ref{algRegisterCompoundMapping} using as accessor expression either $ca$ if given or $\createExpression{d}$. The follow-up compound mode after a creation of variable mappings is $TRANSLATE$. @@ -491,5 +491,5 @@ \end{algorithm} -First, Algorithm \ref{algTranslateAnnotationDeclarations} determines in line \ref{algTranslateAnnotationDeclarationsCa} the accessor expression, i.e., either $ca$ if given (e.g., as $d$ is nested such as a compound slot) or $d$. The further translation depends on whether variable $v$ including actual value / type is available (lines \ref{algTranslateAnnotationDeclarationsTranslateVStart}-\ref{algTranslateAnnotationDeclarationsTranslateVEnd}) or we have to resort to a type-only translation\footref{fnVariableNull} based on nested declarations of $d$ (lines \ref{algTranslateAnnotationDeclarationsTranslateDStart}-\ref{algTranslateAnnotationDeclarationsTranslateDEnd}). In both cases, Algorithm \ref{algTranslateDeclaration} is called on the respective annotation declaration, annotation variable (if available) and accessor expression. The accessor expression is created by: +First, Algorithm \ref{algTranslateAnnotationDeclarations} determines in line \ref{algTranslateAnnotationDeclarationsCa} the accessor expression, i.e., either $ca$ if given (e.g., as $d$ is nested such as a compound slot) or $d$. The further translation depends on whether variable $v$ including actual value / type is available (lines \ref{algTranslateAnnotationDeclarationsTranslateVStart}-\ref{algTranslateAnnotationDeclarationsTranslateVEnd}) or we have to resort to a type-based translation\footref{fnVariableNull} based on nested declarations of $d$ (lines \ref{algTranslateAnnotationDeclarationsTranslateDStart}-\ref{algTranslateAnnotationDeclarationsTranslateDEnd}). In both cases, Algorithm \ref{algTranslateDeclaration} is called on the respective annotation declaration, annotation variable (if available) and accessor expression. The accessor expression is created by: % \begin{align*} @@ -513,11 +513,11 @@ \ForAll{$d \iterAssng decls(a)$} {\label{algTranslateAnnotationAssignmentsLoopStart} $a_d\assng ea[name(d)]$\; \label{algTranslateAnnotationAssignmentsObtainEA} - $x\assng translateAnnotationAssignment(a_d, d, ca, \variableMapping)$\; - $add(\otherConstraints, \set{x}, false, \undef)$\; \label{algTranslateAnnotationAssignmentsTranslateBasic} + $x\assng translateAnnotationAssignment(a_d, d, ca, \variableMapping)$\; \label{algTranslateAnnotationAssignmentsTranslateBasic} + $add(\otherConstraints, \set{x}, false, \undef)$\; \label{algTranslateAnnotationAssignmentsAdd} $t \assng type(d)$\; \If{$isCompound(t)$} {\label{algTranslateAnnotationAssignmentsIsCompoundStart} \If{$v \neq \undef$}{ \label{algTranslateAnnotationAssignmentsActTypeStart} $w \assng nested^*(v, name(d))$\; - \uIf{$n \neq \undef \wedge\text{ } value(w) \neq \undef$} { + \uIf{$w \neq \undef \wedge\text{ } value(w) \neq \undef$} { $t \assng type(value(w))$\; } @@ -543,15 +543,20 @@ \end{algorithm} -In line \ref{algTranslateAnnotationAssignmentsUpdateEA}, Algorithm \ref{algTranslateAnnotationAssignments} updates the effective assignments $ea$ by adding all assignment data objects defined by the actual annotation assignment $a$. For a given annotation assignment block $a$, the algorithm processes all declared variables (lines \ref{algTranslateAnnotationAssignmentsLoopStart}-\ref{algTranslateAnnotationAssignmentsLoopEnd}). For each variable, the algorithm obtains the effective assignment data $a_d$ in line \ref{algTranslateAnnotationAssignmentsObtainEA}, creates the default value assignment constraint and adds it to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsTranslateBasic}. If the declared variable is of compound type (lines \ref{algTranslateAnnotationAssignmentsIsCompoundStart}-\ref{algTranslateAnnotationAssignmentsIsCompoundEnd}), we also must consider the compound slots. Therefore, the algorithm determines in lines \ref{algTranslateAnnotationAssignmentsActTypeStart}-\ref{algTranslateAnnotationAssignmentsActTypeEnd} the actual type of the declared variable $d$, which may differ from the declared type for annotations of compound type due to type refinement. In line \ref{algTranslateAnnotationAssignmentsAccess}, the algorithm determines the access expression $ac$ to the declared compound variable $d$, which may either be $ca.d$ if $ca$ is given, $v.d$ if $v$ is given or, as fallback, just $d$. Now, the algorithm can iterate over all slots of the compound annotation (lines \ref{algTranslateAnnotationAssignmentsSlotsStart}-\ref{algTranslateAnnotationAssignmentsSlotsEnd}), create an access expression for each slot in line \ref{algTranslateAnnotationAssignmentsSlotAccess}, i.e., $ac.s$, create the assignment constraint in line \ref{algTranslateAnnotationAssignmentsSlotConstraint} and add the resulting constraint to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsSlotConstraintAdd}. Finally, the algorithm recursively processes the nested annotation assignments in lines \ref{algTranslateAnnotationAssignmentsNestedStart}-\ref{algTranslateAnnotationAssignmentsNestedEnd} by calling Algorithm \ref{algTranslateAnnotationAssignments} recursively. - -In lines \ref{algTranslateAnnotationAssignmentsTranslateBasic} and \ref{algTranslateAnnotationAssignmentsSlotConstraint}, Algorithm \ref{algTranslateAnnotationAssignments} relies on the translation of an individual assignment data object. The translation of a single assignment from an assignment data object $a$ leads to the creation of an assignment constraint as shown below. +In line \ref{algTranslateAnnotationAssignmentsUpdateEA}, Algorithm \ref{algTranslateAnnotationAssignments} updates the effective assignments $ea$ by adding mappings for all assignments, i.e., annotation name to data object, defined by the actual annotation assignment $a$. Then, the algorithm processes all variables declared declared in $a$ (lines \ref{algTranslateAnnotationAssignmentsLoopStart}-\ref{algTranslateAnnotationAssignmentsLoopEnd}). For each variable, the algorithm obtains the effective assignment data $a_d$ in line \ref{algTranslateAnnotationAssignmentsObtainEA}, creates the default value assignment constraint in line \ref{algTranslateAnnotationAssignmentsTranslateBasic} and adds it to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsAdd}. If the declared variable is of compound type (lines \ref{algTranslateAnnotationAssignmentsIsCompoundStart}-\ref{algTranslateAnnotationAssignmentsIsCompoundEnd}), we must also translate the annotations of the compound slots. Direct recursion is not needed, as this will happen through Algorithm \ref{algTranslateDeclaration}. Therefore, the algorithm determines in lines \ref{algTranslateAnnotationAssignmentsActTypeStart}-\ref{algTranslateAnnotationAssignmentsActTypeEnd} the actual type of $d$, which may differ from the declared type for annotations of compound type due to compound refinement. In line \ref{algTranslateAnnotationAssignmentsAccess}, the algorithm determines the access expression $ac$ for $d$, which may either be based on the nesting path of the accessor $ca.d$ if $ca$ is given, $v.d$ if $v$ is available or, in type-based translations, just $d$. Now, the algorithm can iterate over all slots of the compound annotation (lines \ref{algTranslateAnnotationAssignmentsSlotsStart}-\ref{algTranslateAnnotationAssignmentsSlotsEnd}), create the respective access expression $ac.s$ in line \ref{algTranslateAnnotationAssignmentsSlotAccess}, create the assignment constraint in line \ref{algTranslateAnnotationAssignmentsSlotConstraint} and add the resulting constraint to $\otherConstraints$ in line \ref{algTranslateAnnotationAssignmentsSlotConstraintAdd}. Finally, the algorithm processes the nested annotation assignments in lines \ref{algTranslateAnnotationAssignmentsNestedStart}-\ref{algTranslateAnnotationAssignmentsNestedEnd} by calling Algorithm \ref{algTranslateAnnotationAssignments} recursively. + +In lines \ref{algTranslateAnnotationAssignmentsTranslateBasic} and \ref{algTranslateAnnotationAssignmentsSlotConstraint}, Algorithm \ref{algTranslateAnnotationAssignments} relies on the translation of an individual assignment data object. The translation of an assignment data object $a_d$ (in the context of declaration $d$, its accessor expression $ca$ and variable mapping $\variableMapping$) leads to the creation of an assignment constraint as shown below: \begin{align*} - translate&AnnotationAssignment(a, d, ca, \variableMapping) = \\ - \createConstraint{\varSubstitutionSelfVarMapping{\IVML{assign}&(\IVMLMeta{ann}(\closedCases{ca, & \text{if } ca \neq \undef\\ d, & \text{if } ca = \undef \wedge \text{ }vm[d] = \undef \\ vm[d] &\text{else}}, \\ - &findAnnotation(d, name(a))), default(a))}{ca}} + translate&AnnotationAssignment(a_d, d, ca, \variableMapping) = \\ + \createConstraint{\varSubstitutionSelfVarMapping{ + \IVMLassign{\\ + \IVMLacc + {&\closedCases{ca, & \text{if } ca \neq \undef\\ d, & \text{if } ca = \undef \wedge \text{ }vm[d] = \undef \\ vm[d] &\text{else}}} + { findAnnotation(d, name(a_d))} + }{\\&default(a_d)}} + {ca}} \end{align*} -If a compound accessor $ca$ is given, the annotation is accessed through $ca$. If no accessor is given and the declaration $d$ is not in the variable mapping $\variableMapping$, $d$ is taken as basic accessor expression, else the actual expression in $\variableMapping$. The access expression is completed by, the annotation declaration retrieved from the underlying variable declaration $d$. Ultimately, the accessor is used as left side of an IVML assignment operation, the right side (value) is made up of the default value expression given by the assignment data $a$ after an appropriate variable substitution. +As usual, the left side of the assignment constraint is an accessor expression, here for an annotation of $d$ denoted by $a_d$. The default value of the annotation is given in terms of $a_d$. If a compound accessor expression $ca$ is given, the annotation $name(a_d)$ in the context of $d$ is accessed through $ca$ as the nesting takes precedence. If no accessor is given, there might be an accessor expression for $d$ in $\variableMapping$, i.e., we either take $vm[d]$ or, as fallback for type-based translations, $d$ as accessor. The annotation variable used as second argument of the accessor expression is retrieved from the underlying variable declaration $d$ using the function $findAnnotation$ (cf. Section \ref{sectNotationProject}). Ultimately, the accessor is used as left side of an IVML assignment operation, while the right side (value) is determined by default value expression specified by the assignment data $a$ after an appropriate variable substitution. Here, $ca$ for \IVMLself{} is sufficient as \IVMLself{} can only be used in (nested) compounds, where $ca$ is always known. \subsection{Constraint variables}\label{sectConstraintVariables}