Index: /reasoner/mainAlgorithms.tex =================================================================== --- /reasoner/mainAlgorithms.tex (revision 193) +++ /reasoner/mainAlgorithms.tex (revision 194) @@ -152,12 +152,15 @@ -Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. As a side effect, the constraint translation identifies and translates the constraints in the respective project\footnote{The top-translation steps in this algorithm are realized in the implementation by an IVML model visitor implicitly identifying and handling the types without iterating over the project multiple times as the notation here might suggest.}. To prioritize the constraints correctly, the reasoner uses four global sets, which are populated during the constraint translation and, finally, in Algorithm \ref{algTranslateConstraints} added to the constraint base. In more details, the reasoner maintains the following temporary constraint sets +%Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. As a side effect, the constraint translation identifies and translates the constraints in the respective project\footnote{The top-translation steps in this algorithm are realized in the implementation by an IVML model visitor implicitly identifying and handling the types without iterating over the project multiple times as the notation here might suggest.}. +To prioritize the constraints correctly, the constraint translation uses four global sets, which are populated during the constraint translation and, finally, in Algorithm \ref{algTranslateConstraints} added to the constraint $base$. In more details, the translation maintains the following temporary constraint sequences: \begin{enumerate} - \item \emph{Default constraints $\defaultConstraints$} containing constraints setting the default values of all variables. In particular, this set can contain constraints that assign compound and container initializers, i.e., modify multiple values at once. - \item \emph{Deferred default constraints $\deferredDefaultConstraints$} containing default initialization constraints to be evaluated after all constraints in $\defaultConstraints$, but before the remaining two constraint sets below. $\deferredDefaultConstraints$ is required as setting individual variables may be accidentally overridden by compound and container initializers assigned through constraints in $\defaultConstraints$. - \item \emph{Top level constraints $\topLevelConstraints$}, i.e., constraints directly specified in a project, in top-level eval-blocks, in top-level assignment blocks as well as constraints attached to top-level variables, e.g., through derived types. These constraints originating from the top-level scope shall take precedence over constraints in nested scopes~\cite{IVML-LS}. - \item \emph{Remaining other constraints $\otherConstraints$} in particular in in nested structures, including compound types used in containers, nested assignment blocks or constraint variables. + \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{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. \end{enumerate} + +These constraint sets are filled as side effects of the calls in line \ref{algTranslateConstraintsTranslationStart}-\ref{algTranslateConstraintsTranslationEnd}. Please note that adding constraints to such a constraint set involves completing constraints through prefix quantification, identifying constraints from constraint variable values, filtering out unneeded constraints according to the reasoning mode as well as indexing constraints and their used variables. This is done by the $add$ function (e.g., in line \ref{algTranslateConstraintsAdd}), which we will detail below in Section \ref{sectContainerBase}. The $add$ function receives the target constraint set, the constraint(s) to add, a flag whether checking for constraint values is needed and an optional variable to which new constraints shall be related to (in $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$). The $add$ function considers the $inEvals$ flag\footnote{We follow here the implementation, where the visitor is an own class communicating this information via an instance variable.}, which enforces a higher priority for (eval) constraints to be added. According to the priority of the constraint sets introduced above, Algorithm \ref{algTranslateConstraints} composes in line \ref{algTranslateConstraintsCompose} the constraint base (keeping remaining constraints from prior project evaluations on the same configuration). Finally, Algorithm \ref{algTranslateConstraints} clears the temporary constraint sets in lines \ref{algTranslateConstraintsClearSetsStart}-\ref{algTranslateConstraintsClearSetsEnd} and copies the constraint $base$ in the first run of the incremental reasoning mode with re-used constraint base. \begin{algorithm}[H] @@ -192,6 +195,4 @@ -These constraint sets are filled as side effects of the calls in line \ref{algTranslateConstraintsTranslationStart}-\ref{algTranslateConstraintsTranslationEnd}. Please note that adding constraints to such a constraint set involves completing constraints through prefix quantification, identifying constraints from constraint variable values, filtering out unneeded constraints according to the reasoning mode as well as indexing constraints and their used variables. This is done by the $add$ function (e.g., in line \ref{algTranslateConstraintsAdd}), which we will detail below in Section \ref{sectContainerBase}. The $add$ function receives the target constraint set, the constraint(s) to add, a flag whether checking for constraint values is needed and an optional variable to which new constraints shall be related to (in $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$). The $add$ function considers the $inEvals$ flag\footnote{We follow here the implementation, where the visitor is an own class communicating this information via an instance variable.}, which enforces a higher priority for (eval) constraints to be added. According to the priority of the constraint sets introduced above, Algorithm \ref{algTranslateConstraints} composes in line \ref{algTranslateConstraintsCompose} the constraint base (keeping remaining constraints from prior project evaluations on the same configuration). Finally, Algorithm \ref{algTranslateConstraints} clears the temporary constraint sets in lines \ref{algTranslateConstraintsClearSetsStart}-\ref{algTranslateConstraintsClearSetsEnd} and copies the constraint $base$ in the first run of the incremental reasoning mode with re-used constraint base. - %Adding constraints or sets of constraints to the constraint base involves constraint filtering in order to respect the incremental reasoning mode as well as constraints that initialize compounds and containers through respective initializer expressions. This is done by a specific operation, which we will discuss in Section \ref{sectContainerBase}. During algorithm discussion, we ill just use the respective function $add(s, c, b)$, which adds constraint $c$ to constraint set $s$, considering compound and container initialization expressions if $b = true$. Compound and container initialization expressions are a specific and relevant case here, as they represent complex compound or container values containing (interrelating) expressions that can only be evaluated during reasoning in contrast to constant values, which are already resolved by the IVML parser (or by a simple configuration initialization mechanism). These expressions are particularly important to correctly consider constraints stemming from constraint variables. While most translation algorithms rely on default values or actual values (e.g., through the $relevantValue$ function defined in Section \ref{sectNotationValues}, compound and container initializers can only be obtained from assignment constraints, i.e., completed and instantiated constraints, which are only available when adding constraints to a constraint set or the constraint base. Thus, We will skip container and compound initializers in the translation algorithms, focus on actual or constant default values, and finally consider these specific cases in Section \ref{sectContainerBase}.