Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 45) +++ /reasoner/reasoner.tex (revision 46) @@ -64,5 +64,9 @@ Over the last years, we approached the analysis and reasoning for IVML from different perspectives, including traditional reasoning mechanisms or rule engines \cite{QMD42}. Although these mechanisms are powerful in their own respect and typically available as implementation, using them for IVML requires translating an IVML model and its constraints into the model of the respective mechanism and executing that mechanism on the translated model. While traditional reasoners allow for completing the model through feasible ground instances, they typically also perform a kind of constrained state space evaluation. Considering the size of usual configuration models (currently the largest IVML model we are aware of has more than 16.000 variables), just applying a traditional reasoner to usual IVML models is an inefficient approach. Other related mechanisms such as rule engines can be applied to some degree, however, according to our experience \cite{EichelbergerQinSizonenko+16, QMD42, QMD43} lead to a significant and infeasible runtime overhead. Moreover, these both kinds of approaches are limited as they typically do not directly support the breadth of OCL operations, in particular container iterators, quantifiers and user-defined constraint operations. In contrast, specific reasoning approaches, e.g., for OWL partially support quantification, but are similarly limited. Moreover, relying on OCL reasoning mechanisms could be a feasible approach, but would require significant extension to enable value propagation and IVML-specific operations. -Due to these experiences, we decided to realize a \emph{mixed reasoning approach}, which attempts to reduce / simplify the reasoning problem towards an instance that (if needed) can finally be handled by a traditional reasoning approach. The basis is \emph{forward-chaining}, i.e., evaluation of a given constraint set as long as no constraints are left over, while re-scheduling constraints attached to a variable if the variable changes during reasoning. It is important to notice that IVML \cite{IVML-LS} supports a declarative specification of constraints, i.e., they can be given regardless of their actual evaluation sequence. To ensure that values are uniquely determined, IVML allows changing the value of a constraint only once within a project scope, otherwise requiring that a reasoning mechanism issues an error. Thus, reasoning must happen project-wise, in a depth-first traversal along the project import dependencies. Moreover, to speed up reasoning in certain cases, some form of squence of the constraints can be indicated through eval-blocks within a project, i.e., (nested) blocks containing constraints. Here the rule is that a project is considered as the outermost eval-scope, then eval-blocks are evaluated in their nesting sequence (whereby eval-blocks on the same nesting level do not imply any sequence). Based on our experience (and the specific requirements of default-value logic, project scopes, eval-block scopes), the reasoning mechanism shall directly operate on an IVML model instead of performing a model transformation first. However, as constraints in IVML can be attached to types (to increase consistency and to avoid repeated constraints), first a constraint transformation is needed, which instantiates constraints towards variables and their respective types. Then, forward-chaining is executed on this constraint base. Extending approaches may continue on a the result of a failed reasoning through forward-execution. +Due to these experiences, we decided to realize a \emph{mixed reasoning approach}, which attempts to reduce / simplify the reasoning problem towards an instance that (if needed) can finally be handled by a traditional reasoning approach. The basis is \emph{forward-chaining}, i.e., evaluation of a given constraint set as long as no constraints are left over, while re-scheduling constraints attached to a variable if the variable changes during reasoning. It is important to notice that IVML \cite{IVML-LS} supports a declarative specification of constraints, i.e., they can be given regardless of their actual evaluation sequence. To ensure that values are uniquely determined, IVML allows changing the value of a constraint only once within a project scope, otherwise requiring that a reasoning mechanism issues an error. Thus, reasoning must happen project-wise, in a depth-first traversal along the project import dependencies. Moreover, to speed up reasoning in certain cases, some form of sequence of the constraints can be indicated through eval-blocks within a project, i.e., (nested) blocks containing constraints. Here the rule is that a project is considered as the outermost eval-scope, then eval-blocks are evaluated in their nesting sequence (whereby eval-blocks on the same nesting level do not imply any sequence). + +However, not all IVML constraints can be directly used for reasoning. This is in particular true for constraints defined directly on compound types, or indirectly, through types used within collections. Specifying IVML constraints on types, such as compounds, rather than variables (where applicable) simplifies the model (for a compound such constraints are automatically valid for all instances without explicit quantification), supports consistency and helps reduces the model size and complexity. Such constraints typically utilize local variables defined within the compound including the special pre-defined variable \IVML{self} pointing to the actual compound instance. Cross-references to other types are required to be specified through an explicit accessor, i.e., an expression mentioning the variable and the respective nested variable(s). During reasoning, constraints over types cannot be evaluated, as the actual values are not available. Thus, we perform first a \emph{constraint translation step} to instantiate the constraints for configuration variables based on the actual type of the variable or its value. An alternative here could be reasoning over the type constraints and modifying the mapping on demand before evaluation. This could save memory and runtime (for constraint translation / creation), but, however, increases complexity in managing the actual constraints to be evaluated. So we opted for instantiating the constraints and keeping only the new, failed or recently affected ones in the constraint base. + +Based on our experience \cite{EichelbergerQinSizonenko+16, QMD42, QMD43} and taking into account the specific requirements of default-value logic, project scopes, eval-block scopes), the reasoning mechanism shall directly operate on an IVML model. In particular, model transformations such as the constraint translation shall happen only if required to reduce overhead on the reasoning time. In particular no complete model transformations as we did in previous approaches to maximize reuse of existing reasoning mechanisms is infeasible. After the required constraint translation, constraint evaluation and forward-chaining is executed on this constraint base. As this approach is not reasoning complete (while through construction IVML complete), we can imagine that specific reasoning engines such as SMT could complement the described approach. Therefore, translating the failed constraints into a model that is suitable for sophisticated reasoning approaches could enable advanced capabilities, such as value determination, instance creation or configuration completion / repair. Typically, reasoning over all variables of a project including all constraints is needed. However, in some use cases considering all constraints is not needed and even not efficient with respect to reasoning time. The first case is \emph{incremental reasoning}, i.e., starting with a given (valid) configuration and just analyzing the changes made by the user. The idea is to provide nearly immediate results, so that reasoning even on complex and large models can happen on every change made by the user. The second case is \emph{runtime reasoning}, e.g., reasoning for validity at runtime of a system to identify deviations and to trigger re-configuration or adaptation \cite{Eichelberger16}. For these cases, we introduce two main \emph{reasoning modes}, namely full reasoning and incremental reasoning, while the latter can be achieved through the following two techniques. @@ -86,5 +90,5 @@ 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. +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 \addMap \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. @@ -279,4 +283,8 @@ 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}. +Algorithm \ref{algTranslateConstraints} illustrates the top-level constraint translation. In line \ref{algTranslateConstraintsClearMapping}, algorithm \ref{algTranslateConstraints} clears the actual variable mapping $\variableMapping$. The variable mapping is a core data structure of the constraint translation and specific for the project under translation, i.e., mappings for other already processed projects are not needed. + +From a technical point of view, the variability mapping consists of mapping entries relating a variable declaration with an access expression if needed. For directly accessible variables such as top-level variables directly defined within a project, no such mapping is needed ($\undef$). For variables used in constraints within compounds or containers, an appropriate accessor is needed, created and registered when starting to translate the respective type. The respective constraints for that type are then enumerated, copied and while copying the variables registered in the variable mapping are replaced by the accessor expressions in the mapping. It is important to ensure that the mapping for the respective type is complete before constraint translation, so that all variables including cross references within the same type can be replaced properly. References to other variables are already given as accessor expressions and do not need to be considered here. + \begin{algorithm}[H] \SetAlgoLined @@ -284,5 +292,5 @@ \KwData{constraint $base$ , variable mapping $\variableMapping$} - $\variableMapping \assng \setEmpty$\; % clear + $\variableMapping \assng \setEmpty$\; \label{algTranslateConstraintsClearMapping} %>ConstraintTranslationVisitor \ForAll{$d \iterAssng varDeclarations(p)$}{ %translateDeclarationDefaults @@ -303,11 +311,9 @@ \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. + +Then, 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 \ref{algTranslateConstraints} added to the constraint base. In more details, the reasoner maintains the following constraint sets \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} @@ -320,4 +326,7 @@ 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}. + + + 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.