Automating the analysis of stateful feature models

AUTOMATING THE ANALYSIS OF STATEFUL FEATURE MODELS PABLO TRINIDAD MART´ IN-ARROYO PhD dissertation Supervised by Dr. Antonio Ruiz Cort´es Universidad de Sevilla December 2012 First published in January 2013 by Pablo Trinidad Mart´ ın-Arroyo Copyright © MMXIII http://www.lsi.us.es/˜trinidad [email protected] This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by Pablo Trinidad. All persons copying this information are expected to adhere to the terms and constraints invoked by each author’s or holders’ copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder. Support: PhD dissertation granted by the University of Seville, the European Commission (FEDER) and Spanish Government under CICYT project SETI (TIN2009-07366) and the Andalusian Government projects ISABEL (TIC-2533) and THEOS (TIC-5906) A mis abuelos y a Joaqu´ ın AGRADECIMIENTOS i El desarrollo de una tesis es un camino largo, en el que se encuentran muchos obst´ aculos, momentos dif´ ıciles y momentos de euforia. En este camino he tenido muchos compa- ˜ neros de viaje que me han empujado y animado a llevar a cabo con ´ exito esta tesis. He tenido la suerte de recorrer este camino con Antonio. No puedo entender este trabajo sin su capacidad de sacar siempre algo m´ as y esforzarse al m´ aximo para llegar m´ as all´ a de donde creemos posible. Este trabajo es fruto de nuestra ambici´ on, que nos ha llevado tal vez m´ as lejos de lo que la costumbre establece pero que esperamos que marque un antes y un despu´ es en nuestra vida investigadora. Para ´ el toda mi gratitud y afecto. Quiero agradecer los ´ animos y el cari˜ no que he recibido de aquellas personas con las que comparto mi d´ ıa a d´ ıa y que hacen que compensen todas las desavenencias que sufrimos a diario. A Carlos, amigo desde ”chiquititos” que me sufre a diario en todas mis versiones; A Sergio, Jos´ e Mar´ ıa, Guti, Cristina y Adela, con quien comparto y disfruto gran parte de mi d´ ıa a d´ ıa; A David Ruiz, cuyos consejos me ayudan a mejorar d´ ıa a d´ ıa; A David Benavides, mi primer compa˜ nero de viaje, que juntos comenzamos a creer en esto de la investigaci´ on y con quien comparto muchos ´ exitos y momentos felices; A Manolo, el mejor compa˜ nero en mis aventuras docentes y espero que en un futuro muy pr´ oximo tambi´ en en mis aventuras investigadoras; A Jes´ us, ”mi becario” que me recuerda mucho a cuando era insultantemente joven y ten´ ıa energ´ ıas para comerme el mundo. Espero poder dedicarte todo mi esfuerzo en sacar lo mejor de ti; Y al resto de personas con quien comparto menos momentos pero no por ello menos gratificantes: Jos´ e Antonio, Kino, Bea, Amador, Octavio, Ana Bel´ en, Pablo, Jose y Sergio Pozo. Por ´ ultimo, y no por ello menos importante, a Miguel Toro porque en dos ocasiones me hizo encontrar la pieza que faltaba para que todo encajara. Quisiera tambi´ en hacer una menci´ on especial a los miembros del tribunal, que en los meses previos a la defensa se han prestado a revisar este trabajo y han ofrecido puntos de vista que han ayudado a mejorar este trabajo. Gran parte del sobreesfuerzo y el desgaste lo sufre mi familia. A mis padres, hermanos, primos y t´ ıos para los que me faltan palabras para agradecerles su cari˜ no y apoyo. A Mar´ ıa, mi principal soporte en este largo camino y que me ha ayudado en los mejores y peores momentos a sacar esto adelante. Y a mis abuelos y a Joaqu´ ın, todos los d´ ıas que hab´ eis faltado siempre hab´ eis estado presentes. ♦♦♦ I’d like to make a special mention to the panel members who, in the months before the defense, have contributed with their valuable revisions, which has helped to improve the quality of this work. ii ABSTRACT iii Modeling variability is a major task in developing Software Product Lines (SPLs).Feature Models (FMs) are the most widely used model for this purpose. A FM represents as a hierarchy of features, the set of decisions that users can take to configure their products. To date, these decisions are limited to select and remove features, preventing decisions on other important elements such as cardinalities and attributes. Moreover, the automated extraction of information from FMs, a.k.a Automated Analysis of Feature Models (AAFM) is a thriving topic that has caught the attention of researchers for the last twenty years. The AAFM offers a wide range of analysis operations for different purposes. The general approach to solve these analysis operations is to give an operational semantics in terms of declarative languages that allow the extraction of information by means of logic solvers. Following this approach over 30 operations analysis have been proposed to date. A subset of these transactions so-called explanatory operations offers the possibility of providing explanations for the relationships that cause certain errors or conflicting user decisions to be repaired in a configuration. However, of all proposed explanatory operations to date, only a subset of them has a formal semantics. In this scenario there are three problems that this thesis faces: first, FMs are not fully-configurable since they prevent decisions on any kind of element. Second, it is necessary to endow all the explanatory operations with a formal semantics. Third, there is a large number of analysis operations that do not support fully-configurable FMs. It raises a need to propose a new formal framework for their support. In this work we start from two conjectures: that there is a correlation between explanatory and non-explanatory operations, and it is possible to interpret both types of operations as Deductive and Abductive Problems (DAPs). Relying on these assumptions, in this thesis we present three main contributions in order to solve the raised problems: (i) we propose Stateful Feature Models (SFMs) as fully-configurable models that enable users to make decisions about all of its elements, (ii) the use of SFMs and its interpretation as DAPs allow us to give a formal semantics for explanatory analysis in a compact manner, performing all the operations proposed to date as special cases of two explanatory operations, (iii) as we propose a new model, we see the opportunity to review the entire catalogue AAFM operations, proposing a simplified catalogue operations and a set of composition mechanisms which give flexibility to define new analysis operations. With these contributions, we believe that this work sets the basis for the Automated Analysis of Stateful Feature Models (AASFM) that solves the limitations identified in this work for the AAFM and simplifies the formalisation process and the implementation and testing of the analysis engines. iv RESUMEN v El modelado de la variabilidad es una de las principales tareas en el desarrollo de l´ıneas de productos software (LPS). Los FMs son el modelo m´ as utilizado para ello. Los FMs representan el conjunto de decisiones que pueden tomar los usuarios para configurar su producto como una jerarqu´ ıa de caracter´ ısticas. Hasta la fecha, estas decisiones se limitan a elegir y descartar las caracter´ ısticas que se desean, impidiendo la toma de decisiones sobre otros elementos importantes como son las cardinalidades y los atributos. Por otro lado, la extracci´ on autom´ atica de informaci´ on de los FMs, tambi´ en conocida como an´alisis autom´atico de FMs (AAFM) es un tema que ha sido objeto de investigaci´ on en los ´ ultimos veinte a˜ nos. El AAFM ofrece un amplio cat´ alogo de operaciones de an´ alisis para distintos prop´ ositos. El enfoque general para resolver estas operaciones de an´ alisis consiste en dar una sem´ antica operacional en t´ erminos de lenguajes declarativos que permiten la extracci´ on de informaci´ on por medio de resolutores l´ ogicos. Siguiendo este enfoque se han propuesto hasta la fecha m´ as de 30 operaciones de an´ alisis. Un subconjunto de estas operaciones denominadas explicativas ofrecen la posibilidad de obtener explicaciones sobre las relaciones que provocan determinados errores o las decisiones de usuario conflictivas que deben repararse en una configuraci´ on. Sin embargo, de todas las operaciones explicativas propuestas hasta la fecha, s´ olo un subconjunto de ellas dispone de una sem´ antica formal. En este escenario encontramos tres problemas a los que esta tesis se enfrenta: en primer lugar, los FMs no son modelos completamente configurables al impedir la toma de decisiones sobre todos sus elementos. En segundo lugar, es necesario dotar a todas las operaciones explicativas de una sem´ antica formal. En tercer lugar, existe un elevado n´ umero de operaciones y la incapacidad de algunas de ellas para trabajar con FMs completamente configurables plantea una necesidad de proponer un nuevo marco de trabajo formal que les de soporte. En este trabajo partimos de dos conjeturas: que existe una correlaci´ on entre determinadas operaciones explicativas y otras no explicativas; y que es posible interpretar CONTENTS A.2.3 Representing relationships as constraints . . . . . . . . . . . . . . 168 A.2.4 Representing user decisions as constraints . . . . . . . . . . . . . 169 A.2.5 Generalising stateful feature models . . . . . . . . . . . . . . . . . 171 A.2.6 Collecting user decisions . . . . . . . . . . . . . . . . . . . . . . . 172 A.3 Extensibility ................................... 173 A.3.1 Variationpoints............................. 173 A.3.2 An example of extensibility: supporting attributes . . . . . . . . . 174 B Implementation 177 B.1 Constraint programming . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177 B.1.1 Mapping from FOL to CSP . . . . . . . . . . . . . . . . . . . . . . 178 B.1.2 Deduction in constraint programming . . . . . . . . . . . . . . . . 179 B.1.3 Abduction in constraint programming . . . . . . . . . . . . . . . . 182 B.2 Defaultlogic................................... 186 B.3 Otherimplementations............................. 188 C First-order logics 193 D Acronyms 197 Bibliography 201 xii LIST OF FIGURES xiii 2.1 An example of a product built from a smart home SPL . . . . . . . . . . 16 2.2 A feature diagram example representing a smart home software system 17 2.3 Feature cardinalities may lead to ambiguous situations . . . . . . . . . . 18 2.4 An excerpt of a feature diagram representing an extended FM . . . . . . 19 2.5 An example of a validation operation of the SHS FM . . . . . . . . . . . . 23 2.6 An example of operation for configuration validation . . . . . . . . . . . 24 2.7 An example of the configuration validation and explanation operations 25 2.8 Example of anomalies in a FM . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.9 Example of dead feature detection and explanation . . . . . . . . . . . . 26 2.10 General schema of the AAFM . . . . . . . . . . . . . . . . . . . . . . . . . 27 3.1 Aone-invertercircuit.............................. 38 3.2 Thefive-personexample............................ 43 5.1 A visual metaphore of FMs, Configuration Models (CMs) and SFMs . . . . 60 5.2 A geometrical interpretation of basic concepts in SFMs . . . . . . . . . . 62 5.3 An example of a Stateful Feature Diagram . . . . . . . . . . . . . . . . . . 69 5.4 Stateful Feature Metamodel in UML format . . . . . . . . . . . . . . . . . 71 5.5 An example of a user configuration . . . . . . . . . . . . . . . . . . . . . . 73 5.6 An example of a user configuration . . . . . . . . . . . . . . . . . . . . . . 74 5.7 An example of state reset operation . . . . . . . . . . . . . . . . . . . . . . 74 6.1 General schema of the AASFM . . . . . . . . . . . . . . . . . . . . . . . . 79 6.2 A stateful feature diagram example . . . . . . . . . . . . . . . . . . . . . . 82 7.1 An example of products listing operation . . . . . . . . . . . . . . . . . . 93 LIST OF FIGURES 7.2 An example of a propagation operation . . . . . . . . . . . . . . . . . . . 96 8.1 An example of ’why are the explanation not valid? operation . . . . . . . 105 8.2 An example of ’why is a configuration not valid?’ operation . . . . . . . 107 9.1 An example of a void and a non-void (valid) SFM . . . . . . . . . . . . . 116 9.2 An example of products counting . . . . . . . . . . . . . . . . . . . . . . . 117 9.3 An example of configure with propagation . . . . . . . . . . . . . . . . . 118 9.4 Anexampleoffiltering............................. 119 9.5 An example of optimisation operation . . . . . . . . . . . . . . . . . . . . 119 9.6 Example of anomalies in SFMs . . . . . . . . . . . . . . . . . . . . . . . . 122 9.7 An example of compound explanatory operation for a void SFM . . . . . 127 10.1FAMAFWArchitecture ............................ 135 10.2 Overview on the STateful fEature model Analyser (STEAm) operation . . . 136 10.3 Process followed by STEAm to analyse SFMs in SPEM format . . . . . . 138 10.4 Metamodels used in STEAm . . . . . . . . . . . . . . . . . . . . . . . . . . 140 10.5StaPLeMetamodel ............................... 141 10.6CSPMetamodel................................. 144 10.7 Verification of STEAm using BeTTy . . . . . . . . . . . . . . . . . . . . . 148 A.1 Stateful Feature Metamodel in UML format . . . . . . . . . . . . . . . . . 163 A.2 Generic classes of the SFMM . . . . . . . . . . . . . . . . . . . . . . . . . . 164 A.3 Features and cardinalities in the SFMM . . . . . . . . . . . . . . . . . . . 165 A.4 Elementslifecycle................................ 166 A.5 Kindsofrelationship .............................. 169 A.6 Kinds of configuration constraints . . . . . . . . . . . . . . . . . . . . . . 170 A.7 Stateful Feature Model class in detail . . . . . . . . . . . . . . . . . . . . . 172 A.8 An example of extension of the SFMM for a basic attributes support . . . 174 C.1 Elements of First Order Languages and their Relationships . . . . . . . . 194 xiv LIST OF TABLES xv 2.1 Current support for configuration explanations . . . . . . . . . . . . . . . 31 2.2 Current support for relationship explanations . . . . . . . . . . . . . . . . 33 3.1 Traceability table for the one-inverter circuit DP . . . . . . . . . . . . . . 39 5.1 A comparison of the use of elements in different kinds of feature models 61 5.2 Kinds of relationship constraints in a SFM . . . . . . . . . . . . . . . . . . 64 5.3 Kinds of decision constraints in a SFM . . . . . . . . . . . . . . . . . . . . 65 6.1 SemanticsforaSFMP.............................. 86 6.2 Traceability table for constants and variables . . . . . . . . . . . . . . . . 87 7.1 A DP representing the example in Figure §6.2 . . . . . . . . . . . . . . . . 91 8.1 Abduction problem for relationships explanation . . . . . . . . . . . . . . 102 8.2 Abduction Problem for configuration explanation . . . . . . . . . . . . . 104 9.1 Basic operations in the AASFM . . . . . . . . . . . . . . . . . . . . . . . . 115 9.2 Scenarios and their relationship with query and explanatory operations 127 B.1 Mapping Explanatory Operations into a CSP . . . . . . . . . . . . . . . . 180 B.2 ExampleSFMasaCSP............................. 181 B.3 Example SFM as a CSP for relationship explanation . . . . . . . . . . . . 184 B.4 Example SFM as a CSP for configuration explanation . . . . . . . . . . . 185 B.5 Example SFM in terms of default logic for relationships explanation . . . 189 B.6 Example SFM in terms of default logic for configuration explanation . . 190 LIST OF TABLES xvi INTRODUCTION PART I 1 INTRODUCTION 3 The secret of happiness is not in doing what one likes, but in liking what one does. Sir James Matthew Barrie (1860–1937), Novelist This Chapter presents an overview on the results presented through this dissertation. In Section §1.1 we review the research context. In Section §1.2 we motivate this work, explaining its purpose. Section §1.3 details the problem in terms of research questions. Section §1.4 defines several goals for this work. In Section §1.5 we anticipate the approach followed to fulfil the goals. Section §1.6 presents the context in which this dissertation has been carried. Last, the structure of this dissertation is presented in Section §1.7. CHAPTER 1. INTRODUCTION 1.1 RESEARCH CONTEXT The construction of products tailored to the specific needs of each customer is one of the challenges that the hardware industry has faced. In the crafts a client is free to customise a product choosing its features, but its cost can skyrocket. In mass production, costs are greatly reduced but the customer loses its ability to make decisions and must submit to the products already manufactured. Product lines are an alternative to achieve the so-called mass customisation, an intermediate point between craft and mass production where customers are allowed to make a set of decisions to customise the final product that best suits their needs within a range of possible features. Producing customised software product is demanded in many different scenarios. So for example, Android OS must be adapted to work in different mobile devices; or Ubuntu OS that can be adapted to different user needs by offering a wide range of configuration options before and after installation. Developing and maintaining a specific OS for each terminal or user computer is generally an unfeasible approach in terms of cost and time. SPLs [23] incorporate successful practices in hardware product lines to the software world. SPLs propose a set of techniques for the development, maintenance and evolution of customised software products in which the end user plays a key role. Since the set of products that can be manufactured in a SPL can be huge, with thousands of products [57,80] it is necessary to have models that make it possible both to represent the complete set of products in a compact manner and to enable its systematic and automated management. Feature Models (FMs) [53] are one of the most widely used models for this purpose, proposing a compact representation of all the products in an SPL in terms of their features. A feature is an increment in product functionality [5]. Features are connected by means of relationships among them, forming a tree-like structure. Relationships constrain the way in which features can be combined. Besides features, FMs might use cardinalities to group features in the so-called Cardinality-Based Feature Models (CBFMs) and/or attributes to remark non-functional characteristics of products in the so-called Extended Feature Models (EFMs). The process by which one or more users define the product that best fits their needs by making successive decisions on a particular FM is called configuration process. This process is successfully accomplished when a threefold condition fulfils: there are no more user decisions to make, there exists only one product in the SPL satisfying each and every user decision, and there are no contradictions among decisions. The deci- 4 1.1. RESEARCH CONTEXT sions made by users in a configuration process are collected by the so-called Configuration Model (CM), or simply a configuration. The automated extraction of information from FMs and CMs, a.k.a Automated Analysis of Feature Models (AAFM)1is a thriving topic that has caught the attention of researchers for the last twenty years [7,14]. It is commonly accepted that this extraction is carried out by the so-called analysis operations for which there is already a catalogue with over 30 analysis operations. The analysis operations allow for example to know whether a feature model is valid (i.e. it represents at least one product), how many products a FM represents, whether a CM is valid (i.e. each and every user decision can be made) or to calculate different metrics. One of the most important applications of the AAFM is the so-called FM debugging [7,53,89], a process to produce error-free FMs. Debugging might be performed in three steps: error detection, error explanation and reparation. Detection performs several analysis operations to find different kinds of error. Error explanation identifies the relationships that cause such errors. These explanations are used to assist with the manual or automatic reparation of errors. Besides debugging, explanations have other applications such as explaining the conflicting user decisions in invalid configurations [99] or explaining why a FM has certain properties [85]. In general terms, an explanation can be defined as an analysis operation that takes a FM, optionally a CM and an analysis operation as inputs and returns information (so-called explanations) about the reasons of why or why not the corresponding response of the operation. The use of declarative paradigms in the AAFM is the main trend, due to the availability of off-the-shelf solvers able to reason about them. Most of the proposals in the AAFM perform analysis operations by means of propositional logic [5,64], constraint programming [10,89,99] or description logic [39] among others. This approach has enabled the development of AAFM engines such as AHEAD [6], FaMa Framework [90], Gears [79], pure::variants [72] and SPLOT [62]. The use of declarative techniques, executable by solvers, endow the analysis operations with an operational semantics [48]. Alternatively, some authors [9,16,22] have proposed an axiomatic semantics to prove certain properties of FMs. Dur´ an et al. [36] propose a translational semantics that can be used to check the correctness of the analysis operation implementations [78]. The AAFM in general is a research field with an important focus on formalisation. However, only a few proposals dare to formalise explanations such as [5,37,89,99,100]. 1Traditionally the term configuration model has been omitted both in the acronym AAFM and in the definition, although it has been always implicitly present. 5 CHAPTER 1. INTRODUCTION 12 2 BACKGROUND INFORMATION 13 Humour is part of life, and therefore should not be shut out even from serious literature Lin Yutang (1895–1976), Chinese writter In this Chapter we present the background concepts that are provided for a better understanding of the problems and solutions described in this dissertation. First, we present FMs in Section §2.2. Section §2.3 describes the configuration process and a general configuration model. Section §2.4 presents the AAFM as a set of techniques for the automated extraction of useful information from FMs. To illustrate its scope, some of the most used analysis operations and the general approach to implement AAFM operations are presented. In Section §2.5 we focus on the state of the art of explanatory analysis, a remarkable subset of AAFM operations. Section §2.6 provides an overview on constraint satisfaction problems which are a widely used approach in the AAFM. Finally, Section §2.7 summarises the background concepts and advances their relationship with this dissertation. CHAPTER 2. BACKGROUND INFORMATION 2.1 SOFTWARE PRODUCT LINES The mass production aims to reduce the costs in the production of a large amount of hardware products. Unitary costs are reduced while the benefit margins increase, enabling the investment in technological improvements that improve the quality of the products. A mass production produces identical products which may not fit into user needs, and therefore limiting the target market. Adapting a product to user needs is usually considered a craftwork whose costs are quite higher than a massive product. The mass customisation aims to be competitive in the production of customised products. A user is given a margin of freedom in their decisions so that products are customised while the benefits of a mass production are still kept. It allows to produce customised products at very competitive costs. The digital distribution of software has almost buried the physical distribution and therefore the mass production of software. However the mass customisation in software at a low cost and time-to-market is still an open-issue. The Software Product Line (SPL) approach [23] offers a set of techniques, methods and methodologies to produce customised products in mass. It is based in the similarity and segmentation among products. So products are produced in a specific domain where the commonalities and variabilities among demanded products is well-known. SPLs systematise the reuse of software, building a common base of assets that are later combined to generate products that are adapted to user needs. This approach is opposite to ad-hoc reuse which searches for reusable software pieces from other already-built products to reduce the time to market. 2.2 FEATURE MODELS One of the main challenges in SPLs is about the definition of all the possible products that a user can choose. Since the number of products can be very large, it is necessary to represent all of them compactly. One of the most used techniques to represent all the products within a SPL are the so-called Feature Models (FMs). Products are described in terms of features, which are distinctive characteristics a user can observe [53]. A FM can de defined as follows: 14 2.2. FEATURE MODELS Definition 2.1 - Feature Model. A FM is a tuple (F,P)such that Fis the set of features in the SPL and Pthe set of products defined as a subset of the powerset of features, i.e. P⊆ P(F), such that a product is defined by a set of features in F. Let us take a SPL of Smart Home Systems (SHSs) as an example. Its set of features F and a possible product P1(see Figure §2.1) can be defined as follows: F={SmartHome,Lighting,ControlSystem,CellPhone,ControlPanel, Antithe f tAlarm,Internet,Ethernet,3G,WiFi −b/g,WiFi −n,MoviePlayers, HDTV42, HDTV32,PCPlayer,Contents,VideoOnDemand,Providers, Cache,DMS} P1={SmartHome,Lighting,CellPhone,Alarm,HDTV42, HDTV32,DMS,VideoOnDemand} In order to define the set of products, a FM comprises a set relationships that limits the allowed feature combinations, so that a product must satisfy all the relationships. Relationships in a FM are mainly hierarchical. Any FM has a root feature that represents the whole functionality of any product. The root feature is refined in child features, which decompose the behaviour or functionality of the root feature into subfeatures, which describe the scope of the root feature in more detail. This refinement process is repeated for the child features to conform a tree-like structure. Although the hierarchical structure helps to represent the feature refinement, it can hinder the representation of restrictions that affect features in different branches of the tree. In these circumstances, cross-tree constraints can be used. Feature diagrams [75,76] are probably the most used graphical representation of FMs. Figure §2.2 presents a feature diagram for a SPL of SHSs. The so-called basic FMs have evolved in time adding new elements to the set of features and relationships. So Czarnecki et al. [29] and Riebisch et al. [75] propose CBFMs as an evolution of basic FMs that introduce cardinalities. They allow to group a set of features and assign them a cardinality that denotes the number of features (cardinal) that can be selected at the same time. CBFMs increase the succinctness of the model, and they are as expressive as basic FMs, as Schobbens et al. [76] proved. CBFMs use the following kinds of hierarchical relationships in FMs: 15 CHAPTER 2. BACKGROUND INFORMATION !"#$%&%'&($)*'#+ ,-%."#$-/+ 01*-)+ 234+5!+ 634+7(5!+ ,8+ 8$11+,9%'$+ :$;<%-=+ (">";*1+?$#"*+ @$-.$-+A(?@B+ Figure 2.1: An example of a product built from a smart home SPL •Mandatory: a mandatory relationship affects a parent and child feature. It forces the child feature to appear in a product whenever its parent feature does. For example, any SHS must have lighting and controlSystem features. If a videoOn- Demand feature is selected, then providers must also be selected. •Optional: a child feature connected to a parent feature by means of an optional relationship may be optionally selected whenever its parent feature is. For example, the antitheftAlarm and Internet connection are optional features in a SHS. •Set relationship: set relationships affect a parent feature and a set of two or more child features. It contains a set of natural numbers or cardinality that constraints the number of child features to be selected in a product whenever its parent feature is selected. For example, if the Internet feature is selected, then 1 to 4 features must be selected from Ethernet,3G,WiFi-b/g and WiFi-n features. 16 2.2. FEATURE MODELS !"#$%&'(")& *+,-./,&0(/%$(1& !23%)"& 4(5+)& 61#2)$3& 7/.8%-)9& 71#$"& 0(/%)/%3& 0)11&:-(/)&0(/%$(1& :#/)1& ;<==>?& @+A)(&(/& B)"#/A& B+,+%#1&4)A+#& !)$5)$& ;<==>?& 'BC@&D>E& 'BC@&F>E& ;<==F?& G%-)$/)%& FH& ;<==D?& I+J+8KL,& I+J+8/& :$(5+A)$3& 0#M-)& :$(5+A)$&7& :$(5+A)$&N& ;<==>?& :0:1#2)$& *),)/A& 4#/A#%($2& O6.(/#1& B)6)/A3& !)%& GPM1QA)3& R/%)$/)%& Figure 2.2: A feature diagram example representing a smart home software system Alternative relationships can be interpreted as a particular case of set-relationship with a [1..1]cardinality, where only one child feature may be selected in a product at the same time if the parent feature is selected. In turn, or-relationships are those set relationships whose cardinality is [1..N]such that Nis the number of child features. For example, the InternetConnection feature is the parent in an orrelationship. Besides hierarchical relationships, cross-tree constraints break the tree-like structure to represent non-hierarchical relationships. The most used cross-tree constraints are: •Dependency: a feature depends on another feature if the second one must be part of a product whenever first one is selected. For example, the cache feature requires for a digitalMediaServer feature to store video and the antitheftA- larm requires a controlPanel for de/activation. •Exclusion: two features exclude themselves if both of them cannot be part of a 17 CHAPTER 2. BACKGROUND INFORMATION !"#$ %&#'$ ("#)$ *+,$ -.//.0$ -1//10$ Figure 2.3: Feature cardinalities may lead to ambiguous situations product at the same time. For example the antitheftAlarm feature is incompatible with a cellPhone feature for security reasons. Riebisch et al. [75] also propose a feature cardinality relationship, where a parent and a child feature are linked by a cardinality which indicates the number of valid instances of the child features that can be selected in a product. The cardinality [0..1] is equivalent to an optional relationship and [1..1]to a mandatory relationship. Features in a FM are unique, which means that no other feature can refer to the the same functionality. However, with feature cardinalities it is possible to create more than one feature instance, although the concept of instance still has an ambiguous interpretation. The FM in Figure §2.3 shows an example where the ambiguity arises. A car must have 4 tires, each of which can be hard or soft. Must all the tires be either soft or hard? Or is it possible to combine them anyhow? How do we distinguish between rear and front tires in case we want to combine hard and soft tires? Due to the ambiguity that arises from the use of feature cardinalities, they are usually avoided in CBFMs. Besides features, FMs can collect additional information by using the so-called attributes. An attribute represents relevant information such as feature development cost, versions, RAM consumption, performance or technological requirements. FMs that use attributes are known as EFMs [10]. Figure §2.4 shows an example of a FM with attributes. It adds information regarding Internet bandwidth to an excerpt of the FM in Figure §2.2. Each kind of connection provides a different bandwidth. Since more than one connection can be chosen, the maximum available Internet bandwidth in the SHS is the maximum bandwidth provided by each chosen connection. An EFM may contain constraints that affect attributes which reduce even more the set of products an EFM describes. So for example, if a constraint sets the Internet max 18 2.3. PROCESSES AND MODELS OF CONFIGURATION !"#$%"$#& '#($%"$#& )*& +,--./& 01213456& 01213"& 789:8";<1;#(=&>?8#& @$%?3A8BC$&D&E-E& & 48";<1;#(=&>?8#& F$%?3A8BC$&D&E-E& 48";<1;#(&G&H.&I&48";<1;#(&J&KEE& & 48";<1;#(=&>?8#& F$%?3A8BC$&D&E-E& 48";<1;#(&1"&LKMNM,OM,PMO.M)KM.PMH.Q& & 48";<1;#(=&>?8#& F$%?3A8BC$&D&E-E& :8";<1;#(&JD&O-.& & 48";<1;#(=&>?8#& F$%?3A8BC$&D&E-E& :8";<1;#(&JD&,EE& & !"#$%"$#-789:8";<1;#(&D& R89S'#($%"$#-48";<1;#(M& )*-48";<1;#(M& 01213456-48";<1;#(M& 01213"-48";<1;#(T& Figure 2.4: An excerpt of a feature diagram representing an extended FM bandwidth to at least 80 Mbps then it forces any SHS to have at least an Ethernet or Wifi-n connection since they are the only features providing such bandwidth. In this dissertation we coin the term Extended Cardinality-Based FM (ECBFM) as an FM that incorporates all the capabilities of CBFMs and EFMs. Henceforth, we use the term FM to refer to an ECBFM for the sake of simplicity unless it is necessary to distinguish among them. 2.3 PROCESSES AND MODELS OF CONFIGURATION The process by which one or more users define the product that best fits their needs by making successive decisions on a particular FM is called a configuration process. The decisions made by users in a configuration process are collected in a Configuration Model (CM), or simply a configuration. Depending on how users organise the decisions, three kinds of configuration processes are considered: •Individual configuration: only one user participates in the configuration process. A new decision cannot contradict any decision that has been previously made by the same user. Thus, a feature that is already selected cannot be removed later. •Staged configuration [29]: more than one user performs the configuration process in stages. At each stage one user makes decisions, updating the CM. It is 19 CHAPTER 2. BACKGROUND INFORMATION possible that a user wants to change a decision on a feature that has already been selected or removed by another user in a previous stage. In this sense, the contradiction must be annotated in the CM so that the user that selected or removed the features previously is informed so that the conflict can be solved among users. •Parallel configuration [99]: more than one user makes decisions at the same time and in any order, enabling users to contradict each other. So for example, a user might remove a feature that is being selected by another user at the same time. •Collaborative configuration [63]: this process lies halfway between staged and parallel configuration processes. A number of users are allowed to make decisions in parallel but only on a specific part of the FM. These parts are previously calculated so that conflicts among decisions are avoided. Users usually express their decisions in terms of feature selections or removals, i.e. which features must be part of a product or left aside. In order to collect these decisions CMs are structured as follows: Definition 2.2 - Configuration model. Given a FM as a tuple (F,P), a configuration for this FM, denoted as γFM is a threetuple of the form (S,R,U)in which S,Rand Udenote three disjoint finite sets of selected, removed and undecided features respectively in such a way that all the features of Fmust belong to one and only one of these three sets, i.e. γFM = (S,R,U)⇔F=S∪R∪Uand S∩R∩U=∅ When a configuration process starts, all the features are in the undecided set to indicate that no decision has been made about them. Whenever a user selects a feature, it is moved from the undecided set to the selected set. If a feature is discarded then it is moved from the undecided set to the removed set. Depending on the distribution of features among the three sets, we can define a configuration state as follows: Definition 2.3 - Configuration states. A configuration γFM is partial if there are still decisions to be made, otherwise it is said to be a full configuration. Both states are denoted as partial(γFM)and f ull(γFM). partial(γFM)⇔U,∅ f ull(γFM)⇔U=∅ 20 2.3. PROCESSES AND MODELS OF CONFIGURATION Whether partial or full, a configuration is said to be valid if there is at least one product in the corresponding FM that contains all the features in the selected set and no feature in the removed set; otherwise it is said to be an invalid configuration. Both states are denoted as valid(γFM)and invalid(γFM). valid(γFM)⇔ ∃p∈P·S⊆p∧R∩p=∅ invalid(γFM)⇔¬∃p∈P·S⊆p∧R∩p=∅ From the above definitions, we have an alternative way to consider a product of a FM, namely: Definition 2.4 - Product. Any valid full configuration γFM defines a product that only contains the selected features. We denote this product as product(γFM): product(γFM) = S⇔f ull(γFM)∧valid(γFM) For example, the following configuration for a SHS is partial since some features have already been selected, some others have been removed and others are still to be decided what to do with them: S={SmartHome,Lighting,ControlSystem,CellPhone,Internet,Ethernet} R={ControlPanel,MoviePlayers} U={Antithe f t,Contents,VideoOnDemand,DMS,...} Full configurations are the result of a completed configuration process. For the SHS example, the following configuration is full: S={SmartHome,Ligthing,ControlSystem,CellPhone,Internet,Ethernet} R={ControlPanel,MoviePlayers,Antithe f t,Contents,Videoondemand,...} U=∅ The following example describes a valid partial configuration for the SHS SPL since there exists at least one product with the selected features and without the removed features: S={SmartHome,Lighting,ControlSystem,Cellphone,Internet,Ethernet} R={ControlPanel,Antithe f talarm,Contents,...} U=∅ 21 CHAPTER 2. BACKGROUND INFORMATION [101,102] that map FMs into SMV model checker. Some authors have also proposed ad-hoc algorithms to solve specific analysis operations [3,47,87,94,95]. Each representation enables a subset of analysis operations, each of which having a different performance [12]. So for example a representation can be more suitable for product counting while its performance decreases for product listing. 2.4.3 Tools for the automated analysis of feature models There exist many SPL development tools that use the AAFM such as CaptainFeature [55], Feature Model Plugin [28], XFeature [18], featureIDE [54] and pure::variants [72]. However none of them was conceived as a general-purpose AAFM tool but used it as a means to solve other SPL problems such as product configuration, feature modelling or product derivation. As the AAFM and the tools using it grows, the need of a specialised AAFM tool also increases. Trinidad et al. [90] build FAMA Framework (FW)1, the first general-purpose tool for the AAFM whose main goal is to provide for an implementation of the state of the art techniques and algorithms for the AAFM. FAMA FW is an open-source SPL of AAFM tools where research results can be added as new features. As an SPL, a user can define a custom product selecting the desirable features for a AAFM tool. SPLOT [62] is a web application for the AAFM presented in 2009. It is a FM repository that allows their edition, analysis and product configuration. It relies on SAT solvers to analyse the anomalies such as void FMs and dead features, and BDD solvers for metrics calculation. 2.5 EXPLANATORY ANALYSIS Debugging FMs and CMs is considered to be one of the main challenges in the AAFM [7,14]. The goal of debugging is detecting, explaining and repairing any error in FMs and configurations. In error detection, several analysis operations are used to detect errors such as dead features, false-optional features or wrong cardinalities; in error explanation, we obtain the possible reasons why errors have been detected; in error reparation, errors are removed by manual or automated means, assisted by the 1http://www.isa.us.es/fama 28 2.5. EXPLANATORY ANALYSIS information provided by the explanations. Many authors [37,64,86,93,100,101] have dealt with error detection. However, the explanation and further reparation of errors still presents many open issues [85]. But explanations are not only regarded to errors, but to explain other situations such as invalid configurations, or explaining why a feature is core or variant or why a product is optimal for a given criterion [85]. We coin the term explanatory analysis to refer to all the operations that provide explanations for any given situation. Depending on the model from which we want to obtain explanations, there are two main kinds of operations in the explanatory analysis: configuration and relationships explanation. The solutions proposed for both operations are different. In Section §2.5.1 we overview the proposals that deal with configuration explanation. In Section §2.5.2 we overview those that deal with relationships explanation. 2.5.1 Current support for configuration explanations Configuration explanations provide the reasons why a configuration is invalid in terms of the user decisions that are provoking the invalidness. These explanations can be used to correct the configuration manually or automatically which should lead to a valid configuration. Czarnecki et al. [29,30] are the first authors in proposing the staged configuration process. In every stage in this process, a new FM, named as specialised FM, is generated to reflect all the user decisions that have been made. Moreover, they propose maintaining a CM where user decisions are explicitly collected. Both models, CM and specialised FMs are two sides of the same coin. While users cannot make decisions about cardinalities, cardinalities are only affected by user decisions indirectly when decisions are made on features. The strategy for dealing with errors in the configurations is to avoid situations in which user can make conflicting decisions. They propose a tool that is able to give explanations on conflicting configurations, but no details are given on its implementation, White et al. [98][99] interpret the configuration explanations as a diagnosis problem, providing an implementation using constraint programming. Besides obtaining explanations, the proposed solution is able to suggest reparations to restore the validness of a configuration. It provides a prototype tool that supports parallel configuration processes. 29 CHAPTER 2. BACKGROUND INFORMATION Mendonc¸a et al. [63] introduce the concept of collaborative configurations. Conflicts might arise when all the user decisions are collected, so it proposes algorithms to divide the FM in safe subtrees each of which is assigned a different user and where decisions can be made without conflicts. They ensure the correct merging of the different parts in which the decision process is divided. Elfaki et al. [37] interpret FMs as a set of Prolog rules that can be used to support the configuration process, providing for explanations whenever an invalid configuration is found. The proposed algorithms suggest the user decisions that must be removed to repair an invalid configuration. This approach only supports individual configuration processes. Bagheri et al. [4] propose an algorithm to find the minimal sets of conflicting user decisions in configurations. However, they only provide one solution instead of all the possible solutions. Although it is not explicitly remarked, this approach could be used in parallel configuration processes. Despite the work of N¨ ohrer and Egyed [67] does not propose specific solutions to provide explanations, it is worth making a mention to their approach. They propose to allow users to continue making decisions despite an invalid configuration is detected. They suggest to keep on collecting as many user decisions as possible in order to increase the quality of the explanations. Table §2.1 analyses several aspects of all these proposals. First, we remark if these proposals provide a formal semantics and/or an implementation of the solution in a tool or prototype. Second, the repairing strategies to deal with conflicting configurations is remarked, distinguishing among three strategies: • Avoiding any situation that might lead to a conflict among user decisions. The main complexity on this approach resides on the difficulty of ensuring that there is no conflicting situation that might arise due to unexpected scenarios in a configuration process. • Explaining the source of a conflict. In this case, users are allowed to make decisions despite of leading to contradictory configurations. • Repairing conflicts. This approach suggests ways of automatically repairing a configuration instead of reporting the users about the conflictive decisions. Third, the kind of input FM and the elements on which users can make decisions 30 2.5. EXPLANATORY ANALYSIS are remarked. All the proposals work with CBFMs and they only permit users to make decisions on features, giving no support for decisions on cardinalities or attributes in user decisions. Last, the kind of configuration process they assume is remarked, either individual, staged, parallel or collaborative. Configuration explanation† Work Sem. Impl. Contrad. Model Dec. Process Bagheri et al. [4] + - Explain CBFM F Staged Czarnecki et al. [29,30] - + Avoid CBFM F Staged Mendonc¸a et al. [63] + + Avoid CBFM F Collaborative N¨ ohrer and Egyed [67] - - Explain N/D N/D Staged Elfaki et al. [37] + + Repair CBFM F Individual White et al. [99] + + Repair CBFM F Parallel †+ Supported - Unsupported N/D Undefined Table 2.1: Current support for configuration explanations 2.5.2 Current support for relationships explanations Relationships explanations provide the reasons why given a FM, an input configuration is valid or invalid in terms of relationships in the FM [85]. If the input configuration is invalid, it is the FM which is supposed to contain errors so explanations are obtained in terms of the relationships in the FM that make the configuration invalid. They are known as a ’why not?’ operations. If the input configuration is valid, explanations are obtained in terms of the minimal set of relationships that make the configuration valid. They are known as ’why?’ operations. The explanations provided by ’why not’ operations might assist a manual reparation of a FM. Unlike configuration explanations, the automatic reparation of FMs is still an open issue, maybe due to the complexity of FM relationships compared with user decisions in CMs where features can only be selected or removed. Kang et al. [53] firstly proposed the need to debug FMs using logical representations, specifically Prolog. However they proposed no specific algorithm or technique to deal with explanations. Batory [5] proposes to use truth maintenance systems to find relationships in a FM that make a configuration to be invalid. 31 CHAPTER 2. BACKGROUND INFORMATION Wang et al. [96] represents a FM into Alloy Analyser, using its ability to obtain explanations in unsatisfiability cases. It can be used to explain configurations and the FM itself in terms of the failing relationships. [81] interprets a FM as a description logic and uses OWL reasoners capabilities to obtain explanations. In both cases, neither a semantics is given nor implementation details are provided. Trinidad et al. [89] propose the first work where explanations are dealt from a formal point of view. They endow explanations with an axiomatic semantics, interpreting void FMs, dead features and false-optional features in terms of theory of diagnosis. They also propose an operational semantics in terms of CSPs. These operations are later supported by FAMA FW [90] tool suite. In the last years, FAMA FW has incorporated new explanatory operations into its catalogue, providing explanations for wrong cardinalities, optimisation and invalid configurations. Trinidad and Ruiz-Cort´ es [85] propose the most extensive catalogue of explanatory operations up to date. 7 ’why not?’ and 4 ’why?’ operations are proposed, but no clear semantics is given. van den and Galv˜ ao [93] represent FMs as generalised feature trees, proposing adhoc algorithms to obtain explanations for void FMs and dead features. Zaid et al. [100] propose yet another work that interprets a FM in terms of a description logic to provide explanations on void FMs. Table §2.2 summarises all these proposals from the point of view of the operations they support from the catalogue in [85]. For each operation, we analyse three factors: which works have proposed the operation but no solution or an informal solution is given; which works provide a formalisation of these operations; and which tools provide a support for them. To this list of operation we have added a new operation that we call unique cardinalities, a new operation that has arisen as a side result of this dissertation. 2.6 CONSTRAINT SATISFACTION PROBLEMS Constraint programming is a mature field in artificial intelligence [58]. The expressive power of Constraint Satisfaction Problems (CSPs) and the wide catalogue of open-source solvers has turned them into the most used paradigm to deal with the AAFM. Constraint programming is a constantly evolving research topic where many 32 2.6. CONSTRAINT SATISFACTION PROBLEMS Relationship explanation operations Informal or no Formal Operation semantics semantics Tool Why not? Invalid configuration [5,53,81,85,96] [93] [6,90] Void FM [5,53,85] [81,89,93,100] [6,90] Dead Feature [85,89] [89,93] [6,90] False-optional [85,89] [89] [90] Optimisation [85] - [90] Wrong cardinalities [85] - [90] Unique cardinalities - - - Why? Core features [85] - - Variant features [85] - - Valid configuration [85] - - Optimisation [85] - - Table 2.2: Current support for relationship explanations algorithms and heuristics are arising yearly to improve the performance of commercial and free solvers. A CSP is a declarative paradigm to model and solve problems using constraints [92]. It is defined as a 3–tuple (V,D,C)where Vis a set of variables, each ranging on a finite domain from set D, and Cis a set of constraints restricting the values that the variables can take simultaneously. A solution to a CSP is an assignment to each variable of a value from its corresponding domain so that all constraints are satisfied simultaneously. Consider for instance, the CSP: ({a,b},{ {0,1,2},{0,1,2} },{a+b<4})where both variables aand btake value in the domain {0,1,2}and are constrained by {a+b<4}. The only value assignment that does not satisfy a+b<4 is {a7→ 2,b7→ 2}, so there are eight solutions. There are four basic operations to obtain conclusions from CSPs: Operation 1 - Searching for all the solutions. This operation searches for all the value assignments that satisfy all the constraints in 33 CHAPTER 2. BACKGROUND INFORMATION the CSP. For the given example, this operation obtains 8 solutions. Operation 2 - Searching for one random solution. This operation searches for one solution that satisfies all the constraints. It is a nondeterministic operation since the solution obtained depends on the search algorithms which can use random criterion or heuristics to search for a solution. Operation 3 - Satisfiability. A CSP is satisfiable if there is at least one valid value assignment. This operation detects if a CSP is valid or not. An example of inconsistent CSP take is ({a,b},{ {0,1,2}, {0,1,2}{a+b<0})since there is no possible value assignment satisfying the constraints. Operation 4 - Constraint propagation. Searching for an equivalent CSP such that the available values in the domain are reduced according to the constraints in the CSP. For example, this operation obtains for an input CSP ({a,b},{ {0,1,2},{0,1,2}{a+b<2}), another equivalent CSP in the form ({a,b},{ {0,1},{0,1}{a+b<2})since it is not possible to find for any solution that assigns 2 as a value for either aor b. In many real–life applications, it is needed to find a good solution to a CSP rather than anyone. A solution quality or goodness is usually measured by an application– dependent function called objective function. The goal is finding a solution that satisfies all the constraints and minimise or maximise the objective function. Such problem is known as a Constraint Optimisation Problem (COP) is a 4-tuple (V,D,C,O)that adds an optimisation function Oto a CSP. An objective function maps every solution in the CSP to a numerical value that is used for maximisation or minimisation. The adoption of COPs allow to define a new operation: Operation 5 - Optimisation. This operation searches for the solution/s that satisfy all the constraints in the CSP and minimise or maximise the objective function. If we define a COP ({a,b},{ {0,1,2}, {0,1,2} },{a+b<4})where the optimisation function is O(s) = a, which maximises the value of a. There are two solutions in the original CSP { {a7→ 2,b7→ 0},{a7→ 2,b7→ 1} }, that maximises the value of the objective function and are therefore the solutions of the COP. 34 2.7. SUMMARY 2.7 SUMMARY This Chapter presents the main concepts on which this dissertation relies. FMs and configurations have been presented as the two models used in SPLs to represent all the products that can be built and the user decisions to find for the most suitable product among the available ones. The AAFM is introduced as an approach to extract information from FMs and configurations. Some examples of AAFM operations have been presented and the general schema used to solve them. Specifically, we focus on explanatory operations, detailing their state of the art. The AAFM usually relies on declarative techniques to support the analysis. The most used approach are CSPs. They have been briefly introduced to show their declarative capabilities. In the next Chapter we introduce a declarative framework to represent problems from which information can be extracted using deductive and abductive reasoning. 35 CHAPTER 2. BACKGROUND INFORMATION 36 3 DEDUCTION AND ABDUCTION PROBLEMS 37 Imagination is more important than knowledge. For knowledge is limited, whereas imagination embraces the entire world, stimulating progress, giving birth to evolution. It is, strictly speaking, a real factor in scientific research Albert Einstein (1879 – 1955), Scientist The main approach to deal with the AAFM is transforming a FM into a declarative paradigm where the analysis operations are interpreted in terms of operations in that paradigm. Despite of the differences among those paradigms, they share the way of reasoning that they implement. In this dissertation we conjecture that most of the analysis operations in the AAFM can be interpreted in terms of deduction and abduction, two well-known ways of reasoning about a given knowledge. In this Chapter we present the Deductive and Abductive Problem (DAP) framework to describe problems in such terms that deduction and abduction can be used to extract information from them by means of operations. In Section §3.1 we propose Deduction Problems (DPs) and define the operations that are available to perform deduction. In Section §3.2 we propose Abduction Problems (APs) and define the operations that are available to perform abduction. In Section §3.3 we summarise the contributions of this Chapter and advance how DAPs are used in this dissertation. CHAPTER 3. DEDUCTION AND ABDUCTION PROBLEMS friend(E,A),f riend(D,E),introduce(A,E,D)|=f riend(A,D) which means that A and E are common friends of D and they can be introduced to turn A and D into friends. 3.2.1 Minimal explanations In the friendship example, there are 120 possible explanations, but we are not interested in all of them, but in those that are more probable. According to the Occam’s razor principle or parsimony law, the succinctest or minimal explanations are the most probable ones. Minimal explanations are usually sufficient to explain a situation and in case they are not, they guide the process to obtain new observations that delimit the explanations. Different minimality criteria can be used in to obtain minimal explanations: • Minimal subset: an explanation is minimal if no proper subset of it is also an explanation: minS(E)≡ {e|e∈E∧ ¬∃e0(e0∈E∧e0⊂e)} • Minimal number of assumptions: an explanation is minimal if there exists no explanation with a fewer number of elements. min#A(E)≡ {e|e∈E∧ ¬∃e0(e0∈E∧ |e0|<|e|)} For example the minimal explanations obtained for the friendship problem can be reduce to {introduce(A,E,D)}since it only has one element while the other two explanations have two elements. • Minimal weighted explanation: weights are defined for each formula in the hypotheses set, establishing an order relationship vpbetween hypotheses. An explanation is minimal if there exists no other explanation with less weight: minω(E)≡ {e|e∈E∧ ¬∃e0(e0∈E∧e0vpe)} • Circumscription: same as minimal number of assumptions criterion but only a kind of predicates from the hypotheses set is taken into account ignoring remaining ones. For example, in the friendship AP only introduce predicates can be taken into account for explanations. 44 3.2. ABDUCTION PROBLEMS Given the above minimality criteria, we propose an abductive operation to perform minimal explanations on APs: Operation 1 - Minimal Explanation. This operation obtains the minimal explanations for an AP. We denote this operation as a function in the following form: minExpl :AP →H∗ minExpl(AP(C,V,(F,H,O),S,min(X))) ≡min({∆|∆⊆H,F6|=O,F∪∆|=O}) For the friendship example, let αbe the AP that represents the problem. If the minimal subset criterion is used, the following minimal explanations are obtained: minExpl(α) = { {introduce(A,E,D)}, {introduce(A,B,C),introduce(A,C,D)}, {introduce(B,C,D),introduce(A,B,D)}} 3.2.2 Conflict sets When a DP defines a KB with contradictory formulas, the DP is said to be not satisfiable, i.e. it has no solutions. In this situation it is important to obtain the set of formulas in the KB that are in conflict. Obtaining such sets can be interpreted in terms of abduction. For that sake, the KB is divided in two sets of facts and hypotheses, i.e. KB =F∪H. The set of facts contains the set of formulas in the KB that are certainly known to be correct, if any. The set of hypotheses contains all the remaining formulas that can be provoking the unsatisfiability. These two sets are used to define an AP in the form AP(C,V,(F,H,∅),S,min(X)). Since the set of observations is empty, there is no behaviour to explain, so the minimal explanation operation cannot be used to detect contradicting formulas. In this situation, we are interested in searching for the minimal conflict sets, which are defined as follows: Definition 3.3 - Conflict Set. Let αbe an AP in the form (C,V,(F,H,∅),S,min(X)) such that the set of facts Fis consistent. A subset of hypotheses ∆⊆His said to be a conflict set iff ∆contradicts the knowledge in the set of facts, i.e. F∪∆|=⊥ 45 CHAPTER 3. DEDUCTION AND ABDUCTION PROBLEMS Let us consider a catalogue of cars as an example. A car has three properties: transmission, colour and cost. There are three available cars with different properties. A customer is searching for a black car with a manual transmission that costs less than 15,000e. However, it is not possible to find a car with such properties. In this case, we build an AP that distinguishes among facts and hypotheses. The set of facts contains the database of cars, since the catalogue cannot be changed. The set of hypotheses contains the customer decisions, which can be relaxed or changed to find for a suitable car. The AP that describes this problem results as follows: C={C1,C2,C3,GEAR,MANUAL,AUTO,COLOR,RED,BLACK} ∪ N V=∅ F={car(C1,MANUAL,RED,12000), car(C2,AUTO,RED,13500), car(C3,MANUAL,BLACK,16000), value(GEAR,MANUAL)⊕value(GEAR,AUTO), value(COLOR,BLACK)⊕value(COLOR,RED)} H={value(GEAR,MANUAL), ∃x·value(COST,x)∧x<15000, value(COLOR,BLACK)} O=∅ S={car(model,gear,color,cost)≡product(model)⇔value(GEAR,gear)∧ value(COLOR,color)∧value(COST,cost)} min(X) = {x|x∈X∧ ¬∃x0(x0∈X∧x0⊂x)} There is no car satisfying the customer’s demand because DP(C,V,F∪H,S)is not satisfiable. Let us name the three hypotheses as H1={value(GEAR,MANUAL)}, H2={∃x·value(COST,x)∧x<15000}and H3={value(COLOR,BLACK)}. The conflict set operation detects six conflict sets: {H2},{H3},{H1,H2},{H1,H3},{H2,H3} and {H1,H2,H3}, As for minimal explanations, we are not interested in all the potential conflict sets, but in those sets that are minimal. Therefore we define the following operation for this purpose: Operation 2 - Minimal Conflict Sets. This operation obtains the set of minimal conflict sets for a given AP. We denote this operation as a function in the following form: minCon f licts :AP →H∗ minCon f licts(AP(C,V,(F,H,∅),S,min(X))) ≡min({∆|∆⊆H,Fis consistent F∪∆|=⊥}) 46 3.3. SUMMARY For the above example and given the minimal subset criterion, the minimal conflict sets are {H2}and {H3}since remaining conflict sets are supersets of them. So the customer must resign either the black colour or the cost restriction. 3.3 SUMMARY In this Chapter we propose DPs and APs as two frameworks that support deductive and abductive reasoning, two forms of reasoning used in the AAFM. These frameworks aim to make reasoning independent of specific paradigms or solvers, offering an abstract layer where problems can be defined in general terms and reasoning can be performed by means of operations. One of the problems we have found in the AAFM is the myriad of declarative approaches that solve the same operations in terms of different paradigms such as CSPs, Binary Decision Diagrams (BDDs) or SAT. In [85] we had the intuition that most of the AAFM operations could be interpreted independently of the specific paradigm as a form of deduction and abduction. That work has led us to propose DPs and APs as frameworks to describe problems that use both forms of reasoning. In this dissertation, we describe SFMs in terms of DPs in Chapter §7 to perform analysis operations that rely on deduction, and in terms of APs in Chapter §8 to perform analysis operations that rely on abduction. This way, DPs and APs enable to give an operational semantics to analysis operations in a solver-independent form. 47 CHAPTER 3. DEDUCTION AND ABDUCTION PROBLEMS 48 OUR CONTRIBUTION PART II 4 MOTIVATION 51 The people who get on in this world are the people who get up and look for the circumstances they want, and, if they can’t find them, make them. George Bernard Shaw (1856–1950), Playwrighter and Nobel Prize in Literature Once we have raised a number of research questions and goals, we aim to motivate the problems and to justify the solutions that we approach in this dissertation. In Section §4.1, we analyse current proposals on configuration modelling, explanatory analysis and formalisation, which lead to state three research questions and to define goals to answer them. In Section §4.2 we discuss our proposal to achieve these goals. Finally, Section §4.3 summarises the conclusions and justifies the following structure of our contribution. CHAPTER 4. MOTIVATION 4.1 ANALYSIS OF CURRENT SOLUTIONS This dissertation aims to overcome the drawbacks that we have found in AAFM regarding modelling and analysis. This Section focuses on remarking the limitations that have led to state the research questions in Chapter §1. First, we study why current FMs are not fully-configurable due to the expressiveness of CMs in Section §4.1.1. Next, we present the limitations we have found in explanatory analysis in Section §4.1.2. Finally, we analyse the AAFM formalisation challenges in Section §4.1.3. 4.1.1 Configuration models CMs have not been specifically studied in the AAFM, being widely accepted the three-set model that represents user decisions in terms of selected, removed and undecided features. We have found three limitations in this CM that we aim to save in this dissertation. First, despite cardinalities and attributes are used in ECBFMs to represent relevant information, current CMs are unable to represent decisions on them, only enabling the decision making on features. It impedes a user making decisions about attributes such as ’I want a SHS that costs less than 2.000 e’, or about cardinalities such as ’I want a SHS with two Internet connections’. We affirm that current FMs are not fullyconfigurable since CMs are unable to make decisions on any element of the FM. Second, a strong relationship between elements in the FM and in the CM arises when attributes and cardinalities come into play. A CM must ensure that a user decision on an attribute is made within the attribute domain, which is specified in the FM. The same happens for cardinalities, whose valid values for user decisions are modelled in the FM. FMs and CMs share elements and the values those elements can take in a user decision. There are two main approaches to deal with information sharing: keeping two separate models in constant synchronisation, communicating any change in the FM to CMs, or combining FMs and CMs in a unique model around the common elements. Third, some authors [20,99] have used annotations on FMs to depict decisions on features. But there is no graphical representation that supports attributes and cardinalities. From these problems we have found regarding CMs, we state the following re- 52 4.1. ANALYSIS OF CURRENT SOLUTIONS search question: Is it possible to extend CMs to enable fully-configurable ECBFMs? In order to find an answer for this question, we define three goals: 1. Propose a CM that enables the representation of user decisions on attributes and cardinalities. 2. Taking advantage of the information that FMs and CMs share. 3. Representing CMs together with FMs in a backwards-compatible graphical notation. 4.1.2 Explanatory analysis The explanatory analysis covers configuration and relationships explanation, where the research has progressed unevenly. Regarding configuration explanations, the work of White et al. [99] can be considered as the most complete one to date since they are able to explain and repair configurations in parallel configuration processes. However, they are only able to deal with user decisions on features, ignoring attributes and cardinalities. This is a common limitation of every studied proposal. Regarding relationships explanations, we have detected several open issues in the works we have analysed. First, a formal semantics has only been given to a subset of operations [53,81,85,96]. In particular those operations in which cardinalities and attributes are involved such as wrong and unique cardinalities, and optimisation, have been left out of any proposal. Second, the tools support more operations than those that have been published to date. There are operations that have been implemented but no formal semantics has been given, making it impossible to verify their correctness or to replicate them in other tools. According to this scenario, we have found three main limitations in the explanatory analysis that we aim to save in this dissertation. First, we can affirm that current proposals on the explanatory analysis are not available for fully-configurable FMs and therefore they are unable to deal with cardinalities and/or attributes. Second, we have detected that the implicit procedure to solve most of the relationship explanations consists of simulating a user setting a configuration and then performing an explanation of a valid or invalid configuration. We conjecture that those 53 CHAPTER 5. STATEFUL FEATURE MODELS !! !"#$%&'() *+) *,) !!P!"#$! *-) *.) !"#$%&'() !P (E) ! !! ! ! !"#$%&'() /01)234)25.45,45-66) 5,) 5-) 301)234)2*.4*,4*-4*+66) 7301)284)2*.4*,4*-4*+64)25.45,45-66) P!"#$! 5.) (a) Feature model!(b) Configuration model!(c) Stateful feature model! Figure 5.1: A visual metaphore of FMs, CMs and SFMs 5.1 RATIONALE A FM describes the set of products in terms of features and relationships. A product is a subset of features that satisfy all the relationships. From these definitions, we can interpret a FM in terms of the following sets. Let Fbe the set of features in a SPL, and let P(F)be the set of all the possible combination of features. The relationships can be interpreted as constraints on P(F). These constraints define the set of products (P) as a subset P⊆ P(F). CMs represent the user decisions in terms of three sets of selected, removed and undecided features. User decisions can be interpreted as another different way to constrain the set of all the possible combination of features P(F)with a different kind of constraints. Therefore FMs and CMs can be regarded as two different models that describe subsets of P(F). This vision also fits into CBFMs and EFMs where cardinalities and attributes are added to the set of features. In this case, a new set that represents all the features, cardinalities and attributes in an ECBFM is necessary. This set is denoted as the set of elements E. In this case, relationships can be interpreted as constraints on P(E), i.e. the space of all the possible combinations of elements. Symmetrically, user decisions in CMs could also be interpreted as constraint on P(E)if they were fully-configurable, but current CMs keep on interpreting the CM as a subset of P(F). In order to enable fully-configurable FMs, we propose extending CMs to support cardinalities and attributes besides features. The resulting models must also satisfy three main requirements in order to save the limitations presented in Section §4.1: 60 5.2. MAIN CONCEPTS (i) user decisions can only refer to elements in Eso it must avoid any reference to invalid cardinalities or attribute values; (ii) CMs must allow multiple users making decisions at the same time, and (iii) CMs must distinguish between user and automatic decisions. As a solution, we propose incorporating FMs and CMs together in a single model that we have coined as Stateful Feature Model (SFM). The resulting model stores together the set of elements E, and two sets of constraints, one for relationships and another one for user decisions (see Figure §5.1). An SFM supports multiuser configurations and distinguishes between user and automatic decisions. SFMs are the first fully-configurable FMs, able to represent user decisions on attributes and cardinalities. Table §5.1 compares the capability of dealing with features, cardinalities and attributes in SFMs, basic FMs, CBFMs, EFMs and ECBFMs. In next Section we propose an abstract model for SFMs and the relevant concepts that arise from their use. Elements affected by constraints† Constraint Basic FM CBFM EFM ECBFM SFM Relationship F F, C F, A F, C, A F, C, A Configuration F F F F F, C, A †F = Features, C = Cardinals, A = Attributes Table 5.1: A comparison of the use of elements in different kinds of feature models 5.2 MAIN CONCEPTS An SFM contains information about the elements in a SPL, which are features, cardinalities and attributes, hitherto stored in FMs. Depending on the decisions a user can make on elements, each element has its own set of states. So features have a selected or removed state; Cardinalities have as many states as cardinals in its range; Attributes have as many states as values they can take. An assignment of states for every element in the SFM defines the characteristics of what is called a potential product. To determine which of the potential products can be built within the SPL, a set of relationships constrains the valid combinations of states, defining what is called the set of SPL products. An SFM also collects all user decisions, which are constraints that define a subset of potential products named configuration. The set of SPL products that 61 CHAPTER 5. STATEFUL FEATURE MODELS !P (E)! !"#$ "%&'()*+$ !P (E)! !P (E)! ,&-./(%01&-$ ,&2301456$ "%&'()*+$ !P (E)! $ "&*6-105$ "%&'()*+$ 76501&-+893+$ :(*&201)$ '6)9+9&-+$ Figure 5.2: A geometrical interpretation of basic concepts in SFMs are also found in the configuration is called the set of compatible products, and brings together the SPL products that meet all user decisions. SFMs distinguish among user and automatic decisions. An automatic decisions is the one that is made by an AAFM operation to support the configuration process. An automatic decision can be defined as the one that if a user makes it, the set of compatible products remains unaltered. They are computed and stored separately from user decisions unless a user explicitly makes such a decision. Figure §5.2 proposes a geometrical interpretation of the concepts presented in this Section. 5.3 ABSTRACT MODEL FOR SFMS In this Section we give a transformational semantics to SFMs in terms of set theory, relying on a new vision of products as an assignment of states to elements. In FMs, each product is described as a different subset of features. In SFMs, all the products share the same set of elements, denoted by a non-empty set E={E1,...,En}where each Eiis an element in that model, either features, cardinalities or attributes. A product is defined as an assignment of states to every element in Esuch that each element 62 5.3. ABSTRACT MODEL FOR SFMS has a set of available states that depends on the kind of element. This way, features have selected or removed states to indicate their presence or absence in a product; a cardinality has a cardinal value as state to indicate the number of features that are in a selected state within a set relationship; attributes have a state which corresponds to a value that represents the quality or behaviour of a linked feature. To define which states every element can have, an SFM has a set of available state sets AS1,..., ASnsuch that ASjis the set of available states for an element Ej. Let us consider an SPL with 5 elements E={FR,FA,FB,FC,C1,Mem}as an example. The available states for each elements could be: ASFR={sel},ASFA=ASFB=ASFC= {sel,rem},ASC1={1,2,3},ASMem ={128,256}. This way, the root feature FRmust have a selected state, features FA,FBand FCcan be either in a selected or removed state, C1cardinality, which affects features FA,FBand FC, must be either 1, 2 or 3 and the product can have a 128 or 256 kilobytes memory size. We define the set of potential products as follows Definition 5.1 - Set of potential products. Let ASjbe the set of available states for the jth element ej∈E. The set of all the potential products in an SFM is defined by the cartesian product D=AS1×... ×ASn. Apotential product corresponds to any tuple (s1,...,sn)∈D. In the previous example, the set of potential products Dis comprised of 32 different potential products. S1= (sel,sel,sel,sel,2,256)and S2= (sel,rem,sel,rem,1,128)are examples of potential products. However, not all of them are SPL products, i.e. products that effectively can be built in the SPL. To define the set of all the SPL products, a first option that consists of enumerating all of them is immediately discarded when the number of SPL products shoots up. A set in general can be defined by a list of its elements or by a subset that satisfies a condition or constraint. SFMs use constraints to define the set of SPL products as a subset of the set Dof potential products. An SFM has a set of relationships R ={R1,..., Ri}that sets the conditions a potential product must necessarily fulfil to be an SPL product. So the set of SPL products is defined as follows: Definition 5.2 - Set of SPL products. Let R={R1,...,Ri}be the set of relationships in an SFM and Dits set of potential products. The set of SPL products defined by the SFM is: P={(s1,...,sn)∈D|R1∧... ∧Ri} 63 CHAPTER 5. STATEFUL FEATURE MODELS It might be the case that there exist no product satisfying all the relationships and therefore P=∅. In this case, it is said that the SFM is void or invalid. The kinds of constraint that we propose for SFMs are the same than those used for FMs. Table §5.2 shows a list of constraints that can be used to represent the relationships in an SFM. So for example, if Ais a parent feature linked by a set relationship with three child features A,Band Cand affected by cardinality C1, the following constraint and set of SPL products can be defined: P={(sR,sA,sB,sC,sC1,sMem)|set3(sR,sC1,sA,sB,sC)} Kinds of relationship constraints mandatory(sp,sc)≡sp=sc optional(sp,sc)≡sc=sel ⇒sp=sel ∧sp=rem ⇒sc=rem set2(sp,sc,sc1,sc2)†≡sp=sel ⇔numSelChild2(sc,sc1,sc2)∧ sp=rem ⇒sc1=rem ∧sc2=rem set3(sp,sc,sc1,sc2,sc3)†≡sp=sel ⇔numSelChild3(sc,sc1,sc2,sc3)∧ sp=rem ⇒sc1=rem ∧sc2=rem ∧sc3=rem ... ... depends(s1,s2)≡s1=sel ⇒s2=sel excludes(s1,s2)≡ ¬(s1=sel ∧s2=sel) †numSelChildi(sc,sc1,...,scn)is a predicate that is true whenever the number of selected states in sc1,...,scncoincides the cardinal sc. Table 5.2: Kinds of relationship constraints in a SFM An SFM also stores a configuration which comprises all the decisions made by one or more users in a given moment. Decisions are collected in any order, supporting a parallel configuration process. These user decisions set a partition on the set of potential products Din a SPL: those that satisfy user decisions and those that do not. Following this criterion, we define a configuration as follows: Definition 5.3 - Configuration. Let U={U1,...,Uj}be a set of constraints defined on D, describing the user decisions in an SFM. A configuration CUis defined as the set of potential products that satisfy all the user decisions: CU={(s1,...,sn)∈D|U1∧... ∧Uj} 64 5.3. ABSTRACT MODEL FOR SFMS Users can make two kinds of decisions as shown in Table §5.3. A user can either make a choose decision, that assigns a state for one element, or a discard decision that avoids an element having a certain state. So for example, U1=choose(sB,sel)identifies a user selecting feature B;U2=discard(sMem,128)identifies a user refusing a 128Kb bandwidth. With these two kinds of decisions, users delimit the set of potential products by means of successive refinements. In case that user decisions contradict each other, as two users choosing selected and removed states for the same feature for example, then the set CU=∅. This situation is known as a contradictory configuration. Kinds of decision constraints choose(se,S)≡se=S discard(se,S)≡se<> S Table 5.3: Kinds of decision constraints in a SFM From the configuration and the set of SPL products, it can be determined the set of compatible products, i.e. the subset of SPL products that satisfy the criteria established by user decisions. The set of compatible products is defined as follows: Definition 5.4 - Set of compatible products. Let Pbe the set of SPL products defined by the relationship constraints R1,...,Ri, and let CUbe a configuration defined by the user decision constraints U1,...,Uj. The set of compatible products (CP) is defined as: CP =P∩CU={(s1,...,sn)∈D|R1∧... ∧Ri∧U1∧... ∧Uj} With the above definitions, we are able to represent an SFM in a compact manner as follows: Definition 5.5 - Stateful Feature Model. An SFM can be represented by a 4- tuple (E,D,R,U)such that Eis the set of elements in the SFM, Dis the set of potential products, Ris the set of relationships and Uis the set of user decisions. From the information contained in this tuple, the set of potential, SPL and compatible products can be deduced. Next we introduce three concepts that can be defined on top of SFMs: SFM states, element states and automatic decisions. 65 CHAPTER 5. STATEFUL FEATURE MODELS 5.3.1 SFM states From the set of compatible products (CP), it is possible to identify singular situations or SFM states: • Initial state: an SFM is in its initial state when there exist no user decisions, i.e. U=∅. In this case, the configuration coincides with the space of potential states (CU=D) and therefore the set of compatible products coincides the set of products, i.e. CP =P. • Final state: an SFM is in a final state when it only determines one compatible product, i.e. |CP|=1. When a final state is reached, it can be affirmed that a product satisfying all the user decisions has been found. The final adjective comes from the inability of the CP set to evolve in a manner that the set of compatible products is reduced even more. • Intermediate state: A state is intermediate if U,∅and |CP|>1. This is the most common state in an SFM and it corresponds to a situation in which users may still made decisions. • Invalid state: if CP =∅at any moment, an SFM is said to reach an invalid state. This state can be reached because the set of SFM products is empty (P=∅), or the configuration is contradictory (CU=∅), or there exist no compatible product satisfying the user decisions (P∩CU=∅). An SFM state makes reference to the instant in which the configuration process is. This way, the configuration process starts with an SFM in its initial state. User decisions provoke the SFM state to change to an intermediate state. A final state can be reached if there exist only one product satisfying all the user decisions. In case a configuration defines no compatible product, an invalid state is reached. 5.3.2 Element states and automatic decisions From an SFM, it is possible to extract relevant information about the elements and states on which users might still make decisions without reaching an invalid state. For this purpose, we define the concept of element state as the set of all the states an element has for every compatible product in CP. 66 5.3. ABSTRACT MODEL FOR SFMS Definition 5.6 - Element State. Let Eibe an element in an SFM and CP the set of compatible products. The element state for that element Eiis defined as follows: State(Ei) = [ s∈CP πi(s) Being πi(s)the projection function that extracts the ith element from a tuple sthat represents a compatible product. So for example, let us consider the following set of compatible products: E={FR,FA,FB,FC,C1,Mem} CP ={P1,P2,P3} P1={sel,rem,sel,sel,2,256} P2={sel,rem,rem,sel,1,128} P3={sel,rem,sel,sel,2,128} The following element states are obtained from these compatible products: State(FR) = {sel},State(FA) = {rem},State(FB) = {sel,rem}, State(FC) = {sel},State(C1) = {1,2,},State(Mem) = {128,256} An element state is used to infer what we call the set of automatic decisions (A). An automatic decision is the one that if it is made by a user, the set of compatible products remains unaltered. This way, if A={A1,..., Ak}represents the set of automatic decisions, and being CAthe subset of all the potential states that satisfy such automatic decisions: CA={(s1,...,sn)∈D|A1∧... ∧Ai} it is possible to affirm that CP ∩CA=CP ⇒CP ⊆CA This set of automatic decisions is used to assist users in the decision making process, avoiding as far as possible to reach for invalid states. Automatic decisions can be calculated from the element states. Let Eibe an element in an SFM having ASias available states and State(Ei)as its corresponding element state. Depending on the element state, an automatic decision can or cannot be inferred as follows: 67 CHAPTER 5. STATEFUL FEATURE MODELS •State(Ei) = ASi: in this case, the element is said to be in an undecided state. It means that no user has made any decision that affects it and no automatic decision can be made on it. •|State(Ei)|=1: in this case, it can be interpreted that an automatic decision has been made on Eito choose the unique state in State(Ei) •|ASi|>|State(Ei)|>1: in this case, it can be interpreted that all the states that are not in State(Ei)have been discarded. It means that those states in the set ASi−State(Ei)can be automatically discarded. •State(Ei) = ∅: this situation can only be given if CP =∅in which case it does not make sense to calculate any automatic decision since there is no compatible product. Each automatic decisions obtained following the above criteria must be checked if it already exists as a user decision, in which case they are disposed. For the previous example, the following set of automatic decisions can be inferred: A={choose(sA,sel),choose(sC,sel),discard(sC1,3)} From here and on, attributes are left out of the next steps in this dissertation. Our next contributions are given for features and cardinalities as the only elements in an SFM. Attributes can have discrete and continuous domains. Discrete domains can be treated like cardinalities, but continuous domains might introduce problems that have not been explored in this dissertation. However our proposal is built thinking in their addition as a future work as approached in Section §A.3. 5.4 STATEFUL FEATURE DIAGRAMS Stateful feature diagrams are a graphical notation of SFMs based on feature diagrams [76]. The representation of elements and relationship constraints is the same that FMs: a tree-like structure where features are boxes linked by different kinds of lines that represent the relationships among features. Cardinalities are also drawn together with the corresponding set relationship. User and automatic decisions are not explicitly depicted in the diagram. Instead of it, element states are drawn. If a feature state is {sel}, it is drawn as a tick (3) within a 68 5.4. STATEFUL FEATURE DIAGRAMS !"#$%&'(")& *+,-./,&0(/%$(1& !23%)"& 4/%)$/)%& 5(6+)& 71#2)$3& 8/.9%-):& 81#$"& 0(/%)/%3& 0)11&;-(/)&0(/%$(1& ;#/)1& <=>>?@& A+B)(&(/& C)"#/B& C+,+%#1& 5)B+#&!)$6)$& <=>>?@&!8D?E& && 'CFA&G?H& 'CFA&I?H& <=>>I@& J%-)$/)%& IK& <=>>G@&!&D=L?LIE& M+N+9OP,& M+N+9/& ;$(6+B)$3& 0#Q-)&& ;$(6+B)$&8& ;$(6+B)$&R& <=>>?@& ;0;1#2)$& S)1#.(/3-+73& 5#/B#%($2& T7.(/#1& C)7)/B3& !)%& JUQ1VB)3& !& !& !& !&!& !&!& !& !& !& "& & &&&&C)Q+3+(/3& & !)1)Q%)B& S)"(6)B& 0#$B+/#1+%2& W/B)Q+B)B& <=>>?@&!&D?E& "& !&!& "& <=>>?@&!8&D?E& 0(/%$#B+Q%($2& W3)$&8V%("#.Q& !" Figure 5.3: An example of a Stateful Feature Diagram circle in a corner of the feature box; if a feature state is {rem}, a cross (7) is used instead; if a feature is undecided, no specific mark is assigned; if two or more users have made contradictory decisions on a feature, it is marked as ε. It the feature state is inferred by user decisions, then a filled circle is used; if it can only be inferred by automatic decisions, a non-filled circle is used instead. Decisions on cardinalities are drawn as Cd→Cswhere Cdis the cardinality domain and Csis the element state for that cardinality. For example a cardinality [1..3]whose state has been set to {2}is drawn as [1..3]→ {2}. If state 2 is removed but no other state has been chosen, it is represented as [1..3]→ {1,3}. Just in case the cardinality state is inferred only from automatic decisions, Cd→ACsis used to remark that its state has changed due to automatic decisions. Figure §5.3 shows an example of a stateful feature diagram. Since attributes have been left out of the scope of this dissertation, our proposal on stateful feature diagrams does not incorporate them. 69 CHAPTER 5. STATEFUL FEATURE MODELS 76 6 AUTOMATED ANALYSIS OF STATEFUL FEATURE MODELS 77 I will be so brief I have already finished Salvador Dali (1904–1989), Painter, artist The definition of a new kind of model such as SFMs suggests the proposal of techniques for their automated analysis. This Chapter defines the scope of the Automated Analysis of Stateful Feature Models (AASFM) and provides a general schema for it in Section §6.1. In Section §6.2 we propose a taxonomy of analysis operations for the AASFM. Section §6.3, proposes a generic logical representation for SFMs that is used as an intermediate model to ease the mapping to DAPs in the following Chapters for the formalisation of the AASFM. Last, Section §6.4 summarises the contributions in this Chapter. CHAPTER 6. AUTOMATED ANALYSIS OF STATEFUL FEATURE MODELS 6.1 GENERAL SCHEMA The proposal of a new model suggests the adaptation of the AAFM to the new characteristics of SFMs. This is why we propose what we call the AASFM which we, inspired by Benavides et al. [14], define as follows: Definition 6.1 - Automated Analysis of Stateful Feature Models (AASFM). The AASFM can be defined as the computer-aided extraction of information from SFMs by automated means. The main innovation in SFMs resides in their fully-configurable capabilities. Apart from this, SFMs retain all the expressiveness of FMs and CMs. This implies that the set of analysis operations for the AASFM must contain at least all the operations defined to date for the AAFM. Such as for the AAFM, we propose the transformation of SFMs into a logical language that encodes the information in the form of logical formulas. A logical language confers an operational semantics to SFMs while enabling logical reasoning which allows the derivation of conclusions from the logical formulas. The mechanisms for logical reasoning are precisely defined and allow the automation of reasoning and therefore the automation of the AASFM. Besides analysis capabilities, these transformations provide a translational semantics to SFMs. There is a wide catalogue of logical languages that can be used for the AASFM: first-order logics, CSPs, binary decision diagrams, temporal logics, description logics, etc. Independently of the particular language used to reason, there are three main kinds of reasoning: deduction, abduction and induction. All the operations proposed for the AAFM can be interpreted as cases of deduction and abduction [85]. Abduction is used to obtain explanations why certain situations are given such as dead features, false-optional features or a void FM. Deduction is used to extract any other information from a FM such as counting the number of products, obtaining a list of products, etc. Instead of proposing a formalisation of the AASFM based on a specific logic, we propose a formalisation as independent of logics as possible. For that purpose, we interpret SFMs as DAPs, that can be used to perform deductive or abductive-based analysis operations. Thanks to this approach, we are able to identify which AASFM operations correspond to basic DAP operations, defining a set of basic operations for the AASFM. This way, remaining AAFM operations can be interpreted in the AASFM as a 78 6.1. GENERAL SCHEMA combination of such basic operations in what we call compound operations. This division allows us to define a taxonomy of analysis operations that we propose in Section §6.2. When transforming SFMs into DPs and APs for their analysis, we realise that there exist many common elements between both transformations. For this reason we propose a Stateful Feature Model Problem (SFMP) as a generalisation of DAPs. An SFMP acts as an indirection level between SFMs and DAPs that collects the common artefacts in DAPs and the common mapping rules in the transformation from SFMs. It can be seen as an mere engineering instrument to avoid the repetition of mapping rules. All these contributions result in a AASFM general schema that is depicted in Figure §6.1. !!"#$% !"#$%&'(#& )*+(,-.&'(#& /& &'()*% +,-./0/12)*% 0123& 3456787"79:;% !! "& !456787"75#7<7=;7>?05@;;% 34%=-A% $6B(CD% $#?0E% 4)2-/F% "/GAH% !4%=-A% $?0620H% $?0+,-.% 012& 45#,67& Figure 6.1: General schema of the AASFM 79 CHAPTER 6. AUTOMATED ANALYSIS OF STATEFUL FEATURE MODELS 6.2 A TAXONOMY OF OPERATIONS The approach that we follow to formalise the AASFM allows us to propose the following taxonomy of operations: • Basic operations: if a SFM is interpreted as a DP and an AP, a basic operation is solved using one and only one reasoning operation (such as solutions, satisfiability, minimal explanations, etc.). Depending on the kind of reasoning operation that is used, two subtypes of basic operations are distinguished: –Query operations: the goal of a query operation is to extract implicit information from a SFM and make it explicit. They are implemented as deductive operations on a DP. –Explanatory operations: The goal of explanatory operations is obtaining explanations why the user decisions or the relationships provoke a certain behaviour. They are implemented as abductive operations on an AP. • Compound operations: a compound operation combines basic operations to perform higher-level operations. The main benefit of this taxonomy is that only basic operations need to be given a formal semantics, while remaining operations are defined as a combination of them. The composability of model edition operations together with the combination of basic operations allow to propose a wide catalogue of analysis operations. In this dissertation we propose a catalogue of AASFM operations that corresponds with most of the AAFM operations defined up to date. We also propose new analysis operations that were not considered for the AAFM which are now possible using SFMs. 6.3 A LOGICAL REPRESENTATION OF STATEFUL FEATURE MODELS Representing SFMs in terms of logics implies the definition of all the needed elements for logical reasoning. Many different logics can be used to encode and to reason on a model. There exist commonalities among logics. In particular, any logic requires a language with a formal syntax and a precise semantics, a notion of logical entailment 80 6.3. A LOGICAL REPRESENTATION OF STATEFUL FEATURE MODELS and rules for manipulating expressions. We propose a logical framework that we coin as SFMP, which can be defined as follows: Definition 6.2 - Stateful Feature Model Problem (SFMP). A SFMP is a 7-tuple SFMP(C,V,D,R,U,A,S)such that Cis a set of constants representing elements and the element-specific states; Vis a set of variables representing the state for each element; Dis a set of formulas that define the element available states or domains;R,Uand Aare sets of formulas for relationships, user and automatic decisions respectively; and Sis a semantics for the formulas used in R,Uand A. An SFMP relies on FOL. We use natural numbers, algebraic functions and any other element that are not defined in classical FOL wherever they ease the representation. The |=symbol is used along this dissertation to represent an inference operation applying the corresponding semantics to the logical language. Despite the use of FOL, we think that our approach can be easily adapted to be represented in different kinds of logics that can benefit from the use of automated reasoning tools. It will be the work of specific implementations to find the most suitable logic for this representation. The inference rules to obtain semantic and syntactic consequences are undefined in this representation. Depending on the kind of analysis operation to perform, the reasoning problem to solve may change and so the reasoning mechanisms. In Chapters §7 and §8 we interpret the different SFM analysis operations as DPs and APs, using the SFMP representation as a starting point. Next we propose a mapping to create a SFMP from a SFM. We guide the mapping through an example in Figure §6.2. 6.3.1 Constants (C) A constant in Crepresents a static item in a SFM. In this case they represent the elements (E) and states (S) in a SFM. Caps letters are used for each constant. The following set of constant results for the given example: C={Froot,FA,FB,FC,FD,FE,C1,sel,rem,1,2,3} 6.3.2 Variables (V) A variable in Vrepresents a dynamic item in a SFM. Variables are used to represent the current element states. So every element in Ei∈Ehas its corresponding variable 81 CHAPTER 6. AUTOMATED ANALYSIS OF STATEFUL FEATURE MODELS !" #" $" %" &'()*" +,,-" ." !" "" Figure 6.2: A stateful feature diagram example sEi∈V. The following set of variables results for the given example: V={sFroot ,sFA,sFB,sFC,sFD,sFE,sC1} 6.3.3 Domains (D) The set of domains defines the available states in terms of logical predicates. For this purpose, any sj∈ASeisuch that ASEiis the set of available states for an element Ei∈E, is represented by a state(Ei,Sj)predicate such that Eiand Sjare the corresponding element and state constants. In a product, an element can only have one state from the available ones. This approach is followed to represent the domain as a mutual exclusion of the available states1. So for example, the available states for a feature are described in the domain as a logical formula in the following form: state(Fi,sel)⊕state(Fi,rem) Initially, neither state(Fi,sel)nor state(Fi,rem)can be confirmed to be true or false, so the above formula represents the undecided state itself. If state(Fi,sel)and state(Fi,rem) 1The ⊕operator corresponds to mutual exclusion and can be defined as follows: a⊕b≡(p∧ ¬q)∨ (¬p∧q). 82 6.3. A LOGICAL REPRESENTATION OF STATEFUL FEATURE MODELS are true at the same time, then a contradiction state arises. If any of the states is discarded, then the other state can be assumed to be true. For example if a feature cannot be selected then it can be immediately concluded that the feature must be removed: state(Fi,sel)⊕state(Fi,rem)∧ ¬state(Fi,sel)|=state(Fi,rem) A root feature can only have the selected state so that its domain is defined simply as state(FRoot,sel). Cardinalities can be represented by a mutual exclusion of the available cardinals as for features. However, and due to the representation that we propose later for set relationships, we model them in a different manner. The widest possible range of cardinals in cardinalities is [0..n]such that nis the number of child features in the set relationship. If a more restrictive range is defined, the corresponding domain must not only define the valid cardinals but those cardinals that cannot be given. So for example, the domain formula for a set relationship with three child features and a cardinality {1,2,4}results as follows: (state(C,1)⊕state(C,2)⊕state(C,4)) ∧ ¬state(C,0)∧ ¬state(C,3) Lastly, the domain also includes a formula to link element constants with the corresponding state variables as follows: state(E1,sE1)∧state(E2,sE2)∧... ∧state(En,sEn) Following the above rules, we obtain this set of domain formulas results from the example: D={state(Froot,sel), state(FA,sel)⊕state(FA,rem), state(FB,sel)⊕state(FB,rem), state(FC,sel)⊕state(FC,rem), state(FD,sel)⊕state(FD,rem), state(FE,sel)⊕state(FE,rem), (state(C1,1)⊕state(C1,2)) ∧ ¬state(C1,3), state(FRoot,sFRoot )∧state(FA,sFA)∧state(FB,sFB)∧state(FC,sFC)∧ state(FD,sFD)∧state(FE,sFE)∧state(C1,sC1)} 83 CHAPTER 6. AUTOMATED ANALYSIS OF STATEFUL FEATURE MODELS 6.3.4 Relationships (R) The set of relationships contains formulas to represent the relationships in a SFM. For each relationship in the SFM, one formula is added, depending on the kind of relationship: • Mandatory: a parent feature Pthat has a mandatory relationship with a child feature Cis represented by: mandatory(FP,FC) • Optional: a parent feature Pthat has an optional relationship with a child feature Cis represented by: optional(FP,FC) • Depends: if a feature Adepends on another feature B, the relationship is represented by: depends(FA,FB) • Excludes: two features Aand Bin mutual exclusion are represented by: excludes(FA,FB) • Set: let us consider a parent feature Pin a set relationship with a set of child features C1,...,Cj. If the cardinality for the set-relationship is represented by a constant Ci, then the following formula is defined: setj(FB,Ci,FC1,...,FCj) The following set of relationships results for the given example: R={optional(Froot,FA), depends(FD,FE), mandatory(Froot,FB), excludes(FA,FC), set3(FB,C1,FC,FD,FE)} 84 6.3. A LOGICAL REPRESENTATION OF STATEFUL FEATURE MODELS 6.3.5 User and automatic decisions (U, A) These two sets of decisions contain formulas that represent the user and automatic decisions. Each user and automatic decision is mapped into a logical formula in the following form: • Choose decision: a decision that chooses a state Sjfor an element Eiis represented by: choose(Ei,Sj) • Discard decision: a decision that discards a state Sjfor an element Eiis represented by: discard(Ei,Sj) The following set of relationships results for the given example: U={choose(FC,sel)} A={choose(FA,rem)} 6.3.6 Semantics (S) Logical formulas have no meaning unless a semantics is given to its symbols. In this case, every formula used to represent relationships and decisions are given a meaning describing how they affect the SFM state. The way each kind of relationship affects the state is defined in terms of state predicates as shown in Table §6.1. The terms used in the formulas are variables such as fcor fp. They are substituted in each relationship by the corresponding constants. So for example, the semantics for mandatory(Froot,FB)is state(Froot,sel)⇔state(FB,sel)∧state(FRoot,rem)⇔state(FB,rem). As it can be noticed, the semantics is the same for every SFM, which makes it an invariant artefact in a SFMP. 6.3.7 Traceability table A traceability table contains a bijective relationship between SFM artefacts and constants and variables in a SFMP. It keeps the traceability between SFMPs and SFMs, allowing to interpret any result of logical reasoning in terms of SFM artefacts. For example during the generation of D,R,Uand Athis table is used to find the adequate 85 CHAPTER 7. INTERPRETING QUERY OPERATIONS AS DEDUCTION OPERATIONS to elements that satisfy all the domain, relationships and decision formulas. A valid assignment of states satisfies all the sentences in the KB: the domain, relationships and decisions. In terms of a SFM an assignment can be interpreted as a product that satisfies all the relationships, user and automatic decisions. Thus, this operation can be used for products listing. • Satisfiability: this operation determines if there is at least one valid assignment of constants to variables. Since an assignment is identified with a product, satisfiability can be used to determine if there exists at least one product satisfying all the logical formulas. Depending on the set of user decisions, there are two possible scenarios: i)if it is non-empty, satisfiability helps to detect if there exists at least one product satisfying those decisions; ii) if the set of user decisions is empty, satisfiability detects if there exists at least one product in the SPL, i.e. the SFM is valid. We call validation to the AASFM operation that results from the application of the satisfiability operation. • Inference: this operation determines if a logical sentence can be concluded from the DP. DPs rely on state predicates so conclusions obtained from the DP must be defined on their terms. For example, inference can be used to determine if state(FB,sel)can be concluded from the example in Table §7.1. It can be used to obtain automatic decisions based on existing user decisions, domains and relationships. The computation of automatic decisions on FMs is known as propagation, name that we keep for the AASFM. • Solution checking: this operation checks if a given assignment is a solution for the DP. Since an assignment corresponds to a product, this operation can be used to check if a given product is valid or not. User configurations can be used instead of an input assignment to set the state for any element in the SFM. The resulting model can be checked if it is valid by means of satisfiability. Due to the existence of an alternative to perform model checking, and for the sake of keeping the set of basic operations minimal, we define no basic query operation in AASFM that uses model checking. Based on this analysis we propose three basic query operations that can be solved using deductive reasoning: product listing, validation and propagation. Next we define a correspondence between these query operations and DP operations. 92 7.2. BASIC QUERY OPERATIONS !"#$%"$#& '#($%"$#& )*& +,--./&!&+,--)/& 01213456& 01213"& !"#$%&'() *+(,-.) 7,&8&9!"#$%"$#:)*;& 7<&8&9!"#$%"$#:)*:'#($%"$#;& 7)&8&9!"#$%"$#:)*:01=3456;& 7.&8&9!"#$%"$#:)*:01=3456:'#($%"$#;& & !& "& !& Figure 7.1: An example of products listing operation 7.2.1 Products listing This operation lists all the products in a SFM that satisfy the current decisions and relationships. Figure §7.1 shows an example of this operation for an excerpt of the SHS FM. It corresponds to the solutions operation of a DP. A solution in a DP can be defined as a function µ:V→C. Each variable in a solution is assigned a constant that represents an available state for the element the variable represents. Only state constants such as sel,rem and cardinals are assigned to the variables, since the domain sets this restriction. Therefore, an assignment represents a product in the SFM. So the solutions operation searches for all the products that satisfy all the sentences in the KB: domains, relationships and decisions. From this rationale, the product listing operation can be interpreted in terms of the solutions operation as follows: products(SFMP(C,V,D,R,U,A,S)) ≡solutions(DP(C,V,D∪R∪U∪A,S)) For the running example described in Figure §6.2, the following assignments are valid: µ1={sFRoot 7→ sel,sFA7→ sel,sFB7→ sel,sFC7→ sel,sFD7→ rem,sFE7→ sel,sC17→ 2} µ2={sFRoot 7→ sel,sFA7→ rem,sFB7→ sel,sFC7→ sel,sFD7→ rem,sFE7→ rem,sC17→ 1} µ3={sFRoot 7→ sel,sFA7→ rem,sFB7→ sel,sFC7→ sel,sFD7→ rem,sFE7→ sel,sC17→ 2} If the DP contains any contradictory logical sentence then the result is an empty set of products. The results from this operation is obtained in terms of constants and variables. In order to interpret the results in terms of SFM elements and states, the traceability table is used. Each feature variable sFicorresponds to a feature constant Fi, which is conveniently linked to a feature in the original SFM in the traceability table. Since products are usually represented only by the selected features, the corresponding 93 CHAPTER 7. INTERPRETING QUERY OPERATIONS AS DEDUCTION OPERATIONS products for the above assignments are: P1={Root,B,E} P2={Root,B,D,E} P3={Root,B,C,E} 7.2.2 Validation A validation operation checks if a SFM is valid or not. It means to check if the decisions within the SFM satisfies all the relationships. In terms of a DP where the set of domains, relationships and decisions form the KB, a validation operation corresponds to the satisfiability operation for the DP: valid(SFMP(C,V,D,R,U,A,S)) ≡isSatis f iable(DP(C,V,D∪R∪U∪A,S)) Let us take the example SFM lo illustrate how validation works. Firstly we expand the semantics of the KB so the reader can understand the validation: optional(Froot,FA)≡state(FA,sel)⇒state(Froot,sel)∧ state(FA,rem)⇒state(Froot,rem) mandatory(Froot,FB)≡state(Froot,sel)⇔state(FB,sel)∧ state(Froot,rem)⇔state(FB,rem) set3(FB,C1,FC,FD,FE)≡state(FB,sel)⇔numSelChild3(C1,FC,FD,FE)∧ state(FB,rem)⇒(state(FC,rem)∧state(FD,rem)∧state(FE,rem)) depends(FD,FE)≡state(FD,sel)⇒state(FE,sel) excludes(FA,FC)≡state(FA,sel)⇔state(FC,rem)∧ state(FC,sel)⇔state(FA,rem) numSelChild3(C1,FC,FD,FE)≡state(C1,0)⇔(state(FC,rem)∧state(FD,rem)∧state(FE,rem)) state(C1,1)⇔(state(FC,sel)⊕state(FD,sel)⊕state(FE,sel))∧ state(C1,2)⇔((state(FC,sel)∧state(FD,sel))∨ (state(FD,sel)∧state(FE,sel))∨ (state(FC,sel)∧state(FE,sel)))∧ state(C1,3)⇔(state(FC,sel)∧state(FD,sel)∧state(FE,sel)) choose(FC,sel)≡state(FC,sel) choose(FA,rem)≡state(FA,rem) . There exists several possible assignments for this DP. Thus, the DP is satisfiable and therefore the SFM is valid. However, if feature Dwere selected then {choose(FD,sel)} 94 7.2. BASIC QUERY OPERATIONS predicate would have to be added to the KB. In this case the resulting DP is unsatisfiable because the depends relationship forces to select feature Eand three child features have to be selected which conflicts with the cardinality [1..2] in the set relationship. In logical terms it is justified by: choose(FD,sel),depends(FD,FE)|=state(FE,sel) choose(FC,sel),choose(FD,sel),state(FE,sel),¬state(C1,3),set3(FB,C1,FC,FD,FE)|=⊥ Since a valid SFM is the one that defines at least one product, this operation can be defined in terms of product listing as follows: valid(SFMP(...)) ≡products(SFMP(...)) ,∅ This definition of the validation operation comes from the consideration of satisfiability as a particular case of the solutions operation. Most of the existing reasoning tools, use different algorithms for satisfiability and finding all the solutions. We prefer to include the validation operation in the set of basic operations to exploit the performance issues in satisfiability algorithms. 7.2.3 Propagation The relationships in a SFM constrain the combinations of states that are considered to be valid. It may imply that an element that apparently can have several states, can effectively have a subset of them due to existing relationships. So for example, feature B has a mandatory relationship with the Root feature. It forces feature Bto have a selected state while removed state must be discarded. User decisions have a similar impact in the states of a SFM. If a user chooses a state for an element, it may imply that some other elements are affected by this decision. So for example, if feature Cis selected, feature Amust be removed as a consequence. The propagation operation receives an input SFM and obtains as a result another SFM where the conclusions that are obtained about the states of all the elements are added to the set of automatic decisions. So every combination of states and elements must be checked if it is still available or not. Figure §7.2 presents an example of propagation. This operation can be interpreted as the extraction of conclusions from the information modelled in the DP. Since we are interested in the effect of relationships and 95 CHAPTER 7. INTERPRETING QUERY OPERATIONS AS DEDUCTION OPERATIONS !"#$%"$#& '#($%"$#& )*& +,--./& 01213456& 01213"& !"#$%"$#& '#($%"$#& )*& +,--./&!7&+,--)/& 01213456& 01213"& !"#$%&%'() !& "& !& "& !& Figure 7.2: An example of a propagation operation configurations in the state for each element in the SFM, this operation discards states that are not available anymore and sets mandatory states for each element affected by relationships and configurations. In terms of a DP, this operation checks for each element-state pair (Ei,sj)if it can be chosen or discarded automatically. Two checks are performed for each pair: •isIn f erred(DP(...),state(Ei,sj)): if it is possible to infer that the element Eimust have the sjstate, then choose(Ei,sj)must be added to the set of automatic decisions. •isIn f erred(DP(...),¬state(Ei,sj)): if it is possible to infer that the element Eicannot have the sjstate anymore, then discard(Ei,sj)must be added to the set of automatic decisions In the example, if we ignore the automatic decision that removes feature A, it can be inferred by means of propagation. Feature Acannot be selected because it is involved in an excludes relationship with feature Cthat is selected in the configuration: isIn f erred (DP(C,V,D∪R∪U∪A,S),state(FA,sel)) is true since {choose(FC,sel),excludes(FA,FC),state(FA,sel)⊕state(FA,rem),...} ≡ {state(FC,sel),state(FC,sel)⇔state(FA,rem)∧...,state(FA,sel)⊕state(FA,rem),...} |=state(FA,rem)∧ ¬state(FA,sel) Cardinalities are checked in the same way features are, it means checking each cardinal for being valid. So if feature Ewere selected in a configuration then cardinal 1 is discarded because: {choose(FC,sel),choose(FE,sel),set3(FB,C1,FC,FD,FE), (state(C1,1)⊕state(C1,2)) ∧state(C1,3),...} |=¬state(C1,1) 96 7.3. SUMMARY Repeating this inference procedure for any pair of elements and states a propagated SFM is obtained as a result. This operation can be defined as follows: propagate (SFMP(C,V,D,R,U,A,S)) ≡SFMP(C,V,D,R,U,A∪Auto,S)s.t. Auto ={choose(Ei,sj)|Ei∈C,sj∈V,isIn f erred(DP(C,V,D∪R∪U∪A,S),state(Ei,sj))}∪ {discard(Ei,sj)|Ei∈C,sj∈V,isIn f erred(DP(C,V,D∪R∪U∪A,S),¬state(Ei,sj))} As for product listing, the traceability table helps to identify the elements and states in the state predicates with the corresponding elements and states in the SFM. 7.3 SUMMARY In this Section we have proposed a straightforward map from a SFMP to a DP. We have identified three basic query operations that are interpreted as deductive operations: product listing, validation and propagation. They can be later combined with model edition operations to perform more complex analysis operations such as errors detection or metric calculation as shown in Chapter §9. We have set the basis to use logical reasoners to execute these operations. The use of FOL as the underlying logic of DPs helps to implement our proposal in terms of different solvers that support deductive reasoning. This benefits are studied in depth in Annex §B. 97 CHAPTER 7. INTERPRETING QUERY OPERATIONS AS DEDUCTION OPERATIONS 98 8 INTERPRETING EXPLANATORY OPERATIONS AS ABDUCTION OPERATIONS 99 He that will not reason, is a bigot; he, who cannot, is a fool; and he, who dares not, is a slave. Sir William Drummond (1585–1649), Poet In this Chapter we give a semantics for SFMs in terms of APs, which allows the use of abductive reasoning to perform some AASFM operations. Specifically, two basic explanatory operations are proposed based on the abductive operations that are useful from the AASFM point of view. In Section §8.1 we establish a connection between the AASFM and abductive reasoning. Section §8.2 proposes a mapping from SFMPs to APs that allows to perform abductive operations. Section §8.3 proposes two basic explanatory operations that cover all the explanatory analysis scenarios for the AASFM. Section §8.4 indicates how to use the traceability tables to map the results obtained for APs back to SFM artefacts. Section §8.5 proofs that some operations that were proposed for the AAFM make no sense or can be defined in terms of the proposed basic explanatory operations. Lastly, Section §8.6 summarises the contributions of this Chapter and discusses the benefits that arise from our approach. CHAPTER 8. INTERPRETING EXPLANATORY OPS. AS ABDUCTION OPS. 8.1 INTRODUCTION The goal of explanatory operations is obtaining explanations why the user decisions or the relationships cause a certain behaviour. Query operations allow the obtention of implicit data within a SFM. However, this reasoning approach is not suitable for those cases in which we want to obtain explanations why certain behaviours are given. For example, the validation operation can detect if a SFM is invalid but it provides no further information about the reasons why it is invalid. Maybe because of some conflicting relationships that avoid to find a product; or because of user decisions that violate existing relationships. In any case, deduction cannot be used to reason about the source of invalidness. As one of the conjectures in our dissertation, we propose the interpretation of explanatory operations as abductive operations. We already proposed this approach for FMs in [85] and we propose that this hypothesis is also valid for SFMs. SFMs need to be interpreted in terms of an AP to perform any abductive operation. An AP defines a set of hypotheses that can be used to explain a given observation. Depending on the terms in which we want to obtain explanations, relationships or user decisions, two different representations of an SFM as an AP can be obtained: one that allows to obtain explanations in terms of the relationships (APR) and another one in terms of user decisions (APU). In this Chapter we present how abductive operations can be used to define and formalise the basic explanatory operations for the AASFM. With this approach we achieve two goals: i) Proposing two explanatory operations to perform any explanatory analysis of SFMs ii) Demonstrating that a subset of explanatory operations that were defined for the AAFM in [85] makes no sense. 8.2 SFMS AS ABDUCTION PROBLEMS In order to perform explanatory operations, an SFM is interpreted as an AP. The process to obtain it is similar to the interpretation of SFMs as DPs. Firstly, an SFM is interpreted as an SFMP. Then, the SFMP is transformed into an AP in a form that depends on the kinds of explanations to obtain. So whether explanations must be given in terms of relationships or user decisions, a different AP is used as shown in the following Sections. 100 8.2. SFMS AS ABDUCTION PROBLEMS 8.2.1 Explaining relationships There are many scenarios where it is important to obtain explanations in terms of relationships. For example, an invalid SFM can be detected by using the validation operation, but it is necessary to find explanations for the invalidness. These explanations are given in terms of the possible sets of conflicting relationships, which can assist the reparation process of the SFM. Another scenario is a SFM such that user decisions are set for every element in a SFM, defining a product. If the SFM is invalid and we certainly know that the user decisions define a valid configuration, it is important to obtain explanations about the invalidness in terms of the set of relationships that make it impossible to obtain that product. Independently of the particular analysis operation, it is possible to define an AP whose objective is obtaining explanations in terms of relationships. We have to determine which logical sentences from a SFMP are the facts, the hypotheses and the observations. The first point is that the set of hypotheses must be correspond to the set of sentences that describe the relationships. This is because explanations will be defined as subsets of relationships. The set of facts defines the set of statements that are known to be true under any circumstance. It corresponds to the set of domain sentences. We certainly know that a feature can be either selected or removed and this fact is invariant and cannot be used to explain an invalid SFM. The set of observations corresponds to the set of user decisions. Therefore the objective of the AP is to explain why a certain set of decisions is valid or invalid for the given relationships. So for example, if it is not possible to select a certain feature (observation), we want to explain why it happens from the given set of relationships (hypotheses). So the AP that can be used to obtain explanations in terms of relationships results as follows1: SFMP(C,V,D,R,U,A,S)7→ APR(C,V,(D,R,U),S,MinS) MinSis any minimality criterion (see Section §3.2.1) to be used to select the most probable explanations. Note that the set of automatic decisions is left out of the AP. Automatic decisions are set by the propagation operation as conclusions that are obtained from the domain, relationships and user decisions. Since the relationship sentences form the set of hypotheses, the subset of intervening relationships changes from explanation to explanation, so an automatic decision could not be concluded using the subset of relationships in an explanation. Thus, automatic decisions are left out of 1see Section §3.2 for a description of the APs structure 101 CHAPTER 8. INTERPRETING EXPLANATORY OPS. AS ABDUCTION OPS. that describes this problem has an empty set of observations so the minimal explanation operation cannot be used to obtain explanations. In this case, the minimal conflict set operation comes into play providing ∆sets that are inconsistent with the set of facts; MinCon f licts(APR(C,V,(D∪R,U,∅),S,min)) ≡min({∆|∆⊆U,D∪Ris consistent,D∪R∪∆|=⊥}) Note that the precondition that D∪Rmust be consistent, establishes that the SFM must be valid without any configuration. For the example SFM in Table §8.2, features C,Dand Eare selected by user decisions. The SFM without any configuration is valid since it defines several products. The configuration makes an SFM invalid since the <1..2> cardinality of the set relationship is violated. Each subset of the configuration is checked if it is a conflict set obtaining the following results: D∪R∪ {choose(FC,sel),choose(FD,sel),choose(FE,sel)}is inconsistent D∪R∪ {choose(FC,sel),choose(FD,sel)}is inconsistent D∪R∪ {choose(FC,sel),choose(FE,sel)}is consistent D∪R∪ {choose(FD,sel),choose(FE,sel)}is consistent D∪R∪ {choose(FC,sel)}is consistent D∪R∪ {choose(FD,sel)}is consistent D∪R∪ {choose(FE,sel)}is consistent Thus two conflict sets are obtained: {choose(FC,sel),choose(FD,sel),choose(FE,sel)} and {choose(FC,sel),choose(FD,sel)}. Since the first one is a superset of the second one, the second one is a minimal conflict set. We define the ’Why are the user decisions not valid?’ operation as the realisation of a minimal conflict set operation on an AP for configuration explanation as follows: WhyNotCon f (SFMP(C,V,D,R,U,A,S)) ≡MinCon f licts(APR(C,V,(D∪R,U,∅),S,min)) 8.4 TRACEABILITY 8.4.1 Relationships explanations The traceability table assists the mapping from AP results to relationships in the original SFM. There is an indirect one-to-one relationship between predicates in the 108 8.5. DISCARDING SENSELESS EXPLANATORY SCENARIOS hypotheses set and relationships. Each predicate indicates the kind of relationship, and its constants represent the elements in the SFM that are affected by the relationship. Since a SFM can only contain one relationship of the same kind that affects a set of elements, it is quite easy to obtain the relationship that corresponds to a predicate. So for the example, we obtained {depends(FD,FE)}as an explanation. The constants FDand FEcorrespond to features Dand Erespectively. Thus, the predicate in the explanation represents a depends relationship between features Dand Eunambiguously. 8.4.2 Configuration explanations The explanations for a ’why is a configuration not valid?’ operation are choose and discard predicates. They can be mapped back to the corresponding ChooseStateConstraint or DiscardStateConstraint instances in the SFM if there exist only one instance that affects a specific pair of element and state. For the previous example, the choose predicates can be traced to the SFM to determine that selecting Cand Dat the same time is a source of conflict. Thus, either the ChooseStateConstraint instance that selects Cor the one that selects Dmust be removed from the SFM to solve the conflict. Note that there exists no problem in case there exist more than one user decision selecting or discarding a state. In that case, all the user decisions that refer to the same pair of element and state will be in the explanation at the same time. 8.5 DISCARDING SENSELESS EXPLANATORY SCENARIOS In this Section we present some scenarios where abductive reasoning cannot be applied to analyse SFMs. Firstly, we present the kinds of configuration that lead to no explanation at all. Secondly, we present two ’why?’ operations that were proposed for FMs in [85] as an exploitation of abductive reasoning. We rely on the formalisation of the explanatory analysis to discard ’why?’ operations as an alternative explanatory operation. 8.5.1 Invalid configurations In a WhyNotRels operation it is not possible to obtain explanations if the precondition D6|=Ufor the minimal explanation operation is violated. There are only two cases where a SFM violates this precondition: 109 CHAPTER 8. INTERPRETING EXPLANATORY OPS. AS ABDUCTION OPS. • Root feature is removed: The configuration that produces inconsistency contains the {choose(FRoot,rem)}sentence. So the WhyNotRels operation searches for the minimal explanations for {¬choose(FRoot,rem)}. Since the domain sentences forces the root feature to be selected, the precondition of minimal explanation operation is violated, because the observation can be inferred from the domain i.e. state(FRoot,sel)|={choose(FRoot,rem)}. • Unique cardinal is chosen: A cardinality Ciin a set relationship has a unique valid cardinal n. So from the domain it can be inferred that D|={state(C,i,n)}. If a configuration sets the sentence {choose(Ci,n)}then a WhyNotRels operation searches for explanations for {¬choose(Ci,n)}which clearly contradicts the domain sentences, so the precondition is violated. As a conclusion, no explanation can obtained if a configuration contradicts any domain sentence. 8.5.2 Why are the relationships valid? In [85], the so-called ’why?’ operations were proposed for the AAFM. They were used to obtain explanations when a FM is valid, instead of when it is invalid. In this Section we rely on the previous formalisation of explanatory operations to demonstrate that these operations for SFMs either makes no sense from the analysis point of view or can be defined in terms of a ’why are the relationships not valid?’ operation. A SFM is valid if the corresponding DP(C,V,KB,S)is consistent. It means that D∪R∪Uis consistent. The general definition of an explanation operation is: MinExpl(AP(C,V,(D,R,U),S,Min)≡Min({∆|∆⊆R,D6|=U,D∪∆|=U}) Analysing the above definition of explanation there are two possible situations for this operation if D∪R∪Uis consistent: 1. Explanations can be obtained if there exists at least a subset ∆of Rsuch that D∪∆|=U. Since D∪R∪Uis consistent because the SFM is valid, for any subset ∆⊆R,D∪∆∪Umust be consistent. At least an explanation ∆is obtained if D∪∆|=U. Since D∪∆∪Uand D∪R∪Uare consistent we can affirm that: D∪∆|=U,∆⊆R,D∪R∪Uis consistent ⇒D∪R|=U. 110 8.5. DISCARDING SENSELESS EXPLANATORY SCENARIOS If D∪R|=U, then it can be affirmed that D∪R∪ ¬Uis inconsistent. Thus we conclude that explanations are only obtained for a ’why?’ operation if it really corresponds to a ’why are the relationships not valid?’ for the negation of the configuration. In other words: WhyRels(SFMP(C,V,D,R,U,A,S)) ≡WhyNotRels(SFMP(C,V,D,R,¬U,A,S)) 2. No explanation is obtained under two circumstances: (a) If the precondition D6|=Uis violated it is because either: • The observation is {state(FRoot,sel)}which is part of the set of facts F. The root must always be selected for any product and asking why it is so is a trivial question. • The observation is F|={state(C,i,n)}being na unique valid cardinal for a cardinality Ciof a set relationship also contradicts the precondition. (b) For no subset of ∆⊆R,Uis a logical consequence. For the given example, determining why feature Ais selectable makes no sense since features are modelled to be selectable. If we set the configuration {choose(FA,sel)}, it is consistent with the existing relationships but it cannot be concluded from the set of domain and relationship sentences. In this case, the ’why?’ operation obtains no result and therefore it makes no sense from the analysis point of view. From the above analysis, we extract an important conclusion that can even be extrapolated to the AAFM: why?’ operations make no sense unless they are implicitly solving a ’why not?’ operation. 8.5.3 Why is a configuration valid? In a symmetry with the previous operation, we have studied if it makes sense to perform a ’why?’ operation for configurations instead of relationships. In this case, the 111 CHAPTER 8. INTERPRETING EXPLANATORY OPS. AS ABDUCTION OPS. input SFM must be valid, therefore D∪R∪Uis consistent. Regarding the ’why not?’ case, explanation problems does not fit into this case since there is no observation. Conflict sets neither fit into this kind of problem since there is no inconsistency. So what can we expect from this operation? No result at all. A configuration is expected to be valid by default, so asking why that is so is a triviality. Therefore ’why is a configuration valid given a SFM?’ is an operation that makes no sense and must be removed from the catalog of explanatory operations. 8.6 SUMMARY In this Chapter we have proposed an interpretation of SFMs as APs to perform the explanatory analysis of SFMs. Two different interpretations are given to obtain explanations in terms of relationships or configurations. For each interpretation, one basic explanatory operation is defined to explain the reasons why a SFM is invalid. So the operation ’why are the relationship not valid?’ explains an invalid SFM in terms of relationships and ’Why are the user decisions not valid?’ explains an invalid SFM in terms of user decisions. These operations covers all the possible analysis scenarios that have been proposed at date for FMs as it is shown in Chapter §9. As an important conclusion we have not only proposed two explanatory operations but we have demonstrated that the so-called ’why?’ operations for the explanatory analysis of FMs can either be defined in terms of a ’why are the relationship not valid?’ operation or they make no sense from the analysis point of view. At this point, we have proposed five basic operations for the AASFM. In the next Chapter we present how they can be combined to perform more complex analysis operations that covers most of the user needs. 112 9 A CATALOGUE OF ANALYSIS OPERATIONS 113 I often liken the process of physics research to solving a jigsaw puzzle. As we put together pieces to form patches, a certain image of the overall picture emerges, but until the game is sufficiently progressed, we are not quite sure. Benjamin W. Lee (1935–1977), Theoretical physicist Basic operations, either query or explanatory, have set the basis of the AASFM. In this Chapter we explore how these basic operations can be combined to support the automated analysis. For that sake, section §9.1 presents a categorisation of operations. Section §9.2 presents a summary on the basic operations proposed in previous Chapters. Section §9.3 presents a wide catalogue of compound query operations. Section §9.4 presents a set of configurations or scenarios that can be used to realise different compound explanatory operations for SFMs. Section §9.5 shows some examples where query and explanatory operations are combined to perform compound mixed operations. Last, in Section §9.6, some conclusions are approached to study the application of the proposed catalogue of AASFM operations. CHAPTER 9. A CATALOGUE OF ANALYSIS OPERATIONS 9.1 INTRODUCTION In order to define a catalogue of AASFM operations as complete as possible, we take the most complete and thorough catalogue proposed to date by Benavides et al. [14]. However, we want to go further than a one to one correspondence of operations. We propose a new classification of analysis operations that defines a reduced set of operations sufficient to perform the AASFM. It will allow to define new operations as a composition of them and to propose implementations of the AASFM that are fully-fledged with few operations. We distinguish the following kinds of AASFM operations: • Basic: cannot be defined in terms of other operations. Depending on the kind of reasoning that is used to solve them, two subtypes of basic operations are proposed: –Explanatory operations: The goal of explanatory operations is obtaining explanations why the configuration or the relationships are provoke a certain behaviour. They can be interpreted as abduction problems. –Query operations: the goal of a query operation is to extract implicit information from a SFM and make it explicit. Explanatory operations could be considered to fit into this definition so a query operation can also be defined as any non-explanatory operation. They can be interpreted as deduction problems. • Compound: a compound operation can be defined on top of model edition and basic operations. If a compound operation only combines basic query operations, it is called a compound query operation. Symmetrically, if a compound operation only relies on basic explanatory operations, it is called a compound explanatory operation. In case a compound operation combines query and explanatory operations it is called a compound mixed operation. In this Chapter we present how to use compose model edition and basic operations to perform compound operations. The possible combinations grow exponentially being unfeasible to present a complete catalogue of operations. So in this Chapter we present how the most used operations for the AAFM are reinterpreted as compound operations for the AASFM. This approach increases the added-value of the AASFM whose reasoning capabilities increase significantly compared with the AAFM. 114 9.2. BASIC OPERATIONS Basic Operations SFM Operation Problem Reasoning Operation Product Listing DP Solutions Propagation DP Inference Validation DP Satisfiability Why are the relationships not valid? APRMinimal Explanations Why is a configuration not valid? APCMinimal Conflict Set Table 9.1: Basic operations in the AASFM 9.2 BASIC OPERATIONS Five basic operations, that are summarised in Table §9.1, have been defined in previous Chapters for different analysis purposes. We choose to Java as a language to describe how basic and model edition operations are combined. Firstly, it provides a syntax to manipulate metamodel instances. Secondly, model edition operations have already been defined as methods in the SFMM. Thus, each basic operation is assigned to a method prototype in Java that provides its functionality: •Product listing: The prototype for this operation is Set<Product> products(SFM inputSFM) such that the Product class encapsulates a Map<Element,State> instance that contains element-state pairs. •Validation: The prototype for this operation is boolean valid(SFM input). •Propagation: The prototype for this operation is SFM propagate(SFM input). •Why are the relationships not valid?: The prototype for this operation is Set< Set <Relationship>> whyNotRels (SFM input). An explanation is given in the form <Set<Relationship>. Since several explanations can be obtained, the obtained result is a set of explanations Set<Set<Relationship>>. •Why is the configuration not valid?: The prototype for this operation is Set< Set< Configuration>> whyNotConf (SFM input). As it is obvious the configuration in the SFM cannot be empty, otherwise there would be no configuration to diagnose. The implementation of these methods will be discussed in Annex §B. 115 CHAPTER 9. A CATALOGUE OF ANALYSIS OPERATIONS 9.3 COMPOUND QUERY OPERATIONS A compound query operation can be defined as a composition of model edition and basic query operations. Three model edition methods are used for the definitions: setUserDecisions,setAutoDecisions and reset. 9.3.1 Void SFM A SFM is said to be void if it defines no product at all independently of the configurations that are set. A SFM is void mainly due to contradictory relationships that cannot be satisfied at the same time. To ensure that the SFM contains no configuration constraint, the SFM must be reset prior to validation. This operation can be defined as follows: boolean voidSFM (SFM inputSfm) { SFM resetSfm = reset(inputSfm); return !valid(resetSfm); } Figure §9.1 shows an example of this operation. Note the difference between an invalid and a void SFM. A SFM is invalid if its configuration does not satisfy all the relationships in the model. A SFM is void if after removing any configuration the SFM is still invalid. Thus, a void SFM is invalid for any given configuration. !"#$%&'(")& *(+%$(,& !-.%)"&& /+01%2)3& /,#$"&& *),,&42(+)&& *(+%$(,& 4#+),& 567768& !"#$% 96& 9:& 9;& 9<& !"#$%&'(")& *(+%$(,& !-.%)"&& /+01%2)3& /,#$"&& *),,&42(+)&& *(+%$(,& 4#+),& 5:77:8& !"#$% 96& 9:& 9;& 9<& =#,.)& %$>)& Figure 9.1: An example of a void and a non-void (valid) SFM 116 9.3. COMPOUND QUERY OPERATIONS 9.3.2 Products counting This operation counts the number of different products a SFM describes for the given configuration. This operation can be seen as the cardinal of products obtained by the products listing operation so it can be defined in the following form: int count (SFM inputSFM) { return inputSFM.products.size(); } For an invalid SFM, this operation counts zero products. An example of this operation is shown in Figure §9.2. For the invalid SFM in Figure §9.1 the products counting operation returns zero. !"#$%&'(")& !& *+,-./,&!&0(/%$(1& !23%)"&!& 4/%)$/)%& 5(6+)& 71#2)$3& 8/.9%-):& 81#$"& 0(/%)/%3& 0)11&;-(/)&0(/%$(1& ;#/)1& <=>>?@& A+B)(&(/& C)"#/B& C+,+%#1&5)B+#& !)$6)$& <=>>?@&!&D?E& && 'CFA&G?H& 'CFA&I?H& <=>>I@& J%-)$/)%& IK& <=>>G@&!&D=L?LIE& M+N+9OP,& M+N+9/& ;$(6+B)$3& 0#Q-)& ;$(6+B)$&8& ;$(6+B)$&R& <=>>?@& ;0;1#2)$& !"#$%&'() &#%*+*,)STS& Figure 9.2: An example of products counting 9.3.3 Configure with propagation In an individual configuration process, the propagation operation can be executed just after a user decision since it is not possible to receive other configurations from other stakeholders. This operation is implemented as follows: SFM configWithPropagation(SFM inputSfm , Set<Configuration > conf) { SFM intermediateSfm = setUserDecisions(inputSfm , conf); SFM outputSfm = propagate(intermediateSfm); return outputSfm; } 117 CHAPTER 9. A CATALOGUE OF ANALYSIS OPERATIONS we present two of them as samples: •Variability Degree: it measures how restrictive a SFM is. The most flexible SFM that can be built given a set of Nfeatures, is the one where all the features are optional, and therefore any combination of them is allowed. In this situation, the number of products that can be built with the most flexible SFM is 2N. So for the example in Figure §9.2, the variability degree is 0,00531.This metric compares the number of products in a SFM to the most flexible SFM. Following we show an example of implementation of a method supporting this operation: public double variabilityDegree(SFM inputSfm) { SFM resetSfm = reset(inputSfm); int numProducts = count(resetSfm); int numFeatures = inputSfm.getFeatures().size(); int numProductsNoConstraint = Math.pow(2,numFeatures); return numProducts / numProductsNoConstraint; } •Commonality Factor: The commonality factor for a set of features indicates the ratio of products where the features in an input set are selected at the same time. To count the number of products where a set of features appears is as easy as selecting all the features in the set in a configuration and counting its products. The result must be compared to the total amount of products defined by the SFM. So for the feature Video On Demand in Figure §9.2, the commonality factor is 0,724 since it appears in 504 products and the total number of products in the SFM is 696. The following code shows an implementation of this operation: double commonalityFactor(SFM inputSfm , Set<Feature > featureSet) { SFM resetSfm = reset(inputSfm); int numberOfProducts = count(resetSfm); Set<Configuration > configSet = new HashSet <Configuration >(); for (f: featureSet) { configSet.add( new ChosenStateConfiguration (f, new SelectedState ()) ); } SFM configSfm = setAutoDecisions(resetSfm , configSet); int numberOfFilteredProducts = count(configSfm); return numberOfFilteredProducts / numberOfProducts; } 124 9.4. COMPOUND EXPLANATORY OPERATIONS 9.4 COMPOUND EXPLANATORY OPERATIONS The catalogue of explanatory operations for FMs in [85] links each explanatory operation to a query operation. An explanatory operation explains the results obtained from a query operation. So for example dead feature detection is linked to an operation ”why is a feature dead?”. In order to detect a dead feature, the SFM state is reset and a configuration that selects the feature under analysis is set. In case a feature is dead, the same SFM can be used to obtain explanations by means of a ’why are the relationships not valid?’ operation. So the connection between query and explanatory operations is established by means of the configuration used to detect and explain certain behaviours. There is a set of compound query operations that use predefined configurations or scenarios to detect certain behaviours. If the resulting SFM is invalid then an explanatory operation can be used to explain the source of invalidness. Query operations such as anomalies detection, void SFM, core feature and variability degree fit into the following schema: 1. SFM is reset. 2. A scenario is set as a configuration. 3. The list of products is obtained. 4. The output is calculated and returned. If the list of products obtained in step 3 is empty then the SFM is invalid. In that case, an explanatory operation can be realised to obtain explanations why this behaviour happens. The general schema for the compound explanatory operation results as follows: 1. SFM is reset. 2. A scenario is set as a configuration. 3. Why are the relationships not valid? Analysing the list of compound query operations in Section §9.3, six different scenarios are used in their definitions: •Select Feature: It is used by dead feature detection and variability degree operations. Both operations set a configuration {choose(F,sel)}that only selects the feature Funder analysis. 125 CHAPTER 9. A CATALOGUE OF ANALYSIS OPERATIONS •Remove Feature: It is used by the core feature operation. This operation sets a configuration {choose(F,rem)}that removes the feature Funder analysis. •Select Parent, Remove Child: It is used by the false-optional feature detection. This operation sets a configuration {choose(FP,sel),choose(FC,rem)}that selects the parent feature Pand removes the child feature C. •Select Cardinal: It is used by the wrong cardinal detection. This operation sets a configuration {choose(Ci,n)}that chooses a cardinal nfor a given cardinality. •Remove Cardinal: It is used by the unique cardinal detection. This operation sets a configuration {discard(Ci,n)}that discards a cardinal nfor a given cardinality. •Empty: It is used by the void SFM and variability operations. This scenario is a particular case where no configuration is set. In this situation, the configuration cannot be empty and perform the ’why are the relationships not valid?’ operation since the resulting AP has an empty configuration that violates the precondition of the minimal explanation problem. In this case, the configuration can be set as a tautology (>). Since the explanatory operation solves the negation of the observation, the configuration to explain results as a contradiction (⊥). So the WhyNotRels(SFMP(C,V,D,R,>,S)) ≡ ≡MinExpl(APC(C,V,(D,R,⊥),S,minS)) ≡min({∆|∆⊆R,D6|=⊥},D∪∆|=⊥} ≡MinCon f licts(APC(C,V,(D,R,⊥),S,minS)) With this approach we avoid the definition of a new basic explanatory operation that uses minimal conflict operation for the APRproblem. This way the set of basic operations is kept to a minimum. As an example, defining a compound explanatory operation to explain dead features results as follows: Set<Set<Relationship >> explainDead(SFM inputSfm ,GenericFeature f) { Set<Configuration > configSet = new HashSet <Configuration >(); configSet.add( new ChosenElementConstraint (f,new SelectedState()) ); SFM resetSfm = reset(inputSfm); SFM configuredSfm = setAutoDecisions(resetSfm ,configSet); return whyNotRels(configuredSfm); } 126 9.5. COMPOUND MIXED OPERATIONS Compund Explanatory Operations Scenario Query Why...? Empty void SFM, variability ...a SFM is invalid Select Feature Commonality, Dead ...is Fa selectable feature Remove Feature Core ...is Fa removable feature Select Parent, Remove Child False-optional ...is Fa false-optional feature Select Cardinal Wrong cardinal ...is na wrong cardinal for Ci Remove Cardinal Unique cardinal ...is na unique cardinal for Ci Table 9.2: Scenarios and their relationship with query and explanatory operations As a conclusion, compound explanatory operations combine model edition and basic explanatory operations to obtain explanations for unexpected behaviours in SFMs. Each scenario permits the explanation of different behaviours. The relationships among scenarios, query and compound explanatory operations are summarised in Table §9.2. !"#$%&'(")& *(+%$(,& !-.%)"&& /+01%2)3& /,#$"&& *),,&42(+)&& *(+%$(,& 4#+),& 567768& !"#$%&$ '()$*+,$ -./%01$ 9:& 96& 9;& 9<& 567768& /+01%2)3& /,#$"& *(+%$(,& 4#+),& *(+%$(,& !-.%)"& *),,&42(+)&*(+%$(,& 4#+),& !"#$%&'(")& *(+%$(,& !-.%)"& /+01%2)3& #,#$"& Figure 9.7: An example of compound explanatory operation for a void SFM 9.5 COMPOUND MIXED OPERATIONS A compound mixed operation is the one that mixes query, explanatory and/or model edition operations. This category is the miscellany of operations for the AASFM. As an example, we propose an operation that detects and explains a dead feature. In case the feature under analysis is dead, explanations are provided; otherwise an empty 127 CHAPTER 9. A CATALOGUE OF ANALYSIS OPERATIONS set of explanations is given. The definition of this operation results as follows: Set<Set<Relationship >> detectAndExplainDead(SFM inputSfm ,GenericFeature f) { Set<Configuration > configSet = new HashSet <Configuration >(); Set<Set<Relationship >> explanations = new HashSet <Set<Relationship >>(); configSet.add( new ChosenElementConstraint (f,new SelectedState()) ); SFM resetSfm = reset(inputSfm); SFM configuredSfm = setAutoDecisions(resetSfm ,configSet); if (!valid(configuredSfm)) { explanations = whyNotRels(configuredSfm); } return explanations; } 9.6 SUMMARY The proposal of a set of basic and model edition operations has allowed the definition of a wide and extensible catalogue of operations relying on their composition capabilities. We have proposed a reinterpretation of the most used AAFM operations as AASFM operations as an example of the extensibility of our proposal. There exists an important parallelism between AAFM and AASFM. Most of the results obtained in this dissertation are applicable to the AAFM. We have obtained important conclusions for the explanatory analysis. Thus, four out of the eleven explanatory operations in the catalogue in [85], the ’why? questions, have been demonstrated to make no sense from the analysis point of view. Besides remaining operations have been defined as compound explanatory operations that use scenarios to perform the analysis. It is the scenarios that establish a connection between query and explanatory operations that was merely intuited in the original catalogue but now it is clearly stated. The definition of a basic set of analysis operations will allow the implementation of analysis tools for the AASFM that simply propose an implementation for these subset of operations. It simplifies considerably the development effort of AASFM tools. In the next Chapter we propose a proof of concept to verify the ideas presented in this dissertation and to demonstrate the feasibility of our aproach. 128 VERIFICATION OF RESULTS PART III 10 REFERENCE IMPLEMENTATION 131 I do not think there is any thrill that can go through the human heart like that felt by the inventor as he sees some creation of the brain unfolding to success... such emotions make a man forget food, sleep, friends, love, everything. Nikola Tesla (1856–1943), physicist, mathematician, inventor, and electrical engineer The objective of this Chapter is the verification showing some of the results presented in this dissertation. For that sake, we present in Section §10.1 the concept of industryready products and how the verification process play a key role in their construction. Section §10.2 presents an application of these concepts to build FAMA FW, a tool for the AAFM whose analysis capabilities and verification processes have inspired the construction of STEAm. STEAm is a prototype for the AASFM that is described in Section §10.3. It relies on a MDE architecture to implement the results in this dissertation. The verification process that has been applied to STEAm is described in Section §10.4. It has helped to detect errors in our results and in the implementation itself, increasing the confidence in an error-free proposal. Last, a discussion of the conclusions that we have obtained through the construction of FAMA FW and STEAm is shown in Section §10.5. CHAPTER 10. REFERENCE IMPLEMENTATION 10.1 VERIFICATION,VALIDATION AND INDUSTRY-READY TOOLS Bulilding software tools helps on verifying the research results and serves as a means of validation. With tools we demonstrate the technical feasibility of paper results. Verification is a process which objective is the detection of inconsistencies between the implementation and the specification. Those inconsistencies can arise due to implementation errors or errors in the specifications. Thus, verification contributes to repairing errors to produce error-free software. When a tool is verified, it is also important to analyse its complexity and performance. A performance analysis checks that an implementation complexity fits into the theoretical complexity. It helps to determine how a tool scales for different scenarios. With verification and performance analysis, our tools are prepared to be validated in real-world scenarios. At that point, the intervention of third-parties such as research institutions and the industry is necessary. Prototypes are commonly used to take research results to the industry. However, they are far from what the industry expects and more mature software tools are needed to shorten the distance between research and exploitation worlds. The cost and effort of developing tools is very large and they often cannot be assumed by the academy. Although verification and performance analysis improve the perception of a quality product, there still exist a gap that must be covered. So we need to take prototype to a further step that we call industry-ready tools. An industry-ready tool must have three desirable characteristics: • Adaptability: industry-ready tools must target as many third-parties as possible so they must be as customisable as possible to fit into the different business needs. • Maintainability: the industry presents a constant source of research problems. Academia provides solutions to these problems which are incorporated into tools. The academia must have the human and technical resources to keep this wheel spinning, which must in turn be supported by the industry. Industry-ready tools must allow the fastest and cheapest dissemination of research results. • Reliability: prototypes may contain errors. To incorporate a prototype into an industrial product, it must be verified. We define testing plans to increase the trust in tools reliability. Moreover, a tool is verified by the use itself. If they detect an error, flexible architectures permit to quickly repair and deliver tool updates. 132 10.2. FAMA FRAMEWORK Industry-ready products are better prepared to reach the industry than a prototype, since the quality of the software is better and nearer to the quality of a commercial product. Once the gap is saved, the intervention of the industry in our validation process contributes to measure the complexity that our tool would engage with realworld scenarios. Software tools are our main means of dissemination to the industry, which helps the industry on understanding our research and helps us on capturing fundings and obtaining feedback to focus future research. But how are we able to satisfy the three main characteristics of an industry-ready product? Architectures define the adaptability and maintainability of tools. We invest an important effort in defining flexible and customisable architectures to support both requirements. On the other hand, verification improves the reliability of an industryready tool. During the development of this dissertation, we have built an industry-ready tool that has supported our research in SPLs along the last 6 years: FAMA Framework. In Section §10.2 we present how its architecture provides for the maintainability and adaptability required for industry-ready products. The definition of the AASFM as a new paradigm in the SPL world, forces us to revise all the infrastructure that is defined for FAMA Framework. We have found some limitations in FAMA Framework so that the appearance of the AASFM affords us an opportunity to define a new tool whose architecture supports both the AASFM and the AAFM. To date, we have built a prototype that we call STEAm that is described in detail in Section §10.3. It is has been built using a transformational approach very similar to the rationale followed in this dissertation. We have followed a verification process to increase the confidence in the reliability of both tools, which is described in Section §10.4. The results obtained with STEAm arises some conclusions and opens new paths to explore in the future that are discussed in Section §10.5. 10.2 FAMA FRAMEWORK FeAture Model Analyser Framework (FAMA FW) [90] is a flexible Java tool for the AAFM. FAMA FW is an open-source product and is publicly available at www.isa.us. es/fama since 2007 under LGPL v3 License [49]. FAMA FW transforms a FM into a suitable logical representation or reasoner that is used to perform the AAFM. FAMA FW is a two-sided tool. For FM analysers it is a Java library to perform the AAFM; for researchers it is a framework where research results can be easily tested and delivered 133