Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 35) +++ /reasoner/reasoner.tex (revision 36) @@ -41,9 +41,9 @@ \section{Introduction} -In Product Line Engineering, a \textit{variability model} defines the options to customize a software system, while a \textit{configuration} specifies the choices made for a specific instance of the software system. Customization options can depend on each other, e.g., the choice made for an option determines, restricts or even excludes the selection for another option. Such dependencies are typically expressed using different forms of \textit{constraints}. For instantiating a software system, a configuration must be valid, i.e., all (relevant) constraints must be fulfilled. To analyze a configuration for validity, for figuring out the number of remaining configuration options or for propagating derivable values, various forms of \textit{reasoning mechanisms} are utilized. Several reasoning mechanisms are available, such as SAT-solving or SMT-reasoners \TBD{cites}. However, expressiveness of the modeling concepts and supported constraints affect the analyzability of the model \TBD{cite-ICSR}, and, thus, also the applicable reasoning mechanism. +In Product Line Engineering, a \textbf{variability model} defines the options to customize a software system, while a \textbf{configuration} specifies the choices made for a specific instance of the software system. Customization options can depend on each other, e.g., the choice made for an option determines, restricts or even excludes the selection for another option. Such dependencies are typically expressed using different forms of \textbf{constraints}. For instantiating a software system, a configuration must be valid, i.e., all (relevant) constraints must be fulfilled. To analyze a configuration for validity, for figuring out the number of remaining configuration options or for propagating derivable values, various forms of \textbf{reasoning mechanisms} are utilized. Several reasoning mechanisms are available, such as SAT-solving or SMT-reasoners \TBD{cites}. However, expressiveness of the modeling concepts and supported constraints affect the analyzability of the model \TBD{cite-ICSR}, and, thus, also the applicable reasoning mechanism. Besides traditional variability modeling approaches, such as feature modeling \TBD{cite} or decision modeling \TBD{cite}, in recent time several approaches to textual variability modeling have been proposed \TBD{cite-STTT}. Moreover, there seems to be a trend that more recent variability modeling support more powerful modeling conceepts \TBD{cite-STTT}, which then require more powerful analysis and reasoning mechanisms. As stated above, typically these mechanisms then imply limitations of the analysis capabilities, e.g., non-Boolean decisions typically prevent determining the actual number of possible configurations (of course not the number of configuration options that remain to be configured to achieve a complete configuration). -The \textit{Integrated Variability Modeling Language (IVML)} \TBD{cite IVML} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system, multiple-inheritance, collection types, configuration references, imports, orthogonal annotations (for binding times), quantification constraints, or user-defined constraint functions. This even allows for topological variability, i.e., configuring and reasoning over graph structures \TBD{cite IVML-topo}. In this document, we discuss the approach and recent state of the reasoning mechanism for IVML and its realization in EASy-Producer \TBD{cite}. Currently, the reasoning mechanism focuses on translating / creating specifically instantiated constraints for the various IVML concepts and on forward-reasoning, i.e., evaluating the constraints and performing value propoagation as much as possible. So far, this allows performing typical validation and propagation tasks +The \textbf{Integrated Variability Modeling Language (IVML)} \TBD{cite IVML} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system, multiple-inheritance, collection types, configuration references, imports, orthogonal annotations (for binding times), quantification constraints, or user-defined constraint functions. This even allows for topological variability, i.e., configuring and reasoning over graph structures \TBD{cite IVML-topo}. In this document, we discuss the approach and recent state of the reasoning mechanism for IVML and its realization in EASy-Producer \TBD{cite}. Currently, the reasoning mechanism focuses on translating / creating specifically instantiated constraints for the various IVML concepts and on forward-reasoning, i.e., evaluating the constraints and performing value propoagation as much as possible. So far, this allows performing typical validation and propagation tasks \TBD{structure}. However, we are aware of the fact that more advanced tasks like configuration completion are not supported by the current approach. This is subject to future work, for which this document shall provide a solid foundation. @@ -52,17 +52,17 @@ \section{Approach}\label{sectApproach} -IVML is a textual variability and configuration modeling language. The syntax of IVML, which is mostly out of scope here (please refer to \TBD{cite} for the complete specification), is based on well known (programming) language concepts to express the (meta-) model of a configuration as well as individual configuration instances. The main concept of IVML is the \textit{typed variable}, which may have a default value expression. For short, IVML offers basic types (Boolean, Integer, Real, String), user-defined compound types (groups of variables, allows multi-inheritance), collection types (set, sequence), derived types (constraining or aliasing another type) and constraint types, i.e. variables holding a constraint so that it can be overridden by assigning a new constraint. IVML variables can be further detailed and interrelated with other variables through constraints. The constraint (expression) language is largely inspired by OCL concepts (and notation), but, in constrast to OCL, allows side-effect to enable the definition of configurations as well as the propagation of configuration values. IVML models (given in terms of projects), can be imported, staged \TBD{cite} and conditionally frozen, in particular to enable partial instantiation of code, including removal of variation points. +IVML is a textual variability and configuration modeling language. The syntax of IVML, which is mostly out of scope here (please refer to \TBD{cite} for the complete specification), is based on well known (programming) language concepts to express the (meta-) model of a configuration as well as individual configuration instances. The main concept of IVML is the \textbf{typed variable}, which may have a default value expression. For short, IVML offers basic types (Boolean, Integer, Real, String), user-defined compound types (groups of variables, allows multi-inheritance), collection types (set, sequence), derived types (constraining or aliasing another type) and constraint types, i.e. variables holding a constraint so that it can be overridden by assigning a new constraint. IVML variables can be further detailed and interrelated with other variables through constraints. The constraint (expression) language is largely inspired by OCL concepts (and notation), but, in constrast to OCL, allows side-effect to enable the definition of configurations as well as the propagation of configuration values. IVML models (given in terms of projects), can be imported, staged \TBD{cite} and conditionally frozen, in particular to enable partial instantiation of code, including removal of variation points. Over the last years, we approached the analysis and reasoning for IVML from different perspectives, including traditional reasoning mechanisms or rule engines \TBD{cite}. 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 \TBD{cite} 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 collection 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 \textit{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 \textit{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. Based on our experience, 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. - -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 \textit{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 \textit{runtime reasoning}, e.g., reasoning for validity at runtime of a system to identify deviations and to trigger re-configuration or adaptation \TBD{cite}. More specifically, we distinguish between incremental reasoning +Due to these experiences, we decided to realize a \textbf{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 \textbf{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. Based on our experience, 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. + +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 \textbf{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 \textbf{runtime reasoning}, e.g., reasoning for validity at runtime of a system to identify deviations and to trigger re-configuration or adaptation \TBD{cite}. More specifically, we distinguish between incremental reasoning \begin{itemize} - \item with \textit{creation of a partial constraint base}. In this incremental mode, certain constraint types such as default-values (\TBD{or constraints for frozen values}) are not added to the constraint base and the related variables are assumed to be properly instantiated through an initial reasoning run. Thus, reasoning focuses on the non-frozen variables, in particular changed variables. In our experiments, this mode can save up to 65\% reasoning time. This mode can be activated through the reasoner configuration. - \item \textit{re-using a previously build constraint base}. Trading off less reasoning time (\TBD{measure effect}) with memory for storing a copy of the constraint base, we require that the underlying project does not change structurally, i.e., no new types or variables are declared between two reasoning steps. This mode can be activated by requesting a re-usable reasoner instance from the EASy reasoner core and using that instance instead of the default interface (the static reasoning frontend). + \item with \textbf{creation of a partial constraint base}. In this incremental mode, certain constraint types such as default-values (\TBD{or constraints for frozen values}) are not added to the constraint base and the related variables are assumed to be properly instantiated through an initial reasoning run. Thus, reasoning focuses on the non-frozen variables, in particular changed variables. In our experiments, this mode can save up to 65\% reasoning time. This mode can be activated through the reasoner configuration. + \item \textbf{re-using a previously build constraint base}. Trading off less reasoning time (\TBD{measure effect}) with memory for storing a copy of the constraint base, we require that the underlying project does not change structurally, i.e., no new types or variables are declared between two reasoning steps. This mode can be activated by requesting a re-usable reasoner instance from the EASy reasoner core and using that instance instead of the default interface (the static reasoning frontend). \end{itemize} -To implement the IVML reasoner, we designed and realized first an \textit{expression evaluation mechanism}, which is able to evaluate individual IVML expressions. This includes constraint expressions (expressions evaluating to a Boolean value) and as special case default value expressions (evaluating to a value that can be assigned to the respective variable). We do not detail the constraint evaluation mechanism further here, rather than focusing on the IVML reasoning mechanism, which relies on the expression evaluation mechanism for evaluating constraints. +To implement the IVML reasoner, we designed and realized first an \textbf{expression evaluation mechanism}, which is able to evaluate individual IVML expressions. This includes constraint expressions (expressions evaluating to a Boolean value) and as special case default value expressions (evaluating to a value that can be assigned to the respective variable). We do not detail the constraint evaluation mechanism further here, rather than focusing on the IVML reasoning mechanism, which relies on the expression evaluation mechanism for evaluating constraints. @@ -82,9 +82,9 @@ In this section, we briefly discuss the various IVML elements and introduce functions to access their respective properties. We focus on functions that are used for specifying the reasoning algorithm rather than all functions defined by the IVML object model. As convention, we use als parameter names $d$ for a variable declaration, $v$ for a configuration variable, $t$ for a type, $val$ for a value and $cfg$ for a configuration consting of decision variables. For temporary/local variables, we use names close by, e.g., $s$ for an iterator variable used for a set of types. -For all \textit{IVML elements}, we denote $constraints(e)$ as the set of constraints defined for element $e$. Let $s$ be a set of elements, then $constraints(s) = \setWith{constraints(t)}{t\in s}$. - -An IVML\textit{variable declaration} $d$ introduces a configuration variable with $name(d)$ and $type(d)$. $annotations(d)$ is the set of (orthogonal) IVML annotation (variable) declarations for a variable declaration $d$. $default(d)$ is an expression specifying the default value of $d$ ($default(d)$ must evaluate to a type compatible with $type(d)$). Moreover, $parent(d)$ is the model element the declaration $d$ is nested within, typically, a compound or a project. - -An IVML \textit{configuration variable} $v$ is an instance of a variable declaration $d$ as part of a certain configuration $cfg$, i.e., $decision(cfg, d)=v$. For such a combination of declaration $d$ and variable $v$, we define $declaration(v) = d$ as well as $type(v) = type(declaration(v))$. For a variable $v$, the function $isVariable(v)$ returns $true$, else $false$. Let $value(v)$ be the actual value of $v$, with $type(value(v))$ compliant with $type(v)$. As types like container or compound require a nesting of configuration variables, we define generically $nested(v)$ as the set of all variables nested in $v$ (may be empty). Similarly, we define $parent(v)$ as the object $v$ is nested within, which is either the containing configuration in case of a top-level variable or a variable, i.e., $\forall_{n\in nested(v)}:parent(n)=v$. Akin to variable declarations, $annotations(v)$ returns the set of actual annotation variables for variable $v$. Please note that there is a significant difference between $annotations(d)$ for a variable declaration $d$ and $annotations(decision(cfg,d))$, as a declaration only holds the specifically declared attributes for $d$, while a variable is instantiated with all annotations applied to the containing project or variables (in case of compounds or collections). Further, we define two derived helper functions +For all \textbf{IVML elements}, we denote $constraints(e)$ as the set of constraints defined for element $e$. Let $s$ be a set of elements, then $constraints(s) = \setWith{constraints(t)}{t\in s}$. + +An IVML\textbf{variable declaration} $d$ introduces a configuration variable with $name(d)$ and $type(d)$. $annotations(d)$ is the set of (orthogonal) IVML annotation (variable) declarations for a variable declaration $d$. $default(d)$ is an expression specifying the default value of $d$ ($default(d)$ must evaluate to a type compatible with $type(d)$). Moreover, $parent(d)$ is the model element the declaration $d$ is nested within, typically, a compound or a project. + +An IVML \textbf{configuration variable} $v$ is an instance of a variable declaration $d$ as part of a certain configuration $cfg$, i.e., $decision(cfg, d)=v$. For such a combination of declaration $d$ and variable $v$, we define $declaration(v) = d$ as well as $type(v) = type(declaration(v))$. For a variable $v$, the function $isVariable(v)$ returns $true$, else $false$. Let $value(v)$ be the actual value of $v$, with $type(value(v))$ compliant with $type(v)$. As types like container or compound require a nesting of configuration variables, we define generically $nested(v)$ as the set of all variables nested in $v$ (may be empty). Similarly, we define $parent(v)$ as the object $v$ is nested within, which is either the containing configuration in case of a top-level variable or a variable, i.e., $\forall_{n\in nested(v)}:parent(n)=v$. Akin to variable declarations, $annotations(v)$ returns the set of actual annotation variables for variable $v$. Please note that there is a significant difference between $annotations(d)$ for a variable declaration $d$ and $annotations(decision(cfg,d))$, as a declaration only holds the specifically declared attributes for $d$, while a variable is instantiated with all annotations applied to the containing project or variables (in case of compounds or collections). Further, we define two derived functions $$allNested(v) = \begin{cases}\set{}, & \text{if } |nested(v)| = 0 \\ \set{nested(v)} \cup \setWith{allNested(w)}{w\in nested(v)}, & \text{else}\\ \end{cases}$$ @@ -92,21 +92,30 @@ $$allParents(v) = \begin{cases}\set{}, & \text{if } \neg isVariable(parent(v)) \\ \set{parent(v)} \cup allParents(parent(v)), & \text{else}\\ \end{cases}$$ +A \textbf{project} is a named scope, which can contain variable declarations, type declarations, assignment blocks and eval blocks. $varDeclarations(p)$ the set of all variable declarations in project $p$. $assignments(p)$ is the potentially nested set of annotation assignments of project $p$, i.e., if $e\in assignments(p)$ then $varDeclarations(e)$ as well as $constraints(e)$ is defined, but may be empty, similarly for $assignments(e)$. $f \in assignmentData(a)$ for an assignment $a$ provides access to the name of the attribute $name(f)$ and the default value expression $default(f)$ specifying the value to be assigned to the attribute with $name(f)$. Moreover, $evals(p)$ is the potentially nested set of eval-blocks in project $p$, i.e., if $e\in evals(p)$ then $constraints(e)$ is defined, but may be empty, similarly for $evals(e)$. + +A \textbf{compound} is an IVML type, which consists of variable declarations, called slots. Let $t$ be a compound type, then $isCompound(t)$ returns $true$. All slots of a compound $t$ can be accessed through $slots(t)$. Akin to a variable declaration, for a slot $s$ $name(s)$, $default(s)$ and $type(s)$ are defined. Moreover, let $v$ be a compound variable, i.e., a variable of a compound type, then $decision(v, s)$ returns the variable related to slot $s$. $refines(t)$ is the set of compound types directly refined by \TBD{refining?} compound $t$, returning an empty set if there are no such compounds or if $t$ is not a compound type. Assignments $assignments(t)$ is defined for a compound type akin to $assignments(p)$ for a project $p$. Further, we define the following derived functions + +$$inheritedSlots(t) = \setWith{slots(r)}{r\in allRefines^+(t)}$$ + +$$dfltSlots(v) = \setWith{s}{s\in slots(v) \wedge default(s) \neq \undef}$$ %, compound slots of $v$ having default value expressions, empty for all non-compound types + +$$allRefines(t) = \begin{cases}\emptySet, & \text{if } refines(t) = \emptySet \\ allRefines(t) \cup \bigcup_{u\in refines(t)} allRefines(u), & \text{else}\\ \end{cases}$$ + +$$allRefines^+(t) = \begin{cases}allRefines(t) \cup \set{t}, & \text{if } isCompound(t) \\ \emptySet, & \text{else} \\ \end{cases}$$ + +$$parentCompound(d) = \begin{cases} parent(d), & \text{if } parent(d) \neq \undef \wedge{} isCompound(parent(d)) \\ parentCompound(parent(d)), & \text{if } parent(d) \neq \undef \\ \undef, & \text{else}\end{cases}$$ + +$$isOverridden(d) = d \in \setWith{slots(r)}{r\in allRefines(parentCompound(d))}$$ + + +\textbf{collections}... + + +An access expression specifies slots (within a compound variable or through references) or elements (within a collection) to be accessed. In IVML, an accessor looks like: \IVML{cmp.slot}, \IVML{cmp.slot1.slot2}, \IVML{coll[1]}, \IVML{coll[1].slot}. + \begin{itemize} - \item compound - \begin{itemize} - \item $decision(v, s)$ returns the decision variable related to the nested slot $s$ of a compound variable $v$ - \item $isCompound(t)$, $isContainer(t)$, $isConstraint(t)$, $isConstraintContainer(t) = isNested(t) \wedge isConstraint(nestedType(t))$ - \item $name(s)$ is the name of slot $s$ - \item $default(s)$ is the default value expression of slot $s$ - \item $refines(t)$ is the set of compounds directly refining compound $t$, if there are none or $t$ is not a compound $refines(t)=\emptySet$, $slots(t)$ the set of slots of a compound (nested variable declarations),$assignments(t)$ the potentially nested set of annotation assignments, i.e., if $a\in assignments(t)$ then $constraints(a)$ is defined, but may be empty, similarly for $assignments(a)$. Analogously, $evals(t)$ is defined. $inheritedSlots(t) = \setWith{slots(r)}{r\in allRefines^+(t)}$. - \item An access expression specifies slots (within compounds or behind references) or elements (within a collection) to be accessed. Examples: \IVML{cmp.slot}, \IVML{cmp.slot1.slot2}, \IVML{coll[1]}, \IVML{coll[1].slot}. - \item $dfltSlots(v) = \setWith{s}{s\in slots(v) \wedge default(s) \neq \undef}$, compound slots of $v$ having default value expressions, empty for all non-compound types - \item $allRefines(t) = \begin{cases}\emptySet, & \text{if } refines(t) = \emptySet \\ allRefines(t) \cup \bigcup_{u\in refines(t)} allRefines(u), & \text{else}\\ \end{cases}$ - \item $allRefines^+(t) = \begin{cases}allRefines(t) \cup \set{t}, & \text{if } isCompound(t) \\ \emptySet, & \text{else} \\ \end{cases}$ - \item $parentCompound(d) = \begin{cases} parent(d), & \text{if } parent(d) \neq \undef \wedge{} isCompound(parent(d)) \\ parentCompound(parent(d)), & \text{if } parent(d) \neq \undef \\ \undef, & \text{else}\end{cases}$ - \item $isOverridden(d) = d \in \setWith{slots(r)}{r\in allRefines(parentCompound(d))}$ - \end{itemize} \item collections \begin{itemize} + \item $isContainer(t)$, $isConstraint(t)$, $isConstraintContainer(t) = isNested(t) \wedge isConstraint(nestedType(t))$ \item $elements(c)$ is the set of all element values in a collection \item $isNested(c)$ whether a collection is a nested collection and $nestedType(c)$ is the (innermost) nested type @@ -125,9 +134,4 @@ \item A constraint is a boolean expression that requires to be evaluated to \IVML{true}. Creating a constraint through OCL function call notation in angle brackets, e.g., $\createConstraint{\IVML{assign}(x, 25)}$ represents the IVML constraint \IVML{x = 25;} (knowing that the assignment IVML assignment operation returns a boolean value indicating its success). If the constraint is marked as a default constraint, then we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$, if it is an internal \TBD{clarify semantics }constraint for reasoning we use $\createInternalConstraint{\IVML{assign}(x, 25)}$. We indicate IVML operations in teletype font. We denote a partial expression for incrementally building a constraint by $createExpression{expr}$ and indicate IVML meta operations for creating expression parts as follows: $\createExpression{\IVMLMeta{var}(i, t)}$ creates a temporary variable $i$ of type $t$. $\createExpression{\IVMLMeta{acc}(c, s)}$ creates an accessor $c.s$, e.g., to access slot $s$ on compound $c$ (implicitly requiring $isCompound(c) \wedge s\in slots(c)$). \item $isAssignmentConstraint(c)$ whether constraint $c$ is of form \IVML{assign(v, e)} with $v$ variable and $e$ expression - \end{itemize} - \item project - \begin{itemize} - \item $evals(p)$ the potentially nested set of annotation assignments of project $p$, i.e., if $e\in assignments(p)$ then $constraints(e)$ is defined, but may be empty, similarly for $assignments(e)$. $d \in assignmentData(a)$ for an assignment $a$ provides access to the name of the attribute $name(d)$ and the default value expression $default(a)$ specifying the value to be assigned to the attribute with $name(a)$. - \item $varDeclarations(p)$ the set of all variable declarations in project $p$ \end{itemize} \end{itemize}