Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 149) +++ /reasoner/consTranslation.tex (revision 150) @@ -82,5 +82,5 @@ \grayPara{ \begin{gather*} - \patternDerivation{\IVML{typedef } t_i \IVML{ with }(c_i); T v\IVML{;}}{\bigcup_{t_i \in allBase(T)} \varSubstitution{c_i}{decl(t_i)=deref(t_i, v), \variableMapping}} + \patternDerivation{\IVML{typedef } t_i \IVML{ with }(c_i); T\ v\IVML{;}}{\bigcup_{t_i \in allBase(T)} \varSubstitution{c_i}{decl(t_i)=deref(t_i, v), \variableMapping}} \end{gather*} } @@ -114,16 +114,29 @@ \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 \IVML{\}; } C\ v \IVML{; } c(v.s)\IVML{;}}{\varSubstitution{c(v.s)}{\variableMapping}}\\ \end{gather*} } -The first pattern requires an 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. - -Annotation assignments are translated similarly, but require specific handling of default values as we will discuss in Section \ref{sectAnnotationDefaults}. Eval blocks are also translated similarly, but the resulting constraints require a higher constraint evaluation priority in the actual scope as we will detail below. 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. - -The second pattern transforms a top-level constraint defined over a compound variable $v$. Due to the mandatory use of only qualified slot access expressions in IVML, no translation is needed and such constraints are handled through line \ref{algTranslateConstraintsTopLevelConstraints} in Algorithm \ref{algTranslateConstraints}. - -We will now focus on the first pattern and discuss the respective translation Algorithm \ref{algTranslateCompoundDeclaration}. The idea is to visit all slots and constraints in the compound type and its refined compound types, first for creating the variable mapping (Algorithm \ref{algRegisterCompoundMapping}), then for translating all constraints (Algorithm \ref{algTranslateCompoundContent}). In some situations, both steps must be carried out individually instead of a fixed sequence, e.g., to perform the translation of potentially inter-dependent compound slot default values between both steps as discussed for Algorithm \ref{algTranslateDeclaration}. As compound slots are nested variable declarations, Algorithm \ref{algTranslateDeclaration} is responsible for translating slots and their annotations. Akin to Algorithm \ref{algTranslateDeclaration}, default values of annotations (here given in terms of annotation assignments) are only turned into assignment constraints if the reasoner is not in incremental mode. Finally, eval blocks (due to evaluation priority) and then directly nested constraints and constraints in assignment blocks of a compound and all refined compound types are translated. +The compound type translation must consider the following situations (discussed along the pattern sequence given above): + +\begin{enumerate} + + \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{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. + + \item \emph{Annotation assignments: } Also here the nesting becomes transparent and constraints are translated as if they were defined directly in the containing compound type, i.e., similar to the second pattern. However, annotation assignments require specific handling of default values to avoid accidental re-assignment of default values as we will discuss in Section \ref{sectAnnotationDefaults}. + + \item \emph{Top-level constraint defined over a compound variable $v$:} Due to the mandatory use of only qualified slot access expressions in IVML, no translation is needed and such constraints are handled through line \ref{algTranslateConstraintsTopLevelConstraints} in Algorithm \ref{algTranslateConstraints}. + +\end{enumerate} + +We will now focus on the second pattern and discuss the respective translation Algorithm \ref{algTranslateCompoundDeclaration}. The idea is to visit all slots and constraints in the compound type and its refined compound types, first for creating the variable mapping (Algorithm \ref{algRegisterCompoundMapping}), then for translating all constraints (Algorithm \ref{algTranslateCompoundContent}). In some situations, both steps must be carried out individually instead of a fixed sequence, e.g., to perform the translation of potentially inter-dependent compound slot default values between both steps as discussed for Algorithm \ref{algTranslateDeclaration}. As compound slots are nested variable declarations, Algorithm \ref{algTranslateDeclaration} is responsible for translating slots and their annotations. Akin to Algorithm \ref{algTranslateDeclaration}, default values of annotations (here given in terms of annotation assignments) are only turned into assignment constraints if the reasoner is not in incremental mode. Finally, eval blocks (due to evaluation priority) and then directly nested constraints and constraints in assignment blocks of a compound and all refined compound types are translated. \begin{algorithm}[H] @@ -136,5 +149,5 @@ \If{$m = REGISTER$}{ $pushContext(\variableMapping, d, v \neq \undef)$\; \label{algTranslateCompoundDeclarationPushContext} - $transferTypeExcludes(\variableMapping, t)$\; + $transferTypeExcludes(\variableMapping, t)$\;\label{algTranslateCompoundDeclarationTransfer} $registerCompoundMapping(t, ca, \createExpression{d})$\; $next \assng TRANSLATE$\; @@ -155,7 +168,7 @@ Algorithm \ref{algTranslateCompoundDeclaration} integrates the creation of the variable mapping, the constraint translation and the additional functionality for compound value changes controlled by the compound translation mode. Variable mapping and constraint translation are realized by separate algorithms (Algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent}, respectively) to enable their re-use when translating compound containers (cf. Section \ref{sectCompoundDefaults}). In more details, Algorithm \ref{algTranslateCompoundDeclaration} takes a compound variable $v$ of declaration $d$, an optional compound accessor $ca$, the actual type $t$ as well as the desired compound translation mode $m$ and returns the compound mode for a subsequent call of Algorithm \ref{algTranslateCompoundDeclaration}. A type $t$ is processed only if $t$ was not marked as already processed or, implicitly, recording of processed types is disabled (cf. Section \ref{sectVarMapping}). If a type shall not processed, the next compound mode is $NONE$, indicating that no context frame was created that needs to be popped during $TRANSLATE$. -If the variable mapping shall be registered for type $t$, Algorithm \ref{algTranslateCompoundDeclaration} pushes a new context frame for the compound type onto the variable mapping stack $\variableMapping$ (line \ref{algTranslateCompoundDeclarationPushContext}) and transfers potentially excluded (global) types (for faster processing of value type changes) into the actual frame. Then it registers all required compound mappings using Algorithm \ref{algRegisterCompoundMapping} (using a joint accessor expression to $d$ in case that $ca=\undef$). The next compound mode after a registration of variable mappings is $TRANSLATE$. - -If constraints shall be translated for type $t$, Algorithm \ref{algTranslateCompoundDeclaration} performs the translation through Algorithm \ref{algTranslateCompoundContent}, pops the previously created context, records $t$ as processed and returns that no further compound translation ($NONE$) is needed for $t$. +If the variable mapping shall be registered for type $t$, Algorithm \ref{algTranslateCompoundDeclaration} pushes a new context frame for the compound type onto the variable mapping stack $\variableMapping$ (line \ref{algTranslateCompoundDeclarationPushContext}). In line \ref{algTranslateCompoundDeclarationTransfer}, it modifies the actual context frame by enabling (transferring) excluded types (for faster re-scheduling) and storing $t$ as current type. Then it registers all required compound mappings using Algorithm \ref{algRegisterCompoundMapping} (using a joint accessor expression to $d$ in case that $ca=\undef$). The next compound mode after a registration of variable mappings is $TRANSLATE$. + +If constraints shall be translated, Algorithm \ref{algTranslateCompoundDeclaration} calls Algorithm \ref{algTranslateCompoundContent}, pops the previously created context, records $t$ as processed and returns that no further compound translation ($NONE$) is needed for $t$. We detail now the variable mapping for compounds. Algorithm \ref{algRegisterCompoundMapping} visits all slots and annotations of a given compound type $t$, creates access expressions for them and registers them with the current context frame in the variable mapping $\variableMapping$. The access expressions $ca$ is optional and, if given, utilized as prefix to create access expressions for slots and annotations. If $ca$ is not given, $e_d$ is used instead, usually containing an expression to the variable declaration using $t$. Algorithm \ref{algRegisterCompoundMapping} iterates over all slots accessible for the given compound type $t$ and creates for each slot a respective accessor. If the compound access expression $ca$ is not given, Algorithm \ref{algRegisterCompoundMapping} creates a static accessor based on $e_d$. The created accessor $x$ is then registered with $\variableMapping$. Similarly, we register accessors for annotations of the current slot $s$ based on the accessor $x$ for $s$. Finally, the algorithm creates accessors for all annotations declared for the underlying compound variable (through $e_d$). @@ -210,14 +223,21 @@ } \leIf{$ca \neq \undef$}{$e_f\assng ca$}{$e_f\assng d$}\label{algTranslateCompoundDeclarationSelf} - $t_r \assng allRefines^+(t) \text{ } \setminus \text{ } excludedTypes(t)$\; - $t_c \assng currentType(\variableMapping)$\; - $eval \assng \setWithFlat{allEvalConstraints(r)}{r\in t_r}$\;\label{algTranslateCompoundDeclarationEvalStart} - $add(\otherConstraints, \setWith{attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{e_f}}, t_c)}{c\in eval}, true, v)$\;\label{algTranslateCompoundDeclarationEvalEnd} - $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} + $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} +% $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} \caption{Translating compound content (\IVML{translateCompoundContent}).}\label{algTranslateCompoundContent} \end{algorithm} -Then, if we are not reasoning in incremental mode, we translate the default values specified by annotation assignments nested in $t$ in line \ref{algTranslateCompoundDeclarationCompoundAssignments}. In line \ref{algTranslateCompoundDeclarationSelf}, we determine the actual expression $e_f$ for \IVML{self}, i.e., either the access expression $ca$ if given or the declaration $d$. Then, due to their specific priorities, we first translate all eval constraints defined along the type hierarchy for $t$ in lines \ref{algTranslateCompoundDeclarationEvalStart}-\ref{algTranslateCompoundDeclarationEvalEnd}. Finally, we include all remaining compound constraints, i.e., type constraints and constraints in annotation assignments in lines \ref{algTranslateCompoundDeclarationAllStart}-\ref{algTranslateCompoundDeclarationAllEnd} and register them with the constraint variable for constraint-rescheduling (the $register$ operation returns the constraint passed in, cf. Algorithm \ref{algRegisterConstraint}). +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 +% +\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}. 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. @@ -509,4 +529,6 @@ \KwIn{constraint sequence $s$, constraint $c$, perform initializers $check$, variable $v$} \KwData{top level and other constraints $\topLevelConstraints, \otherConstraints$, variable mapping $\variableMapping$, relevant constraints $\relevantConstraintsPerDeclaration$ , incremental flag $inc$, evals flag $inEvals$} + \KwOut{$c$} + $c = composeExpression(\variableMapping, c)$\; \If{$check$}{ @@ -527,4 +549,6 @@ } } + \Return $c$\; + \caption{Adds a constraint to the constraint base ($add$).}\label{algAddConstraint} \end{algorithm} Index: /reasoner/reasoningAlg.tex =================================================================== --- /reasoner/reasoningAlg.tex (revision 149) +++ /reasoner/reasoningAlg.tex (revision 150) @@ -129,4 +129,14 @@ 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 @@ -165,5 +175,5 @@ }\label{algTranslateConstraintsBaseCopyEnd} $clear(\variableMapping)$\; \label{algTranslateConstraintsClearMapping} - \caption{Translating constraints (\IVML{translateConstraints}).}\label{algTranslateConstraints} + \caption{Constraint translation (\IVML{translateConstraints}).}\label{algTranslateConstraints} \end{algorithm}