Index: /reasoner/approach.tex =================================================================== --- /reasoner/approach.tex (revision 224) +++ /reasoner/approach.tex (revision 225) @@ -7,5 +7,5 @@ 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, using them for IVML requires translating an IVML model and its constraints into the model of the respective reasoning mechanism and executing that mechanism on the translated model. In the past, we identified in particular this transformation as a significant performance bottleneck as well as an obstacle to achieve IVML-completeness, i.e., we were often not able to express all IVML concepts in the respective reasoner model. While traditional reasoners allow for completing a model through feasible ground instances, they typically also perform a kind of (constrained) state space exploration. Considering the size of usual configuration models (currently the largest IVML model we are aware of has more than 16.000 variables~\cite{EichelbergerQinSchmid17a, EichelbergerQinSizonenko+16}), we experienced that 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, traditional reasoners as well as rule engines are limited as they typically do not support the range of OCL concepts required for IVML, in particular container iterators, quantifiers and user-defined functions. Further, also specific reasoning approaches, e.g., for the Object Web Language (OWL)~\cite{KahnPorres15, KolliaGlimmHorrocks11} might be an option as they partially support quantification. However, they are often similarly limited regarding the range of OCL operations. Moreover, OCL-based approaches such as~\cite{DemuthLoecherZschaler04, ClavelEgea06} typically also focus on forward-chaining, but would require deep extensions, as OCL does not allow for side-effects or value propagation as required by IVML. -Due to these experiences, we decided to pursue a \emph{mixed reasoning approach}, which attempts to reduce / simplify the reasoning problem towards an instance that (if needed) can be handled by a traditional reasoner. Other work also combine multiple reasoning approaches to achieve advanced reasoning capabilities, e.g., evolutionary algorithms with SAT-solving to realize many-objective optimization for feature modeling~\cite{XiangZhouZheng+2018}. In our case, the basis for a mixed approach is \emph{forward-chaining}, i.e., evaluation of a given constraint base as long as no constraints are left over, while re-scheduling constraints that depend on a variable changed during reasoning. The SSE IVML reasoner as described in this document realizes this basis, while the actual mixed approach is part of future work. +Due to these experiences, we decided to pursue a \emph{mixed reasoning approach}, which attempts to reduce / simplify the reasoning problem towards an instance that (if needed) can be handled by a traditional reasoner. Other work also combine multiple reasoning approaches to achieve advanced reasoning capabilities, e.g., evolutionary algorithms with SAT-solving to realize many-objective optimization for feature modeling~\cite{XiangZhouZheng+2018}. In our case, the basis for a mixed approach is \emph{forward-chaining}, i.e., evaluation of a given constraint base as long as no constraints are left over, while re-scheduling constraints that depend on a variable changed during reasoning. The SSE IVML reasoner as described in this report realizes this basis, while the actual mixed approach is part of future work. It is important to notice that IVML~\cite{IVML-LS} supports declarative specification of constraints, i.e., modeling concepts and constraints can be specified regardless of their actual evaluation sequence. To ensure that values for variables are uniquely determined, in particular in presence of default values, IVML allows changing the value of a variable only once within a project scope. Otherwise the reasoning mechanism must issue an error. Thus, reasoning must happen project-wise, along a depth-first traversal along the project import dependencies. Moreover, to speed up reasoning in specific situations, some form of sequence of the constraints can be indicated through the concept of partial evaluations, i.e., in terms of so called eval-blocks stated within a project or a compound. An eval-block consists of constraints or nested eval-blocks, while nested eval-blocks implicitly define an evaluation sequence. In other words, a project is the outermost (implicit) eval-block and nested eval-blocks shall be evaluated in their nesting sequence, while eval-blocks on the same nesting level do not imply any evaluation sequence. @@ -23,3 +23,3 @@ \end{itemize} -To implement the IVML reasoner, we first designed and realized an \emph{expression evaluation mechanism}, which is able to evaluate individual IVML expressions. The evaluation mechanisms covers constraint expressions (expressions evaluating to a Boolean value) as well as general default value expressions. In the algorithms described in this document, we just refer to the evaluation mechanism without further detailing it. We assume that the mechanism either returns the correctly evaluated value of an expression with respect to a given model / configuration or that it indicates that the evaluation result is undefined, e.g., as configuration variables used in the evaluated expression are undefined. +To implement the IVML reasoner, we first designed and realized an \emph{expression evaluation mechanism}, which is able to evaluate individual IVML expressions. The evaluation mechanisms covers constraint expressions (expressions evaluating to a Boolean value) as well as general default value expressions. In the algorithms described in this report, we just refer to the evaluation mechanism without further detailing it. We assume that the mechanism either returns the correctly evaluated value of an expression with respect to a given model / configuration or that it indicates that the evaluation result is undefined, e.g., as configuration variables used in the evaluated expression are undefined. Index: /reasoner/introduction.tex =================================================================== --- /reasoner/introduction.tex (revision 224) +++ /reasoner/introduction.tex (revision 225) @@ -1,3 +1,3 @@ -\section{Introduction} +\section{Introduction}\label{sectIntro} 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. @@ -7,5 +7,5 @@ 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 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: +In this report, 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 report. Therefore, this report 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} @@ -17,3 +17,3 @@ \end{itemize} -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. +This report is structured as follows: Section \ref{sectApproach} provides an overview of our approach. Section \ref{sectNotation} introduces the notation that we use throughout this report 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/ivmlCompleteness.tex =================================================================== --- /reasoner/ivmlCompleteness.tex (revision 224) +++ /reasoner/ivmlCompleteness.tex (revision 225) @@ -1,7 +1,7 @@ \section{IVML-Completeness}\label{sectCompleteness} -In this section, we discuss the completeness of the reasoner with respect to IVML concepts defined in \cite{IVML-LS}. Reasoning completeness, e.g., involving advanced reasoning capabilities such as narrowing down value instances by limiting constraints or instance creation, is currently not supported by the approach and may be subject to future work. - -To assess the IVML completeness, we enumerate all IVML concepts relevant to reasoning, their defining section in the IVML specification~\cite{IVML-LS}, the transformation path along the algorithms presented in this document and the test cases validating the transformation and the reasoning results. The referenced test cases are detailed in Appendix \ref{appendixTestCases}. A '*' in a test id indicates a wildcard, e.g., A*1 means all annotation-related tests. Test cases are referenced by ids in order to indicate that all relevant combinations are subject to regression testing in the continuous build process of EASy-Producer. An entry 'no specific constraints' in the transformation path indicates that for the respective concept no constraints can be defined / translated as explained in Section \ref{sectNotationOthers}. +In this section, we discuss the completeness of the reasoner with respect to IVML concepts. Although the algorithms are designed along the IVML specification~\cite{IVML-LS}, it is important to explicitly assess and validate the coverage of the design and the realization, in particular as a basis for future work. However, as explicitly stated in Section \ref{sectIntro}, reasoning completeness, e.g., involving advanced reasoning capabilities such as narrowing down value instances by limiting constraints or instance creation, is currently out of scope and may be subject of future work. + +To assess the IVML completeness, we enumerate all IVML concepts relevant to reasoning, their defining section in the IVML specification~\cite{IVML-LS}, the transformation path along the algorithms presented in this report and the test cases validating the transformation and the reasoning results. The referenced test cases are detailed in Appendix \ref{appendixTestCases}. A '*' in a test id indicates a wildcard, e.g., A*1 means all annotation-related tests. Test cases are referenced by ids in order to indicate that all relevant combinations are subject to regression testing in the continuous build process of EASy-Producer. An entry 'no specific constraints' in the transformation path indicates that for the respective concept no constraints can be defined / translated as explained in Section \ref{sectNotationOthers}. We present the argumentation in four parts grouped according to IVML concepts, namely 1) top-level concepts / basic types (Table \ref{tab:completenessTopLevelTypes}), compound types (Table \ref{tab:completenessCompounds}), container types (Table \ref{tab:completenessContainers}) and annotations (Table \ref{tab:completenessAnnotations}). Index: /reasoner/mainAlgorithms.tex =================================================================== --- /reasoner/mainAlgorithms.tex (revision 224) +++ /reasoner/mainAlgorithms.tex (revision 225) @@ -34,5 +34,5 @@ In the \textbf{full reasoning part}, data structures are set up to store constraints for reuse in the incremental part (if $reuse$ is enabled), here for storing a copy of the constraint base ($base_c$) as well as $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$ storing specific constraint relations. $\relevantConstraintsPerDeclaration$ and $\relevantConstraintVariables$ are important for efficient access to constraints during constraint re-scheduling, i.e., when variable values change as a side effect of value propagation. $\relevantConstraintsPerDeclaration$ is a mapping that links a variable declaration to the constraints using the variable. $\relevantConstraintVariables$ is a bi-directional mapping between constraint values assigned to configured decision variables. $base_{\relevantConstraintsPerDeclaration}$ and $base_{\relevantConstraintVariables}$ are the respective copies if $reuse$ is enabled. -The resoning process takes each individual project (as top-level evaluation scope) into account and evaluates the constraints defined by the respective project. However, as projects can depend on each other, the reasoning process must follow the import dependencies of the projects starting at those without imports continuing with the dependent projects up to the top-level project in the given configuration $c$. In general, the imports of IVML projects can form a graph with loops, because imports my be cyclic~\cite{IVML-LS} as required in complex topological models. Thus, we determine the project sequence through a cycle-free depth-first traversal of the import graph, i.e., we pretend that the import graph is a tree and ignore imports of already seen projects. The traversal determines the project sequence, a partial ascending order of projects according to their (number of) dependencies. In this sequence, projects with no imports are at the beginning of the sequence and projects with imports are are listed after all their depending projects. line \ref{algMainLoopDiscover}, $discoverProjects(cfg)$\footnote{The algorithm is not further detailed in this document} determines the project sequence of all projects involved in $c$. The loop in lines \ref{algMainLoopStart}-\ref{algMainLoopEnd} processes this project sequence as long as no timeout occurred (global flag $hasTimeout$) or the user stops the reasoning process (global flag $stop$). +The resoning process takes each individual project (as top-level evaluation scope) into account and evaluates the constraints defined by the respective project. However, as projects can depend on each other, the reasoning process must follow the import dependencies of the projects starting at those without imports continuing with the dependent projects up to the top-level project in the given configuration $c$. In general, the imports of IVML projects can form a graph with loops, because imports my be cyclic~\cite{IVML-LS} as required in complex topological models. Thus, we determine the project sequence through a cycle-free depth-first traversal of the import graph, i.e., we pretend that the import graph is a tree and ignore imports of already seen projects. The traversal determines the project sequence, a partial ascending order of projects according to their (number of) dependencies. In this sequence, projects with no imports are at the beginning of the sequence and projects with imports are are listed after all their depending projects. line \ref{algMainLoopDiscover}, $discoverProjects(cfg)$\footnote{The algorithm is not further detailed in this report} determines the project sequence of all projects involved in $c$. The loop in lines \ref{algMainLoopStart}-\ref{algMainLoopEnd} processes this project sequence as long as no timeout occurred (global flag $hasTimeout$) or the user stops the reasoning process (global flag $stop$). \begin{algorithm}[H] Index: /reasoner/notation.tex =================================================================== --- /reasoner/notation.tex (revision 224) +++ /reasoner/notation.tex (revision 225) @@ -13,5 +13,5 @@ In some cases, we also need to express a \emph{mapping} between key elements and associated value elements. We denote such a mapping as a set of pairs $\mapEntry{k}{v}$ relating a key $k$ to a value $v$. Within a mapping, key-value pairs are unique with respect to the key. We denote adding a key-value pair to a map by $m \addMap \mapEntry{k}{v}$, assuming that an existing entry for $k$ (accessible by $m[k]$) is overridden by the new entry. If there is no mapping for a certain key, $m[k]$ is $\undef$. We denote removing elements from a map by set differences, either mentioning the pairs, e.g., for one entry $m \setminus \mapEntry{k}{v}$ or just the keys, e.g., $m \setminus \set{k_1, k_2, \ldots}$. Iterating over a map, e.g., in an algorithm, means iterating over the entries of a map in an arbitrary sequence. -As this document is intended to detail the actual implementation and to ease mapping from code to algorithms and back, we use for the \emph{algorithms} (where feasible from the space / layout point of view) the actual name from the implementation. Further, we use parameters and return values as done in the implementation. If global, static or instance data is used, we indicate this in `data' section of the respective algorithm description. +As this report is intended to detail the actual implementation and to ease mapping from code to algorithms and back, we use for the \emph{algorithms} (where feasible from the space / layout point of view) the actual name from the implementation. Further, we use parameters and return values as done in the implementation. If global, static or instance data is used, we indicate this in `data' section of the respective algorithm description. \subsection{IVML elements} @@ -144,5 +144,5 @@ -As usual in IVML, we denote collection operations using the arrow and iterator notation, which involves the $|$ symbol for separating iterator variables from iterator expressions. However, as we use in this document the '$|$' symbol for variable substitutions, also using the same symbol in IVML collection expressions may be confusing. Thus, we use in collection expressions in this document ':' instead of '$|$', e.g., instead of $\IVMLforallSep{\IVML{o}}{\IVML{x}}{\IVML{|}}{\constraintWith{c}{\IVML{x}}}$ we denote $\IVMLforall{\IVML{o}}{\IVML{x}}{\constraintWith{c}{\IVML{x}}}$ to indicate an all-quantized expression over a collection \IVML{o} applying the iterator variable \IVML{x} to some constraint $\constraintWith{c}{\IVML{x}}$. +As usual in IVML, we denote collection operations using the arrow and iterator notation, which involves the $|$ symbol for separating iterator variables from iterator expressions. However, as we use in this report the '$|$' symbol for variable substitutions, also using the same symbol in IVML collection expressions may be confusing. Thus, we use in collection expressions in this report ':' instead of '$|$', e.g., instead of $\IVMLforallSep{\IVML{o}}{\IVML{x}}{\IVML{|}}{\constraintWith{c}{\IVML{x}}}$ we denote $\IVMLforall{\IVML{o}}{\IVML{x}}{\constraintWith{c}{\IVML{x}}}$ to indicate an all-quantized expression over a collection \IVML{o} applying the iterator variable \IVML{x} to some constraint $\constraintWith{c}{\IVML{x}}$. %In summary, let \IVML{o} be an IVML collection of Integers, then \IVML{o->forall(i:i>20);} requires that all values in $o$ must be greater than 20. To create such a constraint with $o$ being an algorithm variable, we denote $\createConstraint{o\IVML{->forall(i:i>20)}}$. @@ -150,5 +150,5 @@ %Similarly, we denote creating a constraint originating from a constraint variable by `$c$', e.g., $b \assng \createConstraintConstraint{\IVML{assign}(x, 25)}$ for which $\isConstraintConstraint{b} = true$ holds. -Often, constraints cannot be created in a single step, i.e., a constraint must be created iteratively from sub-expressions. To indicate this, we denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for the IVML expression \IVML{x + 25}. When creating container (iterator) expressions incrementally, also a notation for creating a temporary (local) IVML variable is needed. We state the creation of such a variable by $\IVMLMeta{var}(t)$ and indicate thereby the creation of a local variable\footnote{We don't care for the variable name in this document.} of type $t$. For a variable $v=\IVMLMeta{var}(t)$, $isLocal(v) = true$ holds. +Often, constraints cannot be created in a single step, i.e., a constraint must be created iteratively from sub-expressions. To indicate this, we denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for the IVML expression \IVML{x + 25}. When creating container (iterator) expressions incrementally, also a notation for creating a temporary (local) IVML variable is needed. We state the creation of such a variable by $\IVMLMeta{var}(t)$ and indicate thereby the creation of a local variable\footnote{We don't care for the variable name in this report.} of type $t$. For a variable $v=\IVMLMeta{var}(t)$, $isLocal(v) = true$ holds. Before reasoning over the constraints given in an IVML project, several kinds of constraints must be transformed, in particular to instantiate constraints defined for types through qualifying access expressions based on top-level variables. To provide an overview of the transformations performed by an algorithm, we use constraint transformation patterns. The algorithm then applies constraint and expression creations as well as variable substitutions to realize the respective transformations. @@ -285,5 +285,5 @@ No specific constraint translation is needed for \emph{basic types} (Boolean, Integer, Real, String), the constraint type introduced in Section \ref{sectNotationConstraints} as well as for enums, because IVML does not support attaching constraints to these types. Constraints for these types can only be defined indirectly as global constraints for variable declarations, as nested compound constraints for compound slots or via derived types as introduced in Section \ref{sectNotationDerivedTypes}. Thus, no specific functions for these types must be introduced here. -%The available IVML functions and operations for these types, such as adding two integer values, are subject of the creation of expressions / the IVML model, e.g., through the IVML parser as well as of the IVML expression evaluation mechanism, rather than the reasoning algorithms discussed in this document. +%The available IVML functions and operations for these types, such as adding two integer values, are subject of the creation of expressions / the IVML model, e.g., through the IVML parser as well as of the IVML expression evaluation mechanism, rather than the reasoning algorithms discussed in this report. In IVML, a \emph{configuration reference} points to a variable defined in the same or another imported project. IVML configuration references require specific treatment during constraint translation. Therefore we introduce the following specific functions. A configuration reference is a generic type $t$ defined for the base type $base(t)$ of the variable the reference points to. If $t$ is a reference, $isReference(t)$ returns true. Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 224) +++ /reasoner/reasoner.tex (revision 225) @@ -82,5 +82,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}. 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. +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 report, 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}