Index: /reasoner/reasoner.bib =================================================================== --- /reasoner/reasoner.bib (revision 39) +++ /reasoner/reasoner.bib (revision 39) @@ -0,0 +1,269 @@ + +@misc{QMD41, + title = "Quality-aware Processing Pipeline Modeling", + author = "{QualiMaster consortium}", + note = "Deliverable D4.1, http://qualimaster.eu", + year = 2014 +} + +@misc{QMD42, + title = "Quality-aware Processing Pipeline Adaptation V1", + author = "{QualiMaster consortium}", + note = "Deliverable D4.3, http://qualimaster.eu", + year = 2015 +} + +@misc{QMD43, + title = "Quality-aware Processing Pipeline Adaptation V2", + author = "{QualiMaster consortium}", + note = "Deliverable D4.3, http://qualimaster.eu", + year = 2016 +} + +@misc{QMD44, + title = "Quality-aware Processing Pipeline Modelling and Adaptation", + author = "{QualiMaster consortium}", + note = "Deliverable D4.4, http://qualimaster.eu", + year = 2016 +} + +@InProceedings{El-SharkawyKroeherEichelbergerSchmid15, + author = "S. El-Sharkawy and C. Kr{\"o}her and H. Eichelberger and K. Schmid", + title = "Experience from Implementing a Complex Eclipse Extension for Software Product Line Engineering", + booktitle = "Eclipse Technology eXchange Workshop", + year = 2015 +} + +@InProceedings{EichelbergerEl-SharkawyKroeher+14, + author = {H. Eichelberger and S. El-Sharkawy and C. Kr{\"o}her and K. Schmid}, + title = {{{EASy}-Producer: {P}roduct Line Development for Variant-rich Ecosystems}}, + booktitle = {Software Product Line Conference (SPLC), Vol 2}, + year = {2014}, + pages = {133--137}, + _address = {New York, NY, USA}, + doi = {10.1145/2647908.2655979}, + _publisher = {ACM}, + _series = {SPLC '14}, + url = {http://doi.acm.org/10.1145/2647908.2655979}, + acmid = {2655979}, + isbn = {978-1-4503-2739-8}, + keywords = {EASy-producer, ecosystems, software product lines}, + _location = {Florence, Italy}, + numpages = {5} +} + +@InProceedings{EichelbergerSchmid15, + author = {Eichelberger, H. and Schmid, K.}, + title = {{IVML: A DSL for Configuration in Variability-rich Software Ecosystems}}, + booktitle = {Software Product Line Conference (SPLC)}, + year = {2015}, + pages = {365--369}, + address = {New York, NY, USA}, + publisher = {ACM}, + series = {SPLC '15}, + acmid = {2791116}, + doi = {10.1145/2791060.2791116}, + isbn = {978-1-4503-3613-0}, + keywords = {EASy-producer, ecosystems, software product lines}, + location = {Nashville, Tennessee}, + numpages = {5}, + url = {http://doi.acm.org/10.1145/2791060.2791116} +} + +@inproceedings{Eichelberger16, + author = {H. Eichelberger}, + title = "It's about the mix: Integration of Compile and Runtime Variability", + booktitle = "FAS*W Workshop on Dynamic Software Product Lines (DSPL)", + year=2016 +} + +@InProceedings{EichelbergerQinSizonenko+16, + author = {H. Eichelberger and C. Qin and R. Sizonenko and K. Schmid}, + title = {{Using IVML to Model the Topology of Big Data Processing Pipelines}}, + booktitle = {Software Product Line Conference (SPLC)}, + year = {2016}, + pages = {204--208} +} + +@InProceedings{SchmidEichelberger08a, + author = {K. Schmid and H. Eichelberger}, + title = {Model-Based Implementation of Meta-Variability Constructs: A Case Study using Aspects}, + booktitle = {Variability Modeling of Software-intensive Systems (VAMOS)}, + year = {2008}, + pages = {63--71}, + _note = {ICB-Research Report No. 22}, + abstract = {In this paper, we introduce the concept of metavariability, i.e., + variability with respect to basic variability attributes like binding + time or constraints. While the main focus of this paper is on the + introduction of the concept, we will also illustrate the concept + by providing a case study. The case study will feature a simple implementation + environment based on aspect-oriented programming and will include + an example that will exhibit some key characteristics of the envisioned + production process.}, + issn = {1860-2770}, + keywords = {SPL, variability management}, + owner = {Eichelberger}, + pdfavailability = {world}, + timestamp = {2008.03.26} +} + +@InProceedings{EichelbergerKroeherSchmid13, + author = "H. Eichelberger and C. Kr{\"o}her and K. Schmid", + title = "An Analysis of Variability Modeling Concepts: Expressiveness vs. Analyzability", + booktitle = "Intl. Conference on Software Reuse", + pages = "32--48", + year = 2013, +} + +@INPROCEEDINGS{CzarneckiGruenbacherRabiser+12, + author = {K. Czarnecki and P. Gr{\"u}nbacher and R. Rabiser and K. Schmid and A. + Wasowski}, + title = {{Cool Features and Tough Decisions: A Comparison of Variability Modeling + Approaches}}, + booktitle = {{Variability Modelling + of Software-Intensive Systems (VaMoS '12)}}, + year = {2012}, + pages = {173-182}, + doi = {10.1145/2110147.2110167}, + owner = {kroeher}, + timestamp = {2012.03.02} +} + +@Article{CzarneckiHelsenEisenecker05a, + author = {K. Czarnecki and S. Helsen and U. Eisenecker}, + title = {Staged Configuration Through Specialization and Multi-Level Configuration of Feature Models}, + journal = {J. SPIRE}, + year = {2005}, + volume = {10}, + number = {2}, + pages = {143--169}, + abstract = {Feature modeling is a key technique for capturing commonalities and + variabilities in system families and product lines. In this paper, + we propose a cardinality-based notation for feature modeling, which + integrates a number of existing extensions of previous approaches. + We then introduce and motivate the novel concept of staged configuration. + Staged configuration can be achieved by the stepwise specialization + of feature models or by multi-level configuration, where the configuration + choices available in each stage are defined by separate feature models. + Staged configuration is important because in a realistic development + process, different groups and different people make product configuration + choices in different stages. Finally, we also discuss how multi-level + configuration avoids a breakdown between the different abstraction + levels of individual features. This problem, sometimes referred to + as “analysis paralysis”, easily occurs in feature modeling because + features can denote entities at arbitrary levels of abstractions + within a system family.}, + file = {X\:\\restricted\\CzarneckiHelsenEisenecker05.pdf:X\:\\restricted\\CzarneckiHelsenEisenecker05.pdf:PDF}, + keywords = {SPL, Modelling, variability management}, + owner = {schmid}, + review = {The paper describes and summarizes several extensions to feature modelling. + This includes: group and feature based cardinality: includes sequences + of cardinalities. Specialization Staged configuration (mapping between + feature models) - stages can be different binding times multi-staged + configuration seems to include modification of constraints, however, + no reasonable semantics is given. Multi-staged configuration relies + an a transfer notation that maps one feature model upon another.}, + timestamp = {2008.02.29} +} + +@TechReport{KangCohenHess+90, + author = {K. Kang and S. Cohen and J. Hess and W. Novak and A. Peterson}, + title = {{F}eature-{O}riented {D}omain {A}nalysis ({FODA}) {F}easibility {S}tudy}, + year = {1990}, + number = {CMU/SEI-90-TR-21 ESD-90-TR-222}, + _institution = {{Software Engineering Institute Carnegie Mellon University}}, + abstract = {Successful software reuse requires the systematic discovery and exploitation + of commonality across related software systems. By examining related + software systems and the underlying theory of the class of systems + they represent, domain analysis can provide a generic description + of the requirements of that class of systems and a set of approaches + for their implementation. This report will establish methods for + performing a domain analysis and describe the products of the domain + analysis process. To illustrate the application of domain analysis + to a representative class of software systems, this report will provide + a domain analysis of window management system software.}, + file = {KangCohen+90.pdf:restricted/KangCohen+90.pdf:PDF}, + keywords = {SPL, variability management}, + owner = {eichelberger}, + pdfavailability = {group}, + timestamp = {2007.04.23} +} + +@article {CzarneckiHelsenEisenecker05, + title = {Formalizing cardinality-based feature models and their specialization}, + journal = {Software Process: Improvement and Practice}, + volume = {10}, + year = {2005}, + _month = {01/2005}, + pages = {7 - 29}, + abstract = {Feature modeling is an important approach to capture the commonalities +and variabilities in system families and product lines. +Cardinality-based feature modeling integrates a number of existing +extensions of the original feature-modeling notation from +Feature-Oriented Domain Analysis. Staged configuration is a process +that allows the incremental configuration of cardinality-based feature +models. It can be achieved by performing a step-wise specialization of +the feature model. In this article, we argue that cardinality-based +feature models can be interpreted as a special class of context-free +grammars. We make this precise by specifying a translation from a +feature model into a context-free grammar. Consequently, we provide a +semantic interpretation for cardinality-based feature models by +assigning an appropriate semantics to the language recognized by the +corresponding grammar. Finally, we give an account on how feature +model specialization can be formalized as transformations on the +grammar equivalent of feature models.}, + issn = {1099-1670}, + doi = {10.1002/spip.213}, + url = {http://www3.interscience.wiley.com/cgi-bin/fulltext/109932076/PDFSTART}, + attachments = {http://gsd.uwaterloo.ca/sites/default/files/spip05a.pdf}, + author = {Czarnecki, Krzysztof and Helsen, Simon and Ulrich, Eisenecker} +} + +@ARTICLE{EichelbergerSchmid15a, + author = "H. Eichelberger and K. Schmid", + title = "Mapping the Design-Space of Textual Variability Modeling Languages: A Refined Analysis", + journal = "Intl. Journal of Software Tools for Technology Transfer", + volume = 17, + number =5, + pages = "559--584", + year = 2015, +} + +@ARTICLE{SchmidJohn04, + author = {K. Schmid and I. John}, + title = {A Customizable Approach To Full-Life Cycle Variability Management}, + journal = {Science of Computer Programming}, + year = {2004}, + volume = {53}, + pages = {259--284}, + number = {3}, + abstract = {In order to enable a smooth transition to product development for + an organization that so far did only perform single system development, + it is necessary to keep as much of the existing notations and approaches + in place as possible. This requires adaptability of the basic variability + management approach to the specific situation at hand. In this paper + we describe an approach that enables homogenous variability management + across the different life-cycle stages, independent of the specific + notation. The approach is accompanied by a meta-model and a process + for introducing the variability management approach by developing + a notation- independant representation. This approach has so far + been applied in several cases where our Product Line engineering + method PuLSE$^{TM}$ has been introduced into a software development + organization.}, + displayforuser = {schmid}, + keywords = {SPL, Variability Management}, + owner = {schmid}, + pdf = {restricted/SchmidJohn03.pdf}, + pdfavailability = {group}, + timestamp = {2007.04.22} +} + +@techreport{IVML-LS, + author = {H. Eichelberger and S. El-Sharkawy and C. Kr{\"o}her and K. Schmid}, + title = "INDENICA Variability Modeling Language: Language Specification, version 1.22", + year = 2014, + note = {Available online at: http://projects.sse.uni-hildesheim.de/easy/docs/ivml\_spec.pdf}, +} + + +@Comment{jabref-meta: databaseType:bibtex;} Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 38) +++ /reasoner/reasoner.tex (revision 39) @@ -41,10 +41,9 @@ \section{Introduction} -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 \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, container 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. +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~\cite{EichelbergerKroeherSchmid13}, and, thus, also the applicable reasoning mechanism. + +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 to textual variability modeling have been proposed~\cite{EichelbergerSchmid15a}. Moreover, there seems to be a trend that more recent variability modeling support more powerful modeling conceepts~\cite{EichelbergerSchmid15a}, 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 \textbf{Integrated Variability Modeling Language (IVML)}~\cite{IVML-LS} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system, multiple-inheritance, container 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~\cite{EichelbergerQinSizonenko+16}. In this document, we discuss the approach and recent state of the reasoning mechanism for IVML and its realization in EASy-Producer~\cite{EichelbergerEl-SharkawyKroeher+14, El-SharkawyKroeherEichelbergerSchmid15}. 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. 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. This document is structured as follows: Section \ref{sectApproach} introduces the overall approach to reasoning for IVML. Section \ref{sectNotation} introduces the notation that we use to describe the reasoning algorithm, in particular the notation to access (derived) properties of the various IVML concepts. In Section \ref{sectReasoning}, we discuss the top-level algorithms for transforming constraints, reasoning and reacting to value changes / propagation. In Section \ref{sectTranslation}, we detail the instantiation and translation of constraints for individual configuration settings. In Section \ref{sectCompleteness}, we summarize the translations in order to assess the actual state for completeness with respect to IVML concepts. \TBD{So far no evaluation} In Section \ref{sectConclusion} we conclude and provide an outlook to future work. @@ -52,11 +51,11 @@ \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 \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), container 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 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 \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. It is important to notice that IVML \TBD{IVML-spec} supports a declarative specification of constraints, i.e., they can be given regardless of their actual evaluation sequence. To ensure that values are uniqualy 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 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. - -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 +IVML is a textual variability and configuration modeling language. The syntax of IVML, which is mostly out of scope here (please refer to \cite{IVML-LS} 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), container 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~\cite{CzarneckiHelsenEisenecker05a} 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 \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 \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. 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 uniqualy 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 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. + +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 \cite{Eichelberger16}. More specifically, we distinguish between incremental reasoning \begin{itemize} \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. @@ -79,6 +78,8 @@ Further, we denote the undefined value by $\undef$. If not indicated otherwise, all operations introduced below that are bound to a certain type return $\undef$ if the operation is used with another type. +For individual algorithms, we use the actual name of the implementation (to ease mapping code to algorithms and back) and indicate the name in the caption of the algorithm. For simplicity, we ignore that elements or results of functions in the actual implementation may be a null pointer and respective checks are needed in the actual implementation. In the algorithm descriptions in this document, we simply assume that function return either $\undef$ or (in case of set or sequences) $\set{}$, + \subsection{IVML elements} -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. +In this section, we discuss the IVML elements and types that are relevant to the reasoning. For these elements and types we 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 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}$. No specific functions are required here for \textit{basic types} (Boolean, Integer, Real String). In IVML, a \textit{configuration reference} points to a variable in the same project or elsewhere. A configuration reference is indicated through the generic reference type, e.g., \IVML{refTo(SomeCompound)}. As the actual IVML specification \TBD{IVML-spec} does not define specific properties or operations for reference types, we assume here that variables of reference types are transparent and just provide access to the referenced variable. In particular, this holds even if constraints are defined on that variable, as they are evaluated on the referenced variable. @@ -88,69 +89,7 @@ An IVML 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. -\subsubsection{Configuration Variables} - -An IVML 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 containers). 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}$$ - -$$allParents(v) = \begin{cases}\set{}, & \text{if } \neg isVariable(parent(v)) \\ \set{parent(v)} \cup allParents(parent(v)), & \text{else}\\ \end{cases}$$ - -\subsubsection{Project} - -A 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)$. - -\subsubsection{Constraints}\label{sectNotationConstraints} - -As introduced above, a constraint is a Boolean expression that must always be evaluated to $true$. Otherwise, reasoning shall either fail or, after a change of the involved variables, the constraint shall be re-evaluated potentially whiping out a previous reasoning error. A constraint consists of expressions, that can evaluate to any type supported by IVML. These expressions can be used to determine the default value of variables. - -Moreover, \textit{Constraint} is an IVML type, indicating that a variable actually holds a constraint. From the reasoning point of view, a constraint within a constraint variable is evaluated as any other constraint. However, the value in such a variable may, as for all other variables, be undefined, frozen, or re-defined (once per project scope) implying that the new constraint must also be re-evaluated. - -We define two basic functions, namely $isConstraint(t)$ indicating wether type $t$ is a constraint type and $isAssignmentConstraint(c)$ whether constraint $c$ changes the value of a variable through an assignment, e.g., for an integer variable \IVML{x} in IVML notation \IVML{x = 25;}. - -As we will discuss in Section \ref{sectTranslation}, various constraints must be instantiated, complemented and rewritten during the constraint translation process, which is executed per project directly before the reasoning step in order to fill the constraint base. For this purpose, we use a specific constraint creation notation, which combines algorithm elements carrying actual values/elements (written in mathematical notation) and IVML expression operation (displayed in teletype) used to build up the constraint expression. In more detail, for creating the IVML constraint \IVML{x = 25;}, we denote $\createConstraint{\IVML{assign(x, 25)}}$, i.e., angle brackets indicate a constraint creation, while \IVML{assing} is the assign operation defined by IVML (actually implementing the equals in \IVML{x = 25;}, returning a Boolean value indicating whether the execution of the operation succeeded). In an algorithm, we may denote $\createConstraint{\IVML{assign}(x, 25)}$, whereby $x$ is determined by the algorithm and used to instantiate the constraint. For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We attach this information to the constraint itself, i.e., for creating a default constraint, then we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$ - -In some cases, expressions used to build up a constraint are created before the actual constraint and stored in structures for lookup. We denote the creation of an expression by $\createExpression{expr}$. Thereby, sometimes the creation of temporary (local) variables, e.g., for an IVML let-expression or a container iterator is required. We this as follows: $\createExpression{\IVMLMeta{var}(i, t)}$ creates a temporary variable $i$ of type $t$. - -\subsubsection{Compounds} - -A 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))}$$ - -Accessors to compound variables aim at accessing a certain slot within that variable, i.e., an accessor must mention the variable and the slot. Let \IVML{cmp} be an IVML variable of compound type, then an accessor to slot \IVML{slot} looks in IVML notation like \IVML{cmp.slot}. If \IVML{slot} is in turn of compound type, also nested accessors may occur, e.g., \IVML{cmp.slot1.slot2}. For creating such an expression, we use the IVML operation \IVML{acc}\footnote{Actually, a constructor call to create an accessor expression tree node.} Then, following the expression creation notation from Section \ref{sectNotationConstraints}, creating the first accessor within an IVML expression happens through $\createExpression{\IVMLMeta{acc}\IVML{(cmp, slot)}}$, while for the second accessor we use $\createExpression{\IVMLMeta{acc}(\IVMLMeta{acc}(\IVML{cmp}, \IVML{slot}),\IVML{slot2})}$. - -\subsubsection{Containers} - -A \textbf{container} is a parameterized structure that holds an arbitrary number of variables / values. IVML ships with two default container types, namely sequence (duplicates allowed, order important) and set (no duplicates allowed, order irrelevant). Let $c$ be a container, then $elements(c)$ denotes is the set or sequence of all element values in $c$, respectively. Let type $t$ be a container type, then $isContainer(t)$ returns $true$ and $contained(t)$ returns the directly contained type, e.g., for a \IVML{setOf(setOf(Integer))} $contained(t)$ returns \IVML{setOf(Integer)}. We define $isNested(t) = isContainer(contained(t))$ and - -$$nested(c)=\begin{cases}nested(contained(t)), & \text{if } isNested(t) \\ contained(t), & \text{else} \\ \end{cases}$$ - -returns the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested(t)$ returns \IVML{Integer}. In some situations, we must identify whether a container contains constraints, i.e., $isConstraintContainer(t) = isNested(t) \wedge isConstraint(nested(t))$. More generally, we also define a function that returns the set of all (contained) types used in a container, i.e., $usedTypes(c) = \setWith{contained(type(e))}{e\in elements(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 \IVML{seq[1]} and the accessor to \IVML{slot} would then be the combined expression \IVML{seq[1].slot}, for creating an expression $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. - -\subsubsection{Derived types} - -In IVML, a derived type creates a new type based on an existing type. A derived type can restrict the base type by specifiying constraints, as well as a type alias if no further constraints are given. - -For a derived type $t$, $isDerived(t)$ returns true and $base(t)$ \TBD{only base or most basic base type?} returns the type $t$ is derived from. For specifying constraints, a base type implicitly declares a variable $decl(d)$ of type $t$. Of course, derived types can be defined based on already existing derived types. In this case, a chain of base types is created, whereby for reasoning typically the most basic type is relevant. For constraint translation in reasoning, it is relevant to iterate over all base types of such a chain, e.g., and to instantiate their declared constraints. Therefore, we define - -$$allBase(t) = \begin{cases}\set{t}, & \text{if } isDerived(t) \wedge base(t) = \undef \\ \set{t} \cup allBase(base(t)), & \text{if } isDerived(t) \wedge base(t) \neq \undef \\ \emptySet, & \text{else}\\ \end{cases}$$ - -\subsubsection{Reasoning structures \TBD{?Misc?}} +Due to the specific semantics of default or frozen variables, IVML variables have an internal state. The state of individual variables is actually changed (indirectly) by the expression evaluator as side effect of constraint evaluation. The following states are defined: \begin{itemize} - \item An assignment state classifies the value in an IVML configuration variabe according to the configuration lifecycle. Relevant assignment states are: - \begin{itemize} \item \IVML{UNDEFINED}: no value has been assigned so far or the value was cleared intentionally. \item \IVML{DEFAULT}: a type compatible default value has been assigned by evaluating the default value expression of the underlying variable declaration. Default values can be changed unless frozen. Then the variable receives one of the following assignment states. @@ -159,8 +98,67 @@ \item \IVML{DERIVED}: a type compatible value has been assigned as a consequence of evaluating constraints, e.g., through the reasoner. \item \IVML{FROZEN}: the variable was frozen through the IVML \IVML{freeze} statement to avoid further changes of the actual value (including no value in state \IVML{UNDEFINED}). Further assignments are not allowed and cause an assignment error. - \end{itemize} \end{itemize} -\TBD{Algorithms + implementation name, for simplicity we ignore here that variable values can be \IVML{null}, would lead to $\undef$ on some operations and shall be filtered out/considered properly by an implementation.} - + +\subsubsection{Configuration Variables} + +An IVML 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 containers). 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}$$ + +$$allParents(v) = \begin{cases}\set{}, & \text{if } \neg isVariable(parent(v)) \\ \set{parent(v)} \cup allParents(parent(v)), & \text{else}\\ \end{cases}$$ + +\subsubsection{Project} + +A 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)$. + +For simplicity, we ignore in the algorithm descriptions that IVML variables can have the IVML value \IVML{null}, i.e., explicity undefined (and different from a null pointer). While the underyling implementation utilizes in specific cases explicit checks, we just assume here that the defined operations lead to $\undef$. + +\subsubsection{Constraints}\label{sectNotationConstraints} + +As introduced above, a constraint is a Boolean expression that must always be evaluated to $true$. Otherwise, reasoning shall either fail or, after a change of the involved variables, the constraint shall be re-evaluated potentially whiping out a previous reasoning error. A constraint consists of expressions, that can evaluate to any type supported by IVML. These expressions can be used to determine the default value of variables. + +Moreover, \textit{Constraint} is an IVML type, indicating that a variable actually holds a constraint. From the reasoning point of view, a constraint within a constraint variable is evaluated as any other constraint. However, the value in such a variable may, as for all other variables, be undefined, frozen, or re-defined (once per project scope) implying that the new constraint must also be re-evaluated. + +We define two basic functions, namely $isConstraint(t)$ indicating wether type $t$ is a constraint type and $isAssignmentConstraint(c)$ whether constraint $c$ changes the value of a variable through an assignment, e.g., for an integer variable \IVML{x} in IVML notation \IVML{x = 25;}. + +As we will discuss in Section \ref{sectTranslation}, various constraints must be instantiated, complemented and rewritten during the constraint translation process, which is executed per project directly before the reasoning step in order to fill the constraint base. For this purpose, we use a specific constraint creation notation, which combines algorithm elements carrying actual values/elements (written in mathematical notation) and IVML expression operation (displayed in teletype) used to build up the constraint expression. In more detail, for creating the IVML constraint \IVML{x = 25;}, we denote $\createConstraint{\IVML{assign(x, 25)}}$, i.e., angle brackets indicate a constraint creation, while \IVML{assing} is the assign operation defined by IVML (actually implementing the equals in \IVML{x = 25;}, returning a Boolean value indicating whether the execution of the operation succeeded). In an algorithm, we may denote $\createConstraint{\IVML{assign}(x, 25)}$, whereby $x$ is determined by the algorithm and used to instantiate the constraint. For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We attach this information to the constraint itself, i.e., for creating a default constraint, then we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$ + +In some cases, expressions used to build up a constraint are created before the actual constraint and stored in structures for lookup. We denote the creation of an expression by $\createExpression{expr}$. Thereby, sometimes the creation of temporary (local) variables, e.g., for an IVML let-expression or a container iterator is required. We this as follows: $\createExpression{\IVMLMeta{var}(i, t)}$ creates a temporary variable $i$ of type $t$. + +\subsubsection{Compounds} + +A 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))}$$ + +Accessors to compound variables aim at accessing a certain slot within that variable, i.e., an accessor must mention the variable and the slot. Let \IVML{cmp} be an IVML variable of compound type, then an accessor to slot \IVML{slot} looks in IVML notation like \IVML{cmp.slot}. If \IVML{slot} is in turn of compound type, also nested accessors may occur, e.g., \IVML{cmp.slot1.slot2}. For creating such an expression, we use the IVML operation \IVML{acc}\footnote{Actually, a constructor call to create an accessor expression tree node.} Then, following the expression creation notation from Section \ref{sectNotationConstraints}, creating the first accessor within an IVML expression happens through $\createExpression{\IVMLMeta{acc}\IVML{(cmp, slot)}}$, while for the second accessor we use $\createExpression{\IVMLMeta{acc}(\IVMLMeta{acc}(\IVML{cmp}, \IVML{slot}),\IVML{slot2})}$. + +\subsubsection{Containers} + +A \textbf{container} is a parameterized structure that holds an arbitrary number of variables / values. IVML ships with two default container types, namely sequence (duplicates allowed, order important) and set (no duplicates allowed, order irrelevant). Let $c$ be a container, then $elements(c)$ denotes is the set or sequence of all element values in $c$, respectively. Let type $t$ be a container type, then $isContainer(t)$ returns $true$ and $contained(t)$ returns the directly contained type, e.g., for a \IVML{setOf(setOf(Integer))} $contained(t)$ returns \IVML{setOf(Integer)}. We define $isNested(t) = isContainer(contained(t))$ and + +$$nested(c)=\begin{cases}nested(contained(t)), & \text{if } isNested(t) \\ contained(t), & \text{else} \\ \end{cases}$$ + +returns the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested(t)$ returns \IVML{Integer}. In some situations, we must identify whether a container contains constraints, i.e., $isConstraintContainer(t) = isNested(t) \wedge isConstraint(nested(t))$. More generally, we also define a function that returns the set of all (contained) types used in a container, i.e., $usedTypes(c) = \setWith{contained(type(e))}{e\in elements(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 \IVML{seq[1]} and the accessor to \IVML{slot} would then be the combined expression \IVML{seq[1].slot}, for creating an expression $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. + +\subsubsection{Derived types} + +In IVML, a derived type creates a new type based on an existing type. A derived type can restrict the base type by specifiying constraints, as well as a type alias if no further constraints are given. + +For a derived type $t$, $isDerived(t)$ returns true and $base(t)$ \TBD{only base or most basic base type?} returns the type $t$ is derived from. For specifying constraints, a base type implicitly declares a variable $decl(d)$ of type $t$. Of course, derived types can be defined based on already existing derived types. In this case, a chain of base types is created, whereby for reasoning typically the most basic type is relevant. For constraint translation in reasoning, it is relevant to iterate over all base types of such a chain, e.g., and to instantiate their declared constraints. Therefore, we define + +$$allBase(t) = \begin{cases}\set{t}, & \text{if } isDerived(t) \wedge base(t) = \undef \\ \set{t} \cup allBase(base(t)), & \text{if } isDerived(t) \wedge base(t) \neq \undef \\ \emptySet, & \text{else}\\ \end{cases}$$ \section{Reasoning algorithm}\label{sectReasoning} @@ -648,3 +646,6 @@ We are grateful to Phani Saripalli for implementing the initial IVML reasoner based on the Jess rules engine. We are also grateful to Roman Sizonenko for implementing and experimenting with the Drools-based IVML reasoner and for realizing the initial SSE IVML reasoner used as basis for the actual version of the reasoner and this documentation. +\bibliographystyle{abbrv} +\bibliography{reasoner} + \end{document}