Index: /reasoner/mainAlgorithms.tex =================================================================== --- /reasoner/mainAlgorithms.tex (revision 194) +++ /reasoner/mainAlgorithms.tex (revision 195) @@ -132,5 +132,5 @@ \item $addAssignment(\scopeAssignments, v)$ indicates that variable $v$ was changed through an assignment within the actual scope. \item $wasAssigned(\scopeAssignments, v)$ returns whether variable $v$ was assigned in the actual scope. This operation is used to validate an assignment before it is performed by the expression evaluator ($\evaluator$). - \item $clearAssignments(\scopeAssignments)$ clears all assignments in all scopes in order to reuse the $\scopeAssignments$ instance. + \item $clearAssignments(\scopeAssignments, scope)$ clears all assignments for scope $scope$. \end{itemize} @@ -151,7 +151,5 @@ Top-level constraints are defined using top-level variables, which are already fully qualified so no translation is needed, because these variables already represent complete access expressions. This is indicated by the first translation pattern. Similarly, constraints defined in top-level (nested) annotation assignments are already qualified and can be directly used for reasoning as indicated by the second translation pattern. Moreover, annotation assignments represent constraints that assign values to annotations of contained declared (top-level) variables. Similarly, these constraints can be used in reasoning without translation. This is implied in the second translation pattern. Also the variables used in constraints listed in (nested) top-level eval-blocks are fully qualified. In contrast, the evaluation of constraints in eval blocks must be prioritized over the other (top-level) constraints~\cite{IVML-LS}. - -%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: +To prioritize the constraints, the constraint translation uses four global sequences, which are populated during the constraint translation and, finally, added to the constraint $base$ (also a sequence). In more details, we maintain: \begin{enumerate} @@ -162,10 +160,14 @@ \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. +Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. The algorithm receives a project $p$ as input and, as a side effect, identifies and translates\footnote{In the implementation, the translation steps in this algorithm are realized in terms of an IVML model visitor implicitly identifying and handling the types without iterating multiple times over the project as the notation here might suggest.} the constraints in $p$. The constraint sequences are filled as side effects of the calls in lines \ref{algTranslateConstraintsTranslationStart}-\ref{algTranslateConstraintsTranslationEnd}, where the algorithm iterates over the top-level constraint types, i.e., variable declarations, constraints, annotation assignments and eval blocks directly contained in project $p$. + +It is important to note that adding constraints to such a constraint sequence involves activities such as completing constraints by quantification, handling constraint variables, filtering out unneeded constraints according to the reasoning mode as well as relating constraints and their used variables (cf. $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$). These activities are realized in the $add$ function (e.g., used in line \ref{algTranslateConstraintsAdd}), which we will detail in Section \ref{sectContainerBase}. For short, the $add$ function receives the target constraint sequence, the constraint(s) to add, a flag whether checking for constraint values is needed and an optional configuration variable to which new constraints shall be related to (for building up $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$). The $add$ function also considers the global $inEvals$ flag\footnote{For documentation purposes, we follow here the style of the implementation, where the visitor is a class communicating such information via instance variables.}, which raises the priority for all (eval) constraints passed in. + +According to the priority of the constraint sequences $\defaultConstraints$, $\deferredDefaultConstraints$, $\topLevelConstraints$ and $\otherConstraints$, Algorithm \ref{algTranslateConstraints} composes in line \ref{algTranslateConstraintsCompose} the constraint base (keeping remaining constraints from prior projects). Then, Algorithm \ref{algTranslateConstraints} clears $\defaultConstraints$, $\deferredDefaultConstraints$, $\topLevelConstraints$ and $\otherConstraints$ in lines \ref{algTranslateConstraintsClearSetsStart}-\ref{algTranslateConstraintsClearSetsEnd} and copies the constraint $base$ to prepare the incremental reasoning mode in its first run. Finally, in line \ref{algTranslateConstraintsClearMapping}, Algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$ so that it can be re-used for translating the next IVML project. \begin{algorithm}[H] \SetAlgoLined \KwIn{project $p$} - \KwData{configuration $cfg$, constraint $base$, constraint base copy $base_c$, constraint sets $\defaultConstraints,\deferredDefaultConstraints, \topLevelConstraints, \otherConstraints$, eval-blocks flag $inEvals$} + \KwData{configuration $cfg$, constraint $base$, constraint base copy $base_c$, constraint sequences $\defaultConstraints,\deferredDefaultConstraints, \topLevelConstraints, \otherConstraints$, eval-block flag $inEvals$} \tcp{start of model visitor}%>ConstraintTranslationVisitor @@ -197,22 +199,20 @@ %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}. -Finally, in line \ref{algTranslateConstraintsClearMapping}, Algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$ so that it can be re-used for translating the next IVML project. - \subsection{Top-level Constraints Evaluation}\label{sectTopLevelConstraintsEvaluation} -When the constraint base is filled for a given project, the constraint evaluation for that project (including potentially left over constraints from previous project evaluations) can start. Algorithm \ref{algEvalLoop} implements the constraint evaluation for a project. As mentioned above, this part heavily relies on the IVML constraint evaluation mechanism. - -An IVML project constitutes a reasoning scope, i.e., no duplicated assignment to the same variable must occur within a project. To prepare validating this rule, Algorithm \ref{algEvalLoop} clears in line \ref{algEvalLoopClearScope} the (global) scope assignments as introduced in Section \ref{sectScopeAssignments}. %Further, it sets $p$ as search space for dynamically dispatched operations on the expression evaluator$e$ (line \ref{algEvalLoopDispatchScope}). - -The main loop (lines \ref{algEvalLoopLoopStart}-\ref{algEvalLoopLoopEnd}) runs as long as there are constraints for evaluation in the constraint $base$, no timeout and no user cancellation request occurred. The (size of the) constraint base changes dynamically during reasoning as Algorithm \ref{algEvalLoop} removes processed constraints and value (type) changes may add constraints, e.g., those involving the changed variable (see Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling} for details). If no value assignment cycles occur, which ultimately lead to a timeout, the evaluation loop either terminates when all constraints are successfully evaluated or failing constraints do not induce the evaluation of further constraints. - -In each iteration of the main loop, the algorithm pops a constraint for evaluation from $base$ (line \ref{algEvalLoopPop}). % and clears the records about used variables (line \ref{algEvalLoopClear}). Recording used variables is required as detailed information for recording reasoning problems and later for creating the detailed reasoning report (last step of Algorithm \ref{algMainLoop}). -To assign values with the correct assignment state (cf. Section \ref{sectNotationConfigVars}), Algorithm \ref{algEvalLoop} registers the actual assignment state for the current constraint $c$ (line \ref{algEvalLoopAssngState}). If $c$ is a default constraint, all subsequent value assignments during the evaluation of $c$ happen with state \IVML{DEFAULT}, else state \IVML{DERIVED}. Next, constraint $c$ is evaluated (line \ref{algEvalLoopAssngEval}) by passing it to the constraint evaluator. %If configuration variables are changed as part of the constraint evaluation, the variables are recorded (not shown in Algorithm \ref{algVarChange}) and their constraints are re-scheduled for reasoning (cf. Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). -Then, the evaluation result is analyzed (still line \ref{algEvalLoopAssngEval}) and, if needed, problem records are created. We distinguish three cases: +When the constraint base is filled for a given project, the constraint evaluation for that project (including potentially left over constraints from previous project evaluations) can start. Algorithm \ref{algEvalLoop} illustrates the constraint evaluation for a project. As mentioned above, this part heavily relies on the IVML constraint evaluation mechanism. + +An IVML project constitutes a reasoning scope, i.e., no duplicated assignment to the same variable must occur within a project. To prepare the validation of this rule, Algorithm \ref{algEvalLoop} clears in line \ref{algEvalLoopClearScope} the (global) scope assignments for $p$ as introduced in Section \ref{sectScopeAssignments}. %Further, it sets $p$ as search space for dynamically dispatched operations on the expression evaluator$e$ (line \ref{algEvalLoopDispatchScope}). + +The evaluation loop (lines \ref{algEvalLoopLoopStart}-\ref{algEvalLoopLoopEnd}) runs as long as there are constraints for evaluation in the constraint $base$ and no timeout as well as no user cancellation request occur. The (size of the) constraint base changes dynamically during reasoning as Algorithm \ref{algEvalLoop} removes processed constraints, while constraint re-scheduling when values change may add constraints (see Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling} for details). The evaluation loop terminates when all constraints are successfully evaluated. When the constraint evaluation does not converge ($|base|>0$ and does not change over time) or value assignment cycle occur, a timeout (or similarly a user cancellation) will also terminate the evaluation loop, but lead to a failing reasoning result. + +In each iteration of the main loop, the algorithm removes the first constraint for evaluation from $base$ (line \ref{algEvalLoopPop}). % and clears the records about used variables (line \ref{algEvalLoopClear}). Recording used variables is required as detailed information for recording reasoning problems and later for creating the detailed reasoning report (last step of Algorithm \ref{algMainLoop}). +To assign values with the correct assignment state (cf. Section \ref{sectNotationConfigVars}), Algorithm \ref{algEvalLoop} defines the actual assignment state for the current constraint $c$ in line \ref{algEvalLoopAssngState}. If $c$ is a default constraint, all subsequent value assignments during the evaluation of $c$ will happen with state \IVML{DEFAULT}, else state \IVML{DERIVED}. Next, constraint $c$ is evaluated (line \ref{algEvalLoopAssngEval}) by passing it to the constraint evaluator. %If configuration variables are changed as part of the constraint evaluation, the variables are recorded (not shown in Algorithm \ref{algVarChange}) and their constraints are re-scheduled for reasoning (cf. Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}). +Then, the evaluation result is analyzed (still line \ref{algEvalLoopAssngEval}) and, if needed, problem records are created. We distinguish three cases regarding the evaluation results for $c$: \begin{enumerate} - \item Constraint $c$ is evaluated successfully so that either no problem record is created or potentially existing problem records for $c$ from previously failed evaluations can be removed from $\problemRecords$. - \item Constraint $c$ is evaluated as undefined. As specified by IVML~\cite{IVML-LS}, a constraint is also considered undefined, if at least one involved variable or expression is evaluated as undefined. This does not lead to the creation of a problem record, as the constraint can either be ignored or will be re-scheduled if one of the (currently undefined) variables is changed through the evaluation of another constraint. - \item The constraint evaluation fails and a problem record for detailed error reporting or further (external) analysis is created. + \item Constraint $c$ is evaluated successfully so that either no problem record is created or existing problem records for $c$ from previously failed evaluations can be removed from $\problemRecords$. + \item Constraint $c$ is evaluated to undefined. As specified by IVML~\cite{IVML-LS}, a constraint is also considered undefined, if at least one involved variable or expression is evaluated to undefined. This does not lead to the creation of a problem record, as the constraint can either be ignored for now or will be re-scheduled if one of the (currently undefined) variables is changed through the evaluation of another constraint. + \item The constraint evaluation fails and a problem record is created. \end{enumerate} @@ -220,7 +220,7 @@ \SetAlgoLined \KwIn{project $p$} - \KwData{constraint $base$, scope assignments $\scopeAssignments$, problem records $\problemRecords$, relevant constraints $\relevantConstraintsPerDeclaration$, expression evaluator $e$, flags $hasTimeout$ and $stop$} + \KwData{constraint $base$, scope assignments $\scopeAssignments$, problem records $\problemRecords$, relevant constraints $\relevantConstraintsPerDeclaration$, expression evaluator $\evaluator$, flags $hasTimeout$ and $stop$} - $clearAssignments(\scopeAssignments)$\; \label{algEvalLoopClearScope}%clearScopeAssignment + $clearAssignments(\scopeAssignments, p)$\; \label{algEvalLoopClearScope}%clearScopeAssignment %$setDispatchScope(e, p)$\; \label{algEvalLoopDispatchScope}%evaluator.setDispatchScope \While {$|base| > 0 \wedge \neg hasTimeout \wedge \neg stop$} { \label{algEvalLoopLoopStart} @@ -228,7 +228,7 @@ $setAssignmentScope(\scopeAssignments, c)$\; \label{algEvalLoopSetScope} %$\usedVariables \assng \emptySet$\; \label{algEvalLoopClear} - $setAssignmentState(e, \isDefaultConstraint{c})$\; \label{algEvalLoopAssngState} - $analyzeEvaluationResult(\problemRecords, evaluate(e, c))$\; \label{algEvalLoopAssngEval} - \If{$constraintFulfilled(e) \wedge \isDefaultConstraint{c}$}{\label{algEvalLoopClearStart} + $setAssignmentState(\evaluator, \isDefaultConstraint{c})$\; \label{algEvalLoopAssngState} + $analyzeEvaluationResult(\problemRecords, evaluate(\evaluator, c))$\; \label{algEvalLoopAssngEval} + \If{$constraintFulfilled(\evaluator) \wedge \isDefaultConstraint{c}$}{\label{algEvalLoopClearStart} $\relevantConstraintsPerDeclaration \assng \relevantConstraintsPerDeclaration \cap \setWith{\mapEntry{v}{c}}{v\in var(c)}$\; }\label{algEvalLoopClearEnd} @@ -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 from $\relevantConstraintsPerDeclaration$, the mapping between variable declarations and constraints in lines \ref{algEvalLoopClearStart}-\ref{algEvalLoopClearEnd}. Please note that no modification of $\relevantConstraintVariables$, the mapping between decision variables and constraints, is needed, as no change of constraint variables or their values occurred here. - -Finally, Algorithm \ref{algEvalLoop} checks for a potential timeout in line \ref{algEvalLoopTimeout} comparing the global $startTime$ set in Algorithm \ref{algMainLoop} with a configured reasoning timeout. If a timeout occurred (not further detailed in this document), the global $hasTimeout$ flag is set to $true$. This flag is also relevant for creating the overall reasoning report as explained for Algorithm \ref{algMainLoop}. +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. + +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$.