Index: /reasoner/reasoner.bib =================================================================== --- /reasoner/reasoner.bib (revision 130) +++ /reasoner/reasoner.bib (revision 131) @@ -154,4 +154,25 @@ keywords = "Consistency, Ontology, UML, Reasoning" } + +@article{XiangZhouZheng+2018, + author = {Xiang, Yi and Zhou, Yuren and Zheng, Zibin and Li, Miqing}, + title = {Configuring Software Product Lines by Combining Many-Objective Optimization and SAT Solvers}, + journal = {ACM Trans. Softw. Eng. Methodol.}, + issue_date = {February 2018}, + volume = {26}, + number = {4}, + month = feb, + year = {2018}, + issn = {1049-331X}, + pages = {14:1--14:46}, + articleno = {14}, + numpages = {46}, + url = {http://doi.acm.org/10.1145/3176644}, + doi = {10.1145/3176644}, + acmid = {3176644}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {Optimal feature selection, many-objective optimization, satisfiability (SAT) solvers, vector angle--based evolutionary algorithm (VaEA)}, +} @InProceedings{SchmidEichelberger08a, Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 130) +++ /reasoner/reasoner.tex (revision 131) @@ -97,5 +97,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 and typically available as implementation, 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 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{EichelbergerQinSizonenko+16, EichelbergerQinSchmid17a}), 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 operations required for IVML, in particular container iterators, quantifiers and user-defined constraint operations. 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, but they are 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 finally be handled by a traditional reasoning approach. The basis for this 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 finally be handled by a traditional reasoning approach. 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. 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}. 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, in 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., 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. @@ -301,5 +301,4 @@ %% - % In some constraint transformations it is important to determine, whether a compound slot is overridden. Let $d$ be a declaration, in particular $d\in slots(t) \wedge isCompund(t)$, then the parent compound of $d$ skipping potentially enclosing nested assignment blocks is @@ -330,21 +329,25 @@ \subsubsection{Containers}\label{sectNotationContainers} -An IVML \emph{container} is a parameterized type representing a structure that holds an arbitrary number of variables / values. IVML defines two default container types, namely \emph{sequence} (duplicates allowed, order important) and \emph{set} (no duplicates allowed, order irrelevant). The type parameters of a container are not relevant for reasoning, as at least the static type compliance is checked by the IVML parser before reasoning. - -Let $c$ be a container, then $elements(c)$ denotes the set or sequence of all element values in $c$, respectively. Let type $t$ be a container type, then $isContainer(t)$ returns $true$. Further, $contained(t)$ returns the directly contained type, e.g., for a \IVML{setOf(setOf(Integer))} $contained(t)$ returns \linebreak \IVML{setOf(Integer)}. We define $isNested(t) = isContainer(contained(t))$ and +An IVML \emph{container} is a parameterized type representing a structure that holds an arbitrary number of variables / values. IVML defines two default container types, namely \emph{sequence} (duplicates allowed, order important) and \emph{set} (no duplicates allowed, order irrelevant). The type parameters of a container are not relevant for reasoning, as we can assume that the static type compliance is checked by the IVML object model or the IVML parser before reasoning. + +Let $c$ be a container, then $elements(c)$ denotes the set or sequence of all element values in $c$, respectively. Let type $t$ be a container type, then $isContainer(t)$ returns $true$. Further, $contained(t)$ returns the directly contained type, e.g., for a \IVML{setOf(setOf(Integer))} in IVML notation, $contained(t)$ returns \IVML{setOf(Integer)}. + +We define $isNested(t) = isContainer(contained(t))$ and % $$nested(t)=\begin{cases}nested(contained(t)), & \text{if } isNested(t) \\ contained(t), & \text{else} \\ \end{cases}$$ % -to return the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested(t)$ returns \IVML{Integer}. If a container $isNested(c)$ for a container $c$, $elements(c)$ contains container values of the nested type. Here, $allElements(c)$ returns the transitively flattened elements of the respective container, i.e., set or sequence, i.e., all leaf elements of a depth-first traversal of the containment tree. - -In some situations, we must identify whether a container consists of constraints, i.e., -% -$$isConstraintContainer(t) = isNested(t) \wedge isConstraint(nested(t))$$. -% -In other situations, we need to know all types that are used in a container (value), i.e., the set +returning the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested(t)$ returns \IVML{Integer}. If $isNested(c)$ is $true$ for a container $c$, $elements(c)$ contains values of the nested type. In some situations, the flattened container is needed, i.e., for nested collections preferrably with the same innermost nested type only the innermost contained values are relevant. For this purpose, $allElements(c)$ returns the transitively flattened elements of the respective container, i.e., set or sequence, i.e., all leaf elements of a depth-first traversal of the containment tree. + +During the constraint translation, we must identify whether a container consists of constraints, i.e., +% +$$isConstraintContainer(t) = isNested(t) \wedge isConstraint(nested(t))$$ +% +In other situations, we need to know all actual innermost nested types that are used in a container, i.e., the set % $$usedTypes(c) = \setWith{contained(type(e))}{e\in allElements(c)}$$ % -For containers, access expressions usually occur only if the collection has a compound as nested type and if the collection is a sequence. Then accessing an element by an index happens through the IVML index access function for sequences. For example, \IVML{seq[1]} accesses an indexed element of the sequence \IVML{seq} and the accessor to \IVML{slot} on \IVML{seq[1]} is then the combined expression \IVML{seq[1].slot}. For creating the respective expression within an algorithm, we denote $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. +This is in particular important if $isCompound(nested(type(c)))$ holds for a container $c$, as then also values of refined types of $nested(type(c))$ may occur in $usedTypes(c)$. + +For containers, \emph{access expressions} usually occur either in quantorized expressions utilizing the iterator variable or if the collection is a sequence (typically of compounds). Then accessing an element by an index happens through the IVML index access function for sequences. For example, let \IVML{seq} be a sequence of compounds, all having a common slot \IVML{slot}. Then \IVML{seq[1]} accesses the second element in the container\footnote{In contrast to OCL, IVML indexes are 0-based.} and accessing \IVML{slot} on the first element happens through \IVML{seq[1].slot}. For creating the respective expression within an algorithm, we denote $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. Akin to compounds, containers can be initialized by complex values, so called \emph{container initializers}, here as a listing of possible complex values. If the container is a sequence, the given order of values in the container initializer used as (initial) order of the sequence elements.