Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 100) +++ /reasoner/reasoner.tex (revision 101) @@ -1,5 +1,6 @@ -\documentclass[12pt]{article} +\documentclass[11pt]{article} \usepackage[utf8]{inputenc} \usepackage{amsmath} +\usepackage{amssymb} \usepackage{multirow} \usepackage{color} @@ -8,4 +9,6 @@ \usepackage{adjustbox} \usepackage[toc,page]{appendix} +\usepackage{xcolor} +\usepackage{adjustbox} \newcommand\TBD[1]{{\color{blue}TBD: #1}} @@ -48,4 +51,5 @@ \newcommand\tabAlgLines[3]{Alg.\ref{#1},\ref{#2}-\ref{#3}} \newcommand\tabAlgFollow[0]{ $\rightarrow$ } +\newcommand\grayPara[1]{\noindent\adjustbox{bgcolor=gray!20,minipage=[t]{\linewidth}}{#1}\linebreak} \let\emph\relax % there's no \RedeclareTextFontCommand @@ -356,6 +360,4 @@ The main reasoning loop implements the overall control for the IVML reasoning process. First, Algorithm \ref{algMainLoop} sets up\footnote{In the implementation, also the re-scheduling of changed variables (Algorithm \ref{algVarChange} in Section \ref{sectTopLevelConstraintsRescheduling}) and recording assigned variables are registered with the expression evaluator, but this is not shown here.} the expression evaluator in line \ref{algMainLoopSetupEval} for use with the configuration $cfg$ and the scope assignments $\scopeAssignments$. The remainder of the algorithm is separated into two parts, 1) the full execution (lines \ref{algMainLoopFullStart}-\ref{algMainLoopFullEnd}), and 2) the incremental part (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}) utilizing a constraint base prepared and stored while running the first part. - -For IVML, the full execution of the reasoner\footnote{In the implementation, constraint translation and reasoning happens in the class \class{Resolver.java}.} must take the structure of IVML models into account, i.e., in particular IVML projects and their imports. As shown in Algorithm \ref{algMainLoop}, first a structure is created to store constraints for reuse (if $reuse$ is enabled). Then, the relevant IVML projects and their sequence are identified. Therefore, $discoverProjects(cfg)$ (line \ref{algMainLoopDiscover}, not further detailed in this document), performs a depth-first traversal of the import structure, ignores already seen cyclic imports and returns a sequence of all projects involved in $cfg$ according to the increasing number of import dependencies. \begin{algorithm}[H] @@ -392,9 +394,11 @@ \end{algorithm} +For IVML, the full execution of the reasoner\footnote{In the implementation, constraint translation and reasoning happens in the class \class{Resolver.java}.} must take the structure of IVML models into account, i.e., in particular IVML projects and their imports. As shown in Algorithm \ref{algMainLoop}, first a structure is created to store constraints for reuse (if $reuse$ is enabled). Then, the relevant IVML projects and their sequence are identified. Therefore, $discoverProjects(cfg)$ (line \ref{algMainLoopDiscover}, not further detailed in this document), performs a depth-first traversal of the import structure, ignores already seen cyclic imports and returns a sequence of all projects involved in $cfg$ according to the increasing number of import dependencies. + Following this sequence, the main reasoning loop considers all IVML projects for a given configuration $cfg$, as long as no timeout occurred (global flag $hasTimeout$) or the user requested a stop of the reasoning operations (global flag $stop$). Further, the algorithm records the start time in line \ref{algMainLoopStartTime} in order to be able to detect timeouts. For each project $p$, the main loop (lines \ref{algMainLoopStart} - \ref{algMainLoopEnd}) translates the constraints in $p$ (and populates the constraint base as a side effect, line \ref{algMainLoopTranslate} discussed / Section \ref{sectTopLevelConstraintsTranslation}) and performs the forward-chaining evaluation of the constraint base, i.e., for $p$, in line \ref{algMainLoopEvaluate} / Section \ref{sectTopLevelConstraintsEvaluation}. If a constraint changes a configuration variable as a side effect, the constraints related to that variable are re-scheduled for evaluation by Algorithm \ref{algVarChange}. As last step for a project $p$, the algorithm freezes the actual values according to the (conditional) freeze-block specifications in $p$ in line \ref{algMainLoopFreeze}. Finally, after all projects have been considered or the main reasoning loop has been terminated prematurely, the main reasoning algorithm composes\footnote{In the implementation, this step happens in the class \class{Engine.java}, the actual reasoner instance, which utilizes and calls instances of \class{Resolver.java}.} a detailed reasoning result based on persisting recorded evaluation problems in line \ref{algMainLoopResult}. This reasoning result also includes whether a timeout or a user-requested cancellation of the reasoning occurred. -For incremental execution (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}), it is sufficient to take the constraints for the respective project, and, as before, to evaluate the constraints and to freeze the variables. +In incremental execution (lines \ref{algMainLoopIncStart}-\ref{algMainLoopIncEnd}), it is sufficient to take over the constraints for the respective project into the constraint base, and, as before, to evaluate the constraints and to freeze the variables. Before starting an incremental execution, it is necessary to clear global storages required by the implementation (but not detailed here), such as error data structures, counters, etc. \subsection{Variable Mapping}\label{sectVarMapping} @@ -429,6 +433,4 @@ The core idea of the constraint translation is to collect the constraints following the structure of an IVML model. On top level, there are IVML variable declarations, global constraints, annotation assignment blocks and eval-blocks. Type definitions become relevant when processing variable declarations, as the individual type of a variable indicates the specific constraints to be collected and instantiated from type constraints to variable constraints. - -Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. In full reasoning mode ($base_c = \undef$), Algorithm \ref{algTranslateConstraints} shall always be executed. If incremental reasoning based on a re-used constraint base is enabled, then this algorithm shall run only if there is no constraint base copy ($|base_c| = 0$), which is then created at the end of the algorithm. \begin{algorithm}[H] @@ -462,4 +464,6 @@ \end{algorithm} +Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. In full reasoning mode ($base_c = \undef$), Algorithm \ref{algTranslateConstraints} shall always be executed. If incremental reasoning based on a re-used constraint base is enabled, then this algorithm shall run only if there is no constraint base copy ($|base_c| = 0$), which is then created at the end of the algorithm. + The algorithm 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 separate and prioritize the constraints, the reasoner uses several global sets, which are populated independently during the constraint translation and, in Algorithm \ref{algTranslateConstraints} added to the constraint base. In more details, the reasoner maintains the following temporary constraint sets @@ -552,7 +556,15 @@ 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) with default value $deflt$, basically $default(v)$, by adding a qualifying access prefix expression $ca$ and turning it into a default value assignment constraint. + +\grayPara{ +$$ + v \leadsto ca.v = deflt +$$ +} + +As this works in a straight forward manner only for basic IVML types, but a given variable $v$ may also be of compound or container type, Algorithm \ref{algTranslateDeclaration} dispatches further on to the other algorithms constituting the reasoner as discssed in the following sections. + In more detail, Algorithm \ref{algTranslateDeclaration} first declares some local variables in line \ref{algTranslateDeclarationDecl}, including the actual type $t$ (to be overridden by the type of the default value expression if needed), the default value expression $dflt$, the actual set of default constraints ($\defaultConstraints$ or $\deferredDefaultConstraints$) to be utilized for adding the final constraint and the actual value of self $s$ (for compound types only). Then, if $t$ is a derived data type, constraints are translated and collected through Algorithm \ref{algTranslateDerivedDatatypeConstraints}. In non-incremental mode, i.e., we translate default value expressions to assignment constraints as well as the default constraints for annotations can then be translated using \ref{algTranslateAnnotationDeclarations}. Due to potential type interferences with derived types, we determine then the actual type through the type of the default value expression if defined. If $t$ is a compound type, we set the value of self $v$ to the actual variable declaration $d$ and execute the specific translations for compound types using Algorithm \ref{algTranslateCompoundDeclaration}. If $t$ is a container type, we call \ref{algTranslateContainerDeclaration} instead. Otherwise, if there is a default value expression and reasoning is not in incremental mode, i.e., we shall translate default value expressions to assignment constraints, and if there is a compound accessor, we just have to schedule a replacement of \IVML{self} by the compound accessor. Remaining default constraints are taken over as defined as long as the reasoner is not operating incremental mode as there no default value assignments are needed. - -If there is finally a default value expression to be recorded in the constraint base, we have to distinguish whether the actual variable is a constraint variable or an usual variable. In the first case, we apply Algorithm \ref{algCreateConstraintVariableConstraint} (cf. Section \ref{sectConstraintVariables}). In the second case, we turn the default value expression into an assignment expression. However, the accessor creation depends on whether $d$ is an annotation or an usual variable. Then, we substitute \IVML{self} and the actual variable mapping on the complete constraint expression and turn the result into a default constraint. We either either it to $\deferredDefaultConstraints$ if the constraint may override a complete value assignment (\IVML{self} is used referring to another variable in the same compound or $d$ is an overridden slot that may accidentally be overriden by a complex compound value) or in all other cases to the usual default constraints set $\defaultConstraints$. \begin{algorithm}[H] @@ -591,4 +603,6 @@ \caption{Translating declarations (\IVML{translateDeclaration}).}\label{algTranslateDeclaration} \end{algorithm} + +If there is finally a default value expression to be recorded in the constraint base, we have to distinguish whether the actual variable is a constraint variable or an usual variable. In the first case, we apply Algorithm \ref{algCreateConstraintVariableConstraint} (cf. Section \ref{sectConstraintVariables}). In the second case, we turn the default value expression into an assignment expression. However, the accessor creation depends on whether $d$ is an annotation or an usual variable. Then, we substitute \IVML{self} and the actual variable mapping on the complete constraint expression and turn the result into a default constraint. We either either it to $\deferredDefaultConstraints$ if the constraint may override a complete value assignment (\IVML{self} is used referring to another variable in the same compound or $d$ is an overridden slot that may accidentally be overriden by a complex compound value) or in all other cases to the usual default constraints set $\defaultConstraints$. \subsection{Derived types}\label{sectDerivedTypes}