Index: /reasoner/introduction.tex =================================================================== --- /reasoner/introduction.tex (revision 182) +++ /reasoner/introduction.tex (revision 183) @@ -1,18 +1,18 @@ \section{Introduction} -In Product Line Engineering, a \emph{variability model} defines the options to customize a software system, while a \emph{configuration} specifies the choices made for a specific instance / product of the product line. Customization options can depend on each other, e.g., the choice made for an option determines, restricts or even excludes the selection for another customization option. Such dependencies are typically expressed using different forms of \emph{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 \emph{reasoning mechanisms} are utilized, such as SAT-solvers in~\cite{BakDiskinAntkiewicz+16, BenavidesTrinidadRuiz-Cortes05, MendoncaBrancoCowan09} or SMT-reasoners in~\cite{BakDiskinAntkiewicz+16}. For some models, specific forms of reasoning were even shown to be efficient, e.g., SAT-solving on feature models~\cite{MendoncaWasowskiCzarnecki09}. However, the expressiveness of the modeling concepts affect the analyzability of the model~\cite{EichelbergerKroeherSchmid13}, and, thus, limit also the feasibility of applying (existing) reasoning mechanisms. +In Product Line Engineering, a \emph{variability model} defines the options to customize a software system. A \emph{configuration} specifies the choices defined by the variability model for a specific instance / product of the product line. Customization options can depend on each other, e.g., the choice made for an option determines, restricts or even excludes the decision for another customization option. Such dependencies are typically expressed using different forms of \emph{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 determining the number of remaining configuration options or for propagating derivable values, various forms of \emph{reasoning mechanisms} are utilized, such as SAT-solvers in~\cite{BakDiskinAntkiewicz+16, BenavidesTrinidadRuiz-Cortes05, MendoncaBrancoCowan09} or SMT-reasoners in~\cite{BakDiskinAntkiewicz+16}. For some models, specific forms of reasoning were even shown to be efficient, e.g., SAT-solving for feature models~\cite{MendoncaWasowskiCzarnecki09}. However, the expressiveness of the modeling concepts affect the analyzability of the model~\cite{EichelbergerKroeherSchmid13}, and, thus, limit also the feasibility of applying a certain reasoning approach. -Besides traditional variability modeling approaches, such as feature modeling~\cite{CzarneckiHelsenEisenecker05, KangCohenHess+90} or decision modeling~\cite{CzarneckiGruenbacherRabiser+12, SchmidJohn04}, in recent time several approaches with more powerful modeling concepts have been proposed, e.g., supporting non-Boolean variability, sets of variabilities or advanced types of constraints, e.g., first-order logic. One rather popular form of approaches is textual variability modeling, as analyzed in more details in~\cite{EichelbergerSchmid15a}. Such more powerful modeling approaches require also adequate reasoning mechanisms, while the expressiveness of modeling concepts trades off with analyzability~\cite{EichelbergerKroeherSchmid13}. For short, typically more powerful modeling concepts imply limitations of the analysis capabilities, e.g., non-Boolean configuration options typically prevent determining the actual number of possible configurations (in contrast to the number of configuration options that remain to be configured to achieve a complete configuration). +Besides traditional variability modeling approaches, such as feature modeling~\cite{CzarneckiHelsenEisenecker05, KangCohenHess+90} or decision modeling~\cite{CzarneckiGruenbacherRabiser+12, SchmidJohn04}, in recent time several approaches with more powerful modeling concepts have been proposed, e.g., supporting non-Boolean variability, sets of variabilities or advanced types of constraints, e.g., first-order logic. Here, one rather popular form of approaches is textual variability modeling, as analyzed in more details in~\cite{EichelbergerSchmid15a}. Such more powerful modeling approaches require also adequate reasoning mechanisms, while the expressiveness of modeling concepts trades off with analyzability~\cite{EichelbergerKroeherSchmid13}. For short, typically more powerful modeling concepts imply limitations of the analysis capabilities, e.g., non-Boolean configuration options typically prevent determining the actual number of possible configurations\footnote{In contrast to the number of configuration options that remain to be configured to achieve a complete configuration.}. -The \emph{Integrated Variability Modeling Language (IVML)}~\cite{IVML-LS} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system inspired by object-orientation, multiple-inheritance, container types, configuration references, imports, orthogonal annotations (e.g., for binding times), quantification constraints, or user-defined constraint functions. The core idea of IVML is to represent a variability, i.e., a configuration option, as a typed variable. IVML even allows for modeling topological variability, i.e., configuring and reasoning over graph structures~\cite{EichelbergerQinSizonenko+16}. +The \emph{Integrated Variability Modeling Language (IVML)}~\cite{IVML-LS} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system inspired by object-orientation, multiple-inheritance, container types, configuration references, imports, orthogonal annotations (e.g., for binding times), quantification constraints, or user-defined constraint functions. The core idea of IVML is to represent a variability, i.e., a configuration option, as a typed variable. IVML even allows for modeling topological variability, i.e., configuring of and reasoning over graph structures~\cite{EichelbergerQinSizonenko+16}. -In this document, we discuss the approach and the design of the reasoning mechanism for IVML as well as its realization in EASy-Producer~\cite{EichelbergerEl-SharkawyKroeher+14, El-SharkawyKroeherEichelbergerSchmid15}, an Open Source product line toolset implementing IVML. At its core, the reasoner focuses on translating / creating specifically instantiated constraints for the various IVML concepts and on forward-reasoning, i.e., evaluating the constraints and performing value propagation as much as possible. On the one hand side, this allows for performing typical validation and propagation tasks, but, on the other hand side, this currently does not support advanced reasoning functionality such as configuration completion. This document is mainly intended to summarize the actual state, the ideas behind individual steps of the reasoning process and the decisions made for realizing the reasoning. Besides the pure technical documentation, our specific contributions are: +In this document, we discuss the approach and the design of the reasoning mechanism for IVML as well as its realization in EASy-Producer~\cite{EichelbergerEl-SharkawyKroeher+14, El-SharkawyKroeherEichelbergerSchmid15}, an Open Source product line toolset implementing IVML. At its core, the reasoner focuses on forward-reasoning, i.e., evaluating the constraints and performing value propagation as much as possible. According to our experience, focusing on forward reasoning allows for performing typical validation and propagation tasks at high reasoning speed. In the IVML context, a complex task is to enable forward reasoning for the various IVML modeling concepts, e.g., to enable reasoning over constraints attached to types rather than variables. However, plain forward reasoning is not reasoning complete and, thus, does not enable advanced reasoning capabilities such as configuration completion. Such advanced capabilities may may impact reasoning speed significantly. In combination, forward reasoning may be a solid basis for realizing such advanced capabilities in a subsequent step at acceptable performance as we envision in this document. Therefore, this document is intended to summarize the actual state, the ideas behind individual steps of the reasoning process and the decisions made for certain tradeoffs. Besides the pure technical documentation, our specific contributions are: \begin{itemize} \item An IVML-complete reasoning mechanism, i.e., translation and reasoning for a complex, rich and typed variability modeling language. - \item Support for IVML type refinements, which can cause implicit effects on the application of constraints. IVML allows defining a type hierarchy, and so the potential types for a configuration option, i.e., a typed variable, can change along the type hierarchy. As types can introduce constraints, the actual constraint base considered during reasoning can change, i.e., constraints must be added or removed as an effect of a value type change. - \item Support for IVML constraint variables, i.e., variables that hold constraints (including sets or sequences) and be changed by the configuration. Through constraint variables, IVML explicitly allows introducing, adding, removing and disabling constraints. Consequently, such changes can affect the constraint base considered during reasoning. - \item Instantiation of type-based constraints to variable-based constraints as a basis for a subsequent reasoning chain. For such subsequent reasoners, the IVML reasoner provides a solid basis, detailed error messages including the failed instantiated constraints so that a chained reasoner can directly continue with these constraints. We envision for future work, that further reasoning steps may add complementing reasoning functions such as identifying a value from narrowing constraints. + \item Support for IVML type refinements, which can cause imply changes to the set of active constraints during reasoning. For short, IVML allows defining a hierarchy of types, and so the potential types for a configuration option can change along the type hierarchy. As types can introduce different constraints, the actual constraint set considered during reasoning can change, i.e., constraints must be added or removed as an effect of a value (type) change. + \item Support for IVML constraint variables. IVML supports variables that hold a constraint, i.e., a configuration can explicitly define, add, remove or disable constraints, i.e., actively change the constraint set during reasoning. + \item Although the current reasoning approach is not reasoning complete, it is designed to act as the first step in a chained reasoning approach. For such subsequent reasoners, the IVML reasoner provides a solid basis, detailed error messages including the failed instantiated constraints so that a chained reasoner can directly continue working with these constraints. \end{itemize} -This document is structured as follows: Section \ref{sectApproach} provides an overview to our approach. Section \ref{sectNotation} introduces the notation that we use throughout this document to specify the algorithms, i.e., we introduce notations for sets, sequences, substitutions as well as relevant parts of the IVML object model realizing the various IVML concepts, here in terms of notations for accessing (derived) properties of the IVML model. In Section \ref{sectReasoning}, we discuss the top-level algorithms for transforming constraints and reasoning. In Section \ref{sectTranslation}, we detail the translation of constraints for all IVML modeling concepts. The result is a set of instantiated constraints that can be used for reasoning. Section \ref{sectTranslation} includes also the mechanism for re-scheduling constraints when value types or constraint variables change, as this mechanism heavily relies on the constraint translations discussed before. In Section \ref{sectCompleteness}, we analyze the translations in order to assess their completeness with respect to IVML concepts and indicate the state of the validation, i.e., regression test cases checking that the constraint translations are applied correctly for specific modeling situations. In Section \ref{sectPerformance}, we summarize performance issues, findings and resolutions we made while revising the reasoner, in particular to avoid that future modifications violate already resolved performance anti-patterns. In Section \ref{sectEvaluation}, we present an evaluation of the actual performance of the reasoning approach for different kinds of IVML models. Finally, in Section \ref{sectConclusion} we conclude and provide an outlook on future work. +This document is structured as follows: Section \ref{sectApproach} provides an overview of our approach. Section \ref{sectNotation} introduces the notation that we use throughout this document to specify the algorithms. There, we introduce notations for sets, sequences, substitutions as well as relevant IVML concepts. In Section \ref{sectReasoning}, we discuss the top-level algorithms for reasoning and constraint transformation. In Section \ref{sectTranslation}, we detail the translation of constraints for all IVML modeling concepts. Section \ref{sectTopLevelConstraintsRescheduling} includes the mechanism for re-scheduling constraints, i.e., how to handle value type or constraint variables changes. In Section \ref{sectCompleteness}, we analyze the translations in order to assess their completeness with respect to the IVML specification~\cite{IVML-LS} and indicate the state of the validation in terms of regression test cases. In Section \ref{sectPerformance}, we summarize performance issues, findings and resolutions we made while developing this version of the reasoner, in particular to avoid that future modifications violate already resolved performance anti-patterns. In Section \ref{sectEvaluation}, we present an evaluation of the actual performance of the reasoning approach for different kinds of IVML models. Finally, in Section \ref{sectConclusion} we conclude and provide an outlook on future work. Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 182) +++ /reasoner/reasoner.tex (revision 183) @@ -73,5 +73,5 @@ \LinesNumbered -Automatically analyzing and reasoning about interdependent configuration settings can be a difficult task, in particular if the configuration modeling approach provides complex modeling concepts or a highly expressive constraint language~\cite{EichelbergerKroeherSchmid13}. In this document, we give an overview on the current state of reasoning for the Integrated Variability Modeling Language (IVML)~\cite{IVML-LS}, a variability and configuration modeling language that contains several advanced and complex modeling concepts as well as an expressive constraint language allowing for first-order logic. We discuss the approach to reasoning for IVML, in particular, the translation of types and constraints for reasoning, the reasoning algorithm, the validation of the approach and its performance for different kinds of models. +Automatically analyzing and reasoning about interdependent configuration settings can be a difficult task, in particular if the configuration modeling approach provides complex modeling concepts or a highly expressive constraint language~\cite{EichelbergerKroeherSchmid13}. In this document, we give an overview on the current state of reasoning for the Integrated Variability Modeling Language (IVML)~\cite{IVML-LS}. IVML is a variability and configuration modeling language that contains several advanced and complex modeling concepts as well as an expressive constraint language, e.g., allowing for first-order logic. We discuss a reasoning approach for IVML, i.e., the reasoning algorithms, the needed constraint translations, the validation of the approach and its performance for different kinds of models. \input{introduction}