Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 138) +++ /reasoner/reasoner.tex (revision 139) @@ -56,5 +56,6 @@ \newcommand\tabAlgFollow[0]{ $\rightarrow$ } \newcommand\grayPara[1]{\noindent\adjustbox{bgcolor=gray!20,minipage=[t]{\linewidth}}{#1}\linebreak} -\newcommand\patternDerivation[2]{#1 \leadsto #2} +\newcommand\patternDerivationSymbol[0]{\leadsto} +\newcommand\patternDerivation[2]{#1 \patternDerivationSymbol #2} \let\emph\relax % there's no \RedeclareTextFontCommand @@ -238,5 +239,5 @@ In IVML, a \emph{constraint} is a Boolean expression that must always evaluate to $true$. Otherwise, reasoning shall either fail. After a change of at least one of the values of the variables involved in the constraint, the constraint may be re-evaluated successfully, causing a cleanup of previous reasoning errors for that constraint. -Technically, a constraint can consist of sub-expressions, that can evaluate to values of some type supported by IVML, in particular of Boolean type. Such expressions can be used to determine the default value of variables and, of course, sub-expressions may make use of / refer to variables. Let $v$ be a constraint, then we indicate, e.g., in transformation patterns, by $c(v)$ that constraint $c$ is using variable $v$. Moreover, if $c$ is an assignment constraint representing $x = y$, the operation $rightSide(c)$ returns $y$ else $\undef$. A specific type of expression is the constant, which holds an IVML value. The operation $const(e)$ returns the value of $e$ if $e$ is a constant expression or $\undef$ otherwise. +Technically, a constraint can consist of sub-expressions, that can evaluate to values of some type supported by IVML, in particular of Boolean type. Such expressions can be used to determine the default value of variables and, of course, sub-expressions may make use of / refer to variables. Let $v$ be a constraint, then we indicate by $c(v)$ that constraint $c$ is using variable $v$. Moreover, if $c$ is an assignment constraint representing $x = y$, the operation $rightSide(c)$ returns $y$ else $\undef$. A specific type of expression is the constant, which holds an IVML value. The operation $const(e)$ returns the value of $e$ if $e$ is a constant expression or $\undef$ otherwise. Moreover, \IVML{Constraint} is an IVML type, indicating that a variable actually holds a constraint. From the reasoning point of view, a constraint stored as a value of a constraint variable is extracted and then evaluated as any other constraint. However, the value in such a variable may, as for all other variables, be undefined, frozen, or re-defined (once per project scope) implying that the old constraint must be discarded or even replaced by the new constraint value and considered in the subsequent reasoning process. $isConstraint(t)$ indicates whether type $t$ is a constraint type. %$isAssignmentConstraint(c)$ indicates whether constraint $c$ is supposed to unconditionally change the value of a variable through an assignment, e.g., for an integer variable \IVML{x} the constraint \IVML{x = 25;} in IVML notation is an assignment Constraint. @@ -253,4 +254,13 @@ In some cases, constraints cannot be created in terms of a single step, i.e., sub-expressions are created iteratively. To indicate this, we denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for the IVML expression \IVML{x + 25}. When creating expressions, in particular in an incremental fashion, sometimes a temporary (local) IVML variable is needed, e.g., for an IVML let-expression or a container iterator. We state the creation of such a variable by $\IVMLMeta{var}(t)$, i.e., request the creation of a temporary variable\footnote{We don't care for the variable name in this document.} of type $t$. For a variable $v=\IVMLMeta{var}(t)$ holds $isLocal(v) = true$. + +Before reasoning over the constraints given in an IVML project, several kinds of constraints must be transformed, in particular to instantiate constraints defined for types through qualifying access expressions based on top-level variables. To illustrate the transformations performed by an algorithm in this document, we apply constraint transformation patterns. A \emph{constraint transformation pattern} indicates how a certain IVML model fragment is instantiated to a corresponding constraint given in IVML constraint notation rather than the algorithm notation for creating constraints introduced in this section. The model fragment is given on the left side of the derivation symbol $\patternDerivationSymbol$, the corresponding constraint on the right side of $\patternDerivationSymbol$. In such a pattern, variable parts are given in italics to indicate the information flow between both sides. Constant parts are given in normal font, IVML syntax in \IVML{teletype}. One or more transformation patterns are displayed in a gray box. For example, the pattern below indicates that an IVML declaration for variable $v$ (with type $T$ and default value expression $deflt$) is translated into an assignment constraint, which assigns the (value of the) default expression $deflt$ to $v$. + +\grayPara{ +\begin{gather*} + \patternDerivation{T \text{ } v = deflt\IVML{;}}{v = deflt} \\ +\end{gather*} +} + \subsubsection{Compounds}\label{sectNotationCompounds} @@ -623,21 +633,19 @@ \section{Constraint translation}\label{sectTranslation} -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. We distinguish three main types of constraints: +The constraint translation analyzes constraints defined for a given IVML model, instantiates those constraints for which reasoning cannot happen directly and fills the constraint base accordingly. In particular, constraints defined over types rather than qualified variable access expressions must be instantiated. We distinguish three main types of constraints, for which the top-level constraint translation algorithm (Algorithm \ref{algTranslateConstraints}) already indicated the subsequent translation calls: \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, typedefs with constraints or, transitively, collections. 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}. + \item \emph{Constraints for default values}. To achieve uniformity of the constraint evaluation and re-scheduling upon value changes (cf. Section \ref{sectReasoning}), we also translate default value assignments to assignment constraints and add them to the constraint base. In more detail, an IVML declaration \IVML{\textit{Type} v = ex;} is translated to a constraint $\createConstraint{v = ex}$. We add assignment constraints to the constraint base with higher priority, i.e., at a lower sequence position than other constraints to ensure that default values are assigned first. For value assignment constraints, we must consider that default value expressions assigning complex values shall have higher priority than default values for individual slots or sequence positions. Otherwise, the value for an individual slot or position may accidentally be overridden by the complex value\footnote{This is partially caused by legacy behavior of the implementation, which cleans the target variable before assigning a complex value. However, re-assignment of values for individual slots or positions in the same scope leads to a reasoning error as required.}. Moreover, default value assignments can change the actual (value) type of a variable implying that a refined set of constraints must be evaluated. Creation of assignment constraints is part of translating variable declarations (called in Algorithm \ref{algTranslateConstraints} in line \ref{algTranslateConstraintsTranslationDeclaration}). + \item \emph{Top-level constraints} are defined using only top-level variables or fully qualifying accessor expressions. Top-level constraints include constraints in top-level eval blocks as well as constraints in top-level annotation assignment-blocks. Top-level constraints are ready for reasoning, i.e., they do not need further translation and can directly be taken over into the constraint base (Algorithm \ref{algTranslateConstraints}, lines \ref{algTranslateConstraintsAdd} - \ref{algTranslateConstraintsTopLevelEvals}). Annotation assignments are processed by Algorithm \ref{algTranslateAnnotationAssignments}. We use that algorithm also for translating annotation assignments in compound types. + \item \emph{Constraints in type definitions}, e.g., in compound types, typedefs with constraints or collections. These constraints must be instantiated, i.e., use of (local) variables and slots defined by a type must be substituted by fully qualifying accessor. We use top-level variables as entry point and perform a (recursive) constraint instantiation based on the type of the variable. Identifying constraints in types happens also during the translation of declarations (Algorithm \ref{algTranslateConstraints} line \ref{algTranslateConstraintsTranslationDeclaration}). \end{enumerate} -The main entry point to the constraint translation are variable declarations. A variable declaration consists of a type, a name, and, if given, a default value. As mentioned above, some types can define constraints that must be instantiated, in particular derived types (typedefs), compounds, containers (through their used types) and contraint variables. Algorithm \ref{algTranslateDeclaration} (in Section \ref{sectTranslationDeclarationTypesDefaults}) performs the translation of variable declarations, related default value expressions and, following the call graph in Figure \ref{figStructure} dispatches further translations according to the type of the variable. Please note that Algorithm \ref{algTranslateDeclaration} is (indirectly) subject to recursion if further variable declarations, in particular compound slots and annotations must be processed. - -We start in Section \ref{sectTranslationDeclarationTypesDefaults} with the translation of variable declarations structure the remainder of this section according to the algorithms called while processing a variable declaration, i.e., the translation of default values in Section \ref{sectTranslationDeclarationTypesDefaults}, derived types in Section \ref{sectDerivedTypes}, annotation assignments in Section \ref{sectAnnotationDefaults} (as already used in (Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}), compound types in Section \ref{sectCompoundDefaults}, container types in Section \ref{sectContainerDefaults}, and, constraint variables in Section \ref{sectConstraintVariables}. A section about algorithms for building the constraint base in Section \ref{sectContainerBase} completes the constraint translation. +We detail now the constraint translation in the remainder of this section. We start in Section \ref{sectTranslationDeclarationTypesDefaults} with the translation of variable declarations, which delegates the translation to further algorithms and is called recursively during the translation of compound and collection variables. Then we follow the algorithms called while processing a variable declaration, i.e., the call graph shown in Figure \ref{figStructure}. Thus, the following sections focus on derived types in Section \ref{sectDerivedTypes}, annotation assignments in Section \ref{sectAnnotationDefaults} (as already used in (Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}), compound types in Section \ref{sectCompoundDefaults}, container types in Section \ref{sectContainerDefaults}, and, constraint variables in Section \ref{sectConstraintVariables}. Finally, we discuss the algorithms for building the constraint base in Section \ref{sectContainerBase}. \subsection{Variable Declarations}\label{sectTranslationDeclarationTypesDefaults} -Algorithm \ref{algTranslateDeclaration} translates all constraints related to a given variable declaration $d$ and respective variable $v$ through their actual type. Basically, the algorithm considers for the given variable, depending on the actual type, derived type constraints, annotation defaults, compound constraints, container constraints, and constraints of overridden slots leading to a deferred default initialization through the global constraints set $\deferredDefaultConstraints$. - -At its core, Algorithm \ref{algTranslateDeclaration} instantiates a given variable $v$ (or attribute in the second case) with default expression $deflt$, basically $default(v)$ turning it into a default value assignment constraint. The patterns below include a right side access prefix ($ca.$), which may be empty for top-level variables. +As introduced in Section \ref{sectNotationVarDecls}, an IVML variable declaration consists of a type, a variable name and an optional default value expression. At its core, the translation of a variable declaration creates an assignment constraint for the default value expressions and instantiates all constraints defined by the variable type. If known, the translation considers the actual type of the variable defined by the configured value, which may in particular have a refined (compatible) compound type and, thus, a refined set of constraint. However, due to the complex structure of IVML types, identifying the constraints defined by a type may require a transitive or even recursive traversal over refined or underlying base types, e.g., in case of a typedef or a container. + +Let $v$ be a given variable with default value expression $deflt$, then the first transformation pattern below turns $default(v)$ into an assignment constraint. If $v$ is nested in a compound or a sequence, a qualified access expression is required. In the transformation pattern, we indicate this by the access expression $ca.$ on the right side, which is empty for top-level variables. As introduced in Section \ref{sectNotationVarDecls}, annotations are variables allowing an an orthogonal configuration dimension for 'ordinary' variables. Thus, an annotation can be translated similarly to an ordinary variable, but require a qualification through the respective ordinary variable as indicated in the second transformation pattern. \grayPara{ @@ -647,4 +655,7 @@ \end{gather*} } + +Algorithm \ref{algTranslateDeclaration} translates all constraints related to a given variable declaration $d$ and respective variable $v$ through their actual type. Basically, the algorithm considers for the given variable, depending on the actual type, derived type constraints, annotation defaults, compound constraints, container constraints, and constraints of overridden slots leading to a deferred default initialization through the global constraints set $\deferredDefaultConstraints$. + For a $v$ of compound or container type, Algorithm \ref{algTranslateDeclaration} dispatches to the other algorithms constituting the reasoner as we will discus in the following sections. Then the patterns can also be applied for initializing compound slots. As a consequence, Algorithm \ref{algTranslateDeclaration} may be called recursively with an incrementally constructed access expression $ca$ that is prefixed before the right side, e.g., let $c$ be the top-level variable of compound type, then $ca=c$ and the pattern $\patternDerivation{v}{ca.v = deflt}$ becomes $c.v=deflt$. In particular in such recursive calls, occurrences of other variables in $deflt$ recorded in $\variableMapping$, e.g., other slots as well as \IVML{self} denoting the actual compound must be substituted properly, i.e., the result is at least $c.v=\varSubstitution{deflt}{\IVML{self}, \variableMapping}$.