Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 147) +++ /reasoner/consTranslation.tex (revision 148) @@ -66,5 +66,5 @@ \end{algorithm} -In line \ref{algTranslateDeclarationRefinedType}, the actual type of the variable is determined, either based on the declaration, the default value expression or the actual value if defined. If $t$ is a compound type, we set in line \ref{algTranslateDeclarationTranslateSelf1} the value of self $v$ to the actual variable declaration $d$ and create the variable mapping for all slots in line \ref{algTranslateDeclarationRegisterCompound} by calling Algorithm \ref{algTranslateCompoundDeclaration}. Typically, this creates a new context frame in the variable mapping $\variableMapping$, which must be correctly cleaned up at the end of Algorithm \ref{algTranslateDeclaration}. We indicate this by the compound mode $c_m$, which is adjusted here and considered in the translation call in line \ref{algTranslateDeclarationTranslateCompound}. +In line \ref{algTranslateDeclarationRefinedType}, the actual type of the variable is determined, either based actual value (if a variable\footnote{\label{fnVariableNull}When initializing a configuration or creating constraints from a constant complex value expression, variables may not already be in place in all cases.} and a value is given), default value expression (as a type approximation of a missing value) or the declaration. If $t$ is a compound type, we set in line \ref{algTranslateDeclarationTranslateSelf1} the value of self $v$ to the actual variable declaration $d$ and create the variable mapping for all slots in line \ref{algTranslateDeclarationRegisterCompound} by calling Algorithm \ref{algTranslateCompoundDeclaration}. Typically, this creates a new context frame in the variable mapping $\variableMapping$, which must be correctly cleaned up at the end of Algorithm \ref{algTranslateDeclaration}. We indicate this by the compound mode $c_m$, which is adjusted here and considered in the translation call in line \ref{algTranslateDeclarationTranslateCompound}. A remaining default value expression $e_d$ is turned into an assignment constraint if $d$ is not an attribute used within an assignment block (this may otherwise collide with default values defined by the assignment block). If the $v$ variable is a constraint variable, we also have to add $e_d$ to the constraint base. This is done by calling Algorithm \ref{algCreateConstraintVariableConstraint} (cf. Section \ref{sectConstraintVariables}). Then, we turn the default value expression into an assignment expression. However, the creation of the sub-expression $ac$ representing the variable $v$ technically depends on whether $d$ is a (nested) annotation or 'ordinary' variable (lines \ref{algTranslateDeclarationCreateACStart}-\ref{algTranslateDeclarationCreateACEnd}). Further, we must determine the constraint set for adding the assignment constraint (line \ref{algTranslateDeclarationTranslateSelf3}): We add the constraint to $\deferredDefaultConstraints$ if the assignment may override a previous value assignment through a complex value. This is (potentially) the case if \IVML{self} is used in $e_d$ or if $d$ is an overridden slot that may be overriden accidentally by a complex compound value. Else, we add the constraint to the set of default constraints $\defaultConstraints$. Ultimately, we create an expression assigning $e_d$ to $ac$, substitute \IVML{self} and the actual variable mapping in this assignment expression, turn the result into a default constraint and add it to the respective constraint set in line \ref{algTranslateDeclarationTranslateDefault}. @@ -127,6 +127,4 @@ 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. -If the value of a compound variable changes during reasoning, the value type may also change along the compound refinement hierarchy. Although constraint re-scheduling will be discussed in Section \ref{sectTopLevelConstraintsRescheduling}, we consider this topic already here to present a complete translation algorithm for compund types instead of refining the algorithm later in Section \ref{sectTopLevelConstraintsRescheduling}. Changing value types require adjusting the constraint base, i.e., more or less constraints must be considered dynamically while reasoning. However, when the actual type of a compound variable changes, executing the full constraint transformation for the new type is possible, but inefficent as already known constraints are added again to the constraint base. Moreover, constraints that are still in the constraint base, as they were not evaluated or not fulfilled so far, are duplicated and may cause multiple error messages for the same violation. Thus, it is desirable to transform just the differences between the involved types, i.e., to translate the constraints for all types in the refinement hierarchy between old and new value type. This requires knowledge about already processed types, type exclusion, as well as conditional creation and release of variable mapping context frames. We represent the conditional handling of context frames in terms of the compound translation mode already mentioned for Algorithm \ref{algTranslateDeclaration}, i.e., by constants that indicate to $REGISTER$ the variable mapping, to $TRANSLATE$ the constraints and $NONE$ for no operation (type is known or excluded and shall not be mapped or transformed). - \begin{algorithm}[H] \SetAlgoLined @@ -153,4 +151,6 @@ \end{algorithm} +If the value of a compound variable changes during reasoning, the value type may also change along the compound refinement hierarchy. Although constraint re-scheduling will be discussed in Section \ref{sectTopLevelConstraintsRescheduling}, we consider this topic already here to present a complete translation algorithm for compund types instead of refining the algorithm later in Section \ref{sectTopLevelConstraintsRescheduling}. Changing value types require adjusting the constraint base, i.e., more or less constraints must be considered dynamically while reasoning. However, when the actual type of a compound variable changes, executing the full constraint transformation for the new type is possible, but inefficent as already known constraints are added again to the constraint base. Moreover, constraints that are still in the constraint base, as they were not evaluated or not fulfilled so far, are duplicated and may cause multiple error messages for the same violation. Thus, it is desirable to transform just the differences between the involved types, i.e., to translate the constraints for all types in the refinement hierarchy between old and new value type. This requires knowledge about already processed types, type exclusion, as well as conditional creation and release of variable mapping context frames. We represent the conditional handling of context frames in terms of the compound translation mode already mentioned for Algorithm \ref{algTranslateDeclaration}, i.e., by constants that indicate to $REGISTER$ the variable mapping, to $TRANSLATE$ the constraints and $NONE$ for no operation (type is known or excluded and shall not be mapped or transformed). + 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$. @@ -160,4 +160,6 @@ 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$). + +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. \begin{algorithm}[H] @@ -181,13 +183,13 @@ \end{algorithm} -Given a complete mapping for a compound type, we can apply Algorithm \ref{algTranslateCompoundContent}. The algorithm performs a transitive / recursive translation of the default values of all (not excluded) slots using the respective accessor calling Algorithm \ref{algTranslateDeclaration} in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} if $v$ is defined ($slots(v)$ also includes all slots for $v$\footnote{This also holds for $slots^-(v)$ if the parent type of $v$ is not excluded.}) or all 8not excluded) slots for type$t$. It is important to note that in both cases, the second occurs in container translations, we call Algorithm \ref{algTranslateDeclaration}, which dispatches for all types and also considers annotations. - -In line \ref{algTranslateCompoundDeclarationSelf}, we determine the actual expression for self, i.e., 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}. Afterwards, we include all remaining compound constraints, i.e., type constraints and annotation constraints in lines \ref{algTranslateCompoundDeclarationAllStart}-\ref{algTranslateCompoundDeclarationAllEnd}. - 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$. +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$. + +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}. Afterwards, we include all remaining compound constraints, i.e., type constraints and annotation constraints in lines \ref{algTranslateCompoundDeclarationAllStart}-\ref{algTranslateCompoundDeclarationAllEnd}. + \begin{algorithm}[H] @@ -200,5 +202,5 @@ $translateDeclaration(s, decision(v, s), \variableMapping[s]))$\; \label{algTranslateCompoundDeclarationTranslateSlotsV} } - } \Else { + } \Else {\label{algTranslateCompoundDeclarationTranslateSlotsMid} \ForAll{$s \iterAssng \setWithFlat{slots^-(u)}{u\in allRefines^+(t)}$ } { $translateDeclaration(s, \undef, \variableMapping[s]))$\; \label{algTranslateCompoundDeclarationTranslateSlotsT} @@ -210,10 +212,10 @@ } } - \leIf{$ca \neq \undef$}{$f\assng ca$}{$f\assng d$}\label{algTranslateCompoundDeclarationSelf} + \leIf{$ca \neq \undef$}{$e_f\assng ca$}{$e_f\assng d$}\label{algTranslateCompoundDeclarationSelf} \MISSING{Register constraints for creating compound constraints (value is constraint value) }\; $eval \assng \setWithFlat{allEvalConstraints(r)}{r\in allRefines^+(t) \text{ } \setminus \text{ } excludedTypes(t)}$\;\label{algTranslateCompoundDeclarationEvalStart} - $add(\otherConstraints, \setWith{attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}, currentType(\variableMapping))}{c\in eval}, true, v)$\;\label{algTranslateCompoundDeclarationEvalEnd} + $add(\otherConstraints, \setWith{attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{e_f}}, currentType(\variableMapping))}{c\in eval}, true, v)$\;\label{algTranslateCompoundDeclarationEvalEnd} $cmp \assng \setWithFlat{allCompoundConstraints(r)}{r\in allRefines^+(t) \text{ } \setminus \text{ } excludedTypes(t)}$\;\label{algTranslateCompoundDeclarationAllStart} - $add(\otherConstraints, \setWith{attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{f}}, currentType(\variableMapping))}{c\in cmp}, true, v)$\;\label{algTranslateCompoundDeclarationAllEnd} + $add(\otherConstraints, \setWith{attach(\createConstraint{\varSubstitutionSelfVarMapping{c}{e_f}}, currentType(\variableMapping))}{c\in cmp}, true, v)$\;\label{algTranslateCompoundDeclarationAllEnd} \caption{Translating compound content (\IVML{translateCompoundContent}).}\label{algTranslateCompoundContent} Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 147) +++ /reasoner/reasoner.tex (revision 148) @@ -12,4 +12,5 @@ \usepackage{adjustbox} \usepackage{float} +\usepackage{footmisc} \newcommand\TBD[1]{{\color{blue}TBD: #1}} Index: /reasoner/reasoningAlg.tex =================================================================== --- /reasoner/reasoningAlg.tex (revision 147) +++ /reasoner/reasoningAlg.tex (revision 148) @@ -95,5 +95,5 @@ \item $popContext(\variableMapping)$ removes the top-most context frame. The initial frame, which is created by default and devoted to the enclosing IVML project, is not removed by this operation. \item $registerMapping(\variableMapping, d, ca)$ registers the access expression $ca$ with the given variable declaration $d$ in the top-most context frame. Essentially, a context frame contains a mapping $m$ and the operation performs $m \assng m \addMap \mapEntry{d}{ca}$. - \item $getMapping(\variableMapping, d)$ returns the mapping for $d$. If no mapping was registered for the actual context frame, all context frames in stack order are considered. If no mapping is registered, the result is $\undef$. + \item $getMapping(\variableMapping, d)$ returns the mapping for $d$ (for short $\variableMapping[d]$). If no mapping was registered for the actual context frame, all context frames in stack order are considered. If no mapping is registered, the result is $\undef$. \item $recordProcessed(\variableMapping, t)$ records a processed type with the closest containing context having processed type registration enabled. If \linebreak[4] $isCompound(t)$, this function registers $allRefined^+(t)$. \item $alreadyProcessed(\variableMapping, t)$ returns whether $t$ was already registered as a processed type in one of the enclosing context frames.