Jean-Bernard Stefani

Components as Location Graphs

This paper presents a process calculus framework for modeling ubiquitous computing systems and dynamic component-based structures as location graphs. A key aspect of the framework is its ability to model nested locations with sharing, while allowing the dynamic reconfiguration of the location graph, and the dynamic update of located processes.

database is destroyed so are its subcomponents). The cache component CC in this example is thus part of two wholes, the database DB and the virtual machine V 1 .

. In bigraphs, for instance, it would be natural to model the containment relationships in our database example as instances of sub-node relationships in bigraphs, because nodes correspond to agents in a bigraph. Yet this is not possible because the sub-node relation in a bigraph is restricted to form a forest. To model the above example as a bigraph would require choosing which containment relation (placement in a virtual machine or being a subcomponent of the database) to represent by means of the sub-node relation, and to model the other relation by means of bigraph edges. This asymetry in modelling is hard to justify for both containment relations are proper examples of whole-part relationships.

, where component containment is modelled as a form of superposition, and can be organized as an arbitrary graph. However, in CommUnity, possible reconfigurations in a component assemblage are described as graph transformation rules that are separate from the behavior of components, making it difficult to model reconfigurations initiated by the component assemblage itself.

To sum up, we are missing a model of computation that allows us to directly model both different forms of interactions and different forms of containment relationships between components; that supports both planned (i.e. built in component behaviors) and unplanned (i.e. induced by the environment) dynamic changes to these relationships, as well as to component behaviors.

Contribution.

In this paper, we introduce a model of computation, called G-Kells, which meets these requirements. We develop our model at a more concrete

Introduction

Motivations. Computing systems are increasingly built as distributed, dynamic assemblages of hardware and software components. Modelling these assemblages requires capturing different kinds of dependencies and containment relationships between components. The software engineering literature is rife with analyses of different forms of whole-part, aggregation or composition relationships, and of their attendants characteristics such as emergent property, overlapping lifetimes, and existential dependency [START_REF] Barbier | Formalization of the whole-part relationship in the unified modeling language[END_REF]. These analyses explicitly consider the possibility for a component to be shared at once between different wholes, an important requirement in particular if one expects to deal with multiple architectural views of a system.

Consider, for instance, a software system featuring a database DB and a client of the database C. The database comprises the following (sub)components: a cache CC, a data store DS and a query engine QE. Both data store and query engine reside in the same virtual machine V 0 , for performance reasons. Client and cache reside in another virtual machine V 1 , also for performance reasons. We have here a description which combines two architectural views, in the sense of [START_REF] Kruchten | Architectural blueprints -The 4+1 view model of software architecture[END_REF]: a logical view, that identifies two high-level components, the database DB and its client C, and the sub-components CC, QE and DS of the database, and a process view, that maps the above components on virtual machines V 0 and V 1 . We also have two distinct containment or whole-part relationships: being placed in a virtual machine, and being part of the DB database. A virtual machine is clearly a container: it represents a set of resources dedicated to the execution of the components it contains, and it manifests a failure dependency for all the components it executes (should a virtual machine fail, the components it contains also fail). The database DB is clearly a composite: it represents the result of the composition of its parts (cache, query engine, and data store) together with their attendant connections and interaction protocols; it encapsulates the behavior of its subcomponents; and its lifetime constrains those of its parts (e.g. if the level than bigraph theory, but we abstract from linguistic details by developing a process calculus framework parameterized by a notion of process and certain semantical operations. Computation in our model is carried out by located processes, i.e. processes that execute at named locations. Locations can be nested inside one another, and a given location can be nested inside one or more locations at once. Locations constitute scopes for interactions: a set of processes can interact when situated in locations nested within the same location. Behaviors of located processes encompass interaction with other processes as well as reconfiguration actions which may change the structure of the location graph and update located processes. In addition, the G-Kells framework supports a notion of dynamic priority that few other component models support, apart from those targeting real-time and reactive systems such as BIP and Ptolemy.

Outline. The paper is organized as follows. The framework we introduce can be understood as an outgrowth of our prior work with C. Di Giusto [START_REF] Di Giusto | Revisiting glues for component-based systems[END_REF], in which we proposed a process calculus interpretation of the BIP model. We recall briefly in Section 2 the main elements of this work, to help explain the extensions we introduce in our G-Kells framework. Section 3 presents the G-Kells framework and its formal operational semantics. Section 4 discusses the various features of the G-Kells framework, and related work. Section 5 concludes the paper.

CAB: a process calculus interpretation of BIP

One way to understand the G-Kells model we introduce in the next section, is to see it as a higher-order, dynamic extension of the CAB model [START_REF] Di Giusto | Revisiting glues for component-based systems[END_REF], a process calculus interpretation of the BIP model. We recall briefly in this section the main elements of CAB.

The CAB model captures the key features of the BIP model: (i) hierarchical components; (ii) composition of components via explicit "glues" enforcing multiway synchronization constraints between sub-components; (iii) priority constraints regulating interactions among components. Just as the BIP model, the CAB model is parameterized by a family P of primitive behaviors. A CAB component, named l, can be either a primitive component C = l[P ], where P is taken from P, or a composite component C = l[C 1 , . . . , C n G], built by composing a set of CAB components {C 1 , . . . , C n } with a glue process G. When l is the name of a component C, we write C.nm = l. We note C the set of CAB components, N l the set of location names, and N c the set of channel names. Behaviors in P are defined as labelled transition systems, with labels in N c .

In CAB, the language for glues G is a very simple language featuring:

-Action prefix ξ.G, where ξ is an action, and G a continuation glue (in contrast to BIP, glues in CAB can be stateful).

-Parallel composition G 1 | G 2 ,
where G 1 and G 2 are glues. This operator can be interpreted as an or operator, that gives the choice of meeting the priority and synchronization constraints of G 1 or of G 2 . -Recursion µ X. G, where X is a process variable, and G a glue.

Actions embody synchronization and priority constraints that apply to subcomponents in a composition. An action ξ consists of a triplet π • a • σ , where π is a priority constraint, σ is a synchronization constraint, and a is a channel name, signalling a possibility of synchronization on channel a. Priority and synchronization constraints take the same form: {l i : a i | i ∈ I}, where l i are location names, and a i are channel names. A synchronization constraint σ = {l i : a i | i ∈ I} requires each sub-component l i to be ready to synchronize on channel a i . Note that in a synchronization constraint σ = {l i : a i | i ∈ I} we expect each l i to appear only once, i.e. for all i, j ∈ I, if i = j then l i = l j . A priority constraint π = {l i : a i | i ∈ I} ensures each subcomponent named l i is not ready to synchronize on channel a i .

Example 1. A glue G of the form {l : a}; c; {l1 : a1, l2 : a2} .G specifies a synchronization between two subcomponents named l1 and l2: if l1 offers a synchronization on channel a1, and l2 offers a synchronization on a2, then their composition with glue G offers a synchronization on c, provided that the subcomponent named l does not offer a synchronization on a. When the synchronization on a takes place, implying l1 and l2 have synchronized with composite on a1 and a2, respectively, a new glue G is put in place to control the behavior of the composite.

Note that the same component l can appear in both the priority and the synchronization constraint of the same action ξ.

The operational semantics of the CAB model is defined as the labeled transition system whose transition relation, → ⊆ C × (N l × N c ) × C, is defined by the inference rules in Figure 2, where we use the following notations:

-C denotes a finite (possibly empty) set of components -C σ denotes the set {C i | i ∈ I}, i.e. the set of subcomponents involved in the multiway synchronization directed by the synchronization constraint σ in rule Comp. Likewise, C σ denotes the set

{C i | i ∈ I}. -C |= p {l i : a i | i ∈ I} denotes the fact that C meets the priority constraint π = {l i : a i | i ∈ I}, i.e. for all i ∈ I, there exists C i ∈ C such that C i .nm = l i and ¬(C i li:ai ---→), meaning there are no C such that C i li:ai ---→ C .
The Comp rule in Figure 2 relies on the transition relation between glues defined as the least relation verifying the rules in Figure 1.

The transition relation is well defined despite the presence of negative premises, for the set of rules in Figure 2 is stratified by the height of components, given by the function height, defined inductively as follows:

height(l[P ]) = 0 height(l[C G]) = 1 + max{height(C) | C ∈ C} Indeed, in rule Comp, if height(l[C G]) = n, then the components in C
that appear in the premises of the rule have a maximum height of n -1. The transitions relation → is thus the transition relation associated with the rules in Figure 2 according to Definition 3.14 in [START_REF] Bol | The meaning of negative premises in transition system specifications[END_REF], which is guaranteed to be a minimal and supported model of the rules in Figure 2 by Theorem 3.16 in [START_REF] Bol | The meaning of negative premises in transition system specifications[END_REF].

Act ξ.G ξ -→ G Rec G{ µ X. G /X } ξ -→ G µ X. G ξ -→ G Parl G ξ -→ G G | G2 ξ -→ G | G2 Parr G ξ -→ G G2 | G ξ -→ G2 | G
l:α --→ l[P ] Comp G π • a • σ -----→ G σ = {li : ai | i ∈ I} ∀i ∈ I, Ci l i :a i ---→ C i C |=p π l[C G] l:a --→ l[(C \ Cσ) ∪ C σ G ]
We now give some intuition on the operational semantics of CAB. The evolution of a primitive component C = l[P ], is entirely determined by its primitive behavior P , following rule Prim. The evolution of a composite component C = l[C G] is directed by that of its glue G, which is given by rules Act, Parl, Parr and Rec. Note that the rules for glues do not encompass any synchronization between branches G 1 and G 2 of a parallel composition G 1 | G 2 . Rule Comp specifies how glues direct the behavior of a composite (a form of superposition): if the glue G of the composite l[C G] offers action π • a • σ , then the composite offers action l : a if both the priority (C |= p π) and synchronization constraints are met. For the synchronization constraint σ = {l i : a i | i ∈ I} to be met, there must exist subcomponents {C i | i ∈ I} ready to synchronize on channel a i , i.e. such that we have, for each i, C i li:ai ---→ C i , for some C i . The composite can then evolve by letting each each C i perform its transition on channel a i , and by letting untouched the components in C not involved in the synchronization (in the rule Comp, the components C i in C are simply replaced by their continuation C i on the right hand side of the conclusion).

The CAB model is simple but already quite powerful. For instance, it was shown in [START_REF] Di Giusto | Revisiting glues for component-based systems[END_REF] that CAB(∅), i.e. the instance of the CAB model with no primi-tive components, is Turing complete1 . Priorities are indispensable to the result, though: as shown in [START_REF] Di Giusto | Revisiting glues for component-based systems[END_REF], CAB(∅) without priorities, i.e. where glue actions have empty priority constraints, can be encoded in Petri nets. We now turn to the G-Kells model itself.

3 G-Kells: a framework for location graphs

Syntax

The G-Kells process calculus framework preserves some basic features of the CAB model (named locations, actions with priority and synchronization constraints, multiway synchronization within a location) and extends it in several directions at once:

-First, we abstract away from the details of a glue language. We only require that a notion of process be defined by means of a particular kind of labelled transition system. The G-Kells framework will then be defined by a set of transition rules (the equivalent of Figure 2 for CAB) that takes as a parameter the transition relation for processes. -We do away with the tree structure imposed by CAB for components.

Instead, components will now form directed graphs between named locations, possibly representing different containment relationships among components. -In addition, our location graphs are entirely dynamic, in the sense that they can evolve as side effects of process transitions taking place in nodes of the graphs, i.e. locations. -CAB was essentially a pure synchronization calculus, with no values exchanged between components during synchronization. The G-Kells framework allows higher-order value passing between locations: values exchanged during synchronization can be arbitrary, including names and processes.

The syntax of G-Kells components is quite terse, and is given in Figure 3. The set of G-Kells components is called K. Let us explain the different constructs:

-0 stands for the null component, which does nothing.

l[P ] is a location named l, which hosts a process P . As we will see below, a process P can engage in interactions with other processes hosted at other locations, but also modify the graph of locations in various ways. l.r h denotes an edge in the location graph. An edge l.r h connects the role r of a location l to another location h.

-C 1 C 2 stands for the parallel composition of components C 1 and C 2 , which allows for the independent, as well as synchronized, evolution of C 1 and C 2 .

C ::= 0 | l[P ] | l.r h | C C l, h ∈ N l r ∈ Nr Fig. 3. Syntax of G-Kells components
A role is just a point of attachment to nest a location inside another. A role r of a location l can be bound, meaning there exists an edge l.r h attaching a location h to r, or unbound, meaning that there is no such edge. We say likewise that location h is bound to location l, or to a role in location l, if there exists an edge l.r h. Roles can be dynamically attached to a location, whether by the location itself or by another location. One way to understand roles is by considering a location l[P ] with unbound roles r 1 , . . . , r n as a frame for a composite component. To obtain the composite, one must complete the frame by binding all the unbound roles r 1 , . . . , r n to locations l 1 , . . . , l n , which can be seen as subcomponents. Note that several roles of a given location can be bound to the same location, and that a location can execute with unbound roles.

Locations serve as scopes for interactions: as in CAB, interactions can only take place between a location and all the locations bound to its roles, and a location offers possible interactions as a result. Unlike bigraphs, all interactions are thus local to a given location. One can understand a location in two ways: either as a composite glue superposing, as in CAB, priority and synchronization constraints on the evolution of its subcomponents, i.e. the locations bound to it, or as a connector, providing an interaction conduit to the components it binds, i.e. the locations bound to it. More generally, one can understand intuitively a whole location graph as a component C, with unbound locations acting as external interfaces for accessing the services provided by C, locations bound to these interfaces corresponding to subcomponents of C, and unbound roles in the graph to possible places of attachment of missing subcomponents.

We do not have direct edges of the form l h between locations to allow for processes hosted in a location, say l, to operate without knowledge of the names of locations bound to l through edges. This can be leveraged to ensure a process is kept isolated from its environment, as we discuss in Section 4. We maintain two invariants in G-Kells components: at any one point in time, for any location name l, there can be at most one location named l, and for any role r and location l, there can be at most one edge of the form l.r k.

Example 3. Let us consider how the example we discussed in the introduction can be modeled using G-Kells. Each of the different elements appearing in the configuration described (database DB, data store DS, query engine QE, cache CC, client C, virtual machines V0 and V1) can be modeled as locations, named accordingly. The database location has three roles s, q, c, and we have three edges DB.s DS, DB.q QE, DB.c CC, binding its three subcomponents DS, QE and CC. The virtual machines locations have two roles each, 0 and 1, and we have four edges V1.0 C, V1.1 CC, V0.0 DS, V0.1 QE, manifesting the placement of components C, CC, DS, QE in virtual machines. Now, the database location hosts a process supporting the semantics of composition between its three subcomponents, e.g. the cache management protocol directing the interactions between the cache and the other two database subcomponents2 . The virtual machine locations host processes supporting the failure semantics of a virtual machine, e.g. a crash failure semantics specifying that, should a virtual machine crash, the components it hosts (bound through roles 0 and 1) should crash similarly. We will see in Section 4 how this failure semantics can be captured.

Operational semantics

We now formally define the G-Kells process calculus framework operational semantics by means of a labelled transition system.

Names, values and environments

Notations. We use boldface to denote a finite set of elements of a given set. Thus if S is a set, and s a typical element of S, we write s to denote a finite set of elements of S, s ⊆ S. We use to denote an empty set of elements. We write ℘ f (S) for the set of finite subsets of a set S. If S 1 , S 2 , S are sets, we write S 1 S 2 = S to mean S 1 ∪ S 2 = S and S 1 , S 2 are disjoint, i.e. S 1 and S 2 form a partition of S. We sometimes write s,

s to denote {s} ∪ s. If C is a G-Kell component, Γ (C) represents the set of edges of C. Formally, Γ (C) is defined by induction as follows : Γ (0) = ∅, Γ (l[P ]) = ∅, Γ (l.r h) = {l.r. h}, Γ (C 1 C 2 ) = Γ (C 1 ) ∪ Γ (C 2 ).
Names and Values. We use three disjoint, infinite, denumerable sets of names, namely the set N c of channel names, the set N l of location names, and the set N r of role names. We set N = N c ∪ N l ∪ N r . We note P the set of processes. We note V the set of values. We posit the existence of three functions fcn : V → N c , fln : V → N l frn : V → N r that return, respectively, the set of free channel names, free location names, and free role names occurring in a given value. The restriction of fcn (resp. fln, frn) to N c (resp. N l , N r ) is defined to be the identity on N c (resp. N l , N r ). The function fn : V → N , that returns the set of free names of a given value, is defined by fn(V ) = fcn(V )∪fln(V )∪frn(V ). The sets N , P and V, together with the functions fcn, fln, and frn, are parameters of the G-Kells framework. We denote by E the set of edges, i.e. the set of triples l.r h of N l × N r × N l . We stipulate that names, processes, edges and finite sets of edges are values:

N ∪ P ∪ E ∪ ℘ f (E) ⊆ V.
We require the existence of a relation match ⊆ V 2 , used in ascertaining possible synchronization.

Environments. Our operational semantics uses a notion of environment. An environment Γ is just a subset of N ∪ E, i.e. a set of names and a set of edges. The set of names in an environment represents the set of already used names in a given context. The set of edges in an environment represents the set of edges of a location graph. the set of environments is noted G.

Processes

Process transitions. We require the set of processes to be equipped with a transition system semantics given by a labelled transition system where transitions are of the following form:

P π • α • σ • ω -------→ P
The label π • α • σ • ω comprises four elements: a priority constraint π (an element of Pr), an offered interaction α, a synchronization constraint σ (an element of S), and an effect ω (an element of A). The first three are similar in purpose to those in CAB glues. The last one, ω, embodies queries and modifications of the surrounding location graph.

An offered interaction α takes the form {a i V i | i ∈ I}, where I is a finite index set, a i are channel names, and V i are values.

Evalution functions. We require the existence of evaluation functions on priority constraints (eval π ), and on synchronization constraints (eval σ ) of the following types eval π : G × N l × Pr → ℘ f (N l × N r × N c ), and eval σ :

G × N l × S → ℘ f (N l × N r × N c × V).
The results of the above evaluation functions are called concrete (priority or synchronization) constraints. The presence of evaluation functions allows us to abstract away from the actual labels used in the semantics of processes, and to allow labels used in the operational semantics of location graphs, described below, to depend on the environment and the surrounding location graph.

Example 4. One can, for instance, imagine a kind of broadcast synchronization constraint of the form * : a V , which, in the context of an environment Γ and a location l, evaluates to a constraint requiring all the roles bound to a locations in Γ to offer an interaction on channel a, i.e.: evalσ(Γ, l, * : a

V ) = {l.r : a V | ∃h, l.r h ∈ Γ }.
We require the existence of an evaluation function on effects (eval ω ) with the type eval ω :

G × N l × A → ℘ f (E)
, where E is the set of concrete effects. A concrete effect can take any of the following forms, where l is a location name:

l : newl(h, P ), l : newch(c), l : newr(r), respectively to create a new location named h with initial process P , to create a new channel named c, and to create a new role named r. l : add(h, r, k), l : rmv(h, r, k), respectively to add and remove a graph edge h.r k to and from the surrounding location graph. l : gquery(Γ ), to discover a subgraph Γ of the surrounding location graph.

l : swap(h, P, Q), to swap the process P running at location h for process Q.

l : kill(h), to remove location h from the surrounding location graph.

Concrete effects embody the reconfiguration capabilities of the G-Kells framework. Effects reconfiguring the graph itself come in pairs manifesting introduction and elimination effects: thus, adding and removing a node (location) from the graph (newl, kill), and adding and removing an edge from the graph (add, rmv). Role creation (newr) is introduced to allow the creation of new edges. Channel creation (newch) allows the same flexibility provided by name creation in the π-calculus. The swap effect (swap) is introduced to allow the atomic update of a located process. The graph query effect (gquery) is perhaps a bit more unorthodox: it allows a form of reflection whereby a location can discover part of its surrounding location graph. It is best understood as an abstraction of graph navigation and query capabilities which have been found useful for programming reconfigurations in component-based systems [START_REF] David | Fpath and fscript: Language support for navigation and reliable reconfiguration of fractal architectures[END_REF].

Operational semantics of location graphs

Transitions. The operational semantics of location graphs is defined by means of a transition system, whose transition relation → is defined, by means of the inference rules presented below, as a subset of G ×K×L×K. Labels take the form π • σ • ω , where π and σ are located priority and synchronization constraints, respectively, and ω is a finite set of located effects (for simplicity, we reuse the same symbols than for constraints and effects). The set of labels is noted L.

A located priority constraint π is just a concrete priority constraint, and takes the form {l i .r i : a i | i ∈ I}, where I is a finite index set, with l i , r i , a i in location, role and channel names, respectively. A located synchronization constraint takes the form {u j : a j V j }, where a j are channel names, u j are either location names l j or pairs of location names and roles, noted l j .r j , and V j are values. Located effects can take the following forms: l : rmv(h, r, k), l : swap(h, P, Q), l : kill(h), h : rmv(h, r, k), h : swap(h, P, Q), and h : kill(h), where l, h, k are location names, r is a role name, P, Q are processes. The predicate located on E identifies located effects. In particular, for a set ω ⊂ E, we have located(ω) if and only if all elements of ω are located.

A transition Γ, C, π • σ • ω , C ∈→ is noted Γ C π • σ • ω
------→ C and must obey the folowing constraint: → • is defined as the least relation satisfying the rules in Figure 4, where we use the following notation: if α = {a i V i | i ∈ I}, then l : α = {l : a i V i | i ∈ I}, and if α = , then l : α = .

-If Γ = u ∪ ∆,
Rule Act simply expresses how process transitions are translated into location graph transitions, and process level constraints and effects are translated into located constraints and concrete effects, via the evaluation functions introduced above. Rule NewL specifies the effect of an effect l : newl(h, Q) , which creates a new location h[Q]. Notice how effect l : newl(h, Q) is removed from the set of effects in the transition label in the conclusion of the rule: auxiliary relation -→ • is in fact used to guarantee that a whole set of concrete effects are handled atomically. All the rules in Figure 4 except Act, which just prepares for the evaluation of effects, follow the same pattern. Rules NewC and NewR specify the creation of a new channel name and of a new role name, respectively. The rules just introduce the constraint that the new name must not be an already used name in the environment Γ . Our transitions being in the early style, the use of the new name is already taken into account in the continuation location graph C (in fact in the continuation process P appearing on the left hand side of the instance of rule Act that must have led to the building of C). This handling of new names is a bit unorthodox but it squares nicely with the explicitly indexed labelled transition semantics of the π-calculus given by Cattani and Sewell in [START_REF] Cattani | Models for name-passing processes: interleaving and causal[END_REF]. Rule AddE specifies the effect of adding a new edge to the location graph. Rule Gquery allows the discovery by processes of a subgraph of the location graph. In the rule premise, we use the notation Γ l to denote the set of edges reachable from location l, formally:

Γ L = {h.r k ∈ Γ | l + Γ h}
, where l + Γ h means that there exists a non-empty chain l.r l 1 , l 1 .r 1 l 2 , . . . , l n-1 .r n-1 l n , l n .r n h, with n ≥ 1, linking l to h in the location graph Γ . As in the case of name creation rules, the exact effect on processes is left unspecified, the only constraint being that the discovered graph be indeed a subgraph of the location graph in the environment.

Transition relation -→. The transition relation -→ is defined by the rules in Figure 5. We use the following notations and definitions in Figure 5: -Function seval is defined by induction as follows (for any l, r, h, V, σ, σ ):

seval(Γ, σ) = seval(Γ, σ ) if σ = {l.r : a V , h : a W } ∪ σ ∧ l.r h ∈ Γ ∧ match(V, W ) seval(Γ, σ) = σ otherwise
-Function aeval is defined by induction as follows (for any l, r, h, k, P, Q, σ, σ ):

aeval(Γ, σ) = aeval(Γ, σ ) if σ = {l : swap(h, P, Q), swap(h, P, Q)} ∪ σ aeval(Γ, σ) = aeval(Γ, σ ) if σ = {l : rmv(h, r, k), rmv(h, r, k)} ∪ σ aeval(Γ, σ) = aeval(Γ, σ ) if σ = {l : kill(h), kill(h)} ∪ σ aeval(Γ, σ) = σ otherwise Act• P π • α • σ • ω --------→ P π• = evalπ(Γ, l, π) σ• = evalσ(Γ, l, σ) ω• = evalω(Γ, l, ω) Γ l[P ] π• • l:α∪σ• • ω• -----------→• l[P ] NewL Γ l[P ] π • σ • l:newl(h,Q),ω -------------→• C h ∈ Γ Γ l[P ] π • σ • ω ------→• C h[Q] NewC Γ l[P ] π • σ • l:newch(c),ω ------------→• C c ∈ Γ Γ l[P ] π • σ • ω ------→• C NewR Γ l[P ] π • σ • l:newr(r),ω -----------→• C r ∈ Γ Γ l[P ] π • σ • ω ------→• C AddE Γ l[P ] π • σ • l:add(h,r,k),ω -------------→• C ¬(∃k, h.r k ∈ Γ ) Γ l[P ] π • σ • ω ------→• C h.r k Gquery Γ l[P ] π • σ • l:gquery(∆),ω -------------→• C ∆ ⊆ Γ l Γ l[P ] π • σ • ω ------→• C Fig. 4. Rules for auxiliary relation -→• Swap Γ l[P ] • • swap(l,P,Q) -----------→ l[Q] Kill Γ l[P ] • • kill(l) --------→ 0 Rmv Γ h.r k • • rmv(h,r,k) ----------→ 0 Act Γ l[P ] π • σ • ω ------→• C located(ω) Γ l[P ] π • σ • ω ------→ C Comp Γ = Γ ∪ Γ (C1) ∪ Γ (C2) π = π1 ∪ π2 fn(Γ ) ∆1 ∆2 = N Γ C1 C2 π |= π σ = seval(Γ , σ1 ∪ σ2) ω = aeval(Γ , ω1 ∪ ω2) Γ ∪ ∆1 C1 π 1 • σ 1 • ω 1 --------→ C 1 Γ ∪ ∆2 C2 π 2 • σ 2 • ω 2 --------→ C 2 Γ C1 C2 π • σ • ω ------→ C 1 C 2 Fig. 5. Rules for transition relation -→ -Assume π = {l i .r i : a i | i ∈ I}, then C π is obtained by replacing in C all the locations {l i [P i ] | i ∈ I} with locations {l i [ P i ] | i ∈ I}
, where P is defined by the LTS obtained from that of P by the following rule:

Trim P π • α • σ • ω -------→ P P • α • σ • ω -------→ P
In other terms, C π is obtained by disregarding the priority constraints that are generated by locations l i mentioned in the priority constraint π.

-Γ C |= {l i .r i : a i | i ∈ I} means that, for all i ∈ I, Γ C |= l i .r i : a i . We write Γ C |= l.r : a to mean that ¬(∃h, π, σ, ω, V, C , l.r h ∧ Γ C π • l:a V ,σ • ω ----------→ C )
Rule Swap specifies that at any point in time a location can see its process swapped for another. Likewise, rules Kill and Rmv specify that at any point in time a location or an edge, respectively, can be removed from a location graph. Rule Act specifies the termination of the atomic execution of a set of concrete effects. All the effects remaining must be located effects, which expect some counterpart (provided by the rules Swap, Kill, and Rmv, when invoking rule Comp) to proceed.

Rule Comp is the workhorse of our operational semantics of location graphs. It specifies how to determine the transitions of a parallel composition C 1 C 2 , by combining the priority constraints, synchronization constraints and effects obtained from the determination of contributing transitions from C 1 and C 2 . The latter takes place in extended environment Γ , that contains the original environment Γ , but also the edges present in C 1 and C 2 , defined as Γ (C 1 ) and Γ (C 2 ), respectively. To ensure the names created as side effects of C 1 and C 2 transitions are indeed unique, the determination of the contributing transition of C 1 takes place in an environment where the already used names include those in Γ as well as those in ∆ 1 , which gathers names that may be created as a side effect of the contributing transition of C 2 . Likewise for determining the contributing transition of C 2 . The constraint fn(Γ ) ∆ 1 ∆ 2 = N ensures that names in ∆ 1 and ∆ 2 are disjoint, as well as disjoint from the already used names of fn(Γ ).

The original aspect of rule Comp lies with the computation of located synchronization contraints and effects resulting from the parallel composition of G-Kells components: we allow it to be dependent on the global environment Γ with the clauses σ = seval(Γ , σ 1 ∪ σ 2 ) and ω = aeval(Γ , ω 1 ∪ ω 2 ), which, in turn, allows to enforce constraints dependent on the location graph as in the definition of function seval. In fact, as we discuss in Section 4 below, we can envisage instances of the framework where different types of location-graphdependent constraints apply.

The use of environments in rule Comp to obtain a quasi-compositional rule of evolution is reminiscent of the use of environment and process frames in the parallel rule of the ψ-calculus framework [START_REF] Bengtson | Psi-calculi: a framework for mobile processes with nominal data and logic[END_REF]. We say our rule Comp is quasicompositional for the handling of priority is not compositional: it relies on the global condition Γ C 1 C 2 π , which requires computing with (an altered view of) the whole composition. The use of the • -operator in rule Comp is reminiscent of the handling of priorities in other works [START_REF] Cleaveland | Priority in process algebra[END_REF]. An easy way to turn rule Comp into a completely compositional rule would be to adopt a more "syntactic" approach, defining C π to be obtained by replacing all locations l[P ] in C by their trimmed version l[ P ], and defining environments to include information on possible actions by trimmed locations. On the other hand, we can also adopt a purely "semantic" (albeit non-compositional) variant by defining C π to be just C. However, in this case, we don't know whether the completeness result in Theorem 1 below still stands.

Example 5. To illustrate how the rules work, consider the following process transitions:

P • • * :a V • newl(h,P ) ---------------→ P P1 • a V 1 • • {newl(h 1 ,P 1 )} -----------------→ P 1 P2 • a V 2 • • ---------→ P 2
Let Γ = {l, l1, l2} ∪ {l.r1 l1, l.r2 l2}, and let ∆, ∆ be such that ∆ ∆ = N \ {l, l1, l2, h, h1}. We assume further that match(V, V1) and match(V, V2), that all names l, l1, l2, h, h1 are distinct, and that

evalσ(Γ, l, * : a V ) = {l.r1 : a V , l.r2 : a V } evalω(Γ, l, {newl(h, P )}) = {l : newl(h, P )} evalω(Γ, l1, {newl(h1, P1)}) = {l1 : newl(h1, P1)} evalω(Γ, l2, ) = evalπ(Γ, l, ) = evalπ(Γ, l1, ) = evalπ(Γ, l2, ) = Applying rule Act•, we get Γ ∪ {h1}, ∆ l[P ] • {l.r 1 :a V ,l.r 2 :a V } • {l:newl(h,P )} --------------------------→• l[P ] Γ ∪ {h}, ∆ l1[P1] • l 1 :a V 1 • {l 1 :newl(h 1 ,P 1 )} -------------------→• l1[P 1 ] Γ ∪ {h}, ∆ l2[P2] • l 2 :a V 2 • ---------→• l2[P 2 ]
Applying rule NewL, we get

Γ ∪ {h1}, ∆ l[P ] • {l.r 1 :a V ,l.r 2 :a V } • ------------------→• l[P ] h[P ] Γ ∪ {h}, ∆ l1[P1] • {h 1 :a V 1 } • -----------→• l1[P 1 ] h1[P1]
Applying rule Act we get

Γ ∪ {h1}, ∆ l[P ] • {l.r 1 :a V ,l.r 2 :a V } • ------------------→ l[P ] h[P ] Γ ∪ {h}, ∆ l1[P1] • {l 1 :a V 1 } • -----------→ l1[P 1 ] h1[P1] Γ ∪ {h}, ∆ l2[P2] • {l 2 :a V 2 } • -----------→ l2[P 2 ]
Finally, applying rule Comp we get

Γ ∪ {h}, ∆ l1[P1] l2[P2] • {l 1 :a V 1 ,l 2 :a V 2 } • -----------------→ l1[P 1 ] h1[P1] l2[P 2 ] Γ l[P ] l1[P1] l2[P2] • • -----→ l[P ] h[P ] l1[P 1 ] h1[P1] l2[P 2 ]
Transition relation -→ as a fixpoint. Because of the format of rule Comp, which does not prima facie obey known SOS rule formats [START_REF] Mousavi | SOS formats and meta-theory: 20 years after[END_REF], or conform to the standard notion of transition system specification [START_REF] Bol | The meaning of negative premises in transition system specifications[END_REF], the question remains of which relation the rules in Figures 4 and5 define. Instead of trying to turn our rules into equivalent rules in an appropriate format, we answer this question directly, by providing a fixpoint definition for -→. We use the fixpoint construction introduced by Przymusinski for the three-valued semantics of logic programs [START_REF] Przymusinski | The well-founded semantics coincides with the three-valued stable semantics[END_REF].

Let be the ordering on pairs of relations in T = G × K × L × K defined as:

R 1 , R 2 T 1 , T 2 ⇐⇒ R 1 ⊆ T 1 ∧ T 2 ⊆ R 2
As products of complete lattices, (T , ⊆) and (T 2 , ) are complete lattices [START_REF] Davey | Introduction to Lattices and Order[END_REF].

One can read the Comp rule in Figures 5 as the definition of an operator F : T 2 → T 2 which operates on pairs of sub and over-approximations of →. Let → 0 be the relation in T 2 obtained as the least relation satisfying the rules in Figures 4 and5, with rule Comp omitted. Operator F is then defined as follows:

F(R1, R2) = (→0 ∪ R1 ∪ r(→0 ∪ R1, R2), R2 ∩ r(R2, →0 ∪ R1)) r(R1, R2) = {t ∈ T | t = (Γ, C1 C2, π • σ • ω , C 1 C 2 ) ∧ comp(Γ, C1, C2, π, σ, ω, C 1 , C 2 , R1, R2)}
where the predicate comp is defined as follows:

comp(Γ, C 1 , C 2 , π, σ, ω, C 1 , C 2 , R 1 , R 2 ) ⇐⇒ ∃π 1 , π 2 , σ 1 , σ 2 , ω 1 , ω 2 , ∆ 1 , ∆ 2 , Γ , Γ = Γ ∪ Γ (C 1 ) ∪ Γ (C 2 ) ∧ π = π 1 ∪ π 2 ∧ fn(Γ ) ∆ 1 ∆ 2 = N ∧ σ = seval(Γ , σ 1 ∪ σ 2 ) ∧ ω = aeval(Γ , ω 1 ∪ ω 2 ) ∧ (Γ ∪ ∆ 1 , C 1 , π 1 • σ 1 • ω 1 , C 1 ) ∈ R 1 ∧ (Γ ∪ ∆ 2 , C 2 , π 2 • σ 2 • ω 2 , C 2 ) ∈ R 1 ∧ Γ C 1 C 2 π |= R2 π
where Γ C |= R {l i : a i | i ∈ I} means that, for all i ∈ I, Γ C |= R l i : a i , and where Γ C |= R l : a stands for:

¬(∃π, σ, ω, V, C , (Γ, C, π • {l : a V } ∪ σ • ω , C ) ∈ R)
The definition of the predicate comp mimics the definition of rule Comp, with all the conditions in the premises appearing as clauses in comp, but where the positive transition conditions in the premises are replaced by transitions in the sub-approximation R 1 , and negative transition conditions (appearing in the Γ C 1 C 2 π |= π condition) are replaced by equivalent conditions with transitions not belonging to the over-approximation R 2 . With the definitions above, if R 1 is a sub-approximation of →, and R 2 is an over-approximation of →, then we have R 1 ⊆ π 1 (F(R 1 , R 2 )) and π 2 (F(R 1 , R 2 )) ⊆ R 2 , where π 1 , π 2 are the first and second projections. In other terms, given a pair of sub and over approximations of →, F computes a pair of better approximations.

From this definition, if it is easy to show that F is order-preserving:

Lemma 1. For all R 1 , T 1 , R 2 , T 2 ∈ T 2 , if (R 1 , R 2 ) (T 1 , T 2 ), then F(R 1 , R 2 ) F(T 1 , T 2 ).
Since F is order-preserving, it has a least fixpoint, F * = (D, U ), by the Knaster-Tarski theorem. We can then define → to be the first projection of F * , namely D. With the definition of C π we have adopted, and noting that it provides a form of stratification with the number of locations in a location graph with non-empty priority constraints, it is also possible to show that →= U , meaning that → as just defined is complete, using the terminology in [START_REF] Van Glabbeek | The meaning of negative premises in transition system specifications II[END_REF]. In fact, using the terminology in [START_REF] Van Glabbeek | The meaning of negative premises in transition system specifications II[END_REF], we can prove the theorem below, whose proof we omit for lack of space:

Theorem 1. The relation → as defined above is the least well-supported model of the rules in Figures 4 and5. Moreover → is complete.

Discussion

We discuss in this section the various features of the G-Kells framework and relevant related work.

Introductory example. Let's first revisit Example 3 to see how we can further model the behavior of its different components. We can add, for instance, a crash action to the virtual machine locations, which can be triggered by a process transition at a virtual machine location of the form P

• • • kill( * )
----------→ 0 with the following evaluation function:

eval ω (Γ, l, kill( * )) = {kill(h) | ∃r, l.r h ∈ Γ }
yielding, for instance, the following transition (where u includes all free names in V 0

[P ] C[P C ] CC[P CC ]): u, {V 0 .0 C, V 0 .1 CC} V 0 [P ] C[P C ] CC[P CC ] • • -----→ V 0 [0] 0 0
This crash behavior can be extended to an arbitrary location graph residing in a virtual machine, by first discovering the location graph inside a virtual machine via the gquery primitive, and then killing all locations in the graph as illustrated above.

Early style. Our operational semantics for location graphs is specified in an early style [START_REF] Sangiorgi | The π-calculus: A Theory of Mobile Processes[END_REF], with values in labels manifesting the results of successful communication. This allows us to remain oblivious to the actual forms of synchronization used. For instance, one could envisage pattern matching as in the ψ-calculus [START_REF] Bengtson | Psi-calculi: a framework for mobile processes with nominal data and logic[END_REF], or even bi-directional pattern matching: for instance we could have a process synchronization constraint r : a x, V matching an offered interaction h : a W, y , which translate into matching located synchronization constraints l.r : a W, V and h : a W, V .

l[P ] = l[P ] l[C1, . . . , Cn G] = l1[C1] l.1 l1 . . . ln[Cn] l.n ln l[ G ] 0 = 0 π • l : a • σ .G = π • {l : a} • σ . G G1 | G2 = G1 | G2 µ X. G = µ X. G {li : ai | i ∈ I} = {i : ai | i ∈ I} evalπ(Γ, l, i : ai) = l.i : ai evalσ(Γ, l, i : ai) = l.i : ai
Mobility vs higher-order. Our operational semantics comprises both mobility features with location binding, and higher-order features with swapping and higherorder interactions. One could wonder whether these features are all needed as primitives. For instance, one could argue that mobility features are enough to model higher-order phenomena as in the π-calculus [START_REF] Sangiorgi | The π-calculus: A Theory of Mobile Processes[END_REF]. Lacking at this point a behavioral theory for the G-Kells framework, we cannot answer the question definitely here. But we doubt that mobility via location binding is sufficient to faithfully encode higher-order communication. In particular, note that we have contexts (location graphs) that can distinguish the two cases via the ability to kill locations selectively.

Directed graphs vs acyclic directed graphs. Location graphs form directed graphs. One could wonder whether to impose the additional constraints that such graphs be acyclic. While most meaningul examples of ubiquitous systems and software structures can be modeled with acyclic directed graphs, our rules for location graphs function readily with arbitrary graphs. Enforcing the constraint that all evolutions of a location graph keep it acyclic does not seem necessary.

Relationship with CAB. The G-Kells model constitutes a conservative extension of CAB. A straightforwward encoding of CAB in the G-Kells framework can be defined as in Figure 6, with translated glues G defined with the same LTS, mutatis mutandis, as CAB glues. The following proposition is then an easy consequence of our definitions:

Proposition 1. Let C be a CAB component. We have C l:a -→ C if and only if C • {l:a} • -------→ C .
Graph constraints in rules. For simplicity, the evaluation functions seval and aeval have been defined above with only a simple graph constraint in the first clause of the seval definition. One can parameterize these definitions with additional graph constraints to enforce different policies. For instance, one could constrain the use of the swap, kill and and edge removal operations to locations dominating the target location by adding a constraint of the form l * h to each of the clauses in the definition of aeval, where l * Γ h means that there exists a (possibly empty) chain l.r l 1 , l 1 .r 1 l 2 , . . . , l n-1 .r n-1 l n , l n .r n h linking l to h in the location graph Γ . Similar constraints could be added to rule AddE. Further constraints could be added to rule Gquery to further restrict the discovery of subgraphs, for instance, preventing nodes other than immediate children to be discovered.

Types and capabilities. The framework presented in this paper is an untyped one. However, introducing types similar to i/o types capabilities in the π-calculus [START_REF] Sangiorgi | The π-calculus: A Theory of Mobile Processes[END_REF] would be highly useful. For instance, edges of a location graph can be typed, perhaps with as simple a scheme as different colors to reflect different containment and visibility semantics, which can be exploited in the definition of evaluation functions to constrain effects and synchronization. In addition, location, role and channel names can be typed with capabilities constraining the transfer of rights from one location to another. For instance, transferring a location name l can come with the right to swap the behavior at l, but not with the right to kill l, or with the right to bind roles of l to locations, but not with the ability to swap the behavior at l. We believe these capabilities could be useful in enforcing encapsulation and access control policies.

Relation with the ψ-calculus framework and SCEL. We already remarked that our use of environments is reminiscent of the use of frames in the ψ-calculus framework [START_REF] Bengtson | Psi-calculi: a framework for mobile processes with nominal data and logic[END_REF]. An important difference with the ψ-calculus framework is the fact that we allow interactions to depend on constraints involving the global environment, in our case the structure of the location graph. Whether one can faithfully encode the G-Kells framework (with mild linguistic assumptions on processes) with the ψ-calculus framework remains to be seen.

On the other hand, it would seem worthwhile to pursue the extension of the framework presented here with ψ-calculus-like assertions. We wonder in particular what relation the resulting framework would have with the SCEL language for autonomous and adaptive systems [START_REF] De Nicola | A formal approach to autonomic systems programming: The SCEL language[END_REF]. The notion of ensemble, being assertionbased, is more fluid than our notion of location graph, but it does not have the ability to superimpose on ensembles the kind of control actions, such as swapping and killing, that the G-Kells framework allows.

Relation with SHR. The graph manipulation capabilities embedded in the G-Kells framework are reminiscent of synchronized hyperdege replacement (SHR) systems [START_REF] Lanese | Mapping fusion and synchronized hyperedge replacement into logic programming[END_REF]. In SHR, multiple hyperedge replacements can be synchronized to yield an atomic transformation of the underlying hypergraph in conjunction with information exchange. Intuitively, it seems one can achieve much the same effects with G-Kells: located effects can atomically build a new subgraph and modify the existing one, and they can be synchronized across multiple locations thanks to synchronization constraints. In contrast, SHR systems lack priorities and the internalization of hyperedge replacement rules (the equivalent of our processes) in graph nodes to account for inherent dynamic reconfiguration capabilities. We conjecture that SHR systems can be faithfully encoded in the G-Kells framework.

Conclusion

We have introduced the G-Kells framework to lift limitations in existing computational models for ubquitous and reconfigurable software systems, in particular the ability to describe dynamic structures with sharing, where different aggregates or composites can share components. Much work remains to be done, however. We first intend to develop the behavioral theory of our framework. Indeed we hope to develop a first-order bisimulation theory for the G-Kells framework, avoiding the difficulties inherent in mixing higher-order features with passivation described in [START_REF] Lenglet | Characterizing contextual equivalence in calculi with passivation[END_REF]. We also need to formally compare G-Kells with several other formalisms, including SHR systems and the ψ-calculus framework. And we definitely need to develop a typed variant of the framework to exploit the rich set of capabilities that can be attached to location names.

Fig. 1 .

 1 Fig. 1. LTS semantics for CAB glues

Fig. 2 .

 2 Fig. 2. LTS semantics for CAB(P)

  where u is a set of names, and ∆ is a set of edges, then fn(∆) ⊆ u and fn(Γ ) = u. fn(C) ⊆ fn(Γ ), i.e. the free names occurring in C must appear in the already used names of Γ . -If l.r h and l.r k are in Γ ∪ Γ (C), then h = k, i.e. we only have a single edge binding a role r of a given location l to another location h. Auxiliary relation -→ • . The definition of → makes use of an auxiliary relation -→ • ⊆ G ×K ×L • ×K, where L • is a set of elements of the form π • σ • ω where π and σ are located priority and synchronizaton constraints, and where ω is a finite set of concrete effects. Relation -

Fig. 6 .

 6 Fig. 6. Encoding CAB in the G-Kells framework

Example 2. An action of the form {l : a} • c • {l : b, l : b} specifies that a synchronization on c is possible provided both subcomponents l and l offer a synchronization on b, and component l does not offer a synchronization on a.

The CAB model is defined in[START_REF] Di Giusto | Revisiting glues for component-based systems[END_REF] with an additional rule of evolution featuring silent actions. For simplicity, we have not included such a rule in our presentation here, but the stated results still stand for the CAB model presented in this paper.

Notice that the database location does not run inside any virtual machine. This means that, at this level of abstraction, our process architectural view of the database composite is similar to a network connecting the components placed in the two virtual machines.

Ackowledgements

Damien Pous suggested the move to an early style semantics. The paper was much improved thanks to comments by Ivan Lanese on earlier versions.


Valerio Cosentino

Massimo Tisi

Javier Luis

Cánovas Izquierdo

A Model-Driven Approach to Generate External DSLs from Object-Oriented APIs

Developers in modern general-purpose programming languages create reusable code libraries by encapsulating them in Applications Programming Interfaces (APIs). Domain-specific languages (DSLs) can be developed as an alternative method for code abstraction and distribution, sometimes preferable to APIs because of their expressivity and tailored development environment. However the cost of implementing a fully functional development environment for a DSL is generally higher. In this paper we propose DSLit, a prototype-tool that, given an existing API, reduces the cost of developing a corresponding DSL by analyzing the API, automatically generating a semantically equivalent DSL with its complete development environment, and allowing for user customization. To build this bridge between the API and DSL technical spaces we make use of existing Model-Driven Engineering (MDE) techniques, further promoting the vision of MDE as a unifying technical space.

Introduction

Modern General-purpose Programming Languages (GPLs) provide facilities for program abstraction and reuse, to foster the development of distributable libraries. Code in a programming library is encapsulated behind Application Programming Interfaces (APIs), that are used in user programs by the mechanisms provided by the GPL (e.g., function call or class inheritance). Sometimes library developers prefer to provide their users with a Domain-Specific Language (DSL), instead of (or in addition to) an API. APIs and DSLs can be seen as alternative methods to access the library functionalities, and are characterized by specific advantages. Programs written in the DSL can be more expressive, maintainable, concise and readable than corresponding GPL programs using the API (e.g., by avoiding the user to write some boilerplate code) [START_REF] Lédeczi | Composing domain-specific design environments[END_REF][START_REF] Kelly | Domain-Specific Modeling: Enabling Full Code Generation[END_REF]. On the other side, APIs allow for natural integration in complex programs written in their native language (or in other languages when coupled with suitable interface bindings).

Literature distinguishes DSLs in internal and external [START_REF] Fowler | Domain-Specific Languages[END_REF]. Internal DSLs are created by embedding DSL constructs into an existing GPL, which acts as host language. Although the internal approach allows DSLs to be easily developed [START_REF] Sánchez Cuadrado | A model-based approach to families of embedded domain-specific languages[END_REF], the corresponding tooling relies on the existing support for the host language, which limits the domainspecific assistance [START_REF] Sánchez Cuadrado | Comparison Between Internal and External DSLs via RubyTL and Gra2MoL[END_REF]. External DSLs instead are characterized by a separate syntax and specific development facilities. An important advantage of this approach is that the domain-specific development environment can be tailored to ease coding in the DSL:

-Static validation can be enriched to enforce semantic constraints hidden in the API.

Thus some runtime errors can be avoided at compile time. -Features like syntax highlighting, code completion, outlining, folding, can be tailored to the DSL. -The DSL interpretation/compilation step can be designed to automatically optimize the DSL code execution.

While, depending on the case, DSL or API (or both) may be the preferable solution [START_REF] Mernik | When and how to develop domain-specific languages[END_REF], the development cost of a DSL, especially if external, is in general much higher. Users have to define the DSL (i.e., abstract and concrete syntaxes, and semantics) and develop the domain-specific environment (e.g., syntax highlighting, code assistance, folding, outline view) which are tedious and time-consuming tasks.

In this paper we propose a method to automatically analyze an existing objectoriented API and generate an external DSL out of it. Our approach leverages modeldriven techniques to analyze and represent APIs at high-level of abstraction (i.e., as metamodels) which are later used to automatically generate the DSL components and the corresponding tooling, including parser, compiler and development environment. Developers can influence the DSL generation by editing the model-based API representation and by specifying design choices about the structure of the DSL to generate.

We provide a proof-of-concept implementation of the method in the DSLit tool, that is able to analyze Java APIs and generate external textual DSLs using the Xtext framework [START_REF] Eysholdt | Xtext: implement your language faster than the quick and dirty way[END_REF]. DSLit is currently able to deal with two API categories that we describe. The first category is called Plain Old Data (POD1 ) and indicates simple APIs that have the purpose of creating and maintaining a data structure. Usually such APIs are composed by classes made exclusively of getters, setters and constructors. The second category is called Fluent and contains those APIs that rely on chaining method calls. The return value of these method calls is an object representing the context of the keyword, and it is used to structure the language, defining which keywords can follow other keywords. For APIs not included in these categories, we also provide a fallback category, called SimpleJava based on a subset of Java which includes statements and declarations.

While currently limited in scope, the DSLit prototype, freely available at the project website2 , demonstrates the feasibility and usefulness of the approach.

The paper is structured as follows. Section 2 presents concrete examples to motivate our approach. Section 3 describes the conceptual framework applied to obtain a DSL from a Java API, while Section 4 presents the implementation of the prototype tool and the solution of the running cases. Section 5 lists the related work and Section 6 finalizes the paper and outlines some further work.

Motivating Examples

While APIs have proven to be a flexible means to encapsulate and reuse program logic, their usage can be cumbersome. A typical example is Java Swing, an API based on the Both examples specify the creation of a frame including a title and a label and the JavaFX Script version is remarkably more concise and readable. Developers in JavaFX are free from writing most of the boilerplate code and can use a declarative language specifically adapted to the creation of user interfaces. However, JavaFX Script was not developed as a DSL for targeting the Java Swing API but as a DSL to develop user interfaces rapidly and effectively. Thus, JavaFX Script code does not compile to the corresponding Java Swing code and it incorporates extra features such as declarative animation or mutation triggers.

As can be seen, a clear correspondence can be drawn among the DSL constructs and the Java API calls. For instance the "title:" element corresponds to a call to setTitle(). In this case DSL and API seem to lay at the same abstraction level, thus theoretically allowing for a purely syntactic translation. Note that this example does not show how to handle user interface event handlers, which can execute arbitrary actions, and are therefore generally written in GPL code.

The snippet in the Fig. 1c is written in the DSL obtained with DSLit by analyzing the Swing API. The snippet shows only a few lexical differences with the JavaFX version. In this sense, the constructs of the automatically-generated DSL mimic the structure defined in the API, e.g., there is a DSL element for each API method. In addition, a compiler is also generated by DSLit that translates this snippet to the program in the Fig. 1a.

As we will show, the conciseness of the previous DSL comes from the particular containment structure of the Swing API. As a significantly different example we show in Fig. 2a a program using jRTF 5 , a Fluent API to construct Rich Text Format (RTF) documents by Java. According to M. Fowler 6 , a Fluent API is an implementation of rtf section { p { "first paragraph" }, p { tab, " second par ", bold{ "with something in bold" }, " and ", italic{ underline{ "italic underline" } } } } out { out } jRTF DSLit rtf().section( p( "first paragraph" ), p( tab(), " second par ", bold( "with something in bold" ), " and ", italic( underline( "italic underline" ) ) ) ).out( out );

(a) (b) Fig. 2. An excerpt of Java code using the jRTF Fluent API and the corresponding automatically-generated DSL an object-oriented API that aims to provide more readable code. It is normally implemented by using method chaining to relay the instruction context of subsequent calls (but the Fluent paradigm is not limited to method chaining). Fluent APIs are becoming a very popular way to implement internal DSLs in Java. The jRTF example in Fig. 2 shows how a method chain in the Fluent API can closely resemble a DSL. Fig. 2b shows the DSL automatically generated from jRTF by DSLit. Differently from the Swing case, the DSL in Fig. 2 provides very little syntactic simplification w.r.t. its corresponding Java code. However, even in this case, the generation allows, for instance, generating an environment that has a domain-specific outline representing the RTF document structure, and it can be augmented with static checking capabilities (that are poor in the fluent API version).

In this paper we present a method that, given an API, generates an equivalent DSL. Our current application of this approach supports APIs fitting in one of the two categories previously defined plus a fallback category which resembles Java-like languages. We provide DSLit, a tool that generates such DSL, together with its development environment and a Java compiler, providing the following benefits:

-The generated DSL development environment has features like syntax highlighting or code completion that are tailored to the API domain. -Semantic constraints can be made explicit and static validation can be enriched by parameterizing the generation process. E.g., the DSL for Swing can be customized so that labels are always created in a single container frame, and the frame name is a mandatory attribute (avoiding at compile time some common mistakes in interface development). -The DSL compiler can be manually improved to optimize the resulting API code (e.g., reordering DSL definition elements to get optimal performance).

3 From API to DSL The process for obtaining a DSL from an API is split into three steps: (1) extracting an API metamodel for the set of class definitions in the API, (2) computing a DSL metamodel from the API metamodel, and (3) generating the grammar and the DSL tooling from the DSL metamodel. The steps are detailed in the following subsections.

API Classes to API Metamodel

The first step generates an API metamodel by applying a bridge between the API and Model TSs. This bridge maps API class definitions into metamodel elements. Thus Java classes are mapped into metaclasses, while attributes and methods are mapped into metaclass attributes and references/operations, respectively. The mapping is not trivial because of the semantic differences between class definitions and metaclasses, but it is well studied in works such as [START_REF] Cánovas Izquierdo | API2MoL: Automating the building of bridges between APIs and Model-Driven Engineering[END_REF] and [START_REF] Cuadrado | The program is the model: Enabling transformations@ run. time[END_REF].

When applied to big APIs, this step may generate very large metamodels. For instance in Fig. 1 the bridge would create a metaclass for each class and interface of the Swing API. Our approach provides a customization mechanism that allows filtering out API elements (e.g., classes, methods, attributes) in order to influence the construction of the DSL metamodel. Filtered elements will typically include technical classes that are out of the developer's interest or do not belong to the level of abstraction of the DSL. For instance, in the Swing example the developer may be interested only in the JFrame and JLabel class, with all their ancestors in the inheritance hierarchy.

Once the API metamodel is generated, developers can leverage in metamodel techniques to make explicit semantics in the DSL that are hidden in Java. An example is the semantics of references in metamodels: references can have containment semantics and multiplicity constraints that are implicit in Java attributes. To this aim, developers may manually enrich the API metamodel to exploit these aspects in the generated DSL, which can be statically checked on the DSL code. For instance, by adding a containment property to the reference between JFrame and JLabel the resulting DSL may automatically check that a label is not contained in two distinct frames.

API Metamodel to DSL Metamodel

API classes represent an internal abstraction mechanism of object-oriented languages, i.e., an in-language abstraction. The API metamodel we obtained in the previous step is an artifact describing this in-language abstraction. The purpose of the second step is to transform the in-language abstraction in a linguistic abstraction, i.e., an abstraction defined by language constructs. We perform the transformation between in-language abstraction and linguistic abstraction within the Model TS as a model transformation, thus creating the DSL metamodel.

Lifting the abstraction to the linguistic level is not a trivial step, as the logic to apply is strongly dependent on the structure of the DSL the user wants to obtain. For instance in the Swing DSL we want to generate language concepts for classes (e.g. JFrame, JLabel) and attributes (e.g. title, size) of the API. Conversely, in the RTF example the language structure contains a concept for each method of the API.

The linguistic abstraction of a DSL contains: (a) the domain concepts, which are extracted from the API metamodel; and (b) its structure and capabilities, which define how the concepts can be defined, linked and composed (e.g., which concepts become Statements, whether the DSL is going to use Blocks, etc.). While the former is domainspecific, the latter can be considered domain-independent and be reused in different DSLs. For instance, in our first example the domain contains the elements JFrame and JLabel (and their attributes) while the structure of programs in the Swing DSL may be composed by a sequence of statements initializing the JFrame and JLabel attributes.

In order to generate the DSL metamodel we built a template system which receives as inputs: (a) the API metamodel, and (b) a template defining the structure and capabilities of the languages. Our approach currently provides three templates for the categories considered in DSLit but more templates can also be plugged in.

DSL Metamodel to DSL Environment

The last step is a bridge between the Model TS and the Grammar TS which produces the needed artefacts for the DSL. The Model TS already contains several well-known tools that help in generating the components of an external textual DSL environment (e.g., Xtext). Therefore, this step is devoted to generate the input artifacts for these tools, including: (1) the mapping of metamodel elements (i.e., the abstract syntax definition of the DSL) into the grammar rules of the concrete syntax, (2) development environment (e.g., validators, type system, etc.) and (3) compiler.

The generation process is parameterized by the DSL metamodel and the template chosen. While the DSL metamodel provides domain-specific information (e.g., concepts, attributes, references) and basic semantics (e.g., cardinalities, containment, etc.), the template drives the grammar structure of the resulting DSL and also the development environment and compiler.

The resulting compiler is able to transform DSL programs in their corresponding Java programs. As shown in Fig. 3 the compiler is an artefact of the Grammar TS, and the execution of the compiled Java program produces the set of API objects in the API TS (plus possibly other objects). Most tools create also a parser towards the Model TS that extracts from programs the corresponding instance of the DSL metamodel.

The next section explains how we implement the approach and illustrates in detail how the motivating examples are addressed.

DSLit

As a proof of concept of the described approach, we have implemented DSLit, a prototype DSL generator integrated in the Eclipse platform. The current prototype contains three DSL templates that aim to address the APIs that fall under the categories previously introduced, respectively POD, Fluent and SimpleJava.

Once one of the provided templates is selected, our tool is able to generate a domainspecific development environment, using Xtext. Currently DSLit supports the generation of a Proposal Provider and Validator components of the environment. In future work we plan to investigate the domain-specific customization of other components.

Grammar Generation

In this section, we describe the DSL templates included in DSLit, covering three possible representations of the information contained within the API metamodel.

POD DSL Generator. DSLit provides an ad-hoc POD DSL Generator. The generator can be applied to any API, but it only considers their POD part (setters, getters and constructors) for the definition of the DSL. This generator has been applied to a Swing subset and generates the DSL in Fig. 1c.

In the following we briefly describe the transformation logic for the generation of the DSL grammar model (conforming to the Xtext metamodel) from the API metamodel. The full code of the transformation is available at the paper website.

The POD DSL extracted out of the API metamodel takes into account only attributes and references contained in the classes defined in the metamodel. All the classes, attributes and references are mapped to grammar rules in Xtext and their names will appear as terminals in the grammar. Each class is transformed into a rule that contains, wrapped into braces, the features that correspond to the attributes and references for that class. Each of those features expands to the rule that represents the type of the corresponding attribute or reference, while its cardinality depends on the cardinality of the corresponding attribute or reference. In particular, a multi valued attribute is expressed as a feature list, an optional attribute is expressed as an optional feature and finally a single valued attribute is expressed as a single feature. Finally, since we know the semantics of the POD template, our tool is able to append additional grammar rules in order to avoid identifying the root class of the API metamodel. Thus, it adds to the template the rules Grammar and Element. The former is the grammar root rule and contains a list of Elements, while the latter includes as alternatives all the rules that correspond to the metaclasses.

In Fig. 4, an excerpt of the generation of the Java Swing DSL is shown. The classes Frame, MenuBar are mapped to the corresponding grammar rules (generated according to the schema className-attrOrRefName-AttrOrRefTypeName). The rule Frame contains as terminal the name of the related class and two optional features menuBar and The former contains the name of the reference menuBar as terminal and the feature next (inserted by the generator) that expand in the rule MenuBar; the latter contains the name of the attribute title as terminal and the feature value (inserted as well by the generator), since the title is defined as a primitive type. The remaining rules MenuBar and MenuBar menuCount EInt follow the same mapping strategy.

Fluent DSL Generator. The Fluent DSL generator transforms a fluent API into an equivalent external DSL. The generator included in DSLit is able to handle simple fluent APIs like the jRTF (Fig. 2). The API metamodel generated from a Fluent API is composed by operations defined over the classes of the metamodel. For each class, a grammar rule is created. It contains a set of alternatives that are the grammar rules corresponding to the operations for that class. Inside these rules, each operation parameter is mapped to a feature that, depending on the parameter cardinality, can be optional or a list. In addition, an optional feature next is defined, that expands to the rule representing the return type of the operation.

It is important to note that in the Fluent DSL, all the names of the operations defined in the classes of the metamodel appear as terminal in the grammar. Fig. 6. Excerpt of the DSL Template for the SimpleJava DSL generator Fig. 5 shows the generation of a Fluent DSL for a small subset of the jRTF API. The classes Rtf and RtfPara are mapped to the corresponding rules; while the operations rtf(), section(RtfPara) and out() are mapped to rules which names follow the schema: className-operationName-parameterNames-returnType.

In particular, Rtf rtf contains as terminal the name of the operation rtf() and an optional feature next, that represents the return type Rtf of the operation rtf(). Rtf section paragraphs RtfPara contains the terminal section, a list of paragraphs that expand the rule RtfPara (not shown in the example) and the optional feature next. Finally, Rtf out contains only the terminal out, since the operation out() has neither parameters nor a return type that is a class of the input API metamodel.

SimpleJava DSL Generator. In the case in which the API does not suit one of the previous templates, the user has still the possibility to generate a fallback DSL. Since no assumptions can be made on the structure of the API and on its intended use, the generated DSL needs to offer similar capabilities to the Java language. The SimpleJava DSL generator produces a DSL that resembles Java but is restricted to the use of the analyzed API. The generated DSL in this case has the purpose of being a starting point for DSL development, since 1) the DSL developer can easily add domain-specific features to the generated environment, 2) moving the domain information to the linguistic level makes it more suitable to automated analysis.

The SimpleJava template (an excerpt is shown in Fig. 6) defines typical Java concepts, e.g. Declaration and Assignment. The transformation API2Grammar expands the SimpleJava template with the information contained within the API metamodel. It is important to note that names of classes, attributes and references in the API metamodel are inserted in the template respectively as alternatives of the grammar rules Type and Attribute.

As mentioned above, the SimpleJava template does not make any assumption on the structure of the API. Therefore, it is applicable to any API, including those for which other templates such as Plain Old Data structure, and Fluent DSL are applicable. Fig. 7 revisits the Swing and jRTF examples: the DSL code samples of Fig. 1 and 2 are now expressed in textual syntaxes derived using the SimpleJava template. This figure further illustrates how SimpleJava works. in that work inspired our research. Works such as [START_REF] Robillard | Automated API Property Inference Techniques[END_REF] investigate current analysis techniques to understand APIs and extract some usage patterns. Such studies could complement ours in identifying specific API features and therefore improve our process.

Integration between the model and the API TS has been considered in works such as [START_REF] Cánovas Izquierdo | API2MoL: Automating the building of bridges between APIs and Model-Driven Engineering[END_REF][START_REF] Cuadrado | The program is the model: Enabling transformations@ run. time[END_REF][START_REF] Song | Supporting runtime software architecture: A bidirectional-transformation-based approach[END_REF], where approaches to define bridges between these two TSs are presented. However, none of them enables the generation of a DSL from an API definition nor the selection of an appropriate structure for the resulting DSL.

Existing approaches such as METABORG [START_REF] Bravenboer | Concrete syntax for objects: domain-specific language embedding and assimilation without restrictions[END_REF], SugarJ [START_REF] Erdweg | SugarJ: Library-based Syntactic Language Extensibility[END_REF] and Helvetia10 enable the definition of internal DSLs and the corresponding generation of the domain-specific environment in the host language. Instead, our approach targets external DSLs. Furthermore ours can automatically generate a DSL definition for an API, which could be used as input for the aforementioned approaches.

Some GPLs with flexible concrete syntaxes like Haskell or Ruby enable direct definitions of DSLs directly using GPL syntax. An example of such a DSL is given in [START_REF] Cunningham | A little language for surveys: constructing an internal dsl in ruby[END_REF]. One problem with this kind of approaches is that DSL concrete syntax must be a subset of GPL concrete syntax (i.e., DSL syntax must be valid GPL code). Another problem is that the corresponding API has to be defined specifically so that GPL syntax may be used directly as a DSL. Therefore, compromises must be made on both API and DSL.

In [START_REF] Kosar | A preliminary study on various implementation approaches of domain-specific language[END_REF] the authors evaluate 10 different approaches to implement DSLs, concluding that embedded DSLs are the simplest to implement. Our approach could be considered as an additional approach with which a significant amount of DSL customization is attainable at a comparatively low cost: (a) it provides a specific textual syntax not limited by a host GPL and (b) it kickstarts a DSL tooling ready to be used for the DSL.

The approach presented in [START_REF] Chodarev | Towards Automated Program Abstraction and Language Enrichment[END_REF] provides abstractions for repeatedly used patterns. Instead, we target on abstracting API calls into DSL constructs. However, both approaches could be combined so that simple DSL construct could be mapped to complex patterns of API usage.

Conclusion and Future Work

In this paper we have presented an approach to automatically generate an external DSL out of an object-oriented API by transforming in-language abstraction into linguistic abstraction. The generation process has been presented as a bridge between the involved technical spaces (i.e., API TS, Model TS, and Grammar TS) and uses a template mechanism, which allows customization of the resulting DSL. Our approach has been implemented on the Eclipse platform, as a plugin called DSLit, which generates an Xtext-based textual DSL out of Java-based APIs. The current prototype incorporates two templates that generate specific DSL structures (POD and Fluent) as well as a fallback template covering a subset of Java (SimpleJava).

In future work we plan to study how our method could cope with APIs that allow custom code extension (e.g., providing implementations of interfaces or abstract classes). We would also like to define more templates allowing for different types of DSLs, which in turn will need a deeper study on API characterization. Another possibility to explore is the generation of DSL interpreters instead of compilers. They would for instance make it possible to load and execute DSL code at runtime. Finally, since a GPL allows interleaving calls to distinct APIs, one open question to study is how the generated DSLs may be combined in order to achieve the same kind of interleaving achievable with a GPL.

Fig. 3 Fig. 3 .

 33 Fig.3gives an overview of the linguistic architecture of our approach, spanning over three technical spaces (TS) 7 : (1) the API TS, in which API objects (i.e., in memory)

Fig. 4 .Fig. 5 .

 45 Fig. 4. Example of the POD DSL for SwingRtf: Rtf_rtf | Rtf_section_paragraphs_RtfPara | Rtf_out Rtf_rtf: 'rtf' next=Rtf? Rtf_section_paragraphs_RtfPara: 'section' '{' paragraphs+=RtfPara ( ',' paragraphs+=RtfPara)* '}' next=Rtf? Rtf_out: 'out' RtfPara

http://en.wikipedia.org/wiki/Plain_old_data_structure

http://www.emn.fr/z-info/atlanmod/index.php/DSLit

http://java.sun.com/products/jdk/awt

http://docs.oracle.com/javafx

http://code.google.com/p/jrtf/

http://martinfowler.com/bliki/FluentInterface.html

The concept of Technical Space (TS) is introduced in[START_REF] Kurtev | Technological Spaces : an Initial Appraisal[END_REF]. It is defined according to a conformance relationship that associates artifacts (e.g. program) with meta-artifacts (e.g. grammar). Bridges can be defined to transfer artifacts from one to another TS.

http://scg.unibe.ch/research/helvetia

f : Frame f.title = "My Java Application" f.width = 500 f.height = 300 l : Label l.text = "Hello World!" f.content = l f.visible = true SimpleJava for Swing SimpleJava for jRTF r : Rtf s : Section r.section = s p1 : RtfPara p1.contents = "first paragraph" p2 : RtfPara t : Tab p2.contents = t p2.contents = " second par " b : Bold b.contents = "text in bold" p2.contents = b p2.contents = " and " i : Italic u : Underline u.contents = "italic underline" i.contents = u p2.contents = i Fig. 7. SimpleJava template applied to Swing and jRTF

Development-Environment Generation

Once the DSL grammar is generated, Xtext is able to produce several artifacts composing a DSL development environment. In particular, it offers 1) a proposal provider that provides a list of accessible keywords according to the current terminal of the grammar (i.e. content assist) and 2) a validator performing static analysis during editing. However, since we know the semantics of the DSL template that has been used to generate the grammar, we can automatically derive improved versions of such environment components by mixing the DSL domain-independent part, that comes from the template structure, and the DSL domain-specific part, that is inferred from the API metamodel. In our prototype, these improved components are generated for the POD and Sim-pleJava DSLs and can be can be eventually redefined by the developer if needed. For the Fluent DSL, since the proposal provider and validator are embedded in the structure of the grammar (i.e., how the feature of a grammar rule expands in other rules), we rely instead on the Xtext default components.

Compiler Generation

Since the semantics of the DSL template is well-defined, a DSL instance can be transformed into its equivalent in Java. For instance concepts like Declaration, Assignment and Statement in the SimpleJava template (Fig. 6) have a one-to-one correspondence with Java programming language's constructs. Xtext provides the capability to generate a model-representation of the DSL grammar according to the Xtext metamodel. Such a DSL model is then transformed to a Java model leveraging on MoDisco 8 that is in turn translated to a Java readable file using Acceleo 9 , a model-to-text transformation tool.


Valmi Dufour-Lussier

Alice Hermann

Florence Le Ber
email: florence.leber@engees.unistra.fr

Jean Lieber

Belief revision in the propositional closure of a qualitative algebra *

Keywords: qualitative algebras, belief revision, belief contraction, propositional closure

Belief revision is an operation that aims at modifying old beliefs so that they become consistent with new ones. The issue of belief revision has been studied in various formalisms, in particular, in qualitative algebras (QAs) in which the result is a disjunction of belief bases that is not necessarily representable in a QA. This motivates the study of belief revision in formalisms extending QAs, namely, their propositional closures: in such a closure, the result of belief revision belongs to the formalism. Moreover, this makes it possible to define a contraction operator thanks to the Harper identity. Belief revision in the propositional closure of QAs is studied, an algorithm for a family of revision operators is designed, and an open-source implementation is made freely available on the web.

Introduction

Belief revision is an operation of belief change that consists in modifying minimally old beliefs so that they become consistent with new beliefs [START_REF] Alchourrón | On the Logic of Theory Change: partial meet functions for contraction and revision[END_REF]. One way to study this issue following a knowledge representation angle is to consider a formalism and to study some belief revision operators defined on it: how they are defined and how they can be implemented.

In particular, it is rather simple to define a revision operator on a qualitative algebra (QA, such as the Allen algebra) by reusing the work of [START_REF] Condotta | A Syntactical Approach to Qualitative Constraint Networks Merging[END_REF]) about the related issue of belief merging. The result of such a belief revision is a set of belief bases to be interpreted disjunctively, and which is not necessarily representable as a single belief base: QAs are not closed under disjunction.

This gives a first motivation for the study of belief revision in the propositional closure of a QA: the revision operator in such a closure gives a result that is necessarily representable in the formalism. Another motivation lies in the possibility of defining a contraction operator in this formalism, thanks to the Harper identity.

The first section of the paper contains some preliminaries about various notions used throughout the paper. The next section briefly describes some properties of such a formalism. Finally, an algorithm and an implementation of this algorithm for a revision operator in the propositional closure of a QA are presented with an example.

The research report [START_REF] Dufour-Lussier | Adapting Spatial and Temporal Cases[END_REF]) is a long version of this paper including more detailed preliminaries, the proofs and some additional examples.

Preliminaries

Qualitative algebras

Qualitative algebras (QAs) are formalisms that are widely used for representation depending on time and/or on space (Stock 1997). Formulas built upon QAs are closed under conjunction, though the symbol ∧ is not systematically used. Some of the usual notations and conventions of QAs are changed to better fit the scope of this paper. In particular, the representation of knowledge by graphs (namely, qualitative constraint networks) is not well-suited here, because of the propositional closure introduced afterwards.

First, the Allen algebra is introduced: it is one of the most famous QAs and it will be used in our examples throughout the paper. Then, a general definition of QAs is given.

The Allen algebra is used for representing relations between time intervals [START_REF] Allen | Maintaining knowledge about temporal intervals[END_REF]. A formula of the Allen Algebra can be seen as a conjunction of constraints, where a constraint is an expression of the form x r y stating that the interval x is related to the interval y by the relation r. 13 base relations are introduced (cf. figure 1); a relation r is either one of these base relations or the union of base relations r 1 , . . . , r m denoted by r 1 . . . r m .

For example, if one wants to express that the maths course is immediately before the physics course which is before the English course (either with a time lapse, or immediately before it), one can write the formula: The set of relations is denoted by R.

A finite set of symbols V, disjoint from B, is given. A (qualitative) variable is an element of V.

A constraint is an expression of the form x r y where x, y ∈ V and r ∈ R.

A formula ϕ is a conjunction of n constraints (n ≥ 1): x 1 r 1 y 1 ∧ . . . ∧ x n r n y n . A constraint of ϕ is one of the constraints of this conjunction. Let L QA be the set of the formulas of the considered QA. The atoms of L QA are the constraints.

A formula ϕ ∈ L QA is under normal form if for every x, y ∈ V with x = y, there is exactly one r ∈ R such that x r y is a constraint of ϕ. Then, this relation r is denoted by r ϕ (x, y).

A scenario σ is a formula under normal form such that, for every variables x and y, x = y, r σ (x, y) ∈ B. Therefore, there are |B| |V|×(|V|-1) scenarios.

Semantics. The semantics of a QA can be defined classically, thanks to a domain, a variable being mapped into a subset of this domain and a relation being mapped on a relation between such subsets. For Allen algebra, the domain is the set Q of rational numbers and, given an interpretation I, a variable x is mapped to an interval

I(x) = [a, b] of Q (a < b).
The semantics of each of the basic relations is defined. For example, I satisfies

x 1 m x 2 if b 1 = a 2 where I(x i ) = [a i , b i ]. I satisfies x 1 (r 1 . . . r m ) x 2 if it sat- isfies one of the constraints x 1 r k x 2 for k ∈ {1, . . . , m}.
A formula is consistent (or satisfiable) if there exists an interpretation satisfying each of its constraints. Finally, for ϕ 1 , ϕ 2 ∈ L QA , ϕ 1 |= ϕ 2 if, for every interpretation I satisfying ϕ 1 , it satisfies also ϕ 2 . The research report give more details on this first definition of the semantics.

The semantics can be characterized a posteriori thanks to consistent scenarios.

Let Ω be the set of consistent scenarios on the variables of V. It can be proven that |Ω| ≤ |B| |V|×(|V|-1)/2 : if x r y is a constraint of a consistent scenario σ then y r -x is also a constraint of σ.

Let M : L → 2 Ω be defined by

M(ϕ) = {σ ∈ Ω | σ |= ϕ} for ϕ ∈ L,
where |= is the entailment relation defined below, thanks to the semantics based on a domain. Ω and M make it possible to define a semantics on L which coincides with the semantics based on a domain (hence the same entailment relation |=): ϕ 1 |= ϕ 2 iff M(ϕ 1 ) ⊆ M(ϕ 2 ). However, this second semantics is more practical to use for defining revision operators on QAs.

Belief change

Belief revision is an operation of belief change. Intuitively, given the set of beliefs ψ an agent has about a static world, it consists in considering the change of their beliefs when faced with a new set of beliefs µ, assuming that µ is considered to be unquestionable by the agent. The resulting set of beliefs is noted ψ ∔ µ, and depends on the choice of a belief revision operator ∔. In [START_REF] Alchourrón | On the Logic of Theory Change: partial meet functions for contraction and revision[END_REF], the principle of minimal change has been stated and could be formulated as follows: ψ is minimally changed into ψ ′ such that the conjunction of ψ ′ and µ is consistent, and the result of the revision is this conjunction. Hence, there is more than one possible ∔ operator, since the definition of ∔ depends on how belief change is "measured". More precisely, the minimal change principle has been formalized by a set of postulates, known as the AGM postulates (after the names of the authors of [START_REF] Alchourrón | On the Logic of Theory Change: partial meet functions for contraction and revision[END_REF]).

In (Katsuno and Mendelzon 1991b), revision has been studied in the framework of propositional logic (with a finite set of variables). The AGM postulates are translated into this formalism and a family of revision operators is defined based on distance functions d on Ω, where Ω is the set of interpretations: the revision of ψ by µ according to

∔ d (ψ ∔ d µ) is such that M(ψ ∔ d µ) = {ω ∈ M(µ) | d(M(ψ), ω) = d * } with d * = d(M(ψ), M(µ)) (1)
Intuitively, d * measures, using d, the minimal modification of ψ into ψ ′ needed to make ψ ′ ∧ µ consistent. This approach can be extended to other formalisms for which a model-theoretic semantics can be defined and such that a distance function can be specified on the set of interpretations Ω. However, in some of these formalisms, a representability issue can be raised: it may occur that a subset Σ of Ω is not representable, i.e. there is no formula ϕ such that M(ϕ) = Σ. This representability issue is addressed below, for the case of QAs.

Belief contraction is the operation of belief change that associates to a set of beliefs ψ and a set of beliefs µ, a set of beliefs ψ ´µ such that ψ ´µ |= µ. In propositionally closed formalisms, the Harper identity makes it possible to define a contraction operator ´thanks to a revision operator ∔ with

ψ ´µ = ψ ∨ (ψ ∔ ¬µ) (2)
Belief merging is another operation of belief change.

Given some sets of beliefs ψ 1 , . . . , ψ n , their merging is a set of beliefs Ψ that contains "as much as possible" of the beliefs in the ψ i 's. Intuitively, Ψ is the conjunction of ψ ′ 1 , . . . , ψ ′ n such that each ψ i has been minimally modified into ψ ′ i in order to make this conjunction consistent. Some postulates of belief merging have been proposed and discussed [START_REF] Konieczny | Merging information under constraints: a logical framework[END_REF], in a similar way as the AGM postulates.

Belief revision in qualitative algebras

In [START_REF] Condotta | A Syntactical Approach to Qualitative Constraint Networks Merging[END_REF]) a belief merging operator is defined that can be easily adapted for defining a revision operator. It is based on a distance between scenarios. Let δ be a distance function on B. Let σ, τ ∈ Ω, be two scenarios based on the same set of variables V. Then, d is defined by

d(σ, τ ) = x,y∈V,x =y δ(r σ (x, y), r τ (x, y))
One of the possibilities for δ is the use of a neighborhood graph, i.e. a connected, undirected graph whose vertices are the base relations: δ(r, s) is the length of the shortest path between r and s. Then, the scenarios of the revision of ψ by µ according to ∔ d are the scenarios of µ that are the closest ones to scenarios of ψ according to d. The set of optimal scenarios is not necessarily representable in (L QA , |=). One solution to address this issue is to consider that the result of revision is a set of scenarios.

Algorithms for implementing this kind of belief revision in QAs are presented in [START_REF] Dufour-Lussier | Adapting Spatial and Temporal Cases[END_REF] and [START_REF] Hué | Revising qualitative constraint networks: Definition and implementation[END_REF].

Propositional closure of a qualitative algebra

The propositional closure of a QA (L QA , |=) is a formalism ( L QA , |=) defined as follows. L QA is the smallest superset of L QA that is closed for ¬ and ∧. Then, L QA is closed for ∨: ϕ 1 ∨ϕ 2 is an abbreviation for ¬(¬ϕ 1 ∧¬ϕ 2 ). The entailment relation is based on the consistent scenarios:

ϕ 1 |= ϕ 2 if M(ϕ 1 ) ⊆ M(ϕ 2 ), M being extended on L QA by M(ϕ 1 ∧ ϕ 2 ) = M(ϕ 1 ) ∩ M(ϕ 2 ) and M(¬ϕ) = Ω \ M(ϕ). Proposition 1 (representability). Every set of scenarios Σ ⊆ Ω is representable in L QA . More precisely, with ϕ = σ∈Σ σ, M(ϕ) = Σ.
Every formula of L QA can be written in DNF (disjunctive normal form, i.e. disjunction of conjunctions of constraints), since it is a propositionally closed formalism, but the following proposition goes beyond that.

Proposition 2 (DNF-w/oN form). Every ϕ ∈ L QA is equivalent to a formula in DNF using no negation symbol.

Belief revision in ( L QA , |=)

Given a distance function d on Ω, a revision operator on ( L QA , |=) can be defined according to equation (1). Indeed, proposition 1 implies that {ω ∈ M(µ

) | d(M(ψ), ω) = d * } is representable.
An algorithm for computing ∔ d in L QA The principle of the algorithm is based on the following proposition.

Proposition 3 (revision of disjunctions). Let ψ and µ be two formulas of L QA and {ψ i } i and {µ j } j be two finite families of L QA such that ψ =

i ψ i and µ = j µ j . Let d * ij = d(M(ψ i ), M(µ j ))
for any i and j. Then:

ψ ∔ d µ ≡ i,j,d * ij =d * ψ i ∔ d µ j with d * = d(M(ψ), M(µ)) Moreover, d * = min ij d * ij (3)
The algorithm for ∔ d in L QA consists roughly in putting ψ and µ in DNF-w/oN form then applying proposition 3 on them, using the ∔ d algorithm on L QA for computing the ψ i ∔ d µ j 's. More details are given in the research report.

Implementation: the REVISOR/PCQA engine REVISOR is a collection of several revision engines that are open-source and freely available. 1In particular, REVISOR/QA implements ∔ d in three QAs: the Allen algebra, INDU-an extension of the Allen algebra taking into account relations between intervals according to their lengths [START_REF] Pujari | INDU: An Interval & Duration Network[END_REF]-and RCC8-a QA for representing topological relations between regions of space [START_REF] Randell | A spatial logic based on regions and connection[END_REF]. Moreover, it is easy to use a different qualitative algebra, by giving in the code some tables (composition table, inverse relation table, and table for the values δ(r, s) for r, s∈ B). The engine is written in Perl, but can be used through a Java library. The worst-case complexity of this implementation is of the order of O |B| , according to a coarse analysis. The following example has been executed using REVISOR/PCQA, and is included with the source code. The README file associated with REVISOR/QA on the REVISOR website explains how it can be executed.

This example uses a belief contraction operator. According to (2), a contraction operator ´d can be defined that is based on ∔ d . Now let us consider the set of beliefs ψ of an agent called Maurice about the dates of birth and death of famous mathematicians. Maurice thought that Boole was born after de Morgan and died before him and that de Morgan and Weierstraß were born the same year (say, at the same time) but the former died before the latter:

ψ = Boole d De Morgan ∧ De Morgan s Weierstraß
where, Boole is the interval of time between the birth and the death of Boole, and so on. Now, Germaine, a friend of Maurice, tells him that she is not sure whether Boole was born strictly after Weierstraß. Since Maurice trusts Germaine (and her doubts), he wants to make the contraction of its original beliefs ψ by µ with µ = Boole bi mi oi f d Weierstraß

The result, computed by REVISOR/PCQA in less than one second, is ψ ´d µ, equivalent to the following formula: In [START_REF] Dufour-Lussier | Adapting Spatial and Temporal Cases[END_REF], other examples of use of REVISOR/PCQA, including an analysis of the computing time, are presented. In particular, it is shown that it may be the case that a family of revision problems, albeit formalizable in both L Allen and in L Allen , are solved in much less time in the more expressive formalism L Allen .

Conclusion

This paper has presented an algorithm for distance-based belief revision in the propositional closure L QA of a qualitative algebra L QA , using the revision operation on L QA . This work is motivated by the fact that it gives a revision operation whose result is representable in the formalism, by the fact that some practical examples are easily represented in L QA whereas they are quite difficult to represent in L QA , and by the fact that it makes it possible to define a contraction operator thanks to the Harper identity (which requires disjunction and negation). The preprocessing of the algorithm consists in putting the formulas into a disjunctive normal form without negation. Then, proposition 3, which reduces a revision of disjunctions to a disjunction of the least costly revisions, is applied. REVISOR/PCQA is an implementation of this revision operator for the Allen algebra, INDU and RCC8.

A first direction of research following this work is the improvement of the computation time of the REVISOR/PCQA system. One way to do it is to parallelize it. A sequential optimization would consist in finding a heuristic for ranking the pairs (i, j), with the aim of starting from the best candidates, in order to obtain a low upper bound of d * sooner (hence a pruning of a part of the search trees developed for the computation of ∔ d in (L QA , |=)).

Another direction of research is to study how other belief change operations can be implemented in this formalism, in particular belief merging [START_REF] Konieczny | Merging information under constraints: a logical framework[END_REF] and knowledge update (Katsuno and Mendelzon 1991a).

  maths m physics ∧ physics b m english L Allen is the set of the formulas of the Allen algebra.Qualitative algebras in general are defined below, first by their syntax and then by their semantics. , oi, si, di and fi represent respectively the inverse relations of the relations represented by b, m, o, s, d and f.

Figure 1 :

 1 Figure 1: The base relations of L Allen .

  implements ∔ d on the propositional closures of the QAs L Allen , INDU and RCC8: it actually uses REVISOR/QA and is one of the engines of REVISOR. The worst-case complexity of this implementation is of the order of O |V| 4 |B| |V|•(|V|-1) 2

(

  Boole d De Morgan ∧ De Morgan s Weierstraß) ∨ (Boole s Weierstraß ∧ De Morgan di Weierstraß) ∨ (Boole s De Morgan ∧ De Morgan s Weierstraß) ∨ Boole d De Morgan ∧ Boole s Weierstraß ∧ De Morgan o Weierstraß Actually, the last term of this disjunction corresponds to the reality, provided that the intervals of time correspond to a year granularity: George Boole (1815-1864), Augustus De Morgan (1806-1871), Karl Weierstraß (1815-1897).

http://revisor.loria.fr

* This research was partially funded by the project Kolflow (http://kolflow.univ-nantes.fr) of the French National Agency for Research (ANR), program ANR CONTINT. Copyright c 2014, Association for the Advancement of Artificial Intelligence (www.aaai.org).