FLAME: FAMA Formal Framework (v 1.0): Technical Report ISA–12–TR–02

FLAME: FAMA Formal Framework (v 1.0) Amador Durán, David Benavides, Sergio Segura, Pablo Trinidad and Antonio Ruiz-Cortés {amador,benavides,sergiosegura,ptrinidad,aruiz}@us.es Applied Software Engineering Research Group University of Seville, Spain March 2012 Technical Report ISA–12–TR–02 This report was prepared by the Applied Software Engineering Research Group (ISA) Department of computer languages and systems Av/ Reina Mercedes S/N, 41012 Seville, Spain http://www.isa.us.es/ Copyright c 2012 by ISA Research Group. Permission to reproduce this document and to prepare derivative works from this document for internal use is granted, provided the copyright and ’No Warranty’ statements are included with all reproductions and derivative works. NO WARRANTY THIS ISA RESEARCH GROUP MATERIAL IS FURNISHED ON AN ’AS-IS’ BASIS. ISA RESEARCH GROUP MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE OR MERCHANTIBILITY, EXCLUSIVITY, OR RESULTS OBTAINED FROM USE OF THE MATERIAL. Use of any trademarks in this report is not intended in any way to infringe on the rights of the trademark holder Support: This work has been partially supported by the European Commission (FEDER) and Spanish Government under CICYT project SETI (TIN2009-07366) and by the Andalusian Government under projects ISABEL (TIC-2533) and THEOS (TIC-5906). Contents 1 Introduction 3 2 Feature models background 5 3 Abstract foundation layer of the FLAME framework 7 3.1 SPLbasicconcepts ................................. 8 3.1.1 SPL basic concepts in Z . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.1.2 SPL basic concepts in Prolog . . . . . . . . . . . . . . . . . . . . . . . . 10 3.2 SPL basic analysis operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.2.1 Validityofaproduct ............................ 10 3.2.2 The set of all valid products . . . . . . . . . . . . . . . . . . . . . . . . 11 3.2.3 The number of all valid products . . . . . . . . . . . . . . . . . . . . . . 11 3.2.4 VoidSPL.................................. 12 3.2.5 Full and partial configurations . . . . . . . . . . . . . . . . . . . . . . . 12 3.2.6 Validity of a configuration . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.2.7 SPLfiltering ................................ 13 3.3 SPLrelations .................................... 14 3.3.1 SPL equivalence (refactoring) . . . . . . . . . . . . . . . . . . . . . . . 14 3.3.2 SPL generalization/specialization . . . . . . . . . . . . . . . . . . . . . 14 3.3.3 SPLarbitraryedit.............................. 15 3.4 SPL feature–related operations . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.4.1 Corefeatures................................ 16 3.4.2 Deadfeatures................................ 16 3.4.3 Variantfeatures............................... 17 3.4.4 Uniquefeatures............................... 17 i 3.4.5 Atomic sets of features . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.5 SPLnumericalindicators.............................. 20 3.5.1 Commonality factor of a configuration . . . . . . . . . . . . . . . . . . . 20 3.5.2 SPLvariability ............................... 20 3.5.3 SPLhomogeneity.............................. 21 4 Characteristic model layer of the FLAME framework 23 4.1 BFM as a characteristic model . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4.1.1 BFMmetamodel .............................. 23 4.1.2 Helper functions for BFM specification . . . . . . . . . . . . . . . . . . 27 4.2 Redefining the SPL type .............................. 28 4.3 Redefining the features–in–a–model function ................... 28 4.4 Redefining the is–instance–of relation....................... 29 5 Test–based validation of the FLAME framework 31 5.1 TheBeTTyframework ............................... 31 5.2 Test–based validation setup . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 5.2.1 Test cases generation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 5.2.2 Tests execution in Prolog . . . . . . . . . . . . . . . . . . . . . . . . . . 33 5.2.3 Tests execution in FaMa . . . . . . . . . . . . . . . . . . . . . . . . . . 33 5.3 Test–based validation results . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 5.3.1 Variant and dead features . . . . . . . . . . . . . . . . . . . . . . . . . . 35 5.3.2 Homogeneity and other numerical indicators . . . . . . . . . . . . . . . 35 5.3.3 Atomic sets semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 5.3.4 Prolog toolkit for sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 6 Related work 39 7 Conclusions and future work 41 A Prolog code of the reference implementation 47 A.1 Sample use of the FLAME framework . . . . . . . . . . . . . . . . . . . . . . . 47 A.2 Abstract foundation layer of FLAME . . . . . . . . . . . . . . . . . . . . . . . . 50 A.2.1 Abstract SPL checking . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ii A.2.2 Validityrelations.............................. 51 A.2.3 Validproducts ............................... 53 A.2.4 Filtering................................... 54 A.2.5 SPLrelations................................ 55 A.2.6 Feature–related operations . . . . . . . . . . . . . . . . . . . . . . . . . 56 A.2.7 Atomicsets................................. 58 A.2.8 Numerical indicators . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 A.3 Characteristic model layer of FLAME . . . . . . . . . . . . . . . . . . . . . . . 61 A.3.1 Helperfunctions .............................. 61 A.3.2 Specific BFM checking . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 A.3.3 Features–in–a–model function . . . . . . . . . . . . . . . . . . . . . . . 63 A.3.4 Is–instance–of relation . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 A.4 SettoolkitofFLAME................................ 67 iii iv Abstract Software product lines are rapidly gaining importance across different application domains. This software production paradigm focuses on the development of related software products using managed reusable assets instead of building each product from scratch. In the software product line community, feature models are recognized as one of the most used notation to represent variability in a product line and their automated analysis is a thriving research area. In a recent systematic literature review, some of the authors summarized the numerous contributions on the topic in the last 20 years and identified several challenges to be addressed. One of them was the lack of formal definitions of the analysis operations, for which most of the reviewed works only provided informal descriptions, leading to misunderstandings and implementation problems in tool development. To face this challenge, this article presents FLAME, a formal framework for the specification of analysis operations on feature models. Its main advantages lie in its formal semantics—described using the Z specification language—and in its high level of abstraction, which allows the reuse of the framework for the formalization of different feature model dialects or even for different variability notations. Furthermore, in order to assure the quality of the formal framework—and to provide a reference implementation for tool developers—, the Z specification has been animated in Prolog and automatically validated using 18,000 test cases automatically generated using metamorphic testing techniques. The results of the performed tests have helped not only to enhance the framework significantly but also to detect inconsistencies both in the previous informal definitions of the analysis operations and in current analysis tools, thus supporting the need for formal semantics. 1 2FLAME: FAMA Formal Framework ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 Chapter 1 Introduction Software product lines (SPLs) are used as a way of managing a set of distinctive software products in a concrete domain. Because of the ubiquity of software systems, the production of software is rapidly shifting to a mass–customization production paradigm where a common platform of features conforms the core of the product line and a set of product–specific features are tailored for specific domain needs. In outline, SPL engineering covers specific processes, methods, models, techniques and tools for supporting SPL adoption [Clements and Northrop, 2001; Pohl et al., 2005]. One of the important issues of this branch of software engineering is the availability of modeling facilities to express the inherent variability in a product line. To this end, Kang et al. [1990] proposed the so–called feature models, which are variability models that represent the set of products in an SPL in terms of their features and the relationships among them. As an essential support for SPL engineers, the automated analysis of feature models is defined by Benavides et al. [2010] as the computer–aided extraction of information from feature models by means of analysis operations, such as determining the number of products represented by a feature model, detecting anomalies, or comparing two models and classifying their relationship. Manual computation of such analysis operations depends on model semantics and is error–prone, tedious, and even infeasible with large–scale feature models. Some of the authors recently performed a systematic literature review on 20 years of automated analysis of feature models where 30 different analysis operations were identified [Benavides et al., 2010]. The review also identified several important challenges that were not covered by existing research. One of them was the lack of formal or rigorous description of analysis operations, which has sometimes led researchers and tool developers to misunderstandings. This article presents FLAME (Fama formaL frAMEwork), a formal framework for defining the semantics of feature model analysis operations using the standard, well–known Z formal specification language [Spivey, 1992; ISO, 2002]. FLAME is designed in two layers. The first one is the abstract foundation layer, which includes not only the definitions of necessary abstract concepts that can or must be redefined in the second layer, but also 18 notation–independent analysis operations. The second layer is the characteristic model layer, where the semantics of specific variability modeling notations are specified. In this article, the second layer is used to specify the semantics of an eclectic feature model dialect known as basic feature model [Benavides et al., 3 10 FLAME: FAMA Formal Framework 3.1.2 SPL basic concepts in Prolog Since most of the basic concepts and operations defined in the previous section are abstract, almost no Prolog code can be associated to the Z specification yet. Nevertheless, some of the followed conventions are: •Z sets are represented as Prolog lists, something common in the animation of Z specifications in Prolog [Hewitt et al., 1997; West and Eaglestone, 1992]. A small toolkit for set operations was developed for that purpose. The interested reader can consult the electronic appendix. •The SPL schema type is represented as the functor spl( F, M ), where Fis the SPL feature set and Mis the SPL characteristic model. Functors are the way of representing compound objects in Prolog, see [Clocksin and Mellish, 2003] for details. •The Conguration type is represented as the functor configuration( S, R ), where Sis the set of selected features and Ris the set of removed features. •The ≺≺ relation (is–an–instance–of ) is represented as the instance of( P, M ) predicate, where Pis a product and Mis a characteristic model. •The Φfunction is represented as the features( M, F ) predicate, where Mis a characteristic model and Fis the set of features used in the model. 3.2 SPL basic analysis operations Once the main abstract concepts have been defined, a number of basic operations can be properly specified, following the naming conventions used by Benavides et al. [2010]. 3.2.1 Validity of a product As previously mentioned, a product is valid for an SPL (denoted as ≺) if it is configured using the features in the SPL and is an instance of its characteristic model. As commented by Benavides et al. [2010], this operation may be helpful for SPL engineers to determine whether a given product is available in an SPL [White et al., 2010]. This can be expressed in Z as the following relation: ≺: Product ↔ SPL [Valid product] ∀ p : Product ; spl : SPL • p ≺ spl ⇔( p ⊆ spl . features ∧ p ≺≺ spl . model ) and transformed into the following Prolog predicate, which needs a backtrackable2version of the 2Abacktrackable predicate can succeed more than once, thus providing all their solutions. See [Clocksin and Mellish, 2003] for details. ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 3.2. SPL basic analysis operations 11 standard predicate subset in order to be used for computing the set of all valid products (see next subsection): valid( P, spl( F, M ) ) :- btrck_subset( P, F ), % backtrackable version of subset instance_of( P, M ). % abstract predicate 3.2.2 The set of all valid products Using the validity relation (≺), the set of all valid products of an SPL (denoted as Π), which may be helpful to identify new valid requirements combinations not considered in the initial scope of an SPL [Benavides et al., 2010], can be defined in Z as the following function: Π: SPL →F Product [Valid products of an SPL] ∀ spl : SPL • Π spl ={ p :F spl . features | p ≺ spl } and in Prolog as follows, using the standard predicate findall(X,P,L) [Clocksin and Mellish, 2003], which returns a list Lwith all values for Xthat satisfy the predicate P. products( spl( F, M ), PRDS ) :- findall( P, valid( P, spl( F, M ) ), PRDS ). 3.2.3 The number of all valid products Obviously, the number of valid products of an SPL (denoted as N), which provides information about the flexibility and complexity of the SPL [Benavides et al., 2010], is the cardinality— denoted in Z as # S —of its aforementioned set of products, i.e.: N: SPL →N[Number of valid products] ∀ spl : SPL • N spl = #Π spl that can be easily transformed into the following Prolog predicate: nop( spl( F, M ), NOP ) :- products( spl( F, M ), PRDS ), length( PRDS, NOP ). A. Durán et al. Seville, March 2011 12 FLAME: FAMA Formal Framework 3.2.4 Void SPL An SPL is considered to be void if there not exists any valid product for it. The automation of this operation is especially helpful when debugging large–scale feature models in which the manual detection of errors is recognized to be an error-prone and time-consuming task [Benavides et al., 2010]. This can be expressed in Z by means of the following predicate: void :P SPL [Void SPL] ∀ spl : SPL • void spl ⇔Π spl =∅ and in Prolog as the following predicate: void( spl( F, M ) ) :- products( spl( F, M ), [] ). 3.2.5 Full and partial configurations As commented by Benavides et al. [2010], a product can always be transformed into a full configuration where the selected features are the product features and the removed features are the features not present in the product. More specifically, a configuration is said to be full or partial with respect to a given SPL if it uses all the features in the SPL or not, i.e.: full , partial : Conguration × SPL [Full and partial relations] ∀ c : Conguration ; spl : SPL • full ( c , spl )⇔( selected c ∪ removed c ) = spl . features ∧ partial ( c , spl )⇔( selected c ∪ removed c )⊂ spl . features These relations can be transformed into the following Prolog predicates: full( configuration( S, R ), spl( F, M ) ) :- union( S, R, U ), equal_set( U, F ). partial( configuration( S, R ), spl( F, M ) ) :- union( S, R, U ), proper_subset( U, F ). 3.2.6 Validity of a configuration As pointed out by Benavides et al. [2010], this operation is useful to provide the user with feedback on the progress of a product configuration, i.e. an analysis tool implementing this operation could ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 3.2. SPL basic analysis operations 13 inform the user as soon as a configuration becomes invalid, thus saving time and effort. Similarly to product validity for an SPL, a product is said to be valid with respect to a given configuration if all the selected features of the configuration are present in the product but none of the removed ones are. This can be specified in Z as follows: C: Product ↔ Conguration [Valid product wrt a configuration] ∀ p : Product ; c : Conguration • p C c ⇔( selected c ⊆ p ∧ removed c ∩ p =∅) On the other hand, a configuration is considered as valid with respect to a given SPL if it is defined using known features and there exists at least one valid product in the SPL which is also valid for the given configuration. This validity concept can be specified as the following predicate in Z: ≺ c : Conguration ↔ SPL [Valid configuration wrt an SPL] ∀ c : Conguration ; spl : SPL • c ≺ c spl ⇔( selected c ∪ removed c )⊆ spl . features ∧ c ≺ c spl ⇔ ∃ p :Π spl • p C c and transformed into the following Prolog predicates: valid_p_c( P, configuration( S, R ) ) :- subset( S, P ), intersection( R, P, [] ). valid_c( configuration( S, R ), spl( F, M ) ) :- union( S, R, U ), subset( U, F ), products( spl( F, M ), PRDS ), member( P, PRDS ), valid_p_c( P, configuration( S, R ) ). 3.2.7 SPL filtering Afiltering or product selection of an SPL over a given configuration is the set of products of the SPL which are valid for the given configuration. As commented by Benavides et al. [2010], this operation may be helpful to assist users to select a desired product according to their key requirements. The specification of this operation in Z is as follows: Πσ: SPL × Conguration →F Product [SPL product selection] ∀ spl : SPL ; c : Conguration • Πσ( spl , c ) = { p :Π spl | p C c } A. Durán et al. Seville, March 2011 14 FLAME: FAMA Formal Framework Its corresponding Prolog predicate is the following, which requires the auxiliary predicate filtered in order to be used as the second argument of the findall predicate, in a similar way to the code in Section 3.2.2: filter( spl( F, M ), configuration( S, R ), RESULT ) :- products( spl( F, M ), PRDS ), findall( P, filtered( P, configuration( S, R ), PRDS ), RESULT ). filtered( P, configuration( S, R ), PRDS ) :- member( P, PRDS ), valid_p_c( P, configuration( S, R ) ). 3.3 SPL relations As most software engineering products, SPLs usually experiment evolving changes during their development. In [Benavides et al., 2010], a number of relations between evolving SPLs are described that can help SPL engineers during the SPL development process. 3.3.1 SPL equivalence (refactoring) An SPL is considered as a refactoring of another SPL if they both represent the same set of valid products, although their sets of features and characteristic models respectively do not have to be the same. In this case, they are also said to be equivalent. This can be expressed in Z as the following relation: ≡: SPL ↔ SPL [SPL equivalence] ∀ spl 1, spl 2: SPL • spl 1≡ spl 2⇔Π spl 1=Π spl 2 that can be directly translated into the following Prolog predicate: equivalent( spl( F1, M1 ), spl( F2, M2 ) ) :- products( spl( F1, M1 ), PRDS1 ), products( spl( F2, M2 ), PRDS2 ), equal_set( PRDS1, PRDS2 ). 3.3.2 SPL generalization/specialization An SPL is considered as a generalization of another SPL if its set of valid products is a superset of the products of the latter SPL. Inversely, an SPL is considered as a specialization of another SPL ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 3.3. SPL relations 15 if its set of valid products is a subset of the latter SPL. Both relations can be expressed in Z as the following: @: SPL ↔ SPL [SPL specialization] A: SPL ↔ SPL [SPL generalization] ∀ spl 1, spl 2: SPL • ( spl 1@ spl 2⇔Π spl 1⊂Π spl 2)∧ ( spl 2A spl 1⇔ spl 1@ spl 2)[inverse relations] The corresponding Prolog predicates are the following: specialization( spl( F1, M1 ), spl( F2, M2 ) ) :- products( spl( F1, M1 ), PRDS1 ), products( spl( F2, M2 ), PRDS2 ), proper_subset( PRDS1, PRDS2 ). generalization( spl( F1, M1 ), spl( F2, M2 ) ) :- specialization( spl( F2, M2 ), spl( F1, M1 ) ). 3.3.3 SPL arbitrary edit The last SPL evolving relation is the so–called arbitrary edit, which is the kind of relation between two SPL when they are neither equivalent nor a generalization or specialization of each other (see [Thüm et al., 2009] for details). This can be expressed in Z as the following relation: hhii : SPL ↔ SPL [SPL arbitrary edit] ∀ spl 1, spl 2: SPL • spl 1hhii spl 2⇔ ¬( spl 1≡ spl 2)∧[not refactoring] ¬( spl 1@ spl 2)∧[not specialization] ¬( spl 1A spl 2)[not generalization] that can be directly translated into the following Prolog predicate: arbitrary_edit( spl( F1, M1 ), spl( F2, M2 ) ) :- not( equivalent( spl( F1, M1 ), spl( F2, M2 ) ) ), not( specialization( spl( F1, M1 ), spl( F2, M2 ) ) ), not( generalization( spl( F1, M1 ), spl( F2, M2 ) ) ). A. Durán et al. Seville, March 2011 16 FLAME: FAMA Formal Framework 3.4 SPL feature–related operations The following operations provide the SPL engineer with relevant information about the presence or absence of the features of a given SPL in its set of valid products that can lead to changes in the corresponding characteristic model. 3.4.1 Core features The core features of an SPL (denoted as Φ C ) are those features that appear in all products of the SPL. As commented by Benavides et al. [2010], this operation is useful to determine which features should be developed in first place or to decide which features should be part of the core architecture of the SPL. This concept can be easily expressed in Z by means of the distributed intersection3(denoted as ∩) operator over the set of products: Φ C : SPL →F Feature [Core features] ∀ spl : SPL • Φ C spl =∩Π spl which is directly translated into the following Prolog predicate in which the version of the intersection predicate accepts also a set of sets (i.e. a list of lists) as its first argument: core_features( spl( F, M ), C ) :- products( spl( F, M ), PRDS ), intersection( PRDS, C ). 3.4.2 Dead features On the other hand, features that do not appear in any product of their SPL are said to be dead features, which are undesired inconsistencies whose detection is essential in SPL engineering. This can be expressed in Z by means of the set difference between the SPL features and the distributed union4(denoted as ∪) over the set of products, i.e. all the features appearing in at least one valid product. Φ D : SPL →F Feature [Dead features] ∀ spl : SPL • Φ D spl = spl . features \∪Π spl Again, its transformation into Prolog is straightforward: 3The distributed intersection (also known as generalized intersection) over A, being A a set of sets, is the set consisting of all objects belonging to every set in A. 4The distributed union (also known as generalized union) over A, being A a set of sets, is the set consisting of all objects belonging to any set in A. ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 3.4. SPL feature–related operations 17 dead_features( spl( F, M ), D ) :- products( spl( F, M ), PRDS ), union( PRDS, U ), subtract( F, U, D ). 3.4.3 Variant features The variant features of an SPL are those features that appear only in some products of the SPL, i.e. the features that are not part of the core features and are not dead features either, something that can be easily expressed in Z by means of the set difference between the SPL features and its core and dead features: Φ V : SPL →F Feature [Variant features] ∀ spl : SPL • Φ V spl = spl . features \Φ C spl \Φ D spl In a similar way to the two previous operations, the corresponding Prolog code is the following: variant_features( spl( F, M ), V ) :- core_features( spl( F, M ), C ), dead_features( spl( F, M ), D ), subtract( F, C, VAUX ), subtract( VAUX, D, V ). Notice that, as a result of the work described in this article, the definition of this operation differs from the presented in [Benavides et al., 2010]. See Section 5.3.1 for details. 3.4.4 Unique features Those features that appear in only one valid product are said to be unique, and are used to measure the homogeneity of an SPL (see section 3.5.3). This operation can be specified in Z using the unique quantifier: Φ U : SPL →F Feature [Unique features] ∀ spl : SPL • Φ U spl ={ f : spl . features | ∃1 p :Π spl • f ∈ p } and transformed in the following Prolog code, in which two auxiliary predicates, unique and contains, have been introduced in order to use the standard findall predicate: A. Durán et al. Seville, March 2011 18 FLAME: FAMA Formal Framework unique_features( spl( F, M ), RESULT ) :- products( spl( F, M ), PRDS ), findall( Fi, unique( Fi, F, PRDS ), RESULT ). unique( Fi, F, PRDS ) :- member( Fi, F ), findall( P, contains( P, Fi, PRDS ), RESULT ), length( RESULT, 1 ). contains( P, F, PRDS ) :- member( P, PRDS ), member( F, P ). 3.4.5 Atomic sets of features First mentioned in [Zhang et al., 2004a] but not formalized yet, the concept of the atomic sets of features of an SPL is relevant as an efficient preprocessing technique for SPL automated analysis [Benavides et al., 2010; Segura, 2008]. Informally, an atomic set is a group of features that can be treated as a unit because they are tightly coupled and always appear together in the SPL products. Atomic sets can be used to create a reduced version of the SPL characteristic model simply by replacing groups of features with the atomic set containing them [Benavides et al., 2010], thus increasing the efficiency of other SPL analysis operations. From a formal point of view, atomic sets are nonempty subsets of features such that for every product in an SPL, all their features appear together in the product or none of them appear at all, i.e. they are a subset or disjoint with respect to every product. There are many atomic sets for a given SPL, but the interesting ones are the maximal subsets which are not contained in any other atomic set and in which the features are grouped in the biggest groups. In order the make the formal specification of the atomic sets easier to understand, the set of all potential atomic sets (denoted as Φ0 A ) is defined first. This set contains all feature subsets with subset–or–disjoint semantics, including all subsets with only one feature as its only member: Φ0 A : SPL →F F1 Feature [Potential atomic sets] ∀ spl : SPL • Φ0 A spl ={ a 0:F1 spl . features | ∀ p :Π spl • a 0⊆ p ∨ a 0∩ p =∅} The corresponding Prolog code is the following, in which two auxiliary predicates potential atomic set and subset or disjoint have been introduced to make possible the use of the standard predicates findall and forall: potential_atomic_sets( spl( F, M ), POTATOMS ) :- products( spl( F, M ), PRDS ), findall( A0, potential_atomic_set( A0, F, PRDS ), POTATOMS ). ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 3.4. SPL feature–related operations 19 potential_atomic_set( A0, F, PRDS ) :- btrck_subset( A0, F ), % backtrackable version of subset A0 \= [], % atomic sets are nonempty forall( member( P, PRDS ), subset_or_disjoint( A0, P ) ). subset_or_disjoint( A, P ) :- subset( A, P ) ; intersection( A, P, [] ). Once Φ0 A is defined, the maximal set of atomic sets (denoted as Φ A ) are those atomic sets which are not included in any other atomic set. Although the Z notation does not include a maximal function, it can be easily defined as a generic relation as follows: [ X ] maximal :P X ↔P P X ∀ S i :P X ; S :P P X • maximal ( S i , S )⇔@ S j : S • S i ⊂ S j and as the following Prolog predicate, where the existential quantifier has been transformed into the universal quantifier using the forall predicate and the logical equivalence @ x • P ( x )≡ ∀ x • ¬ P ( x ): maximal( Si, S ) :- member( Si, S ), forall( member( Sj, S ), not( proper_subset( Si, Sj ) ) ). Now, having defined the maximal relation, Φ A can be specified as those potential atomic sets that are maximal, i.e.: Φ A : SPL →F F1 Feature [Atomic sets] ∀ spl : SPL • Φ A spl ={ a :Φ0 A spl | maximal ( a ,Φ0 A spl )} that can be easily transformed into the following Prolog code: atomic_sets( spl( F, M ), ATOMS ) :- potential_atomic_sets( spl( F, M ), POTATOMS ), findall( A, maximal( A, POTATOMS ), ATOMS ). Notice that the definition of this operation differs significatively from previous informal definitions provided by [Benavides et al., 2010], [Segura, 2008] and [Zhang et al., 2004b], which are feature–model dependent whereas the one provided in this article is much more abstract and independent from the notation used for the characteristic model of an SPL. More details are provided in Section 5.3.3. A. Durán et al. Seville, March 2011 26 FLAME: FAMA Formal Framework BFM ( feature κ( MobilePhone ,{ mandatory ( feature λ( Calls ) ), optional ( feature λ( GPS ) ), mandatory ( feature κ( Screen ),{ only one ({ feature λ( Basic ), feature λ( Colour ), feature λ( HighResolution ) }) }) optional ( feature κ( Media ),{ one or more ({ feature λ( Camera ), feature λ( MP 3) }) }) }), { excludes ( GPS , Basic ), requires ( Camera , HighResolution ) } ) and as Prolog functors as follows: bfm( k_feature( mobile_phone, [ mandatory( l_feature( calls ) ), optional( l_feature( gps ) ), mandatory( k_feature( screen, [ only_one( [ l_feature( basic ), l_feature( colour ), l_feature( high_resolution ) ] ) ] ) ), optional( k_feature( media, [ one_or_more( [ l_feature( camera ), l_feature( mp3 ) ] ) ])) ] ), [ excludes( gps, basic ), requires( camera, high_resolution ), ] ) ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 4.1. BFM as a characteristic model 27 4.1.2 Helper functions for BFM specification In order to make the specification easier to read, some helper functions can be defined over the previously defined BFM abstract syntax. The first ones are simply a pair of functions used to extract the feature tree, i.e. the root feature, and the set of CTCs from a given BFM: tree : Model → TreeFeature [Helper functions tree and ctc] ctc : Model →F CTC ∀ t : TreeFeature ; c :F CTC ; m : Model • tree BFM ( t , c ) = t ∧ ctc BFM ( t , c ) = c Another helper function is the children function, which returns the set of children TreeFeatures in a relationship. Its specification in Z is as follows: children : Relationship →F1 TreeFeature [Helper function children] ∀ t i : TreeFeature ; t :F2 TreeFeature • children mandatory ( t i ) = children optional ( t i ) = { t i } ∧ children one or more ( t ) = children only one ( t ) = t The last helper functions are F T and F R , which return the number of times a given feature appears in a TreeFeature and in a Relationship . Its specification in Z2is as follows: Fτ: Feature × TreeFeature →N [number of times a feature appears in a tree] F R : Feature × Relationship →N [number of times a feature appears in a relationship] ∀ f 1, f 2: Feature ; r :F Relationship • f 1= f 2⇒ Fτ( f 1, feature λ( f 2) ) = 1 ∧ Fτ( f 1, feature κ( f 2, r ) ) = 1 + X r i ∈ r F R ( f 1, r i ) ∀ f 1, f 2: Feature ; r :F Relationship • f 16= f 2⇒ Fτ( f 1, feature λ( f 2) ) = 0 ∧ Fτ( f 1, feature κ( f 2, r ) ) = X r i ∈ r F R ( f 1, r i ) ∀ f : Feature ; r : Relationship • F R ( f , r ) = X t i ∈ children r F T ( f , t i ) 2The use of the summation symbol (Σ) over the elements of a set is not explicitly defined in Z. Since its alternatives are complex, we have decided to use it for the sake of clarity. A. Durán et al. Seville, March 2011 28 FLAME: FAMA Formal Framework 4.2 Redefining the SPL type As commented at the end of section 3.1.1, the abstract SPL schema type can be augmented with additional constraints related to the nature of features or models. In the case of BFM, its feature models are structurally trees, which implies that a feature cannot appear more than once in a model. Using the previously defined Fτfunction, this constraint can be added to the original SPL schema type resulting in the following: SPL model : Model [SPL using BFM] features :F1 Feature Φ model = features ∀ f : features • Fτ( f , tree model )=1 [All features appear only once] 4.3 Redefining the features–in–a–model function Having redefined the Model and the SPL types for using BFM, the Φfunction must also be redefined in order to make concrete the abstract definitions in the AFL. The first step is to specify that the features used in a BFM are the features used either in their tree feature model or in their CTCs, i.e.: Φ: Model →F Feature [Redefinition of Φfor BFM] ∀ m : Model • Φ m =Φτ tree m ∪∪{ ctc i : ctc m •Φχ ctc i } The second step is to specify the Φfunctions for determining the features in a BFM tree (denoted as Φτ) and in a Relationship (denoted as Φ R ). The Z specification of both functions is the following: Φτ: TreeFeature →F Feature [Features in a BFM tree] Φ R : Relationship →F Feature [Features in a BFM relationship] ∀ f : Feature ; r i : Relationship ; r :F Relationship • Φτ feature λ( f ) = { f } ∧ Φτ feature κ( f , r ) = { f } ∪ ∪{ r i : r •Φ R r i } ∧ Φ R r i =∪{ t i : children r i •Φτ t i } Finally, the specification of the function returning the features in a CTC (denoted as Φχ) is the following: ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 4.4. Redefining the is–instance–of relation 29 Φχ: CTC →F Feature [Features in a CTC] ∀ f 1, f 2: Feature • Φχ requires ( f 1, f 2) = Φχ excludes ( f 1, f 2) = { f 1}∪{ f 2} 4.4 Redefining the is–instance–of relation The redefinition of the ≺≺ relation is structurally very similar to the redefinition of the Φfunction described in the previous section. In this case, the first step is to specify whether a product is an instance of an SPL using a BFM as its characteristic model. Basically, a product is an instance of such an SPL if it is an instance of its feature tree and of all their CTCs, i.e. ≺≺ : Product ↔ Model [Redefinition of ≺≺ for BFM] ∀ p : Product ; m : Model • p ≺≺ m ⇔( p ≺≺τ tree m ∧ ∀ ctc i : ctc m • p ≺≺χ ctc i ) The second step is the specification of the ≺≺ relation for BFM trees (denoted as ≺≺τ) and for its relationships (denoted as ≺≺ R ). In the former relation, a product is an instance of a leaf feature if it includes the leaf feature, whereas is an instance of a compound feature if it includes the parent feature and is an instance of all its children relationships, i.e.: ≺≺τ: Product ↔ TreeFeature [Instance of a BFM tree] ∀ p : Product ; f : Feature ; r :F Relationship • p ≺≺τ feature λ( f )⇔ f ∈ p ∧ p ≺≺τ feature κ( f , r )⇔( f ∈ p ∧ ∀ r i : r • p ≺≺ R r i ) With respect to relationships, four cases have to be considered. In the case of mandatory subtrees, a product is an instance if is an instance of the corresponding subtree; in the case of optional subtrees, a product is an instance if is an instance of the subtree or the set of features of the product and of the subtree are disjoint; in the case of one or more and only one subtrees, all their branches are considered as optional, except that the product must be an instance of at least, one of them (and only one in the only one case). ≺≺ R : Product ↔ Relationship [Instance of a BFM relationship] ∀ p : Product ; f : Feature ; t i : TreeFeature ; t :F2 TreeFeature • p ≺≺ R mandatory ( t i )⇔ p ≺≺τ t i ∧ p ≺≺ R optional ( t i )⇔( p ≺≺τ t i ∨ p ∩Φτ t i =∅)∧ p ≺≺ R one or more ( t )⇔ (∀ t j : t • p ≺≺ R optional ( t j )∧ ∃ t k : t • p ≺≺τ t k )∧ p ≺≺ R only one ( m )⇔ (∀ t j : t • p ≺≺ R optional ( t j )∧ ∃1 t k : t • p ≺≺τ t k ) A. Durán et al. Seville, March 2011 30 FLAME: FAMA Formal Framework Finally, the ≺≺ predicate corresponding to CTCs (denoted as ≺≺χ) is the following, where the usual semantics of logic implication and mutual exclusion are specified: ≺≺χ: Product ↔ CTC [Instance of a BFM CTC] ∀ p : Product ; f 1, f 2: Feature • p ≺≺χ requires ( f 1, f 2)⇔( f 16∈ p ∨ f 2∈ p )∧ p ≺≺χ excludes ( f 1, f 2)⇔( f 16∈ p ∨ f 26∈ p ) Once the abstract type Model and the operations Φ(features–in–a–model) and ≺≺ (is–an– instance–of ) have been made concrete for the BFM notation in the CML of FLAME, all the analysis operations defined in the AFL (see Section 3) can be used without modification. Apart of this high level of reuse, BFM–specific operations like those commented in [Benavides et al., 2010] can also be defined in the CML of FLAME. ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 Chapter 5 Test–based validation of the FLAME framework In order to validate the FLAME framework, its reference implementation, i.e. the Prolog animation of the formal specification, was tested using a fully automated approach following the IX commandment of formal methods proposed by Bowen and Hinchey [2012], which stresses the importance of testing when using formal methods. The goal of the test–based validation was twofold: (1) detecting faults in the reference implementation i.e., mismatches between the formal specification and its animation; and (2) detecting flaws in the Z specification, i.e. mismatches between what was intended to be specified and the actual specification. In the following sections the testing framework used, the validation setup and the main results obtained during the validation of the FLAME framework are presented. 5.1 The BeTTy framework The test–based validation of the FLAME framework was performed using the automated approach presented by some of the authors in [Segura et al., 2011] and integrated into the open–source Java framework BeTTy [Segura et al., 2012], which enables the automated generation of test cases for the automated analysis of feature models. In BeTTy, a test case is composed of a set of inputs (a feature model and some other optional parameters) and an expected output of the analysis operation under test. The key idea behind BeTTy is that the result of most analysis operations on feature models can be derived by inspecting theirs set of valid products adequately. Figure 5.1 depicts an example of how BeTTy works. The process starts with a trivial input feature model and its set of valid products. The model is then extended progressively by adding random feature relationships and cross–tree–constraints. The set of products is also updated at each step by using the so–called metamorphic relationships [Segura et al., 2011], i.e. the relationships between incremental changes in a feature model and their effects on the corresponding set of valid products. In Figure 5.1, the new feature relationships and cross– tree–constraints are depicted in gray, whereas the changes in the set of valid products caused by 31 32 FLAME: FAMA Formal Framework their addition are depicted in bold face. Figure 5.1: An example of random feature model generation using metamorphic relationships Once a feature model with the desired properties is created, it is used as nontrivial input for the tests and its set of products is automatically inspected to compute the expected output of the analysis operations under tests. As an example, consider the model and set of products generated in Figure 5.1. The expected output of most of the analysis operations over the model can be obtained by simply answering simple questions such as: •Is the model void? No, the set of products is not empty. •IsP={A,C,F } a valid product? Yes. It is included in the set of products. •How many different products represent the model? There are 4 valid products. •What is the variability of the model? There are 4 valid products and 7 features, so the variability is 4/(27−1) = 0.031 = 3.1% •What is the commonality of feature B?Feature Bis included in 3 out of the 4 products of the set. Therefore its commonality is 75% •Does the model contain any dead features? Yes. Feature Gis dead since it is not included in any of the products represented by the model. The BeTTy framework has not only proved to be effective in detecting faults in actual tools for the automated analysis of feature models such as the FaMa framework [ISA Research Group, 2012] and SPLOT [Mendonca et al., 2009], but it has also shown to be much more effective than manually–designed test cases for the analysis of feature models, as described in [Segura et al., 2011]. ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 5.2. Test–based validation setup 33 5.2 Test–based validation setup The formal specification and the reference implementation were developed in parallel, so it was possible to manually develop and run small tests as long as the analysis operations were specified and animated in Prolog. Although these tests were not developed systematically, they were quite useful for illustrating discussions among the authors and for detecting some problems related with numerical indicators (see Section 5.3.2). Once the reference implementation was finished, the systematic test–based validation was performed in a three–step process, each of which is described below. 5.2.1 Test cases generation For each analysis operation, 1,000 test cases were automatically generated using BeTTy. Each test case was composed of a random input feature model and an expected output. In the case of operations receiving other inputs apart from a feature model (e.g. valid product, which takes a product to be checked), these inputs were generated using a partition equivalence strategy [Beizer, 1990; Myers and Sandler, 2004], e.g. generating valid and non–valid products with equal probability. For efficiency, feature models were generated with 10 features and 0–30% of cross–tree constraints with respect to the number of features. Previous works in testing by Segura et al. [2011] have shown that feature models with 10 features are complex enough to reveal faults effectively. 5.2.2 Tests execution in Prolog Once the test cases for each operation were generated, they were translated into Prolog and integrated with the unit test framework developed by Wielemaker [2012]. An example of such integration for the number of valid products operation is shown in Figure 5.2. Once prepared, the tests were executed against the reference implementation and the results were checked. Whenever a fault was detected, the reference implementation and/or the formal specification were fixed and the tests were executed again. This process was repeated until obtaining a 100% of successful tests for all the analysis operations. 5.2.3 Tests execution in FaMa Finally, all the generated test cases were executed against the FaMa framework [ISA Research Group, 2012], a mature framework previously developed by some of the authors based on a informal description of the analysis operations and already known by the SPL community [Trinidad et al., 2008]. Using the Prolog animation of the formal specification in FLAME as a reference implementation, the FaMa framework was checked in order to prove their correctness and detect possible deviations from expected results. Due to the maturity of the FaMa framework, this step was also considered as a double–check for the reference implementation. A. Durán et al. Seville, March 2011 34 FLAME: FAMA Formal Framework % SPL instances containing feature models generated by BeTTy spl_db( spl_001, spl( ... ) ). ... spl_db( spl_999, spl( ... ) ). % Input data and expected result generated by BeTTy test_data( spl_001, number_of_products, [], 12 ). ... test_data( spl_999, number_of_products, [], 26 ). % Test cases :- begin_tests( number_of_products ). % A test predicate for each test case that... % 1. Retrieves an SPL instance % 2. Retrieves input data and expected results % 3. Performs the analysis operation % 4. Compares the actual and expected results test( number_of_products_001 ) :- spl_db( spl_001, SPL ), test_data( spl_001, number_of_products, [], EXPECTED ), nop( SPL, ACTUAL ), ACTUAL =:= EXPECTED. test( number_of_products_002 ) :- ... :- end_tests( number_of_products ). Figure 5.2: Structure of a Prolog unitary test for the validation of the nop (number of products) operation In order to avoid biased results, the systematic test–based validation process was performed by a group of authors completely independent from those in charge of the development of the formal specification and the reference implementation. 5.3 Test–based validation results The test–based validation of the FLAME framework revealed several flaws, especially in the previous informal definitions of some of the analysis operations in [Benavides et al., 2010]. A description of these faults and how they were fixed are next presented. ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 5.3. Test–based validation results 35 5.3.1 Variant and dead features In [Benavides et al., 2010], variant features are defined as “those [features] that do not appear in all the products of an SPL”. Taking this definition as a reference, the variant features (Φ V ) of an SPL were initially specified as all the features of an SPL except those that appear in all the products, i.e. all the features except the core features (Φ C ): Φ V spl = spl . features \Φ C spl When the test–based validation was performed, it revealed that the previous definition considered dead features (i.e. those that do not appear in any product) as variant, even in the case of void SPLs, where all their features are dead. After a discussion among the authors, the agreement on dead features not being variant was unanimous, so the informal definition in [Benavides et al., 2010] was enhanced to explicitly declare that variant features cannot be dead and both the formal specification and its corresponding reference implementation were corrected (see Section 3.4.3 for the final definition and specification). This new definition of variant features implies that the core, variant and dead features are a partition of the feature set of an SPL, i.e. they are disjoint to each other and their union is the feature set: ∀ spl : SPL • Φ C spl ∩Φ V spl =∅∧ Φ C spl ∩Φ D spl =∅∧ Φ V spl ∩Φ D spl =∅∧ spl . features =Φ C spl ∪Φ V spl ∪Φ D spl Or more succinctly: ∀ spl : SPL • hΦ C spl ,Φ V spl ,Φ D spl ipartitions spl . features 5.3.2 Homogeneity and other numerical indicators During the test–based validation, a problem with the definition of the homogeneity operation was detected. This operation was described in [Benavides et al., 2010] as: H spl = 1 −#(Φ U spl ) N spl and the test–based validation made evident that if an SPL is void, its homogeneity cannot be computed because it includes a division by zero. After reviewing the original definition of the operation by Fernandez-Amorós et al. [2009], it was clear that there was a mistake in the definition of homogeneity in [Benavides et al., 2010], so the formal specification and reference implementation of this operation in the FLAME framework was fixed in order to be compliant with their authors. A. Durán et al. Seville, March 2011 42 FLAME: FAMA Formal Framework arrange other elements but with no associated semantics, has been recognized as an important challenge by Thüm et al. [2011] and Roos-Frantz [2012]. The study of how to include abstract features in FLAME leads to another appealing future work. Exploring other alternatives for specification animation seems also interesting, being Alloy and description logic the more likely candidates. The parallel development of the Z specification and its animation in Prolog—and the positive feedback between the two of them—enhanced them significantly. Using other implementation platforms could bring new synergies and increase the quality of the FLAME framework in the future. Acknowledgments The authors would like to thank José A. Galindo for his help implementing the BeTTy module for generating the tests in Prolog. ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 Bibliography BACHMEYER, R. AND DELUGACH, H. 2007. A conceptual graph approach to feature modeling. In Conceptual Structures: Knowledge Architectures for Smart Applications, 15th International Conference on Conceptual Structures, ICCS. 179–191. BATORY, D. 2005. Feature models, grammars, and propositional formulas. In Software Product Lines Conference. Lecture Notes in Computer Sciences Series, vol. 3714. Springer–Verlag, 7– 20. BEIZER, B. 1990. Software testing techniques (2nd ed.). Van Nostrand Reinhold Co., New York, NY, USA. BENAVIDES, D. 2007. On the automated analysis of software product lines using feature models. Ph.D. thesis, Dpto. Lenguajes y Sistemas Informáticos, ETS. Ingeniería Informática, Universidad de Sevilla. BENAVIDES, D., RUIZ-CORTÉS, A., AND TRINIDAD, P. 2005. Automated reasoning on feature models. In Advanced Information Systems Engineering: 17th International Conference, CAiSE. Lecture Notes in Computer Sciences Series, vol. 3520. Springer–Verlag, 491–503. BENAVIDES, D., SEGURA, S., AND RUIZ-CORTÉS, A. 2010. Automated Analysis of Feature Models 20 years Later: a Literature Review. Information Systems 35, 6. BOWEN, J. P. AND HINCHEY, M. 2012. Ten commandments of formal methods... ten years on. In Conquering Complexity, M. Hinchey and L. Coyle, Eds. Springer London, 237–251. CLEMENTS, P. AND NORTHROP, L. 2001. Software Product Lines: Practices and Patterns. SEI Series in Software Engineering. Addison–Wesley. CLOCKSIN, W. F. AND MELLISH, C. S. 2003. Programming in Prolog: Using the ISO Standard 5 th Ed. Springer–Verlag. CZARNECKI, K., HELSEN, S., AND EISENECKER, U. 2005. Formalizing cardinality-based feature models and their specialization. Software Process: Improvement and Practice 10, 1, 7–29. FAN, S. AND ZHANG, N. 2006. Feature model based on description logics. In Knowledge-Based Intelligent Information and Engineering Systems, 10th International Conference, KES, Part II. Lecture Notes in Computer Sciences Series, vol. 4252. Springer–Verlag. 43 44 FLAME: FAMA Formal Framework FERNANDEZ-AMORÓS, D., HERADIO, R., AND CERRADA, J. 2009. Inferring information from feature diagrams to product line economic models. In Proceedings of the Sofware Product Line Conference (SPLC’09). GHEYI, R., MASSONI, T., AND BORBA, P. 2006. A theory for feature models in alloy. In Proceedings of the ACM SIGSOFY First Alloy Workshop. Portland, United States, 71–80. GHEYI, R., MASSONI, T., AND BORBA, P. 2008. Algebraic laws for feature models. Journal of Universal Computer Science 14, 21, 3573–3591. HEWITT, M., O’HALLORAN, C., AND SENNETT, C. 1997. Experiences with PiZA, an Animator for Z. In ZUM’97: The Z Formal Specification Notation, J. Bowen, M. Hinchey, and D. Till, Eds. LCNS Series, vol. 1212. Springer–Verlag, 35–51. ISA RESEARCH GROUP. Accessed February 2012. FaMa Tool Suite. Available at http://www.isa.us.es/fama/. ISO. 2002. Information technology – z formal specification notation – syntax, type system and semantics. iso/iec 13568:2002. JACKSON, D. 2012. Software Abstractions: Logic, Language, and Analysis Revised Ed. MIT Press. KANG, K., COHEN, S., HESS, J., NOVAK, W., AND PETERSON, S. 1990. Feature–Oriented Domain Analysis (FODA) Feasibility Study. Tech. Rep. CMU/SEI-90-TR-21, Software Engineering Institute, Carnegie Mellon University. Nov. KING, P. 1990. Printing Z and Object–Z L A T EX documents. Tech. rep., University of Queensland. MENDONCA, M., BRANCO, M., AND COWAN, D. 2009. S.p.l.o.t. - software product lines online tools. In Companion to the 24th ACM SIGPLAN International Conference on Object–Oriented Programming, Systems, Languages, and Applications (OOPSLA 2009). Orlando, USA. MENDONÇA, M., WASOWSKI, A., CZARNECKI, K., AND COWAN, D. 2008. Efficient compilation techniques for large scale feature models. In Generative Programming and Component Engineering, 7th International Conference, GPCE , Proceedings. 13–22. MYERS, G. J. AND SANDLER, C. 2004. The Art of Software Testing. John Wiley & Sons. POHL, K., BÖCKLE, G., , AND VAN DER LINDEN, F. 2005. Software Product Line Engineering: Foundations, Principles, and Techniques. Springer–Verlag. ROOS-FRANTZ, F. 2012. Automated analysis of software product lines with orthogonal variability models. Ph.D. thesis, Dpto. Lenguajes y Sistemas Informáticos, ETS. Ingeniería Informática, Universidad de Sevilla. ROOS-FRANTZ, F., BENAVIDES, D., RUIZ-CORTÉS, A., HEUER, A., AND LAUENROTH, K. 2011. Quality-aware analysis in product line engineering with the orthogonal variability model. Software Quality Journal, 1–47. ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 Bibliography 45 SAALTINK, M. 1997. The z/eves system. In ZUM ’97: The Z Formal Specification Notation, J. Bowen, M. Hinchey, and D. Till, Eds. Lecture Notes in Computer Science Series, vol. 1212. Springer Berlin / Heidelberg, 72–85. SCHOBBENS, P., P. HEYMANS, J. T., AND BONTEMPS, Y. 2007. Generic semantics of feature diagrams. Computer Networks 51, 2, 456–479. SEGURA, S. 2008. Automated analysis of feature models using atomic sets. In First Workshop on Analyses of Software Product Lines (ASPL 2008). SPLC’08. Limerick, Ireland, 201–207. SEGURA, S., BENAVIDES, D., AND RUIZ-CORTÉS, A. 2011. Functional Testing of Feature Model Analysis Tools: A Test Suite. IET Software 5, 1. SEGURA, S., GALINDO, J., BENAVIDES, D., PAREJO, J., AND RUIZ-CORTÉS, A. 2012. Betty: Benchmarking and testing on the automated analysis of feature models. In Sixth International Workshop on Variability Modelling of Software–intensive Systems (VaMoS’12). Leipzig, Germany, 63–71. The BeTTy framework is available at http://www.isa.us.es/betty. SEGURA, S., HIERONS, R. M., BENAVIDES, D., AND RUIZ-CORTÉS, A. 2011. Automated Metamorphic Testing on the Analyses of Feature Models. Information and Software Technology 53, 3. SPIVEY, J. M. 1992. The Z Notation: A Reference Manual 2 nd Ed. Prentice–Hall. SUN, J., ZHANG, H., LI, Y., AND WANG, H. 2005. Formal semantics and verification for feature modeling. In Proceedings of the 10th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS). THÜM, T., BATORY, D., AND KÄSTNER, C. 2009. Reasoning about edits to feature models. In International Conference on Software Engineering. 254–264. THÜM, T., KASTNER, C., ERDWEG, S., AND SIEGMUND, N. 2011. Abstract features in feature modeling. In Software Product Line Conference (SPLC’11), 2011 15th International. IEEE, 191–200. TRINIDAD, P., BENAVIDES, D., DURÁN, A., RUIZ-CORTÉS, A., AND TORO, M. 2008. Automated error analysis for the agilization of feature modeling. Journal of Systems and Software 81, 6, 883–896. TRINIDAD, P., BENAVIDES, D., RUIZ-CORTÉS, A., SEGURA, S., AND JIMENEZ, A. 2008. Fama framework. In 12th Intl. Software Product Line Conference - Tool Demonstrations. IEEE CS, 359 –359. VON DER MASSEN, T. AND LITCHER, H. 2005. Determining the variation degree of feature models. In Software Product Lines Conference. Lecture Notes in Computer Sciences Series, vol. 3714. Springer–Verlag, 82–88. WEST, M. M. AND EAGLESTONE, B. M. 1992. Software Development: Two Approaches to Animation of Z Specifications using Prolog. Software Engineering Journal 7, 4. A. Durán et al. Seville, March 2011 46 FLAME: FAMA Formal Framework WHITE, J., BENAVIDES, D., SCHMIDT, D., TRINIDAD, P., DOUGHERTY, B., AND RUIZCORTÉS, A. 2010. Automated diagnosis of feature model configurations. Journal of Systems and Software 83, 7, 1094 – 1107. WHITE, J., DOUGHTERY, B., SCHMIDT, D., AND BENAVIDES, D. 2009. Automated reasoning for multi-step software product-line configuration problems. In Proceedings of the Sofware Product Line Conference. 11–20. WIELEMAKER, J. Accessed February 2012. Prolog unit tests. Available at http://www.swi-prolog.org/pldoc/package/plunit.html. WOODCOCK, J. AND DAVIES, J. 1996. Using Z: Specification, Refinement, and Proof. Prentice– Hall. ZHANG, W., YAN, H., ZHAO, H., AND JIN, Z. 2008. A bdd–based approach to verifying cloneenabled feature models’ constraints and customization. In High Confidence Software Reuse in Large Systems, 10th International Conference on Software Reuse, ICSR, Proceedings. Lecture Notes in Computer Sciences Series, vol. 5030. Springer–Verlag, 186–199. ZHANG, W., ZHAO, H., AND MEI, H. 2004a. A Propositional Logic-Based Method for Verification of Feature Models. In Formal Methods and Software Engineering, J. Davies, W. Schulte, and M. Barnett, Eds. LCNS Series, vol. 3308. Springer–Verlag, 115–130. ZHANG, W., ZHAO, H., AND MEI, H. 2004b. A propositional logic-based method for verification of feature models. In ICFEM 2004, J. Davies, Ed. Lecture Notes in Computer Sciences Series, vol. 3308. Springer–Verlag, 115–130. ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 Appendix A Prolog code of the reference implementation This appendix contains the Prolog code corresponding to the reference implementation of the FLAME framework, which can also be downloaded from http://www.isa.us.es/flame. The structure of this appendix is as follows: Section A.1 shows a sample use of the FLAME framework; Sections A.2 and A.3 include the Prolog code corresponding to the abstract foundation layer (AFL) and the implementation of the semantics of the basic feature model (BFM) notation as a particular case of the characteristic model layer (CML) of the FLAME framework; Finally, Section A.4 includes the code corresponding to the set toolkit used in the FLAME framework. A.1 Sample use of the FLAME framework % ----------------------------------------------------------------------------- % File: FLAME_samples.pl % Content: Sample uses of the FLAME framework % Author: Amador Durán Toro % Date: 05/03/2012 % ----------------------------------------------------------------------------- :- consult( ’afl/afl.pl’ ). % FLAME AFL layer :- consult( ’cml/bfm/bfm.pl’ ). % FLAME CML layer % SPL instances: spl_db( ID, spl( Features, Model ) ) spl_db( bad_spl, spl( [ f1, f2, f3 ], bfm( k_feature( f1, [ mandatory( l_feature( f2 ) ), mandatory( l_feature( f4 ) ), optional( k_feature( f2, [ only_one( [ l_feature( f1 ), l_feature( f5 ), l_feature( f4 ) ] ) ])) ] ), [] % no cross-tree constraints 47 48 FLAME: FAMA Formal Framework ) ) ). spl_db( survey_spl, spl( [ mobile_phone, calls, gps, screen, basic, colour, high_resolution, media, camera, mp3 ], bfm( k_feature( mobile_phone, [ mandatory( l_feature( calls ) ), optional( l_feature( gps ) ), mandatory( k_feature( screen, [ only_one( [ l_feature( basic ), l_feature( colour ), l_feature( high_resolution ) ] ) ] ) ), optional( k_feature( media, [ one_or_more( [ l_feature( camera ), l_feature( mp3 ) ] ) ])) ] ), [ excludes( gps, basic ), requires( camera, high_resolution ), requires( mp3, mp3 ) ] ) ) ). spl_db( atomic_sets_spl, spl( [ a, b, c, d, e, f, g ], bfm( k_feature( a, [ optional( k_feature( b, [ mandatory( l_feature( e ) ) ] ) ), mandatory( l_feature( c ) ), mandatory( k_feature( d, [ one_or_more( [ l_feature( f ), l_feature( g ) ] ) ])) ] ), [ requires( e, f ), requires( f, e ) ] ) ) ). % Sample usage from Prolog prompt: analyze( survey_spl ). analyze( SPL_ID ) :- spl_db( SPL_ID, SPL ), write( ’Checking ’ ), write( SPL_ID ), nl, check_spl( SPL ), write( ’Products of ’ ), write( SPL_ID ), nl, products_verbose( SPL, PRDS ), core_features( SPL, CORE ), write( ’Core features = ’ ), write( CORE ), nl, variant_features( SPL, VARIANT ), write( ’Variant features = ’ ), write( VARIANT ), nl, ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 A.1. Sample use of the FLAME framework 49 dead_features( SPL, DEAD ), write( ’Dead features = ’ ), write( DEAD ), nl, unique_features( SPL, UNIQUE ), write( ’Unique features = ’ ), write( UNIQUE ), nl, homogeneity( SPL, H ), write( ’Homogeneity = ’ ), write( H ), nl, variability( SPL, V ), write( ’Variability = ’ ), write( V ), nl, partial_variability( SPL, PV ), write( ’Partial variability = ’ ), write( PV ), nl, atomic_sets( SPL, ATOMS ), write( ’Atomic sets: ’), write( ATOMS ), nl, fail. A. Durán et al. Seville, March 2011 50 FLAME: FAMA Formal Framework A.2 Abstract foundation layer of FLAME % ----------------------------------------------------------------------------- % File: afl.pl % Content: abstract foundation layer (AFL) package for FLAME % Author: Amador Durán Toro % Date: 24/03/2011 % ----------------------------------------------------------------------------- :- consult( ’sets.pl’ ). % set toolkit :- consult( ’check_spl.pl’ ). % abstract SPL checking :- consult( ’valid.pl’ ). % validity :- consult( ’products.pl’ ). % products :- consult( ’relations.pl’ ). % SPL relations :- consult( ’filter.pl’ ). % filter :- consult( ’features.pl’ ). % feature-related operations :- consult( ’atomic_sets.pl’ ). % atomic sets :- consult( ’indicators.pl’ ). % numerical indicators A.2.1 Abstract SPL checking % ----------------------------------------------------------------------------- % File: check_spl.pl % Content: SPL checks for FLAME % Author: Amador Durán Toro % Date: 24/03/2011 % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % Z definitions (AFL) % +- SPL ------------------------------------ % | model : Model % | features : F1 Feature % +------------------ % | features( model ) = features % | [ characteristic model checks ] % +------------------------------------------ % % Prolog predicates % check_spl( spl( F, M ) ) % % This predicate checks an SPL for internal correctness: % - if its set of features is not empty % - if its set of features is actually a set % - if its model is defined using only its set of features % - if its characteristic model is correct, using the abstract predicate % checkModel, that must redefined in the characteristic model layer. % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % check_spl( SPL ) % It checks an SPL for internal correctnes. % ----------------------------------------------------------------------------- % No features check_spl( spl( [], _ ) ) :- write( ’SPL is not OK!’ ), nl, write( ’Empty feature set.’ ), nl, fail. % Features is not a set, i.e. it contains duplicates ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 A.2. Abstract foundation layer of FLAME 51 check_spl( spl( F, _ ) ) :- not( is_set( F ) ), write( ’SPL is not OK!’ ), nl, write( ’Duplicated features in its feature set.’ ), nl, fail. % Feature model uses unknown features check_spl( spl( F, M ) ) :- features( M, FM ), not( subset( FM, F ) ), write( ’SPL is not OK!’ ), nl, write( ’Feature model includes unknown features ’ ), subtract( FM, F, U ), write( U ), nl, fail. % Some features are not used in the feature model check_spl( spl( F, M ) ) :- features( M, FM ), not( subset( F, FM ) ), write( ’SPL is not OK!’ ), nl, write( ’Feature model does not use some features ’ ), subtract( F, FM, U ), write( U ), nl, fail. % Check characteristic model check_spl( spl( F, M ) ) :- check_model( spl( F, M ) ), % abstract predicate fail. % Success predicate (nothing else to be checked) check_spl( spl( _, _ ) ) :- write( ’No (more) errors found in SPL.’ ), nl. A.2.2 Validity relations % ----------------------------------------------------------------------------- % File: valid.pl % Content: Validity relations of FLAME % Author: Amador Durán Toro % Date: 21/04/2011 % ----------------------------------------------------------------------------- % Update: fixed valid product - configuration; added full and partial % Author: Amador Durán Toro % Date: 09/02/2012 % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % Z definitions % _valid_ : Product <-> SPL % _valid_p_c_ : Product <-> Configuration % _valid_c_ : Configuration <-> SPL % % Prolog predicates % valid( Product, spl( Features, Model ) ) % valid_p_c( Product, Configuration ) % valid_c( Configuration, spl( Features, Model ) ) % why_not_valid( Product, spl( Features, Model ) ) % % The first predicate checks if a product is valid for an SPL. The second does % the same for a configuration. The third checks if a configuration is valid A. Durán et al. Seville, March 2011 58 FLAME: FAMA Formal Framework % ----------------------------------------------------------------------------- atomic_sets( spl( F, M ), ATOMS ) :- potential_atomic_sets( spl( F, M ), POTATOMS ), findall( A, maximal( A, POTATOMS ), ATOMS ). % ----------------------------------------------------------------------------- % potential_atomic_sets( SPL, [ [ Feature ] ] ) % It computes the potential atomic sets of an SPL using the auxiliary predicate % atomicSet. % ----------------------------------------------------------------------------- potential_atomic_sets( spl( F, M ), POTATOMS ) :- products( spl( F, M ), PRDS ), findall( A0, potential_atomic_set( A0, F, PRDS ), POTATOMS ). potential_atomic_set( A0, F, PRDS ) :- btrck_subset( A0, F ), % backtrackable version of subset A0 \= [], % atomic sets are nonempty forall( member( P, PRDS ), subset_or_disjoint( A0, P ) ). A.2.8 Numerical indicators % ----------------------------------------------------------------------------- % File: indicators.pl % Content: Numerical indicators of FLAME % Author: Amador Durán Toro % Date: 10/04/2011 % ----------------------------------------------------------------------------- % Update: homogeneity, commonality and partial variability fixed % Author: Amador Durán Toro % Date: 07/06/2011 % ----------------------------------------------------------------------------- % Update: homogeneity re-fixed % Author: Amador Durán Toro % Date: 13/06/2011 % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % Z definitions % homogeneity : SPL -> R % commonality : SPL x Configuration -> R % variability : SPL -> R % pvariability : SPL -> R % % Prolog predicates % homogeneity( SPL, H ) % commonality( SPL, CONF, C ) % variability( SPL, V ) % partial_variability( SPL, PV ) % % These predicates compute several measures of an SPL. % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % homogeneity( SPL, P ) % It computes the homogeneity of an SPL. % ----------------------------------------------------------------------------- homogeneity( spl( F, M ), H ) :- unique_features( spl( F, M ), UF ), length( UF, NOUF ), ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 A.2. Abstract foundation layer of FLAME 59 length( F, NOF ), His 1 - ( NOUF / NOF ). % ----------------------------------------------------------------------------- % commonality( SPL, CONF, C ) % It computes the commonality factor of a configuration in an SPL. % ----------------------------------------------------------------------------- commonality( spl( F, M ), configuration( _, _ ), 0 ) :- void( spl( F, M ) ). commonality( spl( F, M ), configuration( S, R ), C ) :- filter( spl( F, M ), configuration( S, R ), FILTERED ), nop( spl( F, M ), NOP ), length( FILTERED, NOFP ), Cis NOFP / NOP. % ----------------------------------------------------------------------------- % variability( SPL, V ) % It computes the (total) variability of an SPL % ----------------------------------------------------------------------------- variability( spl( F, M ), V ) :- nop( spl( F, M ), N ), length( F, NOF ), Vis N/(2**NOF - 1 ). % ----------------------------------------------------------------------------- % partial_variability( SPL, V ) % It computes the partial variability of an SPL % ----------------------------------------------------------------------------- partial_variability( spl( F, M ), 0 ) :- variant_features( spl( F, M ), [] ). partial_variability( spl( F, M ), PV ) :- nop( spl( F, M ), N ), variant_features( spl( F, M ), VF ), length( VF, NOVF ), PV is N/(2**NOVF - 1 ). % ----------------------------------------------------------------------------- % potential( SPL, P ) % It computes the number of potential products of an SPL % ----------------------------------------------------------------------------- %potential( spl( F, _ ), P ) :- % length( F, NOF ), % P is 2**NOF - 1. A. Durán et al. Seville, March 2011 60 FLAME: FAMA Formal Framework A.3 Characteristic model layer of FLAME % ----------------------------------------------------------------------------- % File: bfm.pl % Content: CML/BFM package for FLAME % Author: Amador Durán Toro % Date: 24/03/2011 % ----------------------------------------------------------------------------- :- consult( ’helpers.pl’ ). % helper functions :- consult( ’check_model.pl’ ). % BFM model checking :- consult( ’features.pl’ ). % features-in-a-model function :- consult( ’instance.pl’ ). % is-instance-of relation A.3.1 Helper functions % ----------------------------------------------------------------------------- % File: helpers.pl % Content: BFM helper functions for FLAME % Author: Amador Durán Toro % Date: 23/04/2011 % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % Z definitions % children : Relationship -> F1 TreeFeature % feature_count_T : Feature x TreeModel -> N % feature_count_R : Feature x Relationship -> N % % Prolog predicates % children( Relationship, [ TreeFeature ] ) % feature_count_t( Feature, TreeModel, N ) % feature_count_r( Feature, Relationship, N ) % % The first predicate returns the children TreeFeatures of a Relationship. % The two last predicates return the number of times a feature appears in a % TreeModel or in a Relationship. % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % children( Relationship, [ TreeFeature ] ) % It returns the children TreeFeatures of a Relationship. % ----------------------------------------------------------------------------- children( mandatory( Ti ), CHLD ) :- children( optional( Ti ), CHLD ). children( optional( Ti ), [ Ti ] ). children( one_or_more( T ), CHLD ) :- children( only_one( T ), CHLD ). children( only_one( T ), T ). % ----------------------------------------------------------------------------- % feature_count_t( Feature, TreeModel, N ) % It computes the number of times a feature appears in a TreeModel. % ----------------------------------------------------------------------------- feature_count_t( F, l_feature( F ), 1 ). ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 A.3. Characteristic model layer of FLAME 61 feature_count_t( F1, l_feature( F2 ), 0 ) :- F1 \= F2. feature_count_t( F, k_feature( F, RELS ), N ) :- for_each_sum( feature_count_r, F, RELS, NR ), Nis NR + 1. feature_count_t( F1, k_feature( F2, RELS ), N ) :- F1 \= F2, for_each_sum( feature_count_r, F1, RELS, N ). % ----------------------------------------------------------------------------- % feature_count_r( Feature, Relationship, N ) % It computes the number of times a feature appears in a Relationship. % ----------------------------------------------------------------------------- feature_count_r( F, R, N ) :- children( R, CHLD ), for_each_sum( feature_count_t, F, CHLD, N ). A.3.2 Specific BFM checking % ----------------------------------------------------------------------------- % File: check_model.pl % Content: BFM checks for FLAME % Author: Amador Durán Toro % Date: 23/04/2011 % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % Z definitions (CML/BFM) % +- SPL ------------------------------------ % | model : Model % | features : F1 Feature % +------------------ % | features( model ) = features % | forAll f : features @ % | feature_count( f, tree model ) = 1 % +------------------------------------------ % % Prolog predicates % check_model( spl( F, M ) ) % check_tree( F, M ) % % This predicate checks a BFM-based SPL for internal correctness: % - if its tree model is a tree % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % Model is not a tree % ----------------------------------------------------------------------------- check_model( spl( _, bfm( TREE, CTC ) ) ) :- features( bfm( TREE, CTC ), F2 ), check_tree( F2, TREE ), fail. % ----------------------------------------------------------------------------- % check_tree( [ F ], TREE ) % It checks if the features appear only once in the tree model using the % check_feature_count auxiliary predicate. % ----------------------------------------------------------------------------- A. Durán et al. Seville, March 2011 62 FLAME: FAMA Formal Framework check_tree( [], _ ). check_tree( [ Fi | F ], TREE ) :- check_feature_count( Fi, TREE ), check_tree( F, TREE ). check_feature_count( F, TREE ) :- feature_count_t( F, TREE, N ), N > 1, !, write( ’SPL is not OK!’ ), nl, write( ’Feature ’ ), write( F ), write( ’ appears ’ ), write( N ), write( ’ times in the SPL model.’ ), nl. check_feature_count( _, _ ). A.3.3 Features–in–a–model function % ----------------------------------------------------------------------------- % File: features.pl % Content: BFM features-in-a-model function for FLAME % Author: Amador Durán Toro % Date: 23/04/2011 % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % Z definitions % features : Model -> F Feature % tfeatures : TreeFeature -> F Feature % rfeatures : Relationship -> F Feature % xfeatures : CTC -> F Feature % % Prolog predicates % features( Model, [ Feature ] ) % t_features( TreeFeature, [ Feature ] ) % r_features( Relationship, [ Feature ] ) % x_features( CTC, [ Feature ] ) % % These predicates return a set with all the features used in a BFM model. % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % features( Model, [ Feature ] ) % It computes the features in a BMF characteristic model % ----------------------------------------------------------------------------- features( bfm( TREE, CTC ), F ) :- t_features( TREE, F1 ), for_each_union( x_features, CTC, F2 ), union( F1, F2, F ). % ----------------------------------------------------------------------------- % t_features( TreeFeature, [ Feature ] ) % It computes the features in a TreeFeature. % ----------------------------------------------------------------------------- t_features( l_feature( Fi ), [ Fi ] ). t_features( k_feature( Fi, R ), F ) :- for_each_union( r_features, R, FR ), union( [ Fi ], FR, F ). ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 A.3. Characteristic model layer of FLAME 63 % ----------------------------------------------------------------------------- % r_features( Relationship, [ Feature ] ) % It computes the features in a Relationship. % ----------------------------------------------------------------------------- r_features( R, F ) :- children( R, CHLD ), for_each_union( t_features, CHLD, F ). % ----------------------------------------------------------------------------- % x_features( CTC, [ Feature ] ) % It computes the features in a CTC. % ----------------------------------------------------------------------------- x_features( requires( F1, F2 ), F ) :- x_features( excludes( F1, F2 ), F ). x_features( excludes( F1, F2 ), F ) :- union( [ F1 ], [ F2 ], F ). A. Durán et al. Seville, March 2011 64 FLAME: FAMA Formal Framework A.3.4 Is–instance–of relation % ----------------------------------------------------------------------------- % File: instance.pl % Content: BFM is-instance-of relation for FLAME % Author: Amador Durán Toro % Date: 22/04/2011 % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % NOTE: instance is a built-in predicate of SWI-Prolog that cannot redefined % ----------------------------------------------------------------------------- % % Z definitions % _instance_ : Product <-> Model % _tinstance_ : Product <-> TreeFeature % _rinstance_ : Product <-> Relationship % _xinstance_ : Product <-> CTC % % Prolog predicates % instance_of( Product, Model ) % instance_of_t( Product, TreeFeature ) % instance_of_r( Product, Relationship ) % instance_of_x( Product, CTC ) % instance_or_disjoint( Product, TreeFeature, NOI ) % instance_or_disjoint( Product, [ TreeFeature ], NOI ) % % The first predicates check if a product is an instance of a BFM model, a tree, % a relationship, and a CTC. The last one is a helper predicate that checks if a % product is an instance of or does not contain any feature of a list of trees. % It also computes the number of times the product is an instance of the treee % (NOI = Number Of Instances). % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % instance_of( Product, Model ) % It computes if the product is an instance of a BFM model. % ----------------------------------------------------------------------------- instance_of( P, bfm( TREE, CTC ) ) :- instance_of_t( P, TREE ), !, forall( member( CTCi, CTC ), instance_of_x( P, CTCi ) ). % ----------------------------------------------------------------------------- % instance_of_t( Product, TreeFeature ) % It computes if the product is an instance of a TreeFeature. % ----------------------------------------------------------------------------- instance_of_t( P, l_feature( F ) ) :- member( F, P ). instance_of_t( P, k_feature( F, R ) ) :- member( F, P ), forall( member( Ri, R ), instance_of_r( P, Ri ) ). % ----------------------------------------------------------------------------- % instance_of_r( Product, Relationship ) % It computes if the product is an instance of a Relationship. % ----------------------------------------------------------------------------- instance_of_r( P, mandatory( Ti ) ) :- instance_of_t( P, Ti ). ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 A.3. Characteristic model layer of FLAME 65 instance_of_r( P, optional( Ti ) ) :- instance_or_disjoint( P, Ti, _ ). instance_of_r( P, one_or_more( T ) ) :- instance_or_disjoint( P, T, NOI ), NOI >= 1. instance_of_r( P, only_one( T ) ) :- instance_or_disjoint( P, T, NOI ), NOI =:= 1. % ----------------------------------------------------------------------------- % instance_of_x( Product, CTC ) % It computes if the product is an instance of a CTC. % ----------------------------------------------------------------------------- instance_of_x( P, requires( F1, F2 ) ) :- not( member( F1, P ) ) ; member( F2, P ). instance_of_x( P, excludes( F1, F2 ) ) :- not( member( F1, P ) ) ; not( member( F2, P ) ). % ----------------------------------------------------------------------------- % instance_or_disjoint( Product, [ TreeFeature ], NOI ) % instance_or_disjoint( Product, TreeFeature, NOI ) % % It checks if the product is an instance of the TreeFeature or if none of the % features in the product appear in the tree. It also computes how many times % the product is an instance of the tree (NOI = Number Of Instances). % ----------------------------------------------------------------------------- instance_or_disjoint( _, [], NOI ) :- NOI is 0. instance_or_disjoint( P, [ TFi | TF ], NOI ) :- instance_or_disjoint( P, TFi, NOI1 ), instance_or_disjoint( P, TF, NOI2 ), NOI is NOI1 + NOI2, !. instance_or_disjoint( P, TFi, NOI ) :- instance_of_t( P, TFi ), NOI is 1. instance_or_disjoint( P, TFi, NOI ) :- t_features( TFi, F ), intersection( P, F, [] ), NOI is 0. A. Durán et al. Seville, March 2011 66 FLAME: FAMA Formal Framework A.4 Set toolkit of FLAME % ----------------------------------------------------------------------------- % File: sets.pl % Content: Set toolkit for FLAME % Author: Amador Durán Toro % Date: 24/04/2011 % ----------------------------------------------------------------------------- % Update: fixed powerset_subset by sorting both sets before comparing % Author: Amador Durán Toro % Date: 22/05/2011 % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % Prolog predicates (public) % equal_set( [ Set ], [ Set ] ) % equal_superset( [ [ Set ] ], [ [ Set ] ] ) % union( [ [ Set ] ], [ Set ] ) % intersection( [ [ Set ] ], [ Set ] ) % maximal( [ Set ], [ [ Set ] ] ) % proper_subset( [ Subset ], [ Set ] ) % subset_or_disjoint( [ Subset ], [ Set ] ) % power_set( [ Set ], [ [ Powerset ] ] ) % btrck_subset( Subset, Set ) % powerset_subset( [ Subset ], [ Set ] ) % bratko_subset( [ Subset ], [ Set ] ) % safe_sort( [ Set ], [ Set ] ) % for_each_union( Goal, [ Set ], [ Set ] ) % for_each_sum( Goal, [ Set ], N ) % for_each_sum( Goal, K, [ Set ], N ) % for_each_sort( [ [ Set ] ], [ [ Set ] ] ) % % Some of these set-related predicates are implemented in other versions of % Prolog, but not in SWI-Prolog. % ----------------------------------------------------------------------------- % ----------------------------------------------------------------------------- % equal_set( [ Set ], [ Set ] ) % Predicate that checks set equality as mutual inclusion. % ----------------------------------------------------------------------------- equal_set( Set1, Set2 ) :- subset( Set1, Set2 ), subset( Set2, Set1 ). % ----------------------------------------------------------------------------- % equal_superset( [ [ Set ] ], [ [ Set ] ] ) % Predicate that checks superset (set of sets) equality. % ----------------------------------------------------------------------------- equal_superset( S1, S2 ) :- for_each_sort( S1, SS1 ), for_each_sort( S2, SS2 ), equal_set( SS1, SS2 ). % ----------------------------------------------------------------------------- % union( [ [ Set ] ], [ Set ] ) % It computes the distributed union over a set of sets. % ----------------------------------------------------------------------------- union( Superset, Union ) :- flatten( Superset, Flatten ), list_to_set( Flatten, Union ). ISA Research Group - U. of Seville Technical Report ISA–12–TR–02 A.4. Set toolkit of FLAME 67 % ----------------------------------------------------------------------------- % intersection( [ [ Set ] ], [ Set ] ) % It computes the distributed intersection over a set of sets using the % auxiliary predicate dinter. % ----------------------------------------------------------------------------- intersection( [], [] ). intersection( [ S1 | Rest ], Intersection ) :- dinter( [ S1 | Rest ], S1, Intersection ). dinter( [], Result, Result ). dinter( [ S1 | Rest ], PreviousResult, Result ) :- intersection( S1, PreviousResult, Aux ), dinter( Rest, Aux, Result ). % ----------------------------------------------------------------------------- % maximal( [ Set ], [ [ Set ] ] ) % This backtrackable predicate checks if the first set is a maximal subset of % the set of sets passed as the second argument. % ----------------------------------------------------------------------------- maximal( Si, S ) :- member( Si, S ), forall( member( Sj, S ), not( proper_subset( Si, Sj ) ) ). % ----------------------------------------------------------------------------- % proper_subset( [ Subset ], [ Set ] ) % It checks if the first set is a proper subset of the second. In order to % ignore if both sets are sorted, lengths are compared to determine if they % are not the same set. % ----------------------------------------------------------------------------- proper_subset( Si, Sj ) :- length( Si, L1 ), length( Sj, L2 ), L1 \= L2, subset( Si, Sj ). % ----------------------------------------------------------------------------- % subset_or_disjoint( [ Subset ], [ Set ] ) % It checks if the first set is a subset of the second or if they are disjoint. % ----------------------------------------------------------------------------- subset_or_disjoint( A, P ) :- subset( A, P ) ; intersection( A, P, [] ). % ----------------------------------------------------------------------------- % power_set( [ Set ], [ [ Powerset ] ] ) % Powerset predicate. It simply reverses the set before computing its powerset % in order to generate more "human-like" results (first element first, etc.). % ----------------------------------------------------------------------------- power_set( Set, Powerset ) :- reverse( Set, SetReverse ), !, power_set_aux( SetReverse, [[]], Powerset ), !. % ----------------------------------------------------------------------------- % power_set_aux( [ Set ], [ Acc ], [ Powerset ] ) A. Durán et al. Seville, March 2011