Sagar Sen
email: ssen@irisa.fr

Benoit Baudry

Hans Vangheluwe

Towards Domain-specific Model Editors with Automatic Model Completion

Keywords: Meta-model directed editing, Domain-specific modelling language, Structure editor, Partial model, Model completion, AToM 3, Alloy

Integrated development environments such as Eclipse allow users to write programs quickly by presenting a set of recommendations for code completion. Similarly, word processing tools such as Microsoft Word present corrections for grammatical errors in sentences. Both of these existing structure editors use a set of constraints expressed in the form of a natural language grammar to restrict/correct the user (syntax-directed editing) or formal grammar (language-directed editing) to aid document completion. Taking this idea further, in this paper we present an integrated software system capable of generating recommendations for model completion of partial models built in editors for domain-specific modelling languages. We present a methodology to synthesize model editors equipped with automatic completion from a modelling language's declarative specification consisting of a metamodel with a visual syntax. This meta-model directed completion feature is powered by a first-order relational logic engine implemented in ALLOY. We incorporate automatic completion in the generative tool AToM 3 . We use the Finite State Machines modelling language as a concise running example. Our approach leverages a correct by construction philosophy that renders subsequent simulation of models considerably less error-prone.

I. INTRODUCTION

Documents in the form of computer programs, diagrams, chemical formulas, and markup text can currently be edited in document editors called structure editors. These structure editors are cognizant of the document's underlying structure such as the grammatical syntax or a formal grammar of the language. Functionally, these structure editors are syntax or language-directed to aid the user by presenting recommendations for completion of code, text, or a diagram based on correct possibilities prescribed by the underlying structure. This enables faster document development with fewer errors. However, structure editors are separately constructed for each domain-specific language and are built mainly for grammar-based textual languages. We are interested in the subject of extending structure editors from high-level models built using the principles of Model Driven Engineering (MDE) [START_REF] France | Model-driven development of complex software: A research roadmap[END_REF] where domain-specific model editors are automatically synthesized for a variety of modelling languages.

In MDE, given a meta-model specification of a domain-specific modelling language, software tools can automatically generate domain-specific model editors. For example, generative modelling tools such as AToM 3 (A Tool for Multi-formalism Metamodelling) [START_REF] De | Atom 3 : A tool for multi-formalism modelling and meta-modelling[END_REF] [START_REF] Vangheluwe | Domain-Specific Modelling with AToM3[END_REF],GME (Generic Modelling Environment) [START_REF] Ledeczi | Composing Domain-Specific Design Environments[END_REF], GMF (Eclipse Graphical Modelling Framework) [START_REF] Ehrig | Generation of Visual Editors as Eclipse Plug-ins[END_REF] can synthesize a domain-specific visual model editor from a declarative specification of a domain-specific modelling language. A declarative specification consists of a meta-model and a visual/textual syntax that describes how language elements (objects and relationships) manifest in the model editor. The designer of a model uses this model editor to construct a model on a drawing canvas. This is analogous to using an integrated development environment (IDE) to enter a program or a word processor to enter sentences. However, IDEs such as Eclipse present recommendations for completing a program statement when possible based on its grammar and existing libraries [START_REF] Ko | Design requirements for more flexible structured editors from a study of programmer's text editing[END_REF]. Similarly, Microsoft Word presents grammatical correction recommendations if a sentence does not conform to a natural language grammar. Therefore, we ask: Can we extrapolate similar technology or develop new technology for partial models constructed in a model editor for a domain-specific modelling language (DSML)?

Extrapolating code completion techniques for model completion is not feasible in the general case. The first reason is the difference between the underlying structure of code and models. Code completion techniques use the Backus-Naur Form (BNF) grammar of a programming language while models are specified by a meta-model and constraints on it. Second, model completion must consider completing the entire model as constraints can span entire models unlike code completion which presents solutions at a program statement level. Third, in terms of reduction in effort model completion must help reduce the effort of a modeller by automatically satisfying all relevant language constraints since in general they may be too hard for a modeller to resolve manually. The output of model completion must be one or many valid models that conform to their language. This notion of reduction in effort is different from that in code completion. Code completion presents local suggestions to complete navigational expressions or concept names but it does not perform constraint satisfaction to output a valid program. In the general case, model completion may take more time than code or sentence completion which are almost instantaneous. Therefore, there is a need to develop new techniques for model completion with different goals such as relaxing the exigence towards time to complete.

The major difficulty for providing completion capabilities in model editors is to integrate heterogeneous sources of knowledge in the computation of the possible solutions for completion. The completion algorithm must take into account the concepts defined in the meta-model, constraints on the concepts and the partial model built by a domain expert/user. The difficulty is that these three sources of knowledge are obviously related (they refer to the same concepts) but are expressed in different languages, sometimes in different files, and in most cases by different people and at different moments in the development cycle as they are separable concerns.

In this paper, we propose an automatic transformation from heterogenous sources of knowledge to an ALLOY [START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF] [20] constraint model. ALLOY is a declarative constraint language based on quantified first-order logic with support for operators in relational calculus. The generated ALLOY model is then used to synthesize a set of Boolean CNF formulae which are solved using an appropriate satisfiability (SAT) solver. The solutions are parsed and transformed from low-level logic and returned as high-level models to the model editor as recommendations for completing the partial model. These solutions are shown in the concrete visual syntax of the modelling language. Our transformation from the different sources to ALLOY is integrated in the software tool AToM 3 . We select AToM 3 since its has a light-weight python implementation for rapid-prototyping and proof of concept. Also, AToM 3 supports an easy to use icon editor and DSML generator for rapidly synthesizing DSML visual modelling environments from meta-model and visual syntax specifications. A transformation module in AToM 3 can also also serialize standard XMI versions of models for use in industry standard tools such as Eclipse GMF. The simple and easy to use Python-API of AToM 3 allows fast integration of new features and transformations in modelling languages. A similar implementation in widely used tools such as Eclipse GMF is certainly feasible but will need more programming effort as it is Java-based where one needs experience in using the several interdependent libraries available in the Eclipse platform. Nevertheless, any model in the AToM 3 environment can be used in the Eclipse GMF environment using the standard XMI interchange format. The meta-model for a DSML is built directly in AToM 3 's model editor using its class diagram formalism. The constraints on the concepts of this meta-model are defined using ALLOY facts. Using this information and a description of the concrete visual syntax (specified in an icon editor) for a modelling language, AToM 3 synthesizes a visual model editor for the DSML. The partial model can be built and edited in the generated model editor and the designer can ask for recommendations for possible automatic completions. The partial model is automatically transformed to a constraint called an ALLOY predicate. This ALLOY predicate is then augmented to the ALLOY model to give the whole set of constraints. We invoke a solver on this this set of constraints to obtain zero/one/more complete model(s).

In Section II we present related work. An overview of our methodology is presented in Section III. One of the key parts of our methodology is the automatic synthesis of domain-specific model editors from their specification comprising of the meta-model and visual syntax. This process is described in Section IV. The component that will add model completion ability to the synthesized model editor is a transformation from the meta-model and partial model to an ALLOY model. We present this transformation in Section V. Once we include this transformation into the synthesis of a domain-specific model editor we are able to synthesize domain-specific model editors with automatic model completion. We describe the model completion process in Section VI. We present examples of model completion recommendations generated for partial models in Section VII. We conclude in Section VIII.

II. RELATED WORK

Language-directed editors have been around for since the early 1980s. Some of the well-cited research on languagedirected editors are Mentor [START_REF] Donzeau-Gouge | Interactive Programming Environments, chapter Programming environments based on structured editors: The Mentor experience[END_REF], Interlisp [START_REF] Teitelman | The Interlisp Programming Environment[END_REF], Program Synthesizer [START_REF] Teitelbaum | The Cornell Program Synthesizer: A syntax-directed programming environment[END_REF], Rational [START_REF] Archer | Rational's experience using Ada for very large systems[END_REF], PECAN [START_REF] Reiss | Graphical program development with PECAN program development systems[END_REF], and Gandalf [START_REF] Habermann | Gandalf: Software development environments[END_REF]. Most of the existing language-based editors such as in Eclipse are based on attribute grammars [START_REF] Kaiser | Incremental Dynamic Semantics for Language-Based Programming Environments[END_REF]. These systems have been widely adopted and integrated in many editors for tasks such as syntax highlighting and syntax-directed editing. The openArchitectureWare [1] framework , based on the Ecore [START_REF] Frank | Eclipse Modeling Framework, volume 1 of The Eclipse Series[END_REF] meta-modelling framework, supports automatic sentence completion already implemented in Eclipse to help make recommendations to sentences in textual domain-specific modelling languages. These suggestions for sentence completion are based on the textual syntax of the modelling language and do not consider the complete consistency of the model with respect to the meta-model and constraints of the language.

In Model Driven Engineering (MDE), models built in domain-specific model editors pose a new challenge. The challenge is to complete a partial model specified in the model editor. This involves the editor to use domain-specific modelling language constraints to direct the completion of the partial model. Simply put, this involves constraint solving using knowledge described in the partial model to synthesize a model that conforms to the domain-specific modelling language. Constraint solving for model synthesis has been well-studied in the literature such as model design space exploration [START_REF] Neema | Constraint-Based Design Space Exploration and Model Synthesis[END_REF], partial model completion using Prolog [START_REF] Sen | Partial Model Completion in Model Driven Engineering using Constraint Logic Programming[END_REF] and constraint logic programming [START_REF] Krysztof | Constraint Logic Programming with ECLiPSe[END_REF]. In [START_REF] Sen | Domain-specific Model Editors with Model Completion[END_REF] we present a model completion system in a domain-specific editor by combining knowledge from the meta-model and the partial model specified in the model editor to SWI-Prolog. The Prolog program is solved using a backtracking based solver to return results to the domain-specific environment which was originally synthesized by AToM 3 using the meta-model. Our methodology is valid for any domain-specific modelling language in the limits of first-order Horn clause logic of SWI-Prolog. However, their primary limitation is that the number of objects in the complete model is equal to the number of objects in the partial model. No new objects are suggested by the model completion system and the user is limited to specifying only the correct number of objects in the partial model. This is primarily due to the fact that constraints are specified at the object property level in SWI-Prolog and not at the meta-level such as on sets of objects.

We identify the need to develop a model completion system that can automatically suggest complete models especially for DSML meta-models containing constraints both on sets of objects and their properties. This typically involves mapping of a meta-model and constraints based DSML specification to a mathematical formalism with tool support that solves constraints to give correct instances of the DSML. Notably, such instances should contain the network of objects (original object identities need not be preserved) specified in the partial model and additional objects (if required) with appropriate property values such that the complete model conforms to its DSML. We would also like to control the maximum size or scope of the complete model for practical time considerations. Transformation of meta-models expressed in UML/OCL [START_REF] Omg | The Object Constraint Language Specification 2.0[END_REF] to various formal systems is not new [START_REF] Berardi | Reasoning on UML class diagrams[END_REF] [4] [19] [24] [2] [8] [START_REF] Anastasakis | UML2Alloy: A Challenging Model Transformation[END_REF]. In [START_REF] Berardi | Reasoning on UML class diagrams[END_REF] the authors present a transformation from UML Class Diagrams to Description Logics. Their approach is theoretically rigourous where a knowledge base in description logic on its variants is obtained for a UML Class diagram and theorem provers such as FACT [START_REF] Horrocks | Using an expressive description logic: FaCT or fiction?[END_REF] and RACER [START_REF] Haarslev | RACER system description[END_REF] are used to obtain instances by inferring from the knowledge base. They prove that the time for inference using a description logic representation of an UML Class diagram in EXPTIME-complete. However, their approach does not support transformation of meta-level constraints such as those expressed in Object Constraint Language (OCL) [START_REF] Omg | The Object Constraint Language Specification 2.0[END_REF] to description logic. An extension of this work for obtaining instances in finite domain is presented in [START_REF] Cadoli | Finite satisfiability of UML class diagrams by Constraint Programming[END_REF]. The transformation of meta-level constraints such as OCL along with UML class diagrams to formal higher-order logic language called Isabelle has been explored in tools such as HOL-OCL [START_REF] Brucker | The HOL-OCL book[END_REF]. Similarly, we have seen the transformation to constraint programming language ECLiPSE in [START_REF] Cabot | Verification of UML/OCL Class Diagrams Using Constraint Programming[END_REF]. Both, these approaches are used primarily for verification of a UML Class Diagram instance against the UMLCD meta-model specification. A constraint in OCL can be verified against an instance of UMLCD but we need the instance itself. In our pursuit to find complete models we need to automatically synthesize instances of a meta-model rather than verifying an arbitrary constraint against an existing instance.

In our approach, we transform the specification of a domain-specific modelling language and the partial model to the common language of first-order relational logic. The target common language is implemented in ALLOY. Transformation of a meta-model specification from UML to ALLOY has previously been explored in the tool UML2Alloy [START_REF] Bordbar | Uml2alloy: A tool for lightweight modelling of discrete event systems[END_REF] [23] [START_REF] Bordbar | Mda and analysis of web applications[END_REF]. UML2Alloy supports transformation from meta-model concepts to ALLOY model concepts such as class to signature, property to signature field, operation to function, enumeration/enumeration literal to extends signature, and constraints to predicates. In our approach to transforming a meta-model to an ALLOY model we keep the same transformation format such we transform classes to signatures and properties to class fields. In UML2Alloy composition and aggregation are transformed first to OCL constraints and then to ALLOY. In our tool we transform composition and aggregation in a meta-model directly to ALLOY facts. Our, approach to transforming inheritance is the same as in UML2Alloy. Inheritance is transformed to an ALLOY signature that extends an other ALLOY signature. There is no clear specification in UML2Alloy related articles [START_REF] Bordbar | Uml2alloy: A tool for lightweight modelling of discrete event systems[END_REF] [23] [START_REF] Bordbar | Mda and analysis of web applications[END_REF] about transforming multiplicities to ALLOY. In our case we transform multiplicity constraints to ALLOY signature fields in case of occurrence of 0, 0..1, or 0.. * multiplicities. If the multiplicity is variable such as a..b we synthesize an ALLOY fact constraining the size of a set of relations. The constraints in meta-model is restricted to a small subset of OCL as UML2Alloy transforms only this subset of OCL to ALLOY. However, in our tool we propose the user to directly enter ALLOY predicates and facts in the ALLOY model giving the user the flexibility of expressing a wider range of constraints (those that have not been implemented in UML2Alloy) such constraints with transitive closure which cannot be expressed directly in OCL. We also present a method to synthesize ALLOY predicates from a partial model. This use of partial knowledge to synthesize complete models greatly reduces model development time. The tool UML2Alloy, does not support the use of partial model knowledge to help generate models.

III. METHODOLOGY OVERVIEW

The development and use of a domain-specific model editor with automatic model completion can be divided into the following phases and sub-phases:

1) Specification of a domain-specific modelling language (in AToM Solving final ALLOY model and returning complete models as recommendations to the model editor The specification of a domain-specific language is usually done by a language designer who interacts with domain experts to identify the concepts, their properties and relationships in a domain of knowledge, science or engineering. The language designer also develops a repository of constraints among the concepts and its properties. The assembly of the concepts and relationships is expressed as a Class Diagram (CD) by the language designer. In our methodology we use the AToM 3 CD formalism for this purpose. The constraints on the CD are expressed in a formal constraint language. Preferably, a constraint language that has a finite number of solutions and is decidable. In our methodology we use facts expressed in the language ALLOY to represent such constraints. The CD and the set of constraints on it results in the meta-model of a Domain-specific Modelling Language (DSML)

A visual syntax designer specifies a concrete visual syntax for the concepts and relationships in the modelling language. In our methodology we use the AToM 3 icon editor to specify a visual syntax. In Section IV we discuss in detail the specification of the modelling language for Finite State Machines (FSM) along with a visual syntax.

Once we have all the elements (meta-model and visual syntax) necessary for a domain-specific modelling language a model transformation engineer develops a transformation to synthesize a visual domain-specific model editor from these elements. The model editor consists of buttons, menus, and a canvas. A user can select and drop objects on a drawing canvas and connect them using relationships. The objects are manifested as icons as specified in the icon editor for the concrete visual syntax by the visual syntax designer. The relationships are links between these icons. In the model editor by clicking on the icon the user can edit or specify the values of properties.

In our work, we extend this model transformation by transforming the meta-model to an ALLOY model. The transformation also synthesizes a button widget in the domain-specific model editor. A domain expert or user can click on this button resulting in the solving of the ALLOY model augmented with ALLOY predicates synthesized from the partial model drawn on the canvas. Recommendations as one or more complete models (if found) are returned to the model drawing canvas. In Section V we present the transformation from the meta-model and the partial model to ALLOY. An illustrative outline of the model completion methodology is shown in Figure 1.

One of the key benefits in using ALLOY is its ability to handle constraints specified on a set of objects using quantifiers such as some, all, one, and lone. The new system allows us to synthesize models with new objects (if required) to ensure that the complete model is consistent with its meta-model which normally contains quantified constraints on sets of objects of different classes. The solver finds the closest complete model in a given scope and returns the result as a recommendation for model completion.

The methodology described in the paper supports any meta-model with the following characteristics:

• With classes containing attributes of the basic types Integer, String, and Boolean • With classes containing references with variable multiplicities such as a..b to other classes in the meta-model • Constraints on the concepts in the meta-model that are expressible as ALLOY facts and predicates. These facts and predicates are constraints in first-order relational logic with quantifiers. We currently do not support floating-point attributes in meta-models. Although such properties can be approximated as integers. We also do not support the entire range of characters in unicode for string attributes. We either model strings as a sequence of characters or as an integer value. Higher-order constraints where a constraint is specified on another constraint is not supported. In a constraint language such as ALLOY this transforms to the expression of the unsupported higher-order relations (a tuple of relations) instead of supported first-order relations (a tuple of atoms).

IV. SPECIFYING A DOMAIN-SPECIFIC MODELLING LANGUAGE

In this section we explain the steps taken to declaratively specify a domain-specific modelling language. We use Finite State Machines (FSM) as a running example for a modelling language. The FSM modelling language is a visual language with circles representing states and directed arrows representing transitions between states. To define a modelling language and to generate a visual model editor from it requires three inputs:

1) A Meta-model as an AToM 3 Class Diagram (CD) String {"a", "b", "c", "event1", .., }

2) A Set of Alloy Facts on the concepts in the CD 3) A Visual Syntax We briefly describe the specifications of these aspects of the FSM language in the following sub-sections.

A. Meta-model

A model consists of objects and relationships between them. The meta-model of the modelling language specifies the types of all the objects and their possible inter-relationships in a specific domain. The type of an object is referred to as a class. The meta-model for the FSM modelling language is presented in Figure 2. The classes in the meta-model are FSM, State and Transition.

In this paper we use the Class Diagram formalism in AToM 3 for specifying a meta-model. The Class Diagram formalism can specify itself and hence exhibits the property of bootstrapping. We use the visual language notation of class diagrams to specify the meta-model for the FSM modelling language in Figure 2.

Each class in the meta-model has properties. A property is either an attribute or a reference. An attribute is of a primitive type which is either Integer, String, or Boolean. For instance, the attributes of the class State are isInitial and isFinal both of which are of primitive type Boolean. An example domain of values for the primitive attributes is given in Table I. The String variable can be a finite set consisting of a null string, and finite length strings that specify a set of strings. In this paper, we consider a finite domain for each attribute.

Describing the state of a class of objects with only primitive attributes is not sufficient in many cases. Modelling many real-world systems elicits the need to model complex relationships such as modelling that an object contains another set of objects or an object is related to another finite set of objects. This set of related objects is constrained by a multiplicity. When a class is related to another class, the related classes refer to each other via references. For instance, in Figure 2 Apart from attributes and references, objects can inherit properties from other classes. The attributes and references of a class called a superclass are inherited by subclasses. Similarly, a subclass inherits the references in the superclass. There is no inheritance in our FSM meta-model, nevertheless we consider transformation of inheritance relationships in the transformation presented in Section V.

B. Constraints on Meta-model

Constraints on a meta-model are not always conveniently specified using diagrams such as CDs. They are better expressed in a textual constraint language who's semantics have no side-effect (does not change the state of an object or structure of the model) on the meta-model or its instances (models). The OMG standard for constraint specification is the Object Constraint Language (OCL); however, in our current work we use first-order relational logic statements in the form of ALLOY facts. In this paper, we transform OCL constraints to ALLOY manually. In future, we intend to transform a subset of OCL to ALLOY using an automatic model transformation. This is a challenging task as OCL and ALLOY are very different in terms of what they express. OCL is a query language with no side-effects while ALLOY enforces certain values on objects and properties such that facts are always satisfied (if consistent). OCL is a language in higher-order logic without a thoroughly well-defined semantics. ALLOY on the other hand is a first-order relational logic language with quantifiers that has well-defined semantics for analysis. Bridging this gap in expressiveness is the hurdle in completely automating the OCL to ALLOY transformation. Therefore, we directly present ALLOY facts specified on a meta-model's objects and properties. A brief introduction to the ALLOY language is given in Section V-A.

In Table II we present the constraints on the FSM meta-model in natural language and as ALLOY facts.

The ALLOY signatures [START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF] used to specify the ALLOY facts are extracted from the FSM meta-model CD. This transformation is discussed in Section V. In the appendix we present the complete ALLOY model for the FSM modelling language. This ALLOY model can be loaded into the ALLOY Analyzer [START_REF] Jackson | [END_REF] for directly obtaining valid FSM models.

C. Visual Syntax

The final step (in specifying a DSML for synthesizing a model editor) we take is to specify the concrete visual syntax of the class of objects in the meta-model. The visual syntax specifies what an object looks like on a 2D canvas. An icon editor in AToM 3 is used to specify the visual syntax of the classes in the meta-model.

An icon editor is used to specify the visual syntax of meta-model concepts such as classes and relationships. The icon for State is a circle annotated with three of its attributes (isFinal, isInitial, and label). The connectors in the diagram are points of connection between State objects and Transition objects.

The visual syntax can also by dynamically changed based on the properties of the model. In an iconic visual modelling language such as FSM, the first step taken in specifying a visual syntax is drawing an icon that represents a class of objects. If needed it is annotated with text and its properties. Connectors are added to the visual object so that it can be connected to other objects if they are related.

V. TRANSFORMATION FROM META-MODEL AND A PARTIAL MODEL TO ALLOY

The transformation of a meta-model consists of transforming the Class Diagram of a domain-specific modelling language to ALLOY signatures and specification of other constraints as ALLOY facts. We first describe ALLOY and then explain our transformations using relevant examples in the following sections.

A. The ALLOY Language

We present ALLOY [START_REF] Jackson | [END_REF] [10] as a common constraint language equipped with a solver to help complete partial models. It is founded on quantified first-order logic with support for operators in relational calculus. The domain of a constraint model in ALLOY is given by a set of types called signatures. These signatures may contain a number of fields. Constraints may be added as facts or predicates to the ALLOY model to express additional invariants. ALLOY can be used to perform two kinds of analysis. First, we can solve a predicate to generate model instances that satisfy the facts in an ALLOY model. Second, we can use ALLOY to generation counter-examples for assertions that we assume to be true. These, analyses rely on the small scope hypothesis ( [START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF]): only a finite subspace is searched based on the assumption that if there is an instance or a counterexample there is one of small size. The rest of the article contains several commented or described ALLOY listings to give the reader a better intuition of the language.

B. Transformation of a Class Diagram

The transformation of a class diagram consists of the transformation of a class and its properties, transformation of the multiplicity constraints in the class diagram to ALLOY facts, transformation of containment constraints to ALLOY facts and finally the transformation of inheritance to an ALLOY extends relationship between ALLOY signatures. This results in a base ALLOY model. We discuss these transformations in detail below. The class contains properties which are either attributes or references to other objects. We see how these properties are transformed to ALLOY using our State class example. The attributes of the class are transformed to fields in the ALLOY signature. For instance, the label attribute of the State class is transformed to an ALLOY field of type Int. The ALLOY implementation contains a built-in implementation for the definition of integers (Int) for which a domain size can be set using a bit length. The attributes isFinal and isInitial are set as fields of type Bool (boolean values). ALLOY also contains a built-in implementation of Bool. There are several operations defined on the Bool and Int types in ALLOY which allow us to specify several complex constraints on such properties. An attribute of type String is transformed to a String type we define as follows in ALLOY: abstract sig Character{} one sig A extends Character {} one sig B extends Character {} ... sig String { content : seq Character } First, we describe an abstract signature Character and characters such as A,B,C,D,... that inherit from Character. However, the language in ALLOY prevents the use of digits. A substitute will be to use D1, D2,... for the digit 1,2,... respectively. A String signature is now defined as a sequence of characters. In this paper, we consider integers as simplified abstractions for strings and replace all possible string types to integers. After all, characters have a numerical encoding in a computer. To specify constraints on String objects also requires the specification of ALLOY functions on the String class.

1) Class and its

The references of a class are also transformed to fields in the ALLOY signature of its containing class. For instance, in the State object the references outgoingTransition and incomingTransition are transformed to an ALLOY field expressing a set of Transition instances. The set keyword indicates that there can be 0.. * Transition objects related to the State object. The other quantifiers like set are one meaning exactly one and lone meaning 0..1 objects. For instance, the reference fsmStates to one FSM object indicates that there must be exactly one container FSM for all State objects.

2) Multiplicity: If we want to specify a reference to a set of objects with multiplicity between a and b number of objects we synthesize an ALLOY fact. For instance, if we want to specify that a State object has at least 3 and at most 7 Transition object references as incoming transitions, we synthesize the following fact: 4) Inheritance: Inheritance between a superclass and subclass in a meta-model is transformed to an extends relation. The current FSM meta-model used as a running example in the paper does not contain an inheritance relationship. However, imagine a meta-model with an abstract class AbstractState which is inherited by two subclasses State and Composite. We first synthesize an abstract signature for the AbstractState class such as: The attributes isInitial and isFinal attributes are transformed to fields in ALLOY. The field isFinal : one Bool implies that all State objects have an isFinal property that can be either True or False. Similarly, the isInitial field in all State objects can be either True or False. These fields model an intial state, final states, and regular states in an FSM.

abstract

C. Specifying ALLOY facts on the Meta-model

We specify ALLOY facts using the names of the classes and properties on the AToM 3 class diagram in a text-box called Textual Meta-information in the meta-modelling language canvas. The specification of facts in ALLOY is possible because the ALLOY model we generate from the AToM 3 class diagram preserves the names of classes and properties enabling the use of the ALLOY constraint language for specification of constraints on the meta-model. All the facts in Table II are specified on the FSM class diagram. During the model completion process these facts are augmented to the base ALLOY model. This gives us a complete description of the meta-model.

D. Transformation of a Partial Model

We define a partial model as a graph of objects such that: (1) The objects are instances of classes in the modelling language metamodel (2) The partial model either does not conform to the language metamodel or its invariants expressed in a textual constraint language. A complete model on the other hand contains all the objects of the partial model and additional objects or property value assignments in new/existing objects such that it conforms both to the metamodel and its invariants.

A partial model, such as in Figure 3 (a), is automatically transformed to a set of ALLOY predicates by navigating it object by object in the canvas. We navigate all objects of a certain type and put them together as an ALLOY predicate. We want to keep the already specified properties for each object in the partial model but also allow for extensibility. For instance, for all the State objects in the partial model of Figure 3 (a) we create an ALLOY predicate as shown in the first predicate of Figure 3 (b). The ALLOY predicate states that there exists at least one State object s1, at least one State object s2, at least one State object s3, at least one State object s4 (representing the four State objects in the partial model), at least one Transition object t1, and at least one Transition object t2 such that s1,s2,s3,s4 are not equal and t1,t2 are not equal. The predicate also states that the Transition objects t1 and t2 are in the set of outgoing transitions for State object s1. Transition object t1 is in the set of incoming transitions of s1. The Transition object t2 is in the set of incoming transitions of s2. These sets are open for inclusion of new Transition objects. These predicates preserve all knowledge coming from the partial model while allowing the extension to relations to more objects.

We present a procedure to describe the transformation from the partial model to a set of ALLOY predicates below:

The following represents the procedure to synthesize an ALLOY predicate from a partial model 1) We start by synthesizing the header of a partial model: pred partialModel { 2) For all objects of o ij of type Class j in a partial model we synthesize an ALLOY expression: some o ij : Class j , ... | 3) For all objects of o ij of type Class j and all objects o kj of type Class j in a partial model we synthesize an ALLOY expression: o ij ! = o kj , each expression separated by and 4) For all defined attributes a ijk of o ij we synthesize the expression: o ij .a ijk = v, where v is the specified value separated by commas 5) For all defined references r ijk of o ij we synthesize the expression:

v in o ij .r ijk , where v is the object in the set of referred objects separated by commas 6) We finish the predicate by closing the brace.

E. Transforming ALLOY Model Completion Parameters

The user is provided with a dialog box to insert model completion parameters. Model completion parameters include finite scopes such as the upper bound on the number of objects of any class, or the upper-bound on the number of objects for each class, or the exact number of objects for each class, or a mixture of upper bounds and exact number of objects for different classes. The default scope is number of objects in the partial model. An other parameter is the number of solutions required S. This information is used to synthesize an ALLOY run command that is finally inserted in the ALLOY model. For example, if the partial model predicate is called partialModel1 and the user states that he wants exactly one object of class A, up to 10 objects of class B, and a scope of 5 for integers then the following run statements is synthesized: run partialModel1 for exactly 1 A, 10 B, 5 Int

If the number of objects in the partial model is N, then the default run command the editor generates is: run partialModel1 for N

VI. MODEL COMPLETION PROCESS

The model completion process integrated in the domain-specific model editor takes as input the AToM 3 class diagram, augmented ALLOY facts, and a partial model drawn in the model editor synthesized from the class diagram of a modelling language, and set of parameters to define the scope of the complete models to be synthesized. The process is invoked when a user draws a partial model in the modelling canvas and clicks on the Generate Completion Recommendations button.

The following steps are executed during the completion process:

1) An ALLOY model (ALS) file is synthesized containing the signature definitions of the classes in the AToM 3 class diagram and the facts corresponding to the multiplicity and containment constraints as described in Section V-B 2) The modelling language facts are augmented to the ALLOY model. These facts are specified as described in Section V-C

3) The partial model drawn in the model editor canvas is transformed to a predicate as described in Section V-D and augmented to the current ALLOY model 4) The model completion parameters are transformed to a run command (See Section V-E) and augmented to the ALLOY model giving us an adequate description for model completion. 5) An ALLOY API call is made to load the ALLOY model, parse it and store signatures, facts, predicates, run command as objects in memory. 6) An ALLOY API call is made to transform the first-order relational logic signatures, facts, predicates and model completion parameters to a finite Boolean CNF. 7) We then use the ALLOY API to invoke a third-party SAT solver such as ZChaff [START_REF] Mahajan | ZChaff2004: An Efficient SAT Solver[END_REF] or Minisat [START_REF] Een | An Extensible SAT-Solver[END_REF] [START_REF] Een | MiniSat A SAT Solver with Conflict-Clause Minimization[END_REF] to solve the Boolean CNF. 8) If a solution exists, then it is stored as an XML file. If a number of solutions (given by model completion parameter S)

are required then we attempt to produce S solutions and store them in XML Files. 9) The editor then loads and parses these XML files. The complete model recommendations are presented in the domainspecific model editor in their concrete visual syntax. The user can click on Next to scan through all possible completions. The results of model completion are also stored as model files representing graph structures in a temporary directory.

They can be loaded into the model editor when required or used by another program for transformation. It is important to note that the partial model is specified as a source of knowledge about what objects and properties that the user wants to absolutely see in the complete model. In the complete model we can see the intact contents of the partial model. However, the object identifiers of the partial model are not preserved in the complete model. We also do not perform pattern matching to identify the original partial model in the complete model, although such a mechanism can be incorporated if needed. In the default case we find the nearest-consistent complete model(s) to a given partial model.

If a solution is not found the ALLOY API returns a no solution found exception to AToM 3 (the invoker). We show this result in a dialog box in the AToM 3 environment. In our work we do not debug a partial model to find the exact source of inconsistency. This incurs a computational cost and time as we need to check every partial model predicate expression against the meta-model constraints to see which characteristics of the partial model leads to an inconsistency. We leave it to the user and depend on his/her expertise of the DSML to identify the inconsistent part of the partial model and correct it.

VII. EXAMPLES

In this section, we consider four examples of partial models in the FSM modelling language. The examples are shown in Figure 4 (a), 4 (b), 4 (c) , 4 (d) respectively. The synthesized predicates for these models are shown in Figures 4 (e), 4 (f) and 4 (g) , 4 (h). The example in Figure 4 (a) contains only one State object with none of the properties having been set. The example in Figure 4 (b) contains two State objects and a Transition object not connected. In Figure 4 (c) we consider a more complex model with several State and Transition objects with some properties set and some not. Finally, in Figure 4 (d) we present a model containing at least two State objects with isInitial set to True.

We perform the model completion of these models using two methods of setting parameters for completion:

• Scope : Here we specify a scope as a model completion parameter. The scope is a unique number that defines the maximum number of objects for all concepts in the meta-model. We choose the default scope to be 10. The corresponding ALLOY run statement generated is: pred partialModel {} run partialModel for 10 The partialModel predicate is empty and is simply used to obtain a complete model instance. We solve for up to a scope of 10 objects for each concept in the meta-model.

• Exact Number and/or Scope : Another mechanism to complete a model is to specify the exact number of objects and/or scope for objects we expect in the complete model. pred partialModel {} run partialModel for exactly 1 FSM, exactly 5 State, exactly 10 Transition, 5 int Here we find a solution for a partial model containing exactly 1 FSM object, exactly 5 State objects, exactly 10 Transition objects. Finally we set a bit-width for integers which is 5. This means that all integers range between -2 5 to 2 5 . All the above parameters were initially set in the synthesized AToM 3 modelling environment. The user is only exposed to the graphical syntax of the concepts in the meta-model and with a text-box to specify the exact number of objects or a scope. The [START_REF] Een | MiniSat A SAT Solver with Conflict-Clause Minimization[END_REF] from Chalmers University to solve the Boolean CNF synthesized from the ALLOY model. The time to obtain the solutions for the four partial models for the completion parameters is presented in Table III. We show the complete models themselves in Figure 5 with a scope of 10. Normally, there is more than one solution to a model completion. We show one of the possible solutions. We do not show that the complete models synthesized for the exact number of objects due to large size of the models. However, it is interesting to note in Table III that the time taken to synthesize models with the exact number of objects specified for each class is a lot faster even though the models are larger. This is because the additional knowledge about the number of objects makes the search space of the models much smaller, therefore allowing us to obtain a solution faster.

The complete model in Figure 5 (a) satisfies all the meta-model constraints such that the single State label has a unique value 7. There is at least one final state and exactly one initial state. In addition, the complete model contains a Transition object of the State to itself with an event 7. This new object added to the complete model does not violate any of the knowledge already present in the partial model.

The second complete model in Figure 5 The third complete model in 5 (c) contains a complex partial model with additional objects that preserve the knowledge in the partial model. We can scale up to a model with several hundred atoms using ALLOY to obtain results in a reasonable amount of time (for online user interaction with the modelling environment). An atom consists of any non-divisible entity in the ALLOY model. This includes objects and their properties connected via relations.

The fourth partial model in 4 (d) consisted of two initial State objects which is not permitted by the meta-model constraint which states that the FSM meta-model must contain only one initial State object. Therefore, the SAT solver was unable to find a complete model that could take into account the partial model.

A. Scalability Concerns

In this section we address the question of scalability in our approach. We identify two forms of scalability: 1) Scalability in the size of the meta-models such as in the number of classes, properties and complexity of constraints. 2) Scalability in the size of the models that conform to a meta-model. We first consider the scalability of a DSML meta-model. A meta-model can be scaled in terms of the concepts in the class diagram. This includes number of classes, number of attributes in a class, and number of references in a class. We can also scale the implicit constraints in the meta-model class diagram such as number of inheritances, containment relations, and range of multiplicities. Finally, we can scale a meta-model based on the number of facts and arity of each fact on the concepts in the meta-model and the coupling between these constraints. We cannot define the notion of scalability as an increase in the number of classes or attributes to observe greater time to solve. This is because change in constraints on classes and attributes can also lead to higher solution times. Even a simple language such as FSM contains some hard to solve constraints such as noUnreachableStates. This constraint states that any non-initial state will have to be connected to the initial State via at most three transitions. This is a finite approximation of the constraint that there can be no unreachable states in an FSM. The time taken to solve the partial model increases considerably if we increase the depth to 5. The scaled constraint is: The numerical results for model completion are summarized in Table III. In the columns T ime Scope and T ime Exact we present the time taken to solve a model completion for the unscaled meta-model with noUnreachableStates having a depth of 3. In the columns T ime ScopeScaled and T ime ExactScaled we present the time taken to solve a model completion for a scaled meta-model with noUnreachableStates having depth of 5. In general, when the exact number of objects (<= scope) is specified the time taken to solve a model is less than the time taken for a given scope. This is because, the solver knows in advance about the number of objects needed to satisfy all requirements in the model. While, when a scope is specified the solver starts from attempting to solve models with no objects for each signature and incrementally increases the number of objects of each signature until a solution is found. The time taken to solve a partial model for scaled meta-model is about 90 times that of time taken to solve a partial model expressed in an an unscaled version of the meta-model. These results are obtained by averaging and dividing the values shown in columns T ime ScopeScaled and T ime Scope for scope of 10. For exact values the time taken is about 70 times higher for the scaled version of the meta-model. These results are obtained by averaging and dividing the results in the columns T ime Exact and T ime ExactScaled .

fact
We summarize the discussion on the scalability of our approach to variations in meta-model structure. The scalability of this approach cannot be defined based on general rules that increase in the number of classes or properties will increase the time to find solutions. This we see due to the fact that simply increasing the depth of the noUnreachableStates constraint for a 3 class language such as FSM led to a many-fold increase in solution time. There is a complex inter-dependence between the classes, its properties, constraints on them, and the partial model. A thorough experimental study needs to be performed for a specific language where each factor such as number of classes, properties, relationships and constraints are varied over several ranges of values. This can then give us an idea about how a specific language performs using our approach for model completion. This study is out of the scope of our paper as we propose a first solution applicable to any modelling language.

The scalability of the size of the model instances of a meta-model is the second form of scalability. The question is for a given fixed DSML, what is the largest model we can obtain in a reasonable amount of time? For example, we synthesize a complete model from Partial Model 3 using the parameters: exactly 1 FSM object, exactly 8 State objects, exactly 10 Transition objects, 5 Int. The solution was found in 72930 ms (= 73 s). For interactive model completion 73 s could be too much when compared to almost instantaneous code completion in tools such as Eclipse. However, we give the user full control over the model completion parameters. With experience, he can put the correct number of objects he is looking for in the complete model resulting in a faster feedback. When our approach is used for automatic model synthesis such as for automatic test model generation [START_REF] Sen | On combining mullti-formalism knowledge to select test models for model transformaion testing[END_REF] or for design space exploration [START_REF] Neema | Constraint-Based Design Space Exploration and Model Synthesis[END_REF] we pay less attention to instantaneous responses. In these cases we obtain several hundred or even thousands of complete and effective models through several hours of model synthesis.

Scaling model completion also provides reflective insight into the design of the language itself. A language with constraints that are highly constrained or not optimally designed can perhaps take a long time to resolve. However, this does not rule out the fact that manual creation of the model will be easier for a user of the language. He/she can also be entangled in the complexity of the constraint while creating his model. Therefore, automatic model completion also reveals design flaws in modelling languages that can be corrected in parallel to obtain reasonable completion times.

VIII. CONCLUSION

We present a methodology to synthesize domain-specific model editors with meta-model directed model completion for domain-specific modelling languages. Our goal has been to provide model editors with completion capabilities similar to text or code editors in IDEs such as Eclipse or word processors such as Microsoft Word. A potential future application of our approach is generation of test models from partial knowledge. A DSML user draws a partial test model for testing a model transformation and subsequently sets model completion parameters. Then he/she clicks on a button to generate complete test models that are valid test cases for model transformations. Moreover, the model completions are displayed in the concrete visual syntax of the modelling language while evading all the details in the CNF, XML files, or other intermediate low-level representations. This aspect of our tool helps reduce the time to develop models in the modelling environment as the user only works in his domain language. The user does not need to manually transform his models to a different constraint language, solve his models and return the results to the editor anymore since the underlying model completion process is hidden from the user. After all, the goal of MDE is to leverage modelling to the highest possible level of abstraction.

Our approach uses a modelling language metamodel , the syntax, and its static semantics in the form of metamodel constraints to perform model completion. However, since the presented approach is modelling language independent we do not consider dynamic semantics often realized in a simulator for model completion. Nevertheless, we project several implications to simulation as it goes hand in hand with modelling. Model simulators, such as MATLAB/Simulink for causal block diagrams, often contain hard-coded declarative constraints or program statements that check and report on the validity of input models during simulation. For example, a causal block diagram simulator analyzes input models to detect cycles and warns the modeller. These statements that are integrated in simulator code come from heterogenous sources of knowledge such as domain experience, static/dynamic analysis, and testing. This gradual inclusion of model validity knowledge directly into simulator code makes them bulky and slow to execute. This approach also obscures the user from potentially using this knowledge to build correct models. Extracting knowledge from simulators and developing modelling language invariants to guide modellers to create invariant-validated models leverages a correct by construction philosophy. Further, using these invariants for automatic model completion of partial models makes the modelling and simulation process less error-prone as models are first checked and then completed to satisfy invariants before simulation.

Our lightweight approach is effective for small yet useful modelling languages. Time to complete models by the state of the art SAT solvers for about 50 objects in the model is not more than a few minutes for FSM. The completion time greatly depends on the complexity of the DSML. The time taken to obtain complete models also gives us insight about how restricted a DSML is and how it can be relaxed.

As future work we intend to run thorough performance experiments on a specific industry strength DSML. Such a DSML will have a larger meta-model with a several complex constraints. We will limit ourselves to the confines of first-order relational logic in ALLOY as the language to express constraints. We also wish to enlist the set of detailed requirements to synthesize DSML modelling environments with completion. For example, an interesting factor is user interaction time. If a complete model is not returned within a given time then the user can no longer make developments quickly. Other aspects of model completion include completion of models when two or more meta-models are involved, expression of partial models as invariants or constraints, and aiding the user by helping him/her set parameters for model completion.

3

 3 ) a) Specification of a meta-model i) Specification of a class diagram (AToM 3 class diagram in our case) ii) Specification of facts on the concepts in the class diagram (ALLOY facts in our case) b) Specification of a visual syntax in an icon editor (available in AToM 3 ) for concepts in the meta-model 2) Transformation of meta-model and visual syntax to a model editor a) Synthesis of an editor with buttons, menus and icons b) Synthesis of a drawing canvas with features such as automatic layout c) Synthesis of a clickable widget for model completion d) Synthesis of a dialog box for specifying model completion parameters 3) User interaction a) Drawing a partial model on the canvas b) Editing model completion parameters c) Click on a button to generate complete model(s) 4) Model Completion (hidden from user) a) Synthesis of base ALLOY model from the AToM 3 class diagram. b) Augmenting meta-model facts with base ALLOY model c) Synthesis of an ALLOY predicate from partial model and augmentation to base ALLOY model d) Synthesis of run commands from the model completion parameters and augmentation to current ALLOY model e)

  the classes State and Transition refer to each other via references annotated with unidirectional relationships. The multiplicity constraints are also annotated with the relationship. Containment relationships exist between the FSM class and the State and Transition classes. The black-fill ended arrow at the FSM Class signifies that all objects of type State and Transition are always inside an FSM object. There is exactly one FSM object that contains all State and Transition objects.

  fact multiplicity_incomingTransition { #State.incomingTransition >=3 and #State.incomingTransition<=7 } 3) Containment: We synthesize an ALLOY fact from a containment relation between two classes. For example, the fact that all Transition objects are contained in the FSM object is expressed as the following ALLOY fact: fact containmentTransition { Transition in FSM.transitions } All Transition objects in a complete model of the FSM modelling language now have a containment relation with the top-level FSM object.

  (b) originally was a partial model with two State objects and a Transition object. The complete model now contains two final State objects and exactly one initial State object. There is also an inclusion of a Transition object in the complete model. The synthesized model conforms to all meta-model constraints.

  APPENDIX I ALLOY MODEL SYNTHESIZED FROM FSM META-MODEL WITH FACTS AND PARTIAL MODEL PREDICATES , outgoingTransition: set Transition, incomingTransition: set Transition, and t1 in s1.outgoingTransition and s2.isInitial=True and s3.isInitial=True } run partialModel1_Fact for 10 run partialModel2_Fact for 10 run partialModel3_Fact for 10 run partialModel4_Fact for 10 run partialModel1_Fact for exactly 1 FSM, exactly 5 State, exactly 5 Transition, 5 int run partialModel2_Fact for exactly 1 FSM, exactly 5 State, exactly 5 Transition, 5 int run partialModel3_Fact for exactly 1 FSM, exactly 5 State, exactly 5 Transition, 7 int run partialModel4_Fact for exactly 1 FSM, exactly 5 State, exactly 5 Transition, 5 int ACKNOWLEDGMENT We thank the ANR Domino and European S-Cube Projects for research funding.

FigFig. 2 .

 2 Fig. 1. Methodology Overview

Fig. 3 .

 3 Fig. 3. (a) Partial Model (b) Synthesized Predicates from Partial Model

Fig. 4 .

 4 Fig. 4. (a) Partial model 1, (b) Partial model 2, (c) Partial model 3, (d) Partial model 4, (e) Predicate synthesized for Partial model 1 (f) Predicate synthesized for Partial model 2, (g) Predicate synthesized for Partial model 3, (f) Predicate synthesized for Partial model 4

Fig. 5 .

 5 Fig. 5. (a) Complete Model for Partial Model 1 (b) Complete Model for Partial Model 2 (c) Complete Model for Partial Model 3

TABLE II CONSTRAINTS

 II IN NATURAL LANGUAGE AND AS ALLOY FACTS

	Constraint Name and Definition	Alloy Fact
	exactlyOneFSM: There must be exactly
	one FSM object in a FSM model	fact exactlyOneFSM
		{
		one FSM
		}
	atleastOneFinalState : There must be at
	least one final state in a FSM model	fact at leastOneFinalState
		{
		some s:State|s.isFinal==True
		}
	exactlyOneInitialState : There must be
	exactly one initial state in the FSM model	fact exactlyOneInitialState
		{
		one s:State|s.isInitial==True
		}
	sameSourceDiffTarget : All transitions
	with the same source must have different	fact sameSourceDiffTarget
	target	{
		all t1:Transition,t2:Transition|
		(t1!=t2 and t1.source==t2.source) =>
		t1.target!=t2.target
		}
	setTargetAndSource : The target of an
	incoming transition to a State itself and	fact setTargetAndSource
	the source of all its outgoing transitions is	{
	the same State	all s:State |
		s.incomingTransition.target = s and
		s.outgoingTransition.source=s
		}
	noUnreachableStates: There can be no
	unreachable states in the FSM from an	fact noUnreachableStates
	initial state. Since, its a ternary constraint	{
	we approximate it by stating that a non-	all s:State| (s.isInitial==False) =>
	initial state can be reached from an initial	#s.incomingTransition >=1 and
	state up to a maximum depth of N (N=3	(s.isInitial==True and #State > 1) =>
	is the given example).	#s.outgoingTransition >=1 and
		s.outgoingTransition.target!=s
		}
	uniqueStateLabels : All State objects
	have unique labels	fact uniqueStateLabels
		{
		#State>1 => all s1:State,s2:State |
		s1!=s2=>s1.label != s2.label
		}

  Properties: A class is transformed to an ALLOY signature. Consider the State class in the FSM meta-model in Figure2. This class is transformed to the following ALLOY signature:

	sig State
	{
	label: Int,
	outgoingTransition: set Transition,
	incomingTransition: set Transition,
	fsmCurrentState: one FSM,
	fsmStates: one FSM,
	isFinal:one Bool,
	isInitial:one Bool
	}

  T ime Scope (s) T ime Exact T ime ScopeScaled T ime ExactScaled Macbook Pro laptop with an Intel Core 2 Duo processor running at 2.6 GHz clock speed and with 2 GB of RAM. We use the ALLOY analyzer API to invoke the SAT solver Minisat[START_REF] Een | An Extensible SAT-Solver[END_REF]

			TABLE III
			MODEL COMPLETION TIMES
	Partial Model Description
		(I=Inconsistent)
	Fig. 4 (a)	Only one State ob-	1.283	0.447	118.045	32.002
		ject with no proper-
		ties specified
	Fig. 4 (b)	Two State objects	1.289	0.496	115.994	31.488
		and one Transition
		object
	Fig. 4 (c)	Several State and	1.315	0.575	11.4301	32.517
		Transition objects
		with some properties
		specified and some
		not
	Fig. 4 (d)	Several State and	1.291 (I)	0.402 (I)	111.352 (I)	31.734 (I)
		Transition objects
		with two initial
		State objects
	model completions were performed on a


Sagar Sen
email: ssen@irisa.fr

Naouel Moha
email: moha@irisa.fr

Benoit Baudry
email: bbaudry@irisa.fr

Jean-Marc Jézéquel
email: jezequel@irisa.fr

Meta-model Pruning ⋆

Keywords: Meta-model pruning, GPML, DSML, UML, Kermeta, effective modelling domain, test input domain

Large and complex meta-models such as those of Uml and its profiles are growing due to modelling and inter-operability needs of numerous stakeholders. The complexity of such meta-models has led to coining of the term meta-muddle. Individual users often exercise only a small view of a meta-muddle for tasks ranging from model creation to construction of model transformations. What is the effective meta-model that represents this view? We present a flexible meta-model pruning algorithm and tool to extract effective meta-models from a meta-muddle. We use the notion of model typing for meta-models to verify that the algorithm generates a super-type of the large meta-model representing the meta-muddle. This implies that all programs written using the effective meta-model will work for the meta-muddle hence preserving backward compatibility. All instances of the effective meta-model are also instances of the meta-muddle. We illustrate how pruning the original Uml metamodel produces different effective meta-models.

Introduction

Development of complex software systems using modelling languages to specify models at high-levels of abstraction is the philosophy underlying Model-Driven Engineering (MDE). There are two schools of thought that advocate the development of such modelling languages : general-purpose modelling and domain-specific modelling. General-purpose modelling is leveraged by modelling languages such as the Unified Modelling Language (Uml) [START_REF]OMG: UML 2.0 Specfication[END_REF] with a large number of classes and properties to model various aspects of a software system using the same language. The Uml superstructure consists of subsets of visual modelling languages such as Uml use case diagrams, activity diagrams, state machines, and class diagrams to specify models of software systems. Uml is also extensible using the profiles mechanism [START_REF] Fuentes-Fernández | An introduction to uml profiles. UP-GRADE[END_REF] to provide modelling elements from specific domains such as services, aerospace systems, software radio, and data distribution [START_REF]OMG: UML Profile Catalog[END_REF]. One of the primary advantages of the Uml standard and its profiles is inter-operability between related domains in software development. On the other hand, domainspecific modelling promotes the construction of pure domain-specific modelling languages (DSMLs) [START_REF] Van Deursen | Domain-specific languages: an annotated bibliography[END_REF]. One of the main disadvantages of a DSML is finding the ideal scope for its long term use. Identifying the scope involves abstracting DSML concepts in very early stages of its development. This leaves little room for adding concepts later in the lifetime of DSML. Despite the existence of several DSMLs general-purpose modelling languages (GPMLs) such as Uml and its profiles are widely used to model complex software systems.

A major disadvantage of GPMLs such as the Uml is its ever growing complexity and size. The widely accepted modelling language Uml 2.0 has a specification document of about 1000 pages. The Uml 2.0 meta-model used to specify the language contains 246 classes and 583 properties. The large number of classes and properties with several complex dependencies between them has led to the coining of the censorious term meta-muddle [START_REF] Solberg | Navigating the metamuddle[END_REF] to characterize huge GPMLs such as the Uml.T h i sc r i t i c i s mo fUml can be attributed to the fact that it is an overspecification of the real modelling domain for a given application. For instance, if we intend to generate code from Uml state machines there is no need to expose modelling elements for activity diagrams, or use case diagrams to the code generator. In practice, each application of the Uml utilizes a subset of classes and properties in the Uml. What is the effective meta-model that contains these required classes and properties and all its mandatory dependencies? This is the question that intrigues us and for which we provide a solution.

In this paper, we present a meta-model pruning algorithm that takes as input a large meta-model and a set of required classes and properties, to generate a target effective meta-model. The effective meta-model contains the required set of classes and properties. The term pruning refers to removal of unnecessary classes and properties. From a graph-theoretic point of view, given a large input graph (large input meta-model) the algorithm removes or prunes unnecessary nodes (classes and properties) to produce a smaller graph (effective meta-model). The algorithm determines if a class or property is unnecessary based on a set of rules and options. One such rule is removal of properties with lower bound multiplicity 0 and who's type is not a required type. We demonstrate using the notion of model typing that the generated effective meta-model, a subset of the large meta-model from a set-theoretic point of view, is a super-type,f r o ma type-theoretic point of view, of the large input meta-model. This means that all programs written using the effective meta-model can also be executed for models of the original large meta-model. The pruning process preserves the meta-class names and meta-property names from the large input meta-model in the effective meta-model. This also implies that all instances (models) of the effective metamodel are also instances of the initial large input meta-model. All models of the effective meta-model are exchangeable across tools that use the large input meta-model as a standard. The extracted effective meta-model is very much like a transient DSML with necessary concepts for a problem domain at a given time. For example, we present an application of our algorithm to generate an effective meta-model to specify test models for a model transformation. The model transformation is developed by the French Spatial Agency (CNES) to transform Uml models to code for embedded systems.

The paper is organized as follows. In Section 2 we present the motivation for our work. We present related work in Section 3 that attempt to solve problems discussed in motivation. In Section 4 we present the meta-model pruning algorithm. We introduce model typing in Section 5 to show that the effective metamodel is indeed a super-type of the large meta-model. In Section 6 we present the application of meta-model pruning to obtain an effective meta-model for develop test models for a model transformation. We conclude and present future work in Section 7.

Motivation

The motivation for us to develop a meta-model pruning algorithm comes from observations made by us and others in various phases of the MDE process. We categorize our observations in the form of scenarios: Scenario 1: Input Domain of Model Transformations. A large meta-model such as that of Uml is the de facto input meta-model for a large number of model transformations or model processing programs/tools. However, many of these model transformations manipulate only a subset of the concepts defined in the input meta-model. There is a sparse usage of concepts in the input meta-model. For instance, code generators from Uml state machines [START_REF] Niaz | Code generation from uml statecharts[END_REF] normally use only the Uml class diagram and Uml state machine modelling elements. Therefore, often the large meta-model is not the real input meta-model of a model transformation. We illustrate this scenario in Figure 1 (a) where meta-model MM large specifies a large set of models but a model transformation MT is developed to process only a subset of this large set.

Scenario 2: Chain of Model Transformations. A consequence of not defining the real input domain of a model transformation is the non-compatibility/mismatch of outputs and inputs between transformations in chain. Consider a sequence of model transformations as shown in Figure 1 ) then you would want to transform the smallest possible input meta-model to a formal language for constraint satisfaction. Transforming the entire meta-model to a formal language will lead to a enormous constraint satisfaction problem. These large constraint satisfaction problems are often intractable. Solving smaller constraint satisfaction problems obtained from a small set of concepts and subsequently with fewer variables is relatively feasible. The above scenarios are only some of the many possible scenarios where a large meta-model defines the modelling domain while only a sub-domain is in use.

Related Work

There has always been a need to define the effective modelling domain for a given objective in MDE. This is true especially in the case of using large GPMLs such as Uml. In this section we present related work that deal with the problem of obtaining and using the effective modelling domain. We also pinpoint our contributions in this work.

Consider a fundamental task in MDE: Creating a model in a model editor such as in the Eclipse [START_REF] Frank | Eclipse Modeling Framework[END_REF] environment. A popular editor for Uml models is TOPCASED [START_REF] Farail | The TOPCASED project: a toolkit in open source for critical aeronautic systems design[END_REF]. The tool can be used to create Uml models such as class diagrams, state machines, activity diagrams, and use-case diagrams. If a modeller chooses to create class diagrams the tool presents the user with modelling elements for class diagrams such as classes and associations but not Uml state machine modelling elements such as states and transitions. Therefore, the tool inherently prevents the modeller from using an unnecessary part of the Uml meta-model. The hard-coded user interface in TOPCASED in fact presents the modeller with an effective modelling domain.

Model transformations on GPMLs such as Uml are built for specific tasks and can process only a sub-domain of its huge input domain. To filter the input to a model transformation pre-conditions [START_REF] Sendall | Model transformation: The heart and soul of modeldriven software development[END_REF] are specified in a constraint language such as Object Constraint Language (OCL) [START_REF]OMG: The Object Constraint Language Specification 2.0[END_REF] [START_REF] Lagarde | Extending ocl to ensure model transformations[END_REF]. Graph transformation based model transformation languages specify pre-conditions to apply a graph rewriting rule on a left-hand side model pattern [START_REF] Taentzer | Model transformation by graph transformation: A comparative study[END_REF]. Both pre-condition contracts and patterns are specified on the entire input meta-model while they refer to only a sub-domain.

In the paper [START_REF] Solberg | Navigating the metamuddle[END_REF] Solberg et al. present the issue of navigating the meta-muddle notably the Uml meta-model. They propose the development of Query/Extraction tools that allow developers to query the metamodel and to extract specified views from the metamodel. These tools should be capable of extracting simple derived relationships between concepts and more complex views that consist of derived relationships among many concepts. They mention the need to extract such views for different applications such as to define the domain of a model transformation and extracting a smaller metamodel from the concepts used in a model. Meta-modelling tools such as those developed by Xactium [START_REF] Limited | Language driven development and xmf-mosaic[END_REF] and Adaptive Software [19] possess some of these abilities. The authors of [START_REF] Solberg | Navigating the metamuddle[END_REF] propose the use of aspects to extract such views. However, the authors do not elaborate on the objectives behind generating such views.

In this paper, we present the following contributions emerging from our observations in MDE and survey of previous work:

-Contribution 1: We present a meta-model pruning algorithm to extract an effective meta-model from a large meta-model. -Contribution 2: We present an application of model typing to verify that an effective meta-model is indeed a super-type of the large input meta-model. All programs written using the effective meta-model are valid also for the original large meta-model. Our approach preserves meta-concept names in the effective meta-model from the large meta-model and hence all instances of the effective meta-model are instances of the large input meta-model.

Meta-model Pruning Algorithm

This section presents the meta-model pruning algorithm to transform a input meta-model to a pruned target meta-model. We acknowledge the fact there can be an entire family of pruning algorithms that can be used to prune a large meta-model to give various effective meta-models. In this paper, we present a conservative meta-model pruning algorithm to generate effective meta-models.

Our initial motivation to develop the algorithm was to help scale a formal method for test model generation [START_REF] Sen | On combining mullti-formalism knowledge to select test models for model transformaion testing[END_REF] in the case of large input meta-models. Therefore, given a set of required classes and properties the rationale for designing the algorithm was to remove a maximum number of classes and properties facilitating us to scale a formal method to solve constraints from a relatively small input meta-model. The set of required classes and properties are inputs that can come from either static analysis of a transformation, an example model, an objective function, or can be manually specified. Given these initial inputs we automatically identify mandatory dependent classes and properties in the meta-model and remove the rest. For instance, we remove all properties which have a multiplicity 0..* and with a type not in the set of required class types. However, we also add some flexibility to the pruning algorithm. We provide options such as those that preserve properties (and their class type) in a required class even if they have a multiplicity 0..*. In our opinion, no matter how you choose to design a pruning algorithm the final output effective meta-model should be a supertype of the large input meta-model. The pruning algorithm must also preserve identical meta-concept names such that all instances of the effective meta-model are instances of the large input meta-model. These final requirements ensure backward compatibility of the effective meta-model with respect to the large input meta-model.

Algorithm Overview

In Figure 3 The output of the algorithm is a pruned effective meta-model MM t = MM effective that contains all classes in C req , all properties in P req and their associated dependencies. Some of the dependencies are mandatory such as all super classes of a class and some are optional such as properties with multiplicity 0..* and whose class type is not in C req . A set of parameters allow us to control the inclusion of these optional properties or classes in order to give various effective meta-models for different applications. The output meta-model MM effective is a subset and a super-type of MM s . Type Operations: The operations on types used in this paper are: (a) t.isInstanceOf (X) that returns true if t is of type X or inherits from X.( b ) t.allSuperClasses(), if t.isInstanceOf (Class), returns the set of all its super classes t.Super including the super classes of its super classes and so on (multilevel). Definition 5. A property p is a 7-tuple p := (name,oC,type,lower, upper, opposite, isComposite), where name is a String identifier, oC is a reference to the owning class type, type is a reference to the property type, lower is a positive integer for the lower bound of the multiplicity, upper is the a positive integer for the upper bound of the multiplicity, opposite is a reference to an opposite property if any, and isComposite determines if the objects referenced by p are composite (No other properties can contain these objects).

Property Operations: The operations on properties in this paper is p.isConstrained() which returns true if constrained by any invariant i such that p ∈ i.P I . This is checked for all invariants i ∈ MM.Inv. Definition 6. An invariant I is a 3-tuple c := (T I ,P I , Expression), where T I is the set of types used in the invariant I and P I is the set of properties used in I.A nExpression is a function of T I and P I that has a boolean value. The Expression is often specified in a constraint language such as OCL [START_REF]OMG: The Object Constraint Language Specification 2.0[END_REF]. Note: Throughout the section, we use the relational dot-operator to identify an element of a tuple. For example, we want to refer to the set of all types in a meta-model we use the expression MM.T,or MM.P to refer to the set of all properties. Also, we do not consider user-defined meta-model operations or its argument signatures in our approach.

The Algorithm

The meta-model pruning algorithm (shown in Algorithm 1 has four inputs: (a) A source meta-model MM s (b) Initial set of required types T req (c) Initial set of required properties P req (d) The top-level container class type C top .(e)Parameter which is a Boolean array. Each element in the array corresponds to an option to add classes or properties to the required set of classes and properties. In this paper, we consider three such options giving us a Parameter vector of size 3.

The output of the algorithm is the pruned target meta-model MM t .W ebriefly go through the working of the algorithm. The target meta-model MM t is initialized with the source meta-model MM s . The algorithm is divided into three main phases: [START_REF]OMG: UML 2.0 Specfication[END_REF] Computing set of all required types T req in the meta-model, (2) Set of all required properties P req in the meta-model (3) Removing all types and properties not that are not in T req and P req .

The first phase of the algorithm involves the computation of the entire set of required types T req . The initial set T req is passed as a parameter to the algorithm. We add the top-level container class C top of MM s to the set of required types T req as shown in Step 2. In Step 3, we add the types of all required properties P req to the set of required types T req . In Step 4, we add types of all mandatory properties to T req . Types of all properties with lower bound greater than zero are added to the set of required types T req (Step 4.1). Similarly, if a property is constrained by an invariant in MM.Inv then its type is included in T req as shown in Step 4.2. If a property has an opposite type then we include the type of the opposite property, the owning class of the opposite property, and the type of the property to T req in Step 4.3. The algorithm provides three options to add types of properties with lower multiplicity zero and are of type Class, PrimitiveType, and Enumeration respectively. The inclusion of these types is depicted in Steps 4.4, 4.5, and 4.6. The truth values elements of the Parameter array determine if these options are used. These options are only examples of making the algorithm flexible. The Parameter array and the options can be extended with general and user-specific requirements for generating effective meta-models. After obtaining T req we add all its super classes across all levels to the set T req asshowninStep5.

The second phase of the algorithm consists of computing the set of all required properties P req . Inclusion of mandatory properties are depicted from Step 6.1 through Step 6.5. In Step 6.1, we add all properties whose type are in T req to P req . In Step 6.2 we add all properties whose owning class are in T req to P req . In Step 6.3, we add properties with lower multiplicity greater than zero to P req . If a property is constrained by a constraint in MM.Inv we add it to P req as depicted in Step 6.4. We add the opposite property of a required property to P req . Finally, based on the options specified in the Parameter array, the algorithm adds properties to P req with lower multiplicity zero and other characteristics.

In the third phase of the algorithm we remove types and properties from MM t . In Step 7, we remove all properties that are not in P req (Step 7.1) and all properties who's types are not in T req (Step 7.2). In Step 8, we remove all types not in T req . The result is an effective meta-model in MM t . In Section 5, we present model typing for meta-models to show that MM t is a super-type of MM s . As a result, any program written with MM t can be executed using models of MM s .

Implementation

The meta-model pruning algorithm has been implemented in Kermeta [START_REF] Muller | Weaving executability into objectoriented meta-languages[END_REF]. Kermeta is a language for specifying metamodels, models, and model transformations that are compliant to the Meta Object Facility(MOF) standard [START_REF]OMG: Mof 2.0 core specification[END_REF]. The tool supports input meta-models in the Eclipse Modelling Framework's (EMF) [START_REF] Frank | Eclipse Modeling Framework[END_REF] Ecore meta-modelling standard. The tool with usage instructions is available for download [START_REF] Sen | Meta-model pruning kermeta implementation[END_REF].

Algorithm 1 metamodelPruning(MM s , T req , P req , C top , Parameter)

Model Typing

In the section we describe the notion of model typing.W eu s em o d e lt y p i n gt o verify that meta-model pruning algorithm indeed generates a super-type of the input meta-model. Model typing corresponds to a simple extension to objectoriented typing in a model-oriented context [START_REF] Steel | On model typing[END_REF]. A model typing is a strategy for typing models as collections of interconnected objects while preserving type conformance, used as a criterion of substitutability.

The notion of model type conformance (or substitutability) has been adapted and extended to model types based on Bruce's notion of type groups and type group matching [START_REF] Bruce | Semantics-driven language design: Statically typesafe virtual types in object-oriented languages[END_REF]. The matching relation, denoted <#, between two metamodels defines a function of the set of classes they contain according to the following definition: Metamodel M' matches another metamodel M (denoted M' <# M )i ff for each class C in M, there is one and only one corresponding class C' in M' such that every property p and operation op in M.C matches in M'.C' respectively with a property p' a n da no p e r a t i o nop' with parameters of the same type as in M.C. This definition is adapted from [START_REF] Steel | On model typing[END_REF] and improved here by relaxing the constraint related of the name-dependent conformance on properties and operations.

Let's illustrate model typing with two metamodels M and M' given in Figures 4 and5. These two metamodels have properties and references that have different names. The metamodel M' has additional elements compared to the metamodel M. C1 <# COne because for each property COne.p of type D (namely, COne.name and COne.aCTwo), there is a matching property C1.q of type D' (namely, C1.id and C1.aC2 ), such that D' <# D. Thus, matching between classes may depend on the matching of their related dependent classes. As a consequence, the dependencies involved when evaluating model type matching are heavily cyclical [START_REF] Steel | Typage de modèles[END_REF]. The interested reader can find the details of matching rules used for model types in [START_REF] Steel | Typage de modèles[END_REF].

In Section 6, we illustrate the use of model typing integrated in the model transformation language Kermeta. We show that transformations written using the effective meta-model are also valid for models of the original large metamodel.

Application

We apply the meta-model pruning algorithm to generate an effective meta-model to specify test models for model transformations. The model transformation in our case study is from the French National Space Agency (CNES) to generate embedded systems code from a set of input models. The project is sponsored by the DOMINO project of ANR. We do not discuss the transformation in detail in this paper. We, however, highlight that the transformation uses a subset of Uml Activity diagram models. Our algorithm extracts an effective meta-model with the ultimate objective of testing the transformation. Testing can be done either by manually specifying test models or automatically generating them based on the technique in [START_REF] Sen | On combining mullti-formalism knowledge to select test models for model transformaion testing[END_REF]. We do not elaborate on the testing phase in this paper. ----------------------- The result of executing the algorithm with no options (no parameter specified) is the bare-minimum effective meta-model shown in Figure 6. A bare minimum effective meta-model , in our case, is sufficient to specify input models for the transformation. The meta-model is generated using an initial set of required classes C req . All elements of C req are provided as input the the pruning algorithm in the set T req such that C req ∈ T req . The classes in C req are shown within red boxes in Figure 6. The top-level class C top = Model is specified in a green-dashed box. In the pruned meta-model we observe that all disjoint subgraphs of the Uml meta-model are removed such as Uml State Machines, Uml Class Diagrams, and Uml Use Case Diagrams preserving only a subset of Uml Activity diagram.

We call the resulting MM effective of Uml, UmlCnes. We can verify that UmlCnes is a super-type of Uml using the notion of model types described in Section 5. The type checking rules for model types has been integrated into the typing system of the modelling and model transformation language Kermeta [START_REF] Muller | Weaving executability into objectoriented meta-languages[END_REF]. We can write a transformation using UmlCnes as the input domain as shown in listing 1. The package cnesTransfoMain calls the generateCode operation (in package cnesPackage)w i t ha nUml input model. However, the transformation is defined for the UmlCnes meta-model. The transformation will still execute since UmlCnes is a super-type of Uml. Test models can also be developed as instances of UmlCnes and transformed to Uml without loss of information.

The pruning algorithm is flexible. We briefly illustrate this by pruning Uml for the different options presented in the paper. In Table 1 we summarize the number of classes and properties for the different options of the meta-model pruning algorithm. The algorithm can be used to generate different effective meta-models with various applications. For example, another option that is not dealt with in this paper could be inclusion of all possible containers of a property to the set of required types. Options can be used to relax or tighten the pruning for applications where model transformations may evolve and use more concepts that initially perceived.

7C o n c l u s i o n

Deriving effective modelling domains is an ubiquitous need in MDE. There are several existing ways such as invariants, pre-conditions and hard-coded knowledge in model editors such as TOPCASED to obtain some form of an effective modelling domain. Most of these approaches patch up the modelling domain with constraints or code to obtain a constrained or effective modelling domain. In this paper, we present an algorithm to extract an effective meta-model from a large meta-model via pruning the large meta-model. Very much like extracting the meta-model of a transient DSML. The input to the algorithm includes the large meta-model and a set of required classes and properties. The algorithm finds all mandatory dependencies between these required concepts. It then prunes the large meta-model such that only the required concepts and its mandatory dependencies are preserved. The flexible algorithm also allows inclusions of non-mandatory properties. The effective meta-model typically has fewer classes and properties compared to the input meta-model and is a super-type of the input meta-model. Therefore, any program written for the effective meta-model will also accept models of the large meta-model. In the future, we would like to integrate the meta-model pruning algorithm to dynamically generate an effective meta-model in MDE tool chains such as editors and transformations. There is also scope for adding more options to control the generation of an effective meta-model for various objectives.

Scenario 4 :

 4 Software Process Modelling: Software process models contain several workflows. However, each workflow in a software process uses different sub-domains of a single shared meta-model such as the the Uml. These workflows are often realized by different people and at different times. There are several software process methodologies that use the Uml as the shared modelling language. The most popular of them is the Rational Unified Process (RUP)[START_REF] Kruchten | The Rational Unified Process: An Introduction[END_REF].

Fig. 2 .

 2 Fig. 2. (a) Workflows in RUP and its usage of Uml (b) Workflow of ACCORD and its use of Uml

  , we present an overview of the meta-model pruning algorithm. The inputs to the algorithm are: (1) A source meta-model MM s = MM large which is also a large meta-model such as the meta-model for Uml with about 246 Classes and 583 properties (in Ecore format) (2) A set of required classes C req (3) A set of required properties P req , and (4) A boolean array consisting of parameters to make the algorithm flexible for different pruning options.The set of required classes C req and properties P req can be obtained from various sources as shown in Figure3: (a) A static analysis of a model transformation can reveal which classes and properties are used by a transformation (b) The sets can be directly specified by the user (c) A test objective such as a set of partitions of the meta-model[START_REF] Fleurey | Towards dependable model transformations: Qualifying input test data[END_REF] is a specified on different properties which can be source for the set P req . (d) A model itself uses objects of different classes. These classes and their properties can be the sources for C req and P req .

Fig. 3 .Definition 2 .Definition 3 .

 323 Fig. 3. The Meta-model Pruning Algorithm Overview

Definition 4 .

 4 Am e t a -m o d e lMM is a 2-tuple MM := (T,P,Inv), where T is a finite set of class, primitive, and enumeration types, P is a set of properties, Inv is a finite set of invariants.

  Thus, C1 <# COne requires D' <# D : -COne.name and C1.id are both of type String. -COne.aCTwo is of type CTwo and C1.aC2 is of type C2,soC1 <# COne requires C2 <# CTwo. And, C2 <# CTwo is true because CTwo.element and C2.elem are both of type String.

Fig. 4 .

 4 Fig. 4. Metamodel M Fig. 5. Metamodel M'

  package cnesPackage ; require UMLCNES ; class Transfo<MT : UMLCNES> { // Code generator ... operation generateCode ( source : M T: : Model ) : Void is do ... end } Listing 1. Kermeta Transformation to Demonstr a t eu s eo fE ff e c t i v eM e t a -m o d e l

Fig. 6 .

 6 Fig. 6. The Effective Uml Activity Diagram Meta-model for the CNES Case Study

  1. Initialize target meta-model MMt MMt ← MMs 2. Add top-level class into the set of required types Treq ← Treq ∪ Ctop 3. Add types of required properties to set of required types Preq.each{p|Treq ← Treq ∪ p.type} 4. Add types of obligatory properties MMt.P.each{p| 4.1 (p.lower > 0) =⇒{ Treq ← Treq ∪ p.type} 4.2 (p.isConstrained(MMt.I nv)) =⇒{ Treq ← Treq ∪ p.type} 4.3 (p.opposite! = φ) = ⇒ { Treq ← Treq ∪ p.type, Treq ← Treq ∪ p.opposite.type, Treq ← Treq ∪ p.opposite.oC} Option 1: Property of type Class with lower bound 0 if Parameter[0] == True then 4.4 (p.lower == 0 and p.type.isInstanceOf (Class)) =⇒{ Treq ← Treq ∪ p.type} end if Option 2: Property of type PrimitiveType with lower bound 0 if Parameter[1] == True then 4.5 (p.lower == 0 and p.type.isInstanceOf (P rimitiveT ype)) =⇒ { Treq ← Treq ∪ p.type} end if Option 3: Property of type Enumeration with lower bound 0 if Parameter[2] == True then 4.6 (p.lower == 0 and p.type.isInstanceOf (Enumeration)) =⇒{ Treq ← Treq ∪ p.type}} end if 5. Add all multi-level super classes of all classes in Treq MMt.T .each{t | t.isInstanceOf (Class) = ⇒ t.allSuperClasses.each {s|Treq ← Treq ∪ s}} 6. Add all required properties to Preq MMt.P.each{p| 6.1 (p.type ∈ Treq)= ⇒{ Preq ← Preq ∪ p} 6.2 (p.oC ∈ Treq)= ⇒{ Preq ← Preq ∪ p} 6.3 (p.lower > 0) =⇒ Preq ← Preq ∪ p} 6.4 (p.isConstrained(MMt.I nv)) =⇒{ Preq ← Preq ∪ p} 6.5 (p.opposite!=φ)= ⇒{ Preq ← Preq ∪ p, Preq ← Preq ∪ p.opposite} Option 1: Property of type Class with lower bound 0 if Parameter[0] == True then 6.6 (p.lower == 0 and p.type.isInstanceOf (Class)) =⇒{ Preq ← Preq ∪ p} end if Option 2: Property of type PrimitiveType with lower bound 0 if Parameter[1] == True then 6.7 (p.lower == 0 and p.type.isInstanceOf (P rimitiveT ype)) =⇒ { Preq ←

	.
	Preq ∪ p}
	end if
	Option 3: Property of type Enumeration with lower bound 0
	if Parameter[2] == True then
	6.8 (p.lower == 0 and p.type.isInstanceOf (Enumeration)) =⇒{ Preq ← Preq ∪
	p}}
	end if
	7. Remove Properties
	MMt.P.each{p|
	7.1 p/ ∈ Preq =⇒ (t.P ← t.P -p)
	7.2 p.type / ∈ Treq =⇒ (t.P ← t.P -p)}
	}
	8. Remove Types
	MMt.T .each{t|t/ ∈ Treq =⇒ MMt.T ← MMt.T -t}

Table 1 .

 1 Meta-model Pruning Results for Options Original Uml No Option Option 1 Option 2 Option 3

	Number of Classes	246	31	31	31	31
	Number of Properties	583	15	26	30	30

Programme FP7/2007-2013 under grant agreement 215483 (S-Cube).