Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 50) +++ /reasoner/reasoner.tex (revision 51) @@ -400,17 +400,15 @@ \section{Constraint translation}\label{sectTranslation} -IVML allows defining default value expressions for all variables including top-level project variables as well as compound slots. From the perspective of IVML and its object model, a default value is part of a variable declaration, i.e., per se not a constraint, i.e., the syntax - -\texttt{Type variable = expression;} - -must be translated into a constraint $variable = expression$. Thereby, constraints defined over the type of the variable, e.g., in case of a derived type must be instantiated for the respective variable. - -The top-level transformation is called by Algorithm \ref{algMainLoop}. It considers all variable declarations and constraints in the given project and executes the following algorithms. - -The constraint translation composes the individual constraint sets into the constraint base and translates missing non-default constraints. This is summarized in Algorithm \ref{algTranslateConstraints}. Here, also the incremental reasoning mode is realized assuming that for incremental reasoning first a full reasoning on the same configuration took place, i.e., possible and propagated values are assigned and variables are frozen. Then, in incremental (runtime) reasoning, just changes on the remaining variables can be validated and respective propagations can be performed. - -First, the various constraint sets are composed starting with default constraints ($\defaultConstraints$) adding then the remaining constraints. After transferring the - - +The constraint translation analyzes constraints defined for a given IVML model, identifies those ones that must be instantiated, i.e., turned from constraints on types to constraints on variables, and performs this translation to fill the constraint base. Therefore, we consider three main types of constraints: + +\begin{enumerate} + \item Explicit \emph{top-level constraints} written by the domain expert, which are already using qualified variables. This group of constraints includes also constraints in top-level (nested) eval blocks as well as constraints in top-level annotation assignment blocks. Top-level constraints, eval-block constraints and annotation assignment constraints are ready for reasoning, do not need further translation and can directly be taken over into the constraint base (Algorithm \ref{algTranslateConstraints}, lines \ref{algTranslateConstraintsAdd} - \ref{algTranslateConstraintsTopLevelEvals}). As annotation assignments typically also include variable declarations, we enumerate them through a specific algorithm, which is also used for translating annotation assignments in compound types. However, we pass here parameters that focus on enumerating and adding rather than translating the related constraints. + \item \emph{Constraints introduced through variable types}, e.g., compound types. These constraints must be instantiated through translation, i.e., use of type level variables and slots must be rewritten to use actual variables and slots. Here, we start from top-level variable variables and perform a transitive instantiation based on the respective type of the variable. Where possible, it is important to consider the actual type of the value of the individual variables, as through type compatibility of refined types, the actual value type may be more specific that the declared type of the variable. This is initiated in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}. + \item \emph{Constraints for default values}. To achieve uniformity of the constraint evaluation and variable update process (cf. Section \ref{sectReasoning}), we (currently) translate default value assignments to assignment constraints. In more detail, the IVML declaration \IVML{Type v = ex;} must be translated into a constraint $\createConstraint{v = ex}$. We add these assignment constraints to the constraint base with higher priority than other constraints to ensure that default values are assigned first. Here, we must consider that default value assignments can change the actual value type implying that a refined set of constraints must be evaluated on the respective variable. Moreover, default value expressions for complex values shall have more priorities than default values for individual slots, as otherwise the default value for the individual slot (e.g., given as default value within a compound or a refined slot) may be overridden by a complex value from a containing scope, e.g., a top-level variable declaration. This is also initiated in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}. +\end{enumerate} + +We start with the algorithm for translating declaration types and defaults in Section \ref{sectTranslationDeclarationTypesDefaults}. Then we will discuss more specific algorithms used within the translatation of declaration types and defaults, including derived types in Section \ref{sectDerivedTypes}, annotation assignments in Section \ref{sectAnnotationDefaults} (as already used in (Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}), compound defaults in Section \ref{sectCompoundDefaults}, and, finally, container defaults in Section \ref{sectContainerDefaults}. + +\subsection{Translate Declaration Types and Default Values}\label{sectTranslationDeclarationTypesDefaults} Algorithm \ref{algTranslateDeclarationDefaults} translates the default value expression according to the actual type of the declation $d$ or, if applicable, the value represented by the default value expression. The algorithm @@ -419,5 +417,5 @@ \item Constructs the default value assignment constraints for the annotations (cf. Section \ref{sectAnnotationDefaults}) and stores them into the global set of annotation constraints $\otherConstraints$ \item Translates the default value expression and the constraints for all nested compound slots if $d$ is a compound. Therefore, the algorithm uses the type of $d$ or, if available, or the actual type of the default value expression, which may be a refined type of $d$. The translation of the nested compound slots contributes to the variable-accessor mapping $c$. Then the algorithm substitutes all occurrences of \IVMLself{} by the actual declaration as well as all mapped variables from $\problemRecords$ in the default value expression. It is important that the constraints for the nested compound slots must be translated regardless wether a default value expression for $d$ is specified. - \item Collects all transformed container compounds based on the actual used types if $d$ is a container. If $d$ is a container over compounds, here all potentially refined compound types and their specific constraints are considered (cf. Section \ref{deflt_containers}). + \item Collects all transformed container compounds based on the actual used types if $d$ is a container. If $d$ is a container over compounds, here all potentially refined compound types and their specific constraints are considered (cf. Section \ref{sectContainerDefaults}). \item Translates remaining (slot) default value expression by replacing potential \IVMLself{} usages with the compound access. In case that \IVMLself{} is used in the default value expression or the declaration is an overriding slot, the expression shall be turned into a deferred default value constraint ($\deferredDefaultConstraints$), i.e., a constraint that is evaluated later than all usual default value constraints. Deferring these constraints ensures that individual slots are assigned after values for entire compounds or containers on top-level are assigned, i.e., the individual slot value is not accidentally overridden by a more global value for the entire structure. \item Translates usual container compound constraints independent of any default value expression and stores them into $\otherConstraints$. \TBD{check} @@ -511,5 +509,5 @@ -\subsection{Compound default constraints} +\subsection{Compound default constraints}\label{sectCompoundDefaults} Translating a compound into all its constraints requires considering all slots, all constraints defined within a compound, as well as all supported nested structures, such as eval blocks or attribute value assignment blocks. In particular, if the IVML keyword \IVMLself{} is used, it must be replaced by the actual variable of the respective compound type. First, we define some helper functions, then the translation algorithms. @@ -631,5 +629,5 @@ -\subsection{Container default constraints}\label{deflt_containers} +\subsection{Container default constraints}\label{sectContainerDefaults} Constraints defined on types that are implicitly instantiated within a container must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algTranslateDefaultsCompoundContainer} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested container). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the container using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVMLself{} substituted by the iterator variable $i$.