Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 44) +++ /reasoner/reasoner.tex (revision 45) @@ -7,4 +7,5 @@ \newcommand\TBD[1]{{\color{blue}TBD: #1}} \newcommand\MISSING[1]{{\color{red}MISSING: #1}} +\newcommand\class[1]{\texttt{#1}} \newcommand\IVML[1]{\texttt{#1}} \newcommand\IVMLself[0]{\texttt{self}} @@ -81,11 +82,13 @@ \subsection{General notation} -As usual, we denote a set of elements by $s=\set{1, 2, ...}$ with no duplicates allowed (and \setEmpty as the empty set). We write the derivation of a set based on another set by $s_1=\setWith{i+1}{i\in s}$, i.e., $s_1$ is derived from $s$ by iterating over all elements $i$ in $s$ and deriving new values for each $i$ through $i+1$. We use the part after the \setSepText to indicate the set to take the elements from (possibly including conditions), while the part before the \setSepText indicates how to derive new set elements from the existing ones. $s_2 = s \cup s_1$ denotes the union of the two sets $s$ and $s_1$, i.e., $s_2$ contains all elements from $s_1$ and $s_2$ without duplicates (and the sequence of elements does not matter). - -For some parts of the reasoning algorithm, in particular to prioritize constraint types, we need sequences, i.e., structures that contain elements in the order given by inserting the elements and potentially containing duplicates. We denote a sequence by $q=\seq{2, 1, ...}$ and \seqEmpty as the empty sequence. Akin to sets, the derivation of a sequence from another sequence preserving the order of elements in the originating sequence by $q_1=\seqWith{i+1}{i \in q}$. We denote the sequence concatenation as $q_2=q \addSeq q_1$, i.e., $q_2$ contains all elements in $q$ and $q_1$ including duplicates with the elements of $q$ preceding the elements of $q_1$ in the original sequences as given in $q$ and $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ as a sequence concatenation that omits duplicates. - -Further, we denote the undefined value by $\undef$. If not indicated otherwise, all operations introduced below that are bound to a certain type, e.g., an IVML compound, return $\undef$ if the operation is used with another type, e.g., an IVML basic type. - -For individual algorithms, we indicate and use the actual name as used in the implementation to ease mapping from code to algorithms and back. Further, we use parameters and return values in the fashion the implementation does and indicate access to class or instance attributes in the`data' section of the algorithm descriptions. For ease of reading, we ignore here that elements or results of functions in the actual implementation may be a null pointer implying respective checks. Thus, we simply assume here that unless stated otherwise functions either return $\undef$ or, in case of set or sets or sequences $\setEmpty$ or $\seqEmpty$, respectively. +As usual, we denote a \emph{set} of elements by $s=\set{1, 2, ...}$ with no duplicates allowed (and \setEmpty as the empty set). We write the derivation of a set based on another set by $s_1=\setWith{i+1}{i\in s}$, i.e., $s_1$ is derived from $s$ by iterating over all elements $i$ in $s$ and deriving new values for each $i$ through $i+1$. We use the part after the \setSepText to indicate the set to take the elements from (possibly including conditions), while the part before the \setSepText indicates how to derive new set elements from the existing ones. $s_2 = s \cup s_1$ denotes the union of the two sets $s$ and $s_1$, i.e., $s_2$ contains all elements from $s_1$ and $s_2$ without duplicates (and the sequence of elements does not matter). + +For some parts of the reasoning algorithm, in particular to prioritize constraint types, we need \emph{sequences}, i.e., structures that contain elements in the order given by inserting the elements and potentially containing duplicates. We denote a sequence by $q=\seq{2, 1, ...}$ and \seqEmpty as the empty sequence. Akin to sets, the derivation of a sequence from another sequence preserving the order of elements in the originating sequence by $q_1=\seqWith{i+1}{i \in q}$. We denote the sequence concatenation as $q_2=q \addSeq q_1$, i.e., $q_2$ contains all elements in $q$ and $q_1$ including duplicates with the elements of $q$ preceding the elements of $q_1$ in the original sequences as given in $q$ and $q_1$. Moreover, we use $q_3=q \addSeqNoDupl q_d$ as a sequence concatenation that omits duplicates. + +We also want to express that a \emph{mapping} from a certain key to a value is recorded, retrieved and used in some algorithms. We simply denote such a map as a set of entries $\mapEntry{k}{v}$ relating a key $k$ to a value $v$. As key-value pairs are unique within a mapping, in particular there is only one mapping for a certain key, using a set of such entries is reasonable. We denote adding an entry to a map by $m \assng m \cup \set{\mapEntry{k}{v}}$, assuming that an existing entry for $k$ (accessed by $m[k]$) is overridden by the new entry. If there is no mapping for a certain key, $m[k]$ will return undefined denoted by $\undef$. Iterating over a map means iterating over the entries of a map. + +In general, we use $\undef$ to denote an \emph{undefined result/value}. If not indicated otherwise, all operations introduced below that are bound to a certain type, e.g., an IVML compound, return $\undef$ if the operation is used with another type, e.g., an IVML basic type. + +For individual \emph{algorithms}, we indicate and use the actual name as used in the implementation to ease mapping from code to algorithms and back. Further, we use parameters and return values in the fashion the implementation does and indicate access to class or instance attributes in the`data' section of the algorithm descriptions. For ease of reading, we ignore here that elements or results of functions in the actual implementation may be a null pointer implying respective checks. Thus, we simply assume here that unless stated otherwise functions either return $\undef$ or, in case of set or sets or sequences $\setEmpty$ or $\seqEmpty$, respectively. \subsection{IVML elements} @@ -252,101 +255,27 @@ \newcommand\relevantConstraints[0]{r_t} -The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), translates the constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes. - -For IVML, the reasoner must take the structure of IVML models into account, i.e., in particular IVML projects. An IVML projects constitutes a reasoning scopes, i.e., no duplicated variable assignment must occur within a project. Moreover, a project acts as search space for dynamic dispatch of user-defined operations. The main reasoning loop over the involved IVML projects for a given configuration $cfg$ is shown in Algorithm \ref{algMainLoop}. - -Relevant IVML projects are identified throgh the (potentially cyclic) import structure performing a depth-first search starting with the top-level project of a configuration. $discoverProjects(cfg)$ returns a sequence of IVML projects for $cfg$ listing the projects with less import dependencies first. Following this sequence, Algorithm \ref{algMainLoop} first clears the actual variable mapping $\variableMapping$ as its scope is for a single project. Then, it identifies and translates the constraints in the respective project\footnote{Most of the translation commands in this algorithm can be executed through a single loop, more specifically an IVML model visitor.}. To separate and prioritize the constraints, the reasoner uses several global sets, which are composed into the constraint based before constraint evaluation, namely the set of - -\begin{enumerate} - \item Default constraints $\defaultConstraints$ containing constraints setting the default values. - \item Deferred default constraints $\deferredDefaultConstraints$ containing default initialization constraints to be evaluated after all constraints in $\defaultConstraints$ but before the other usual constraints in $\topLevelConstraints$ and $\otherConstraints$. - \item Top level constraints and derived type constraints $\topLevelConstraints$ - \item Remaining usual constraints including compound types used in containers, constraint variables, compound type constraints, compound eval constraints, constraintVariableConstraints, default annotation constraints and assigned annotation constraints $\otherConstraints$. -\end{enumerate} -Further, the algorithm maintains a global variable mapping $\variableMapping$, a map of already processed variables to accessors so that later processed complex expressions can be substituted with the correct accessors. - -The constraints are appended to the constraint $base$ in this sequence to ensure that variables are properly initialized before other constraints are considered. We will discuss the relevant expressions, constraints and their transformations in detail in Section \ref{sectConstraintTranslation}. - -Following this sequence, the $evaluateConstraints$ function (cf. Algorithm \ref{algEvalLoop}) evaluates each constraint in $base$ in sequence until no more (failing) constraints are available. 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}. Finally, the main reasoning algorithm composes a structured reasoning result based on persisting recorded evaluation problems. - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{configuration $cfg$, incremental $inc$, \TBD{consider frozen}} - \KwData{problem records $m$, relevant constraints $\relevantConstraints$ \TBD{$t$??}} +The reasoner performs forward reasoning, i.e., it identifies relevant constraints (according to the reasoning mode), translates the constraints, evaluates them in a loop until all constraints are processed and adjusts/extends the constraint set upon variable value changes. This section introduces the top-level reasoning algorithms, while the constraint translation will be discussed in detailed in Section \ref{sectTranslation}. + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{configuration $cfg$} + \KwData{problem records $m$, global flags $hasTimeout$ and $stop$} \KwResult{Reasoning result $r$} - $projects \assng discoverImports(cfg)$\; - \ForAll{$p \iterAssng projects \wedge \neg hasTimeout \wedge \neg stop$}{ + $projects \assng discoverImports(cfg)$\; \label{algMainLoopDiscover} + \ForAll{$p \iterAssng projects \wedge \neg hasTimeout \wedge \neg stop$}{ \label{algMainLoopStart} %evaluator.init()\; %evaluator.setResolutionListener(Algorithm \ref{algVarChange})\; %evaluator.setScopeAssignments(sAssng)\; - $translateConstraints(p, t, inc)$\; - $evaluateConstraints(p, base)$\; - $freeze(p)$\; - } - $r \assng createReasoningResult(m)$\; + $translateConstraints(p)$\; \label{algMainLoopTranslate} + $evaluateConstraints(p)$\; \label{algMainLoopEvaluate} + $freeze(p)$\; \label{algMainLoopFreeze} + } \label{algMainLoopEnd} + $r \assng createReasoningResult(m)$\; \label{algMainLoopResult} \caption{Main reasoning loop (\IVML{resolve}).}\label{algMainLoop} \end{algorithm} -The main constraint evaluation loop ($evaluate(p, base)$) is summarized in Algorithm \ref{algEvalLoop}. It heavily relies on the IVML constraint evaluation mechanism, an expression evaluator for IVML expressions based on a given IVML configuration. - -First, the main constraint evaluation loop clears recorded information about the assignments done so far so that the actual scope $p$ is clear. Then it sets the scope for dynamic dispatch of user-defined IVML operations. The algorithm runs as long as there are constraints in the constraint $base$, assuming that the evaluation either terminates as all constraints are successfully evaluated (and value changes may add new constraints, cf. Algorithm \ref{algVarChange}) or constraints fail and do not add further constraints. For each iteration, the algorithm pops a constraint for evaluation from $base$ and clears the records about used variables. Then it sets the actual assignment state of the constraint evaluator. If $c$ is a default constraint, this causes that the subsequent value assignments during the evaluation of $c$ -are done with state \IVML{DEFAULT}, else state \IVML{DERIVED}. - -Finally, each constraint is evaluated. If configuration variables are changed as part of the constraint evaluation, the changed variables are recorded in $u$ (not shown in Algorithm \ref{algVarChange}). Finally, the evaluation result is analyzed and may lead to further problem records, e.g., duplicate variable assignments etc. Here, we distinguish three cases. -\begin{enumerate} - \item The constraint is evaluated successfully so that existing problem records can be removed from $m$. - \item The constraint is evaluated as undefined. As defined by IVML, a constraint for which not all variables or expressions can be evaluated, is considered undefined, but evaluated. This does not lead to a problem record, as the constraint can either be ignored or will be re-scheduled if one of the (undefined) variables is changed through another constraint. - \item The constraint evaluation fails and a problem record is created including the used variables $u$ for detailed error reporting or further (external) analysis. -\end{enumerate} - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{project $p$, constraint $base$} - \KwData{scope assignments $a$, problem records $m$, used variables $u$, constraint evaluator $e$, flags $hasTimeout$ $stop$} - - $clearScopeAssignments(a)$\; - $setDispatchScope(e, p)$\; %evaluator.setDispatchScope - \While {$|base| > 0 \wedge \neg hasTimeout \wedge \neg stop$} { - $c \assng pop(base)$\; - $clear(u)$\; - $setAssignmentState(e, isDefault(c))$\; - $m \assng m \addSeq analyzeEvaluationResult(evaluate(e, c), u)$\; - $checkForTimeout()$\; - } - \caption{Constraint evaluation loop (\IVML{evaluateConstraints}).}\label{algEvalLoop} -\end{algorithm} - -When variable $v$ is changed as side effect of a constraint evaluation during reasoning, Algorithm \ref{algVarChange} is called. If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a container operation nor a local variable defined in a let-expression, the change is registered within the actual scope. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then all known constraints (\MISSING{dynamic value changes}) for both, parent and client variables of $v$ are identified. Both, parents and children must be considered, as value in compounds may have impact on both kinds of siblings. These constraints are appended to the constraint $base$, not adding an individual constraint if it is already scheduled in the constraint base. - -\begin{algorithm}[H] - \SetAlgoLined - \KwIn{decision variable $v$} - \KwData{scope assignments $a$, relevant constraints $\relevantConstraints$} - - \If{$\neg isLocal(v)$}{ - $registerScopeAssignment(a, v)$\; - \MISSING{change constraints if dynamic value type changes}\; - $base \assng base \addSeqNoDupl \bigcup_{p\in allParents(v)}t[v]$\; %constraintsForParent - $base \assng base \addSeqNoDupl \bigcup_{c\in alNested(v)}t[v]$\; %constraintsForChilds, nested geht für alle variablen - } - \caption{Adjusting the constraint base (\IVML{notifyChanged}).}\label{algVarChange} -\end{algorithm} - -%----------------------------------------------------------------------------------------------------------------- - -\section{Constraint translation}\label{sectTranslation} - -IVML allows defining default value expressions for all variables including top-level project variables as well as compound slots. From the perspective of IVML and its object model, a default value is part of a variable declaration, i.e., per se not a constraint, i.e., the syntax - -\texttt{Type variable = expression;} - -must be translated into a constraint $variable = expression$. Thereby, constraints defined over the type of the variable, e.g., in case of a derived type must be instantiated for the respective variable. - -The top-level transformation is called by Algorithm \ref{algMainLoop}. It considers all variable declarations and constraints in the given project and executes the following algorithms. - -The constraint translation composes the individual constraint sets into the constraint base and translates missing non-default constraints. This is summarized in Algorithm \ref{algTranslateConstraints}. Here, also the incremental reasoning mode is realized assuming that for incremental reasoning first a full reasoning on the same configuration took place, i.e., possible and propagated values are assigned and variables are frozen. Then, in incremental (runtime) reasoning, just changes on the remaining variables can be validated and respective propagations can be performed. - -First, the various constraint sets are composed starting with default constraints ($\defaultConstraints$) adding then the remaining constraints. After transferring the + +For IVML, 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 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$). 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}) and performs the forward-chaining evaluation of the constraint base, i.e., for $p$, in line \ref{algMainLoopEvaluate}. 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}. \begin{algorithm}[H] @@ -373,4 +302,85 @@ \caption{Translating constraints (\IVML{translateConstraints}).}\label{algTranslateConstraints} \end{algorithm} + +Algorithm \ref{algTranslateConstraints} illustrates the constraint translation. First, this algorithm clears the actual variable mapping $\variableMapping$ as its scope is for a single project. + +\TBD{Here} + + An IVML projects constitutes a reasoning scopes, i.e., no duplicated variable assignment must occur within a project. Moreover, a project acts as search space for dynamic dispatch of user-defined operations. + +Following this sequence, Algorithm \ref{algMainLoop} first clears the actual variable mapping $\variableMapping$ as its scope is for a single project. Then, it identifies and translates the constraints in the respective project\footnote{Most of the translation commands in this algorithm can be executed through a single loop, more specifically an IVML model visitor.}. To separate and prioritize the constraints, the reasoner uses several global sets, which are composed into the constraint based before constraint evaluation, namely the set of + +\begin{enumerate} + \item Default constraints $\defaultConstraints$ containing constraints setting the default values. + \item Deferred default constraints $\deferredDefaultConstraints$ containing default initialization constraints to be evaluated after all constraints in $\defaultConstraints$ but before the other usual constraints in $\topLevelConstraints$ and $\otherConstraints$. + \item Top level constraints and derived type constraints $\topLevelConstraints$ + \item Remaining usual constraints including compound types used in containers, constraint variables, compound type constraints, compound eval constraints, constraintVariableConstraints, default annotation constraints and assigned annotation constraints $\otherConstraints$. +\end{enumerate} +Further, the algorithm maintains a global variable mapping $\variableMapping$, a map of already processed variables to accessors so that later processed complex expressions can be substituted with the correct accessors. + +The constraints are appended to the constraint $base$ in this sequence to ensure that variables are properly initialized before other constraints are considered. We will discuss the relevant expressions, constraints and their transformations in detail in Section \ref{sectConstraintTranslation}. + + +The main constraint evaluation loop ($evaluate(p, base)$) is summarized in Algorithm \ref{algEvalLoop}. It heavily relies on the IVML constraint evaluation mechanism, an expression evaluator for IVML expressions based on a given IVML configuration. + +First, the main constraint evaluation loop clears recorded information about the assignments done so far so that the actual scope $p$ is clear. Then it sets the scope for dynamic dispatch of user-defined IVML operations. The algorithm runs as long as there are constraints in the constraint $base$, assuming that the evaluation either terminates as all constraints are successfully evaluated (and value changes may add new constraints, cf. Algorithm \ref{algVarChange}) or constraints fail and do not add further constraints. For each iteration, the algorithm pops a constraint for evaluation from $base$ and clears the records about used variables. Then it sets the actual assignment state of the constraint evaluator. If $c$ is a default constraint, this causes that the subsequent value assignments during the evaluation of $c$ +are done with state \IVML{DEFAULT}, else state \IVML{DERIVED}. + +Finally, each constraint is evaluated. If configuration variables are changed as part of the constraint evaluation, the changed variables are recorded in $u$ (not shown in Algorithm \ref{algVarChange}). Finally, the evaluation result is analyzed and may lead to further problem records, e.g., duplicate variable assignments etc. Here, we distinguish three cases. +\begin{enumerate} + \item The constraint is evaluated successfully so that existing problem records can be removed from $m$. + \item The constraint is evaluated as undefined. As defined by IVML, a constraint for which not all variables or expressions can be evaluated, is considered undefined, but evaluated. This does not lead to a problem record, as the constraint can either be ignored or will be re-scheduled if one of the (undefined) variables is changed through another constraint. + \item The constraint evaluation fails and a problem record is created including the used variables $u$ for detailed error reporting or further (external) analysis. +\end{enumerate} + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{project $p$, constraint $base$} + \KwData{scope assignments $a$, problem records $m$, used variables $u$, constraint evaluator $e$, flags $hasTimeout$ $stop$} + + $clearScopeAssignments(a)$\; + $setDispatchScope(e, p)$\; %evaluator.setDispatchScope + \While {$|base| > 0 \wedge \neg hasTimeout \wedge \neg stop$} { + $c \assng pop(base)$\; + $clear(u)$\; + $setAssignmentState(e, isDefault(c))$\; + $m \assng m \addSeq analyzeEvaluationResult(evaluate(e, c), u)$\; + $checkForTimeout()$\; + } + \caption{Constraint evaluation loop (\IVML{evaluateConstraints}).}\label{algEvalLoop} +\end{algorithm} + +When variable $v$ is changed as side effect of a constraint evaluation during reasoning, Algorithm \ref{algVarChange} is called. If the changed variable is not local, i.e., neither a parameter of a user-defined function, an iterator of a container operation nor a local variable defined in a let-expression, the change is registered within the actual scope. This scope information is used by the evaluator prior to a variable assignment to check for illegal duplicate assignments within the same scope. Then all known constraints (\MISSING{dynamic value changes}) for both, parent and client variables of $v$ are identified. Both, parents and children must be considered, as value in compounds may have impact on both kinds of siblings. These constraints are appended to the constraint $base$, not adding an individual constraint if it is already scheduled in the constraint base. + +\begin{algorithm}[H] + \SetAlgoLined + \KwIn{decision variable $v$} + \KwData{scope assignments $a$, relevant constraints $\relevantConstraints$} + + \If{$\neg isLocal(v)$}{ + $registerScopeAssignment(a, v)$\; + \MISSING{change constraints if dynamic value type changes}\; + $base \assng base \addSeqNoDupl \bigcup_{p\in allParents(v)}t[v]$\; %constraintsForParent + $base \assng base \addSeqNoDupl \bigcup_{c\in alNested(v)}t[v]$\; %constraintsForChilds, nested geht für alle variablen + } + \caption{Adjusting the constraint base (\IVML{notifyChanged}).}\label{algVarChange} +\end{algorithm} + +%----------------------------------------------------------------------------------------------------------------- + +\section{Constraint translation}\label{sectTranslation} + +IVML allows defining default value expressions for all variables including top-level project variables as well as compound slots. From the perspective of IVML and its object model, a default value is part of a variable declaration, i.e., per se not a constraint, i.e., the syntax + +\texttt{Type variable = expression;} + +must be translated into a constraint $variable = expression$. Thereby, constraints defined over the type of the variable, e.g., in case of a derived type must be instantiated for the respective variable. + +The top-level transformation is called by Algorithm \ref{algMainLoop}. It considers all variable declarations and constraints in the given project and executes the following algorithms. + +The constraint translation composes the individual constraint sets into the constraint base and translates missing non-default constraints. This is summarized in Algorithm \ref{algTranslateConstraints}. Here, also the incremental reasoning mode is realized assuming that for incremental reasoning first a full reasoning on the same configuration took place, i.e., possible and propagated values are assigned and variables are frozen. Then, in incremental (runtime) reasoning, just changes on the remaining variables can be validated and respective propagations can be performed. + +First, the various constraint sets are composed starting with default constraints ($\defaultConstraints$) adding then the remaining constraints. After transferring the +