Index: /reasoner/approach.tex =================================================================== --- /reasoner/approach.tex (revision 167) +++ /reasoner/approach.tex (revision 168) @@ -9,5 +9,5 @@ It is important to notice that IVML~\cite{IVML-LS} supports declarative specification of constraints, i.e., modeling concepts and constraints can be specified regardless of their actual evaluation sequence. To ensure that values for variables are uniquely determined, in particular in presence of default values, IVML allows changing the value of a variable only once within a project scope. Otherwise the reasoning mechanism must issue an error. Thus, reasoning must happen project-wise, in a depth-first traversal along the project import dependencies. Moreover, to speed up reasoning in specific situations, some form of sequence of the constraints can be indicated through the concept of partial evaluations, i.e., eval-blocks stated within a project or a compound. An eval-block consists of constraints or nested eval-blocks, while nested eval-blocks implicitly define an evaluation sequence. In other words, a project is the outermost (implicit) eval-block and nested eval-blocks shall be evaluated in their nesting sequence, while eval-blocks on the same nesting level do not imply any evaluation sequence. -However, not all IVML constraints can be directly used for reasoning. This is in particular true for constraints defined in compound types, i.e., these constraints must hold for all instances, or, indirectly, through types used within collections, i.e., these constraints must hold for the respective collection elements. Such constraints typically utilize local variables defined within the compound including the special pre-defined variable \IVML{self} pointing to the actual compound instance. Allowing such implicit constraints rather than requiring that all constraints are defined directly on the configuration variables increases consistency and helps reducing model sizes and complexity. +However, not all IVML constraints can be directly used for reasoning. This is in particular true for constraints defined in compound types, i.e., these constraints must hold for all instances, or, indirectly, through types used within collections, i.e., these constraints must hold for the respective collection elements. Such constraints typically utilize local variables defined within the compound including the special pre-defined variable \IVMLself{} pointing to the actual compound instance. Allowing such implicit constraints rather than requiring that all constraints are defined directly on the configuration variables increases consistency and helps reducing model sizes and complexity. %Cross-references to other types are required to be specified through an explicit accessor, i.e., an expression mentioning the variable and the respective nested variable(s). As a consequence, the reasoning mechanism must relate type-based constraints to the correct underlying configuration variables. In our approach, we perform first a \emph{constraint translation} to instantiate the constraints for configuration variables based on the actual type of the variable or its value. An alternative could be reasoning over type constraints and modifying the mapping to the variables on demand before evaluation. This may save memory and runtime (required for constraint translation / creation), but, however, also increases the complexity of managing the actual constraints to be evaluated. Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 167) +++ /reasoner/consTranslation.tex (revision 168) @@ -29,4 +29,6 @@ In the first part, Algorithm \ref{algTranslateDeclaration} first declares some local variables in line \ref{algTranslateDeclarationDecl}, including the default value expression $e_d$ (ignored in incremental mode), the actual value of self $f$ (for compound types only, overridden in line \ref{algTranslateDeclarationTranslateSelf1}) and the compound translation mode ($c_m$, overridden in line \ref{algTranslateDeclarationRegisterCompound} for use 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}. \begin{algorithm}[H] @@ -66,6 +68,4 @@ \end{algorithm} -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 \IVMLself{} 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 \IVMLself{} 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}. @@ -139,4 +139,6 @@ 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. + +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] @@ -163,6 +165,4 @@ \caption{Translating compound declarations (\IVML{translateCompoundDeclaration}).}\label{algTranslateCompoundDeclaration} \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$. Index: /reasoner/notation.tex =================================================================== --- /reasoner/notation.tex (revision 167) +++ /reasoner/notation.tex (revision 168) @@ -216,5 +216,7 @@ \emph{Accessors} to compound variables define a path to access a certain slot within a compound variable, i.e., an accessor specifies the variable and the slot / nested slot path to access. Let \IVML{cmp} be an IVML variable of compound type, then an accessor to slot \IVML{slot} defined in \IVML{cmp} looks in IVML notation like \IVML{cmp.slot}. If \IVML{slot} is in turn of compound type, also nested accessors may occur, e.g., \IVML{cmp.slot1.slot2}. For creating such expressions in the constraint translation, we use the IVML access constructor \IVML{acc}. Then, following the expression creation notation from Section \ref{sectNotationConstraints}, creating the first accessor expression can be expressed by $\createExpression{\IVMLMeta{acc}\IVML{(cmp, slot)}}$, while for the second accessor we use $\createExpression{\IVMLMeta{acc}(\IVMLMeta{acc}(\IVML{cmp}, \IVML{slot}),\IVML{slot2})}$. Let $ce$ be an accessor expression, then $compound(e)$ returns the part referring to the compound if $e$ is a compound accessor, $\undef$ else. -The value of a compound variable can be defined, e.g., as a default value expression or as an assignment constraint, using a complex value expression, a so called \emph{compound initializer}, essentially a name-value mapping. As slots can be in turn of a complex type, e.g., of a compound type, a compound initializer can also contain nested complex values, e.g., nested compound initializers. +The value of a compound variable can be defined using a complex value expression, a so called \emph{compound initializer}, essentially a name-value mapping. As slots can be, in turn, of a complex type, e.g., of a compound type, a compound initializer can also contain nested complex values, e.g., nested compound initializers. + +Within a compound type, \IVMLself{} is a specific pre-defined value, which represents the actual instance of the compound. Thus, \IVMLself{} is only defined in the context of concrete compound values. As a compound initializer represents a compound value, \IVMLself{} can be used in expressions within a compound initializer, sometimes without direct relation to the underlying compound variable. \IVMLself{} can be evaluated in two different ways: 1) The reasoner tells the expression evaluator for each constraint the actual value of \IVMLself{} or 2) the constraint translation substitutes \IVMLself{} with a respective compound accessor. Typically, we rely on the constraint translation as this avoids managing a context for each constraint. However, when evaluating a (nested) compound initializer, defining a substitution is not obvious, also as the top-level (compound) variable is not always directly available, e.g., as it is determined as part of an expression. In this situation, the expression evaluator can track the actual access path more easily, i.e., while in general, the SSE reasoner relies on constraint translation, in specific situations we delegate the evaluation of \IVMLself{} to underlying mechanisms such as the constraint evaluation. \subsubsection{Containers}\label{sectNotationContainers}