Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 195) +++ /reasoner/consTranslation.tex (revision 196) @@ -1,17 +1,19 @@ \section{Constraint translation}\label{sectTranslation} -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: +The constraint translation algorithms analyze IVML language elements for constraints, instantiate the constraints for which reasoning cannot happen directly and indirectly set up the constraint base via the constraint sequences $\defaultConstraints$, $\deferredDefaultConstraints$, $\topLevelConstraints$ and $\otherConstraints$. In particular, constraints defined on types rather than qualified variables or accessors are instantiated by these algorithms. While Algorithm \ref{algTranslateConstraints} illustrated the overall structure of the constraint translation, we will detail in this section the remaining involved algorithms shown in Figure \ref{figStructure}. We distinguish two main types of constraints: \begin{enumerate} - \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}). + \item \emph{Default value constraints}. IVML variable declarations may specify a default value. At a glance, we could evaluate and assign the default value directly while visiting a variable (or slot) declaration the first time. However, default value values are expressions that may depend on other variables, i.e., may first be evaluated successfully when values for the involved variables have been assigned. To avoid a plethora of similar evaluation paths, we opted for a uniform handling of default values and constraints. Thus, we instantiate default values to default value assignment constraints, add them either to $\defaultConstraints$ (primitive and complex default values) or $\deferredDefaultConstraints$ (individual slot default values) and process them as part of the top-level constraint evaluation (Algorithm \ref{algEvalLoopLoopEnd}). The creation of these default assignment constraints is part of translating variable declarations. + \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 accessors. Identifying constraints in types happens also during the translation of variable declarations. \end{enumerate} -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}. +%\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. + +Thus, the next step after the top-level constraint translation is the translation of variable declarations in Algorithm \ref{algTranslateDeclaration} (called by Algorithm \ref{algTranslateConstraints} in line \ref{algTranslateConstraintsTranslationDeclaration}). In Section \ref{sectTranslationDeclarationTypesDefaults}, we will detail Algorithm \ref{algTranslateConstraints}, which performs the translation of variable declarations and the creation of default value constraints, but also delegates further translations to subsequent algorithms (as indicated in Figure \ref{figStructure}). We will discuss the subsequent algorithms in the following sub-sections, namely derived types in Section \ref{sectDerivedTypes}, compound types in Section \ref{sectCompoundDefaults}, container types in Section \ref{sectContainerDefaults}, annotation assignments in Section \ref{sectAnnotationDefaults}, and, constraint variables in Section \ref{sectConstraintVariables}. Finally in Section \ref{sectContainerBase}, we introduce the support algorithms used for building the constraint base. As also shown in Figure \ref{figStructure}, the subsequent algorithms may recursively call Algorithm \ref{algTranslateConstraints} while translating nested types, such as compounds in compounds or compounds in containers. \subsection{Variable Declarations}\label{sectTranslationDeclarationTypesDefaults} -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. +%, e.g., in IVML \IVML{\textit{Type} v = ex;} declares the variable $v$ of type \textit{Type} with expression $ex$ defining the default value for $v$, In essence, for a declaration \IVML{\textit{Type} v = ex;} we simply derive a constraint $\createConstraint{v = ex}$. +As discussed above, an IVML variable declaration consists of a type, a variable name and an optional default value expression. In IVML syntax, a variable declaration looks like \IVML{\textit{Type} v = ex;} with \IVML{v} being the variable name and \IVML{ex} the default value expression. At its core, the translation of variable declarations creates assignment constraints for the default value expressions, i.e., $\createConstraint{v = ex}$, analyzes then the \IVML{\textit{Type}} and instantiates all constraints implied by \IVML{\textit{Type}}. If known, the translation considers the actual type implied by the default value expression rather than the static type given in the declaration. We use the actual type, as it may define more (specific) constraints, e.g., in case of refined compound types. Considering the actual type already during the translation anticipates re-scheduling when the default value is set by the constraint evaluation and avoids immediate modifications of the constraint base. Thus, translating for the actual type may require a transitive traversal over refined / base types, e.g., in case of typedefs, compounds or containers. \grayPara{ @@ -22,5 +24,5 @@ } -Let $v$ be a variable with default value expression $deflt$. The first transformation pattern above turns $deflt$ into an assignment constraint. If $v$ is nested in a compound or a sequence, a qualified access expression is required in the resulting constraint. In the transformation pattern, we indicate this by $access(e)$ on the right side, which returns the given expression $e$ if $e$ is an access to a top-level variable and prefixes $e$ appropriately if $e$ expresses an access to a nested variable. The second pattern refers to annotations. As introduced in Section \ref{sectNotationVarDecls}, annotations are variables represent an an orthogonal configuration dimension on top of 'ordinary' variables. Thus, an annotation $a$ is translated similarly to an ordinary variable, but requires in addition a qualification through the respective ordinary variable $v$. We will defer annotations to Section \ref{sectAnnotationDefaults} and develop here generic functionality for the instantiation of default values, which can then be used by the translation of annotations. +We apply the translation patterns above: Let $v$ be a variable with default value expression $deflt$. The first transformation pattern above turns $deflt$ into an assignment constraint. If $v$ is nested in a compound or a sequence, a qualified access expression is required in the resulting constraint. In the transformation pattern, we indicate this by $access(e)$ on the right side, which returns the given expression $e$ if $e$ is an access to a top-level variable and prefixes $e$ appropriately if $e$ expresses an access to a nested variable. The second pattern refers to annotations. As introduced in Section \ref{sectNotationVarDecls}, annotations are variables represent an an orthogonal configuration dimension on top of 'ordinary' variables. Thus, an annotation $a$ is translated similarly to an ordinary variable, but requires in addition a qualification through the respective ordinary variable $v$. We will defer annotations to Section \ref{sectAnnotationDefaults} and develop here generic functionality for the instantiation of default values, which can then be used by the translation of annotations. Algorithm \ref{algTranslateDeclaration} translates all constraints related to a given variable $v$ (and its declaration $d$) based on the actual type of $v$. As complex types such as compounds may occur, Algorithm \ref{algTranslateDeclaration} delegates such types to more specialized algorithms, which then use Algorithm \ref{algTranslateDeclaration} recursively for nested variable declarations (with a respective access expression $ca$ and an adequately prepared variable mapping $\variableMapping$). These specialized algorithms will be discussed in the following sections. Assignment constraints created in Algorithm \ref{algTranslateDeclaration} are stored either in the global set for default constraints $\defaultConstraints$ or the set for deferred default constraints $\deferredDefaultConstraints$. Index: /reasoner/mainAlgorithms.tex =================================================================== --- /reasoner/mainAlgorithms.tex (revision 195) +++ /reasoner/mainAlgorithms.tex (revision 196) @@ -155,5 +155,5 @@ \begin{enumerate} \item \emph{Default constraints $\defaultConstraints$}, i.e., constraints that initialize default values using primitive and complex values such as compound or container initializers modifying multiple nested variables at once. - \item \emph{Deferred default constraints $\deferredDefaultConstraints$} are default constraints that must be evaluated after all constraints in $\defaultConstraints$, but before other constraints. $\deferredDefaultConstraints$ includes constraints that initialize individual nested variables. Mixing $\defaultConstraints$ and $\deferredDefaultConstraints$ can lead to accidental overrides of already initialized nested variables by compound or container initializers. + \item \emph{Deferred default constraints $\deferredDefaultConstraints$} are default constraints that must be evaluated after all constraints in $\defaultConstraints$, but before other constraints. $\deferredDefaultConstraints$ includes constraints that initialize individual nested variables. Mixing $\defaultConstraints$ and $\deferredDefaultConstraints$ can lead to accidental overrides of already initialized nested variables by compound or container initializers\footnote{This is partially caused by legacy behavior of the implementation, which cleans the target variable before assigning a complex value.}. \item \emph{Top level constraints $\topLevelConstraints$} include constraints that are directly specified in an IVML project, in top-level eval-blocks, in top-level annotation assignments or in terms of constraints attached to top-level variables, e.g., by derived types. These constraints are added to $\topLevelConstraints$ by Algorithm \ref{algTranslateConstraints}. On the one side, these constraints shall take precedence over constraints in nested scopes~\cite{IVML-LS}. On the other side, top-level constraints in eval blocks shall take precedence over other top-level constraints~\cite{IVML-LS}. Thus, constraints from eval blocks are always inserted at the front of $\topLevelConstraints$, while the other top-level constraints are appended to the end of $\topLevelConstraints$. To avoid unnecessary re-evaluations, default constraints in $\defaultConstraints$ or $\deferredDefaultConstraints$ are evaluated before constraints in $\topLevelConstraints$. \item \emph{Remaining other constraints $\otherConstraints$} that shall be evaluated after $\topLevelConstraints$. $\otherConstraints$ includes in particular non top-level constraints originating from constraint variables or complex types such as compounds or compounds in containers. @@ -238,5 +238,5 @@ \end{algorithm} -Successfully evaluated default constraints must not stay in the constraint base as their initialization work has been done. As the evaluation of individual constraints cleans up the constraint base, we just have to avoid that they are accidentally re-scheduled. Therefore, we remove them in lines \ref{algEvalLoopClearStart}-\ref{algEvalLoopClearEnd} also from $\relevantConstraintsPerDeclaration$, the mapping between variable declarations and constraints. Mo modification of $\relevantConstraintVariables$, the mapping between decision variables and constraints, is needed, as no change of constraint variables or their values can occur here. +Successfully evaluated default constraints must not stay in the constraint base as their initialization work has been done. As the evaluation of individual constraints cleans up the constraint base, we just have to avoid that they are accidentally re-scheduled. Therefore, we remove them in lines \ref{algEvalLoopClearStart}-\ref{algEvalLoopClearEnd} also from $\relevantConstraintsPerDeclaration$, the mapping between variable declarations and constraints. No modifications of $\relevantConstraintVariables$ are needed, as no change of constraint variables or their values can occur here. Finally, Algorithm \ref{algEvalLoop} checks in line \ref{algEvalLoopTimeout} for a potential timeout comparing the global $startTime$ (initialized by Algorithm \ref{algMainLoop}) with a configured reasoning timeout. If a timeout occurred (not further detailed here), the global $hasTimeout$ flag is set to $true$.