G Michele Pinna

Representing Dependencies in Event Structures

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The notion of causality is an intriguing one. In the sequential case, the intuition behind it is almost trivial: if the activity e depends on the activity e , then to happen the activity e needs that e has already happened. This is easily represented in Petri nets ( [START_REF] Reisig | Petri Nets: An Introduction[END_REF]), the transition e produces a token that is consumed by the transition e (the net N ). The dependency is testified by the observation that the activity e always precedes the activity e. However this intuition does not reflect other possibilities. If we abandon the sequential case and move toward possibly loosely cooperating system the notion of causality become involved. Consider transition e inhibits the transition e (the net N ). The latter to happens needs that the transition e happens first, and the observation testifies that the activity e needs that e has already happened, though resources are not exchanged between e and e. In both cases the observation that the event e must happen first leads to state that e precedes e and this can be well represented with a partial order relation among events.

This quite simple discussion suggests that the notion of causality may have many facets. In fact, if the dependencies are modeled just with a well founded partial order, inhibitor arcs can be used to model these dependencies, but the notion of partial order does not capture precisely the subtleties that are connected to the notion of causality.

To represent the semantics of concurrent systems the notion of event structure plays a prominent role. Event structures have been introduced in [START_REF] Nielsen | Petri Nets, Event Structures and Domains, Part 1[END_REF] and [START_REF] Winskel | Event Structures[END_REF] and since then have been considered as a cornerstone. The idea is simple: the activities of a system are the events and their relationships are specified somehow, e.g. with a partial order modeling the enabling and a predicate expressing when activities are coherent or not. Starting from this idea many authors have faced the problem of adapting this notion to many different situations which have as a target the attempt to represent faithfully various situations. This has triggered many different approaches. In [START_REF] Gunawardena | Geometric logic, causality and event structures[END_REF] and [START_REF] Gunawardena | Causal automata[END_REF] causal automata are discussed, with the idea that the conditions under which an event may happen are specified by a suitable logic formula, in [START_REF] Gaifman | Partial order models of concurrency and the computation of functions[END_REF] and [START_REF] Gaifman | Modeling concurrency by partial orders and nonlinear transition systems[END_REF] it is argued that a partial order may be not enough or may be, in some situation, a too rigid notion, and this idea is used also in [START_REF] Pinna | On the nature of events[END_REF] and [START_REF] Pinna | On the nature of events: another perspective in concurrency[END_REF] where the notion of event automata is introduced, and it is used also in [START_REF] Pinna | Event structures with disabling/enabling relation and event automata[END_REF] where an enabling/disabling relation for event automata is discussed. Looking at the enabling relation, both bundle event structures ( [START_REF] Langerak | Bundle Event Structures: A Non-Interleaving Semantics for Lotos[END_REF]) and dual event structures ( [START_REF] Langerak | Causal ambiguity and partial orders in event structures[END_REF]) provide a notion of enabling capturing or -causality (the former exclusive or -causality and the latter non exclusive or -causality). Asymmetric event structures ( [START_REF] Baldan | Contextual Petri nets, asymmetric event structures and processes[END_REF]) introduces a weaker notion of causality which models contextual arcs in Petri nets, or in the case circular event structures ( [START_REF] Bartoletti | Circular causality in event structures[END_REF]) the enabling notion is tailored to model also circular dependencies. In flow event structures ([8]) the partial order is required to hold only in configurations. Finally we mention the approaches aiming at modeling the possibility that the dependencies of an event may change either by dropping some of them or by adding new ones ( [START_REF] Arbach | Dynamic causality in event structures[END_REF]). This short and incomplete discussion (the event structures spectrum is rather broad) should point out the variety of approaches present in literature. It should be also observed that the majority of the approaches model causality with a relation that can be reduced to a partial order, hence causality is represented stating what are the events that should have happened before.

In this paper we introduce yet another notion of event structure. Triggered by recent works on adding or subtracting dependencies among events based on the fact that apparently unrelated events have happened ( [START_REF] Arbach | Dynamic causality in event structures[END_REF][START_REF] Arbach | Dynamic Causality in Event Structures[END_REF]), we argue that rather than focussing on how to model these enrichment or/and impoverishment, it is much more natural to focus on the context on which an event takes place. In fact it is a context that can determine the proper dependencies that are applicable at the state where the event should take place and the context holds, and the context can also be used as well to forbid that the event is added to the state. This new relation resembles the one used in inhibitor event structures ( [START_REF] Baldan | Domain and event structure semantics for Petri nets with read and inhibitor arcs[END_REF]), but it differs in the way the contexts are determined. In the case of inhibitor event structures the presence of a certain event (the inhibiting context) was used to require that another one was present as well (representing the trigger able to remove the inhibition). Here the flavour is different as it is more prescriptive: it is required that exactly a set of events is present and if this happens then also another one should be present as well. It should be stressed that triggers and contexts may exchange their role. Consider again the two nets depicted before, we may have that in both cases the trigger is determined by the happening of the event e and the context is the empty set, but we can consider as context the event e and the trigger as the empty set. This simple relation, which we will call context-dependency relation, suffices to cover the various notions presented in literature. It is worth observing that determining the context and the triggers associated to it is quite similar to trying to understand the dependencies. Consider the net N below.

N e e e

Here e may be added either to the empty set or to a set containing both e and e . The context containing e only leads to require that the event e is present (in the spirit of the relation for inhibitor event structures), making e dependent on e . However we could also have chosen to focus on contexts only and in this case the context containing just e is ruled out among the contexts in which, together with some others dependencies, e may take place, and in this case the two contexts are ∅ and {e , e }. As hinted above, it will turn out that the context plays a more relevant role with respect to the dependencies, as the context can be seen positively (it specifies under which conditions an event can be added, together with the dependency) or negatively (it specifies under which conditions an event can be added, and in this case the event cannot be added simply stipulating that it depends on itself).

In this paper we will focus on event structures where the change of state is always triggered by the happening of a single event, hence we will not consider steps (i.e. non empty and finite subsets of events), and where the states (configurations) are finite, though not always explicitly assumed. However the generalization to steps is straightforward.

Organization of the paper: In the next section we will introduce and discuss the new brand of event structure. In 3 we will review and briefly analyze some notions of event structures presented in literature, namely prime event structure ( [START_REF] Winskel | Event Structures[END_REF]), relaxed prime event structure and dynamic causality event structure ( [START_REF] Arbach | Dynamic causality in event structures[END_REF]), inhibitor event structure ( [START_REF] Baldan | Domain and event structure semantics for Petri nets with read and inhibitor arcs[END_REF]) and event structure for resolvable conflicts ( [START_REF] Van Glabbeek | Event structures for resolvable conflict[END_REF]), and, in section 4, we show that the each event structure presented in section 3 can be translated into this new kind of event structure. We will recall also the notion event automata which will can used to compare the various notions of event structure. We will end the paper with some conclusions and we will give some hints for further developments.

Notation: Let A be a set, with let ρ we denote a sequence of elements belonging to A, and with we denote the empty sequence. With ρ we denote the set of elements of A appearing in ρ. Thus ρ = ∅ if ρ = and aρ = {a} ∪ ρ if ρ = aρ . Given a sequence ρ = a 1 • • • a n with len(ρ) we denote its length, with ρ 0 we sometime denote sequence and, if len(ρ) ≥ 1, for each 1 ≤ i ≤ len(ρ) with ρ i we denote the sequence a 1 • • • a i . Let A be a set, with 2 A we denote the subsets of A and with 2 A fin the finite subsets of A.

Context-Dependent Event Structure

We introduce yet another notion of event structure, which is the main contribution of the paper.

We start recalling what an event is and we introduce the notion of configuration. An event is an atomic individual action which is able to change the state of a system. Event structures in particular are intended to model concurrent systems by defining relationships among events such as causality and conflict, establishing the conditions on which a certain event can be added to a state. The state of a system modeled by an event structure is a subset of events (those happened so far), and this set of events is called configuration. States can be enriched by adding other information beside the one represented by the events that have determined the state, either adding information on the relationship among the various events in the state, e.g. adding dependencies among them (the state is then a partial order, [START_REF] Rensink | Posets for configurations![END_REF]) or adding suitable information to the whole state.

We pursue this idea that the happening of an event depends on a set of modifiers (the context) and on a set of real dependencies, which are activated by the set of modifiers.

We recall that in this paper we will consider only unlabelled event structures. To simplify the presentation we retain the classic binary conflict relation. Given a subset X ⊆ E of events and a conflict relation #, which is an irreflexive and symmetric relation, we say that X is conflict free iff ∀e, e ∈ X it holds that ¬(e # e ). The cd-relation models, for each event, which are the possible contexts in which the event may happen (the first component of each pair) and for each context which are the events that have to be occurred (the second component). We stipulate that dependencies and contexts are formed by non conflicting events, though this is not strictly needed, as the relation can model also conflicts. How this relation is used will become clear in the notion of enabling of an event. We have to determine, for each Z e, which of the contexts X i should be considered. To do so we define the context associated to each entry of the cd-relation. Given Z e, where Z = {(X 1 , Y 1 ), . . . , (X n , Y n )}, with Cxt(Z) we denote the set of events |Z| i=1 X i , and this is the one regarding Z e.

Definition 1. A context-dependent event structure (cdes) is a triple E = (E, #, ) where -E is a set of events, -# ⊆ E × E is
Definition 2. Let E = (E, #, ) be a cdes and C ⊆ E be a subset of events.

Then the event e ∈ C is enabled at C, denoted with C[e , if for each Z e, with Z = {(X 1 , Y 1 ), . . . , (X n , Y n )}, there is a pair (X i , Y i ) ∈ Z such that Cxt(Z)∩C = X i and Y i ⊆ C.
Observe that requiring the non emptiness of the set Z in Z e guarantees that an event e may be enabled at some subset of events. The cd-relation could be used to express conflicts: e # e could be modeled by adding {({e}, {e })} e and {({e }, {e})} e to the relation, and the presence of just one of them would model the asymmetric conflict. The conflicts modeled in this way are persistent. Definition 3. Let E = (E, #, ) be a cdes. Let C be a subset of E. We say that C is a configuration of the cdes E iff there exists a sequence of distinct

events ρ = e 1 • • • e n • • • over E such that -ρ = C, -ρ is conflict-free, and -∀1 ≤ i ≤ len(ρ). ρ i-1 [e i .
Denoting with Conf cdes (E ) the set of configurations of a cdes, we introduce the relation among configurations. Given two configurations C and C of a cdes

such that C ∪ {e n+1 } = C , we stipulate that C → cdes C iff C[e n+1 .
We illustrate this new kind of event structure with some examples.

Example 1. Consider three events a, b and c. All the events are singularly enabled but a and b are in conflict unless c has not happened (we will see later that this are called resolvable conflicts). Hence for the event a we stipulate {(∅, ∅), ({c}, ∅), ({b}, {c})} a that should be interpreted as follows: if the context is ∅ or {c} then a is enabled without any further condition (the Y are the empty set), if the context is {b} then also {c} should be present. The set Cxt({(∅, ∅), ({c}, ∅), ({b}, {c})}) is {b, c}.

Similarly, for the event b we stipulate

{(∅, ∅), ({c}, ∅), ({a}, {c})} b
which is justified as above and finally for the event c we stipulate

{(∅, ∅), ({a}, ∅), ({b}, ∅)} c
namely any context allows to add the event.

Below we depict the configurations and how they are related. These examples should clarify how the cd-relation is used and its expressivity.

Event structures

We have introduced a new notion of event structure that we should confront with the others presented in literature (at least some of them). Therefore we review some of the various definitions of event structures.

Prime event structures: Prime event structures are one among the first proposed and the most widely studied ( [START_REF] Winskel | Event Structures[END_REF]), especially for the connections with prime algebraic domains and causal nets. The dependencies among events are modeled using a partial order relation, the incompatibility among events is modeled using a symmetric and irreflexive relation, the conflict relation, and it is required that the conflict relation is inherited along the partial order. Given an event e ∈ E, with e we denote the set {e | e ≤ e}, and the requirement that the partial order is well founded implies that for each e ∈ E, the set e is finite. We say that C is a configuration of the pes P iff C is conflict free and for each e ∈ C it holds that e ⊆ C. The set of configuration of a pes is denoted with Conf pes (P ). Clearly (Conf pes (P ), ⊆) is a partial order. With → pes we denote the relation over Conf pes (P ) × Conf pes (P ) defined as

C → pes C iff C ⊂ C and C = C ∪ {e} for some e ∈ E.
Relaxed prime event structures: Some of the requirements of a pes, the one on the dependencies among events (here called enabling) and the ore regarding the conflicts among events (which does not need to be saturated), can be relaxed yielding a relaxed prime event structure ( [START_REF] Arbach | Dynamic causality in event structures[END_REF][START_REF] Arbach | Dynamic Causality in Event Structures[END_REF]). In this definition the events that must be present in a state to allow the execution of another one are the events in a (finite) subset called immediate causes and often denoted with ic. The intuition is that the → relation plays the role of the causality relation and the conflict relation models conflicts among events, as before. The immediate causes can be seen as a mapping ic : E → 2 E fin . Let T = (E, →, #) be a rpes. Let C be a subset of E. We say that C is a configuration of the rpes T iff there exists a sequence of distinct events ρ = e 1 • • • e n • • • over E such that ρ = C, ρ is conflict free, and for each 1 ≤ i ≤ len(ρ). ic(e i ) ⊆ ρ i-1 . The set of configuration of a rpes is denoted with Conf rpes (T ). In rpes the emphasis is put on the existence of an ordering in which the events are added to a configuration, and this will be valid for many of the kinds of event structures. (Conf rpes (T ), ⊆) is a partial order. With → rpes we denote the relation over Conf rpes (T ) × Conf rpes (T ) defined as

C → rpes C iff C ⊂ C and C = C ∪ {e} for some e ∈ E.
A pes is also a rpes: the causality relation is the enabling relation and the conflict relation is the same one. e is added to a configuration C when its causes are in C and no conflict arises. Given a rpes T = (E, →, #), it is not difficult to see that (E, → * , #) is a pes, where → * is the reflexive and transitive closure of → and # is obtained by # stipulating that # ⊆ # and it is closed with respect to → * , i.e. if e # e → * e then e # e . Indeed, the fact that → * is a partial order is guaranteed by the fact that each event is executable, that → * is well founded is implied by the finiteness of causes for each event e ∈ E and # is the semantic closure of #: no new conflict is introduced.

Dynamic Causality Event Structures: We now review a notion of event structure where causality may change ( [START_REF] Arbach | Dynamic causality in event structures[END_REF][START_REF] Arbach | Dynamic Causality in Event Structures[END_REF]). The idea is to enrich a rpes with two relations, one modeling the shrinking causality (some dependencies are dropped) and the other the growing causality (some dependencies are added). The shrinking and the growing causality relations are ternary relations stipulating that the happening of a specific event (the modifier ) allows to drop or add a specific cause (the contribution) for another event (the target).

We illustrate these relations with the aid of a number of auxiliary subsets of events associated to these relations. Let E be a set of events. A shrinking causality relation is a ternary relation For further comments on this definition we refer to [START_REF] Arbach | Dynamic causality in event structures[END_REF] and [START_REF] Arbach | Dynamic Causality in Event Structures[END_REF]. It should be observed, however, that the definition we consider here is slightly less general of the one presented there, as we add a further condition, the last one, which is defined in [START_REF] Arbach | Dynamic causality in event structures[END_REF] and does not allow that the same contribution can be added and removed by two different modifiers. These are called in [START_REF] Arbach | Dynamic causality in event structures[END_REF] single state dynamic causality event structures and rule out the fact that some causality (or absence of) depends on the order of modifiers. Conditions 1 and 2 simply state that in the case of the shrinking relation the dependency should be present, and in the case of the growing the dependency should be absent; condition 3 says that if a dependency is added then it cannot be removed, or a removed dependency cannot be added, and the final condition express the fact that two modifiers, one growing and the other shrinking, cannot act on the same dependency. Clearly a dces where ¡ and are empty is a rpes. Let D = (E, →, #, ¡, ) be a dces. Let C be a subset of E. We say that C is a configuration of the dces iff there exists a sequence of distinct events ρ = e 1 • • • e n over E such that (a) ρ = C, (b) ρ is conflict-free, and (c) Inhibitor event structures: Inhibitor event structure ( [START_REF] Baldan | Domain and event structure semantics for Petri nets with read and inhibitor arcs[END_REF]) are equipped with a relation

¡ ⊆ E × E × E,
∀1 ≤ i ≤ len(ρ). ((ic(e i ) ∪ ac(ρ i-1 , e i )) \ dc(ρ i-1 , e i )) ⊆ ρ i-1 .
⊆ 2 E 1 × E × 2 E
fin allowing to model conflicts (even asymmetric) as well as temporary inhibitions. With 2 E 1 we denote the subsets of events with cardinality at most one (the empty set or singletons). The intuition behind this relation is the following: given (a, e, A), the event e is enabled at a configuration is whenever the configuration contains the set a, then its intersection with A is non empty. Hence the event in a non empty a inhibits the happening of e unless some event in A has happened as well. We stipulate that given (a, e, A) the events in A are pairwise conflicting (denoted with #(A)). Two events e and e are in conflict if ({e }, e, ∅) and ({e}, e , ∅). An or -causality relation < is definable stipulating that A < e if (∅, e, A), and that if A < e and B < e for some e ∈ A then also B < e. This relation should be interpreted as follows:

A < e means that if e is present, then also an event in A should be present. Definition 7. An inhibitor event structure (ies) is a pair I = (E, ), where E is a set of events and

⊆ 2 E 1 × E × 2 E
fin is a relation such that for each (a, e, A) it holds that #(A) and a ∪ A = ∅.

We briefly recall the intuition: consider an event e and a triple in the relation (a, e, A). Then e can be added provided that if the event in a is present also one in A should be present. Let I = (E, ) be an ies. Let C be a subset of E. We say that C is a configuration of the ies I iff there exists a sequence of distinct events Event structures with resolvable conflicts: We finally recall the notion of event structure with resolvable conflicts ( [START_REF] Van Glabbeek | Event structures for resolvable conflict[END_REF]). Definition 8. An event structure with resolvable conflicts ( rces) is the pair R = (E, ) where E is a set of events and ⊆ 2 E × 2 E is the enabling relation.

ρ = e 1 • • • e n • • • over E such that ρ = C and for each i ≤ n, for each (a, e i , A), it holds that a ⊆ ρ i-1 ⇒ ρ i-1 ∩A = ∅.
No restriction is posed on the enabling relation. The intuition is that stipulating X Y one state that for all the events in Y to occur, also the events in the set X should have occurred first.

The single event transition relation

Y⊆ 2 E × 2 E of a rces R = (E, ) is given by X Y Y ⇔ (X ⊆ Y ∧ |Y \ X| ≤ 1 ∧ ∀Z ⊆ Y. ∃W ⊆ X. W Z)
. With this notion it is possible to define what a configuration is: it is a subset X of events such that X Y X. The requirement that X Y X implies that each subset of events is enabled in the configuration. Let R = (E, ) be a rces. Let C be a subset of E. We say that C is a configuration of the ies I iff there exists a sequence of distinct events ρ = e 1 • • • e n • • • over E such that for each 1 ≤ i ≤ len(ρ) it holds that ρ i-1 and ρ i are configurations, and ρ i-1 Y ρ i . The set of configuration of a rces is denoted with Conf rces (R).

Given two configurations C and C of a rces, such that C ∪ {e n+1 } = C and C Y C, we stipulate again that ρ → dces ρ , defining a relation over Conf rces (R)× Conf rces (R). Observe that the enabling relation is used not only to state under which condition an event may happen but also to stipulate when an event is deducible from a set of events, justifying also the deduction symbol used for this relation. Observe also that → rces is essentially Y. Example 6. Consider three events a, b and c, and ∅ X where X ⊆ {a, b, c} with X = {a, b} and {c} {a, b}. The intuition is that all the events are singularly enabled but a and b are in conflict unless c has not happened. In fact {a, b} is not a configuration as taking {a, b} as the Z ⊆ {a, b} of the notion of single event transition relation, there is no subset of {a, b} enabling these two events.

The configurations and how they are reached are those of the Example 1.

Embedding and comparing Event Structures

We now show that each of the event structure we have seen so far can be seen as a cdes, and also how to compare them. For the sake of simplicity, we will consider event structures where each event e is executable, namely that there is at least a configuration containing it.

Comparing Event Structures: We start by devising how we can compare two event structures of any kind. The intuition is obvious: two event structures are equivalent iff they have the same configurations and the → relations defined on configurations coincide. We recall the notion of event automaton ( [START_REF] Pinna | On the nature of events: another perspective in concurrency[END_REF]).

Definition 9. Let E be a set of events. An event automaton over E (ea) is the tuple E = E, S, →, s 0 such that -S ⊆ 2 E , and -→⊆ S × S is such that s → s implies that s ⊂ s .

s 0 ∈ S is the initial state.

Event automata can easily express configurations of any kind of event structure, provided that for each kind a way to reach a configuration from another is given. The kind of event structure is ranged over by µ, µ ∈ {pes, rpes, dces, ies, rces, cdes}.

Theorem 1. Let X be an event structure of kind µ over the set of events E.

Then G µ (X ) = E, Conf µ (X ), → µ , ∅ is an event automaton.
Using event automata we can decide when two event structures are equivalent.

Definition 10. Let X and Y be event structures over the same set of events E of kind µ and µ respectively. We say that X and Y are equivalent, denoted with

X ≡ Y , iff G µ (X ) = G µ (Y ).
The expressivity is explicitly studied in [START_REF] Arbach | Dynamic causality in event structures[END_REF] and [START_REF] Arbach | Dynamic Causality in Event Structures[END_REF]. Informally a kind of event structure is more expressive with respect to another, when there is a configuration of the former that cannot be a configuration of the latter, whatever is done with the various relations among events. Incomparable means that neither one is more expressive than the other or the vice versa. We shortly summarize part of these findings, when considering finite configurations. pes and rpes are equally expressive, whereas ses and ges are strictly more expressive than rpes, and are incomparable one with respect to the other. These two are both less expressive than dces and rces, which are incomparable. The relative expressivity of other kinds of event structure has not been investigated.

Embedding event structures into cdes: We prove now a more general result, namely that given any event automaton E, which is obtained by the configurations of any kind of event structure, it is possible to obtain a cdes whose configurations are precisely the ones of the event automaton E. We start identifying, in an ea, the events that are in conflict. The conflict relation we obtain is a semantic conflict relation: two events are in conflict iff they never appear together in a state. Definition 11. Let E = E, S, →, s 0 be an ea. We define a symmetric and irreflexive conflict relation # ea as follows: e # ea e iff for each s ∈ S. {e, e } ⊆ s.

In order to obtain the cd-relation we need some further definitions. Fixed an event e, the first one identifies the states where this event can be added, and the second one identifies the states where the event cannot be added. Definition 12. Let E = E, S, →, s 0 be an ea. To each event e ∈ E we associate the subset of events {s ∈ S | s ∪ {e} ∈ S ∧ s → s ∪ {e}}, which we denote with C(E, e). Definition 13. Let E = E, S, →, s 0 be an ea. To each event e ∈ E we associate the set of configuration {s ∈ S | s ∪ {e} ∈ S}, which we denote with I(E, e).

Definition 12 characterizes when an event is enabled giving the allowing context, whereas the Definition 13 gives the context where the event cannot be added, and it is called negative context. These two sets are used to obtain the cd-relation. The theorem has a main consequence, namely that event automata and cdes are equally expressive. As a consequence of the Theorem 2 we have the following result.

Corollary 1. Let X be an event structure of type µ and let G µ (X ) be the associated ea. Then F ea (G µ (X )) is cdes, and X ≡ F ea (G µ (X )).

The construction identifies properly the context in which an event is allowed to happen, and this context becomes the main ingredient of the cd-relation, as the construction does not give the causes but just the context. If on the one hand this suggests that the context, rather than the causal dependencies, is the relevant ingredient, on the other hand it is less informative with respect to the usual causality definitions.

We review some kind of event structures, showing that a more informative cd-relation can be indeed obtained. We will focus only on few of them. pes: In this case the idea is that causes of an event are just the set of events that should be present in the configuration.

Proposition 1. Let P = (E, ≤, #) be a pes. Then F pes (P ) = (E, #, ) is a cdes, where {(∅, e \ {e})} e for each e ∈ E. Furthermore P ≡ F pes (P ). This is not the unique way to associate to the causality relation ≤ of a pes the relation: one alternative would have been to add {(∅, {e })} e for each e < e and another one would be {( e \ {e}, ∅)} e showing that the events causally before e are indeed the context allowing the event e to happen. ies: In the case of ies there are two main observations: one, there is no conflict relation, and second, though there is some similarity between the relation and the relation, there is also a quite subtle difference. When adding an event e to a configuration of an ies, and we have (a, e, A), one would simply add the pairs (a, {e }) for each e ∈ A (as the events in A are pairwise conflicting) but this does not work in the case A is the empty set, as it has a different meaning in the relation with respect to the relation. In the former, it means that the event in a inhibits the event e, whereas in the latter the pair (a, ∅) simply says that if the context a is present then there is no further event needed. Taking into account these differences, the translation is fairly simple. We first define the conflict relation and then the relation , which is almost the same as the relation. Higher order causality: The comparison with event structures with higher-order dynamics of [START_REF] Karcher | Higher-order dynamics in event structures[END_REF] is done indirectly, as these are equivalent to event structures with resolvable conflicts. In this approach the relations ¡ and are generalized to take into account set of modifiers, targets and contributions. The drawback is that the happening of an event implies a recalculation of these relation, similarly to what it is done in causal automata. In fact it is fairly obvious that given one simple step transition graph (meaning that a configuration is reached by another one adding just one event), it is always possible to obtain a cdes.

Conclusion

In this paper we have introduced a new brand of event structure where the main relation, the cd-relation, models the various conditions under which an event can be added to a subset of events. The relation is now defined as

⊆ 2 A × E,
where A ⊆ 2 E × 2 E , thus it stipulates for each event which are the contextdependency pairs, but it can be easily generalized to subsets of events modeling precisely, when events happen together (as it is done in [START_REF] Pinna | Modeling dependencies and simultaneity in membrane system computations[END_REF] or [START_REF] Van Glabbeek | Event structures for resolvable conflict[END_REF]). The focus is on the contexts in which an event can be added, which may change, rather that modeling the dependencies and how these may change. Here the choice is whether it is better to focus on dependencies (and how they may change) or on the context. The advantage of the latter is its generality, whereas the former may be useful in pointing out relations among events. It should be clear that this kind of event structures is capable of modeling the same enabling situation for an event in various way, and it could be interesting to understand if there could be an informative way canonically. In fact, the canonical relation just focus on all the contexts in which an event can be added, and the dependency set is less informative. Thus finding a way to identify minimal contexts together with a set of dependencies may be useful, similarly to what it has been discussed when associating pes to cdes.

It remains to stress that cdes can be generalized not only allowing steps but also representing contexts in a richer way. Here we have considered contexts as subset of events, but they can have a richer structure. This would allow to characterize more precisely contexts, allowing, for instance, to drop the last requirement we have placed on dces, as in this case the order in which the modifiers appear may influence the dependencies. Finally we observe that the idea of context is not new, for instance they have been considered in [START_REF] Leifer | Transition systems, link graphs and petri nets[END_REF] or in [START_REF] Baldan | A semantic framework for open processes[END_REF], and a comparison with these should be considered.

In this paper we have considered various event structures, still some interesting notions remained out of the scope of this paper, like reversible event structures [START_REF] Phillips | Reversibility and asymmetric conflict in event structures[END_REF], but we are confident that our approach can be used also in the reversibility setting.

  a Petri net with inhibitor arcs ([START_REF] Janicki | Semantics of inhibitor nets[END_REF]) where the precondition of the Work partially funded by RAS (Regione Autonoma della Sardegna) -L.R. 7/2007 -Project SardCoin, CUP: F72F16003030002).

Example 2 .Example 3 .

 23 Consider three events a, b and c, and assume that c depends on a unless the event b has occurred, and in this case this dependency is removed. Thus there is a classic causality between a and c, but it can dropped if b occurs. Clearly a and b are always enabled. The cd-relation is {(∅, ∅)} a, {(∅, ∅)} b and {(∅, {a}), ({b}, ∅)} c. Consider three events a, b and c, and assume that c depends on a just when the event b has occurred, and in this case this dependency is added, otherwise it may happen without Thus the classic causality relation between a and c is added if b occurs. Again a and b are always enabled. The cd-relation is {(∅, ∅)} a, {(∅, ∅)} b and {(∅, ∅), ({b}, {a})} c.

Definition 4 .

 4 A prime event structure (pes) is a triple P = (E, ≤, #), where (a) E is a set of events, (b) ≤⊆ E × E is a well founded partial order called causality relation, (c) # ⊆ E × E is an irreflexive and symmetric relation, called conflict relation, such that e # e ≤ e ⇒ e # e , and (c) ≤ ∩# = ∅.

Definition 5 .

 5 A relaxed prime event structure ( rpes) is a triple (E, →, #), where (a) E is a set of events, (b) → ⊆ E × E is the enabling relation such that ∀e ∈ E the set ic(e) = {e | e → e} is finite, and (c) # ⊆ E × E is an irreflexive and symmetric conflict relation.

  and the elements of this relation are denoted with e ¡ [e → e ]. Given e ¡ [e → e ], e is called modifier, e target and e contribution. ShrMod(e ) = {e | e ¡ [e → e ]} is the set of modifiers for a given target e and Drop(e , e ) = {e | e ¡ [e → e ]} is the set of contributions for a given modifier e and a given target e . Let H be a finite subset of E and let e be an event, we define the set dc(H, e) = e ∈H∩ShrMod(e) Drop(e , e) as the set of dropped causes with respect to H for the event e. A growing causality relation is a ternary relation ⊆ E × E × E, and the elements of this relation are denoted as e [e → e ] Given e [e → e ], e is called modifier, e target and e contribution. GroMod(e ) = {e | e [e → e ]} is the set of modifiers for a given target e and Add(e , e ) = {e | e [e → e ]} is the set of contributions for a given modifier e and a given target e . Let H be a finite subset of E and let e be an event, we define the set ac(H, e) = e ∈H∩GroMod(e) Add(e , e) as the set of added causes with respect to H for the event e. The two relation of shrinking and growing causality give the functions dc : 2 E fin × E → 2 E fin . and ac : 2 E fin × E → 2 E fin . Definition 6. A dynamic causality event structure (dces) is a quintuple D = (E, →, #, ¡, ), where (E, →, #) is a r pes, ¡ ⊆ E × E × E is the shrinking causality relation, ⊆ E × E × E is the growing causality relation, and are such that for all e, e , e ∈ E 1. e ¡ [e → e ] ∧ e ∈ E. e [e → e ] =⇒ e → e , 2. e [e → e ] ∧ e ∈ E.e ¡ [e → e ] =⇒ ¬(e → e ), 3. e [e → e ] =⇒ ¬(e ¡ [e → e ]), and 4. ∀e, e ∈ E. e , e ∈ E. e ¡ [e → e ] and e [e → e ].

  The set of configuration of a dces is denoted with Conf dces (D). With → dces we denote the relation over Conf dces (D) × Conf dces (D) defined as C → dces C iff C ⊂ C , C = C ∪ {e} for some e ∈ E and ((ic(e) ∪ ac(C, e)) \ dc(C, e)) ⊆ C. Example 4. Consider the set of events {a, b, c, d, e}, with b → c, a ¡ [b → c], d [e → c], a # e and d # b. a and d are the modifiers for the target c, the happening of a has the effect that the cause b may be dropped, and the one of d that the cause e should be added for c. If the prefix of the trace is bc (the target c is executed before of one of its modifiers a and d) then the final part of the trace is any either a or e, and as d # b we have that d cannot be added. If the modifier a is executed before c then we have the traces ac (as the immediate cause b of c is dropped by a) followed by b or d, and if the modifier d is executed, then before adding c, we need e (the modifier d add the immediate cause e for c), and in this case we cannot add b for sure as it is in conflict with d or a as it is in conflict with e. If both modifiers a and d happen, then the event c is permanently disabled, as it needs the contribution e (growing cause) which is in conflict with a. Below are shown the configurations of this dces and the → dces relation. {a, b, c} {e, b, c} {e, d, c} A shrinking event structure (ses) is a dces where the relation is empty and a growing event structure (ges) is a dces where the ¡ relation is empty.

Example 5 .

 5 The set of configuration of a ies is denoted with Conf ies (I ). With → ies we denote the relation over Conf ies (I ) × Conf ies (D) defined as C → ies C iff C ⊂ C and C = C ∪ {e} for some e ∈ E. Consider three events a, b and c, ({a}, c, {b}) and (∅, b, {a}). The maximal event traces are cab and abc. The event c is inhibited when the event a has occurred unless the event b has occurred as well. The configurations are ∅, {a}, {c}, {a, b}, {a, c} and {a, b, c} and are reached as follows: ∅ → ies {a}, ∅ → ies {c}, {a} → ies {a, b}, {c} → ies {a, c}, {a, b} → ies {a, b, c} and {a, c} → ies {a, b, c}.

Theorem 2 .

 2 Let E = E, S, →, s 0 be an ea. Then F ea (E) = (E, #, ) is a cdes, where # is the relation # ea of Definition 11, and for each e ∈ E we have {(X, ∅) | X ∈ C(E, e)} ∪ {(X, {e}) | X ∈ I(E, e)} e. Furthermore E ≡ G cdes (F ea (E)).

Example 7 .

 7 Consider the rces of the Example 6. The associated event automaton is the one depicted in the Example 1. It has no conflict as all the three events are present in a configuration together. The associated cd-relation, obtained using Definition 12 and Definition 13, is the following one, which is a little different from the one devised in the Example 1 as here it is obtained from an event automaton. {(∅, ∅), ({c}, ∅), ({c, b}, ∅), ({b}, {a})} a because the set C(Conf rces (R), a) contains the sets ∅, {c} and {c, b}, whereas the set of the negative context I(Conf rces (R), a) contains just {b}, the one {(∅, ∅), ({c}, ∅), ({a, b}, ∅), ({a}, {b})} b as C(Conf rces (R), b) contains the sets ∅, {c} and {a, c}, I(Conf rces (R), b) contains {a}, and finally {(∅, ∅), ({a}, ∅), ({b}, ∅)} c as C(Conf rces (R), c) contains the sets ∅, {a} and {b}, and I(Conf rces (R), c) is the empty set.

Example 8 .Example 9 .

 89 Consider the pes ({a, b, c}, ≤, #) where a ≤ b (we omit the reflexive part of the ≤ relation), a # c and b # c. The event traces are , a, ab and c, and the associated configurations are ∅, {a}, {a, b} and {c} (the → pes relation is obvious). The conflict relation is the same and the cd-relation is {(∅, ∅)} a, {(∅, ∅)} c and {(∅, {a})} b. As noticed before we could have stipulated also {({a}, ∅)} b instead of {(∅, {a})} b obtaining the same set of configurations and the same transition graph. dces: The intuition in this case consists in mixing the two approaches above. Proposition 2. Let D = (E, #, →, ¡, ) be a dces. F dces (D) = (E, #, ) is a cdes where the relation is defined as {(X, (ic(e) \ ( e ∈X Drop(e , e))) ∪ e ∈X Add(e , e)) | X ⊆ GroMod(e) ∪ ShrMod(e) e for each e ∈ E. Furthermore D ≡ F dces (G). Concerning the dces of the example 4, the conflict relation is the one of the dces whereas the cd-relation is {(∅, ∅)} a, {(∅, ∅)} b, {(∅, ∅)} e, {(∅, ∅)} d and for c we have {(∅, {b}), ({a}, ∅), ({d}, {b, e}), ({a, d}, {e})} c.

Proposition 3 .Example 10 .

 310 Let I = (E, ) be an ies. F ies (I ) = (E, #, ) is a cdes, where e # e iff ({e}, e , ∅) and ({e }, e, ∅) , and for each e ∈ E, if (a, e, A) and A = ∅ then {(∅, ∅)} ∪ {(a, {e }) | e ∈ A} e, if (a, e, A) and A = ∅ then {(a, {e})} e. Furthermore I ≡ F ies (I ). The ies of the example 5 induces the empty conflict relation, and the cd-relation is {(∅, ∅)} a, {(∅, {a})} b and {(∅, ∅), ({a}, {b})} c.

  an irreflexive and symmetric relation, called conflict relation, and -⊆ 2 A × E, where A ⊆ 2 E fin × 2 E fin , is a relation, called the contextdependency relation ( cd-relation), which is such that for each Z e it holds that • Z = ∅, and • for each (X, Y ) ∈ Z it holds that X and Y are conflict-free. Each element of the cd-relation is called entry.


Jean-Marie Jacquet
email: jean-marie.jacquet@unamur.be

Manel Barkallah
email: manel.barkallah@unamur.be

Scan: a Simple Coordination Workbench

Keywords: Coordination, Bach, animation, verification

Although many research efforts have been spent on the theory and implementation of data-based coordination languages, not much effort has been devoted to constructing programming environments to analyze and reason on programs written in these languages. This paper proposes a simple workbench for describing concurrent systems using a Linda-like language, for animating them and for reasoning on them using a fragment of linear temporal logic. In contrast to some tools developed for traditional process algebras like CCS, a key feature of our workbench is that it maintains a direct relation between what is written by the user and its internal representation in the workbench. Another feature, particularly useful for didactic purposes, is the production of trace examples, replayable, when LTL formulae are satisfied.

Introduction

In the aim of building interactive distributed systems, a clear separation between the interactional and the computational aspects of software components has been advocated by Gelernter and Carriero in [START_REF] Gelernter | Coordination Languages and Their Significance[END_REF]. Their claim has been supported by the design of a model, Linda [START_REF] Carriero | Linda in Context[END_REF], originally presented as a set of inter-agent communication primitives which may be added to almost any programming language. Besides process creation, this set includes primitives for adding, deleting, and testing the presence/absence of data in a shared dataspace.

A number of other models, now referred to as coordination models, have been proposed afterwards. The authors have themselves contributed to that trend of research, as exemplified for instance in [1, 2, 7-10, 15, 17, 21-23]. However, although many pieces of work (including ours) have been devoted to the proposal of new languages, semantics and implementations, few articles have addressed the concerns of practically constructing programs in coordination languages, in particular in checking that what is described by programs actually corresponds to what has to be modeled.

Based on previous work by the first author on a Linda-like dialect, named Bach, this paper aims at introducing a workbench to reason on programs written in Bach extended with several facilities. More specifically, our goal is threefold: Fig. 1. Rush Hour Problem. On the left part, the game as illustrated at https://www.michaelfogleman.com/rush. On the right part, the game modeled as a grid of 6 × 6, with cars and trucks depicted as rectangles of different colors.

to allow the user to understand the meaning of instructions written in Bach, by showing how they can be executed step by step and how the contents of the shared space, central to coordination languages, can be modified so as to release suspended processes; to allow the user to better grasp the modeling of real-life systems in Bach, by connecting agents in Bach to animations, representing the evolution of the modeled system; to allow the user to check properties by model checking temporal logic formulae and by producing traces that can be replayed as evidences of the establishment of the formulae.

In building the workbench, we also aim at two main properties:

the tool should be simple to deploy and to use. As a result, we shall build it as a standalone executable file launched by a simple command line. We shall also propose a simple process algebra that allows the user to concentrate on the key coordination and animation features and consequently avoid him the burden of handling extra features typically required by sophisticated commercial systems; the tool should maintain a direct relation between what is written by the user and its internal representation. This property allows the user to better grasp what is actually computed as well as to produce meaningful traces.

To make our developments more concrete, we shall use the rush hour puzzle as a running example. This game, illustrated in Figure 1, consists in moving cars and trucks on a 6 × 6 grid, according to their direction, such that the red car can exit. It can be formulated as a coordination problem by considering cars and trucks as autonomous agents which have to coordinate on the basis of free places.

The rest of this paper is organized as follows. Section 2 describes the functionalities of Scan and, in doing so, provides an overview of the tool. Section 3 Fig. 2. The interactive blackboard window specifies the coordination language and temporal logic to be used in the tool. Section 4 sketches how Scan is implemented. Section 5 compares our work with related work. Finally, Section 6 draws our conclusion and suggests future work. For illustration purposes, a video demonstrating the use of Scan is available at https://staff.info.unamur.be/jmj/Scan/. A link is also proposed there to download the workbench.

Scan design and overview

Following Linda, the Bach language relies on a shared space to coordinate processes. It is this space that provides the decoupling of time and space of processes which is central to so-called data-based coordination languages [START_REF] Papadopoulos | Coordination Models and Languages[END_REF]. As a natural consequence, following the blackboard metaphor [START_REF] Erman | The Hearsay-II Speech-Understanding System: Integrating Knowledge to Resolve Uncertainty[END_REF], according to which a group of specialists iteratively updates knowledge on a blackboard starting from a problem specification, Scan is articulated around a so-called interactive blackboard. As depicted in Figure 2, it starts by displaying the current contents of the shared space and allows to interact directly through the tell, get and clear buttons. Moreover, it offers to create four types of processes.

The first two processes, named respectively Autonomous Agent and Interactive Agent, allow the user to enter instructions in Bach and to execute them. As depicted in part (a) of Figure 3, windows of the first kind, perform computations step-by-step by letting the user choose which primitives to execute. In contrast, as shown in part (b) of Figure 3, windows of the second type execute computations in one run if the run button is activated or step by step if the next button is selected but in both cases with the Scan workbench deciding (in a random manner) the primitives to be executed. It is worth noting that the execution in the windows are made in a parallel fashion, hence the name agent to indicate entities capable of concurrent activities. The facilities offered by the interactive and autonomous agents are nice to debug, at a low level, concurrent executions executed around the shared space, possibly deadlocking on data not being available. However, they do not provide much insights on whether what is described in Bach really reflects what the programmer intends to model. Moreover, they provide too many details on the main execution steps leading to a solution of the problem under consideration. To that end, Scan provides animations through a third kind of processes launched by the new description button (see Figure 2). As shown in part (a) of Figure 4, such animations are obtained by describing a so-called scene from a set of pictures which are handled by means of primitives for inserting them on the scene at specific places, making them visible or invisible, and making them move to specific places. In doing so, these primitives allow to draw and animate, at a 4. Note that, as these primitives may be inserted inside instructions of autonomous agents, the concurrent execution of these agents provides dynamic simulations of the problem under consideration.

Although nice, simulating graphically systems does not necessarily provide a solution to the problem under consideration. The rush hour problem is a clear example of that. To that end, the Scan workbench offers a fourth type of processes, materialized by the new model checker button of Figure 2 which gen-Fig. 5. Model-checking erates windows of the type depicted in Figure 5. As illustrated in this figure, Scan allows to verify formulae written in a fragment of linear temporal logic, to determine traces of execution that establish the formulae and to replay these traces, including the primitives that generate animations.

Although simple we believe that the Scan workbench meets the threefold goal expressed in the introduction:

by providing a view on the contents of the shared space and by means of the interactive and autonomous agents, the user can better understand the execution of programs written in Bach;

the animation facilities provide a high-level view on what is actually computed as well as an intuitive perception of the modeling of the problem under consideration;

the model checker facilities allow to check properties and, by using animation facilities, to replay executions graphically as a form of visual proofs.

3 The Anim-Bach language and its temporal logic

The facilities offered by Scan being described, let us turn to the process algebra to be used in the workbench. This algebra is subsequently referred to as Anim-Bach.

Definition of data

Following Linda, the Bach language [START_REF] Darquennes | On Multiplicities in Tuple-Based Coordination Languages: The Bach Family of Languages and Its Expressiveness Study[END_REF][START_REF] Jacquet | Coordinating Context-aware Applications in Mobile Adhoc Networks[END_REF] uses four primitives for manipulating pieces of information : tell to put a piece of information on a shared space, ask to check its presence, nask to check its absence and get to check its presence and remove one occurrence. In its simplest version, named BachT, pieces of information consist of atomic tokens and the shared space, called the store, amounts to a multiset of tokens. Although in principle sufficient to code many applications, this is however too elementary in practice to code them easily. To that end, we introduce more structured pieces of information which may employ sets defined by the user. Concretely, such sets are defined by associating an identifier with an enumeration of elements, such as in

set C o l s = { 1 , 2 , 3 , 4 , 5 , 6 } . Rows = { 1 , 2 , 3 , 4 , 5 , 6 } .
As the reader will have easily noticed, these two sets allow to identify an element of the grid of the rush hour example by using the row and column coordinates. We shall subsequently take the convention that the upper leftmost element of the grid is on the first row and on the first column.

The fact that sets are written as enumerations reflects the fact that the elements are naturally ordered by their order of appearance, which then allows to compare them. Moreover, they implicitly define the pred and succ functions, providing respectively the predecessors and successors of elements (if any).

In addition to sets, maps can be defined between them as functions that take zero or more arguments. In practice, Scan uses mapping equations as rewriting rules, from left to right in the aim of progressively reducing a complex map expression into a set element.

As an example of a map, assuming that trucks take three cells and are identified by the upper and left-most cell they occupy, the operation down truck determines the cell to be taken by a truck moving down: map down truck : Rows -> Rows . eqn down truck ( 1 ) = 4 . down truck ( 2 ) = 5 . down truck ( 3 ) = 6 .

Note from this example that mappings may be partially defined, with the responsibility put on the programmer to use them only when defined.

Structured pieces of information to be placed on the store consist of flat tokens as well as expressions of the form f (a 1 , • • • , a n ) where f is a functor and a 1 , . . . , a n are set elements. As an example, in the rush hour example, it is convenient to represent the free places of the game as pieces of information of the form free(i,j) with i a row and j a column.

In summary of this subsection, we may assume subsequently to be defined a series of sets, a series of mappings, and a set of structured pieces of information, say I. Thanks to the mapping definitions, we additionally assume a rewriting relation ; that rewrites any mapping expression into a set element. With this defined, we can proceed with the definition of agents in Anim-Bach.

Agents

The primitives of Anim-Bach consist of the tell, ask, nask and get primitives already mentioned for Bach, which take as arguments elements of I. They can be composed to form more complex agents by using traditional composition operators from concurrency theory: sequential composition, parallel composition and non-deterministic choice. We add another mechanism: conditional statements of the form c → s 1 s 2 , which computes s 1 if c evaluates to true or s 2 otherwise. Conditions of type c are obtained from elementary ones, thanks to the classical and, or and negation operators, denoted respectively by &, | and !. Elementary conditions are obtained by relating set elements or mappings on them by equalities (denoted =) or inequalities (denoted =, <, <=, >, >=).

This being given, the statements of the Anim-Bach language, also called agents by abuse of language, consist of the statements A generated by the following grammar:

A ::= P rim | P roc | A ; A | A || A | A + A | C → A A
where P rim represents a primitive, P roc a procedure call and C a condition.

Procedures are defined similarly to mappings through the proc keyword by associating an agent with a procedure name. As in classical concurrency theory, we assume that the defining agents are guarded, in the sense that any call to a procedure is preceded by the execution of a primitive or can be rewritten in such a form.

As an example, the behavior of a vertical truck can be described as follows:

proc V e r t i c a l T r u c k ( r : Rows , c : C o l s ) = ( ( r >1 & r <5) -> ( g e t ( f r e e ( pred ( r ) , c ) ) ; t e l l ( f r e e ( s u c c ( r ) , c ) ; V e r t i c a l T r u c k ( pred ( r ) , c ) ) + ( ( r <5) -> ( g e t ( f r e e ( down truck ( r ) , c ) ) ; t e l l ( f r e e ( r , c ) ) ;

V e r t i c a l T r u c k ( s u c c ( r ) , c ) ) ) .

The operational semantics of primitives and complex agents are respectively defined through the transition rules of Figures 6 and7. Configurations consist of agents (summarizing the current state of the agents running on the store) and a multi-set of structured pieces of information (denoting the current state of the store). In order to express the termination of the computation of an agent, the set of agents is extended by a special terminating symbol E that can be seen as a completely computed agent. For uniformity purposes, we abuse the language by qualifying E as an agent. To meet the intuition, we shall always rewrite agents of the form (E; A), (E || A) and (A || E) as A. The rules of Figure 6 follow the intuitive description of the primitives. Note however that before being processed, a structured piece of information t is rewritten in u by means of the rewriting relation ;.

(T) t ; u tell(t) | σ -→ E | σ ∪ {u} (A) t ; u ask(t) | σ ∪ {u} -→ E | σ ∪ {u} (G) t ; u get(t) | σ ∪ {u} -→ E | σ (N) t ; u, u ∈ σ nask(t) | σ -→ E | σ
The rules of Figure 7 are quite classical. Rules (S), (P) and (C) provide the usual semantics for sequential, parallel and choice compositions. As expected, rule (Co) specifies that the conditional instruction C → A B behaves as A if condition C can be evaluated to true and as B otherwise. Note that the notation |= C is used to denote the fact that C evaluates to true. Finally, rule (Pc) makes procedure call P (u) behave as the agent A defining procedure P with the formal arguments x replaced by the actual ones u.

Animations

Animations are obtained in a twofold manner: on the one hand, by describing the scene to be painted and, on the other hand, by primitives to place images, to make them appear or disappear and to move them.

The description of a scene is obtained by defining the size of the canvas to be used by the animation, the background image of the animation and a series of images to be used. Such a definition takes the following form: where the file names are given with respect to the path in which Scan is executed.

Images are manipulated by means of the following primitives where coordinates are expressed in pixels with respect to the canvas, with (0, 0) being the upper-left corner of the canvas: place at(i,x,y): to place image identified by i at the coordinates (x, y) move to(i,x,y): to move image identified by i from its current position to the new coordinates (x, y) hide(i): to hide image identified by i show(i) : to make appear image identified by i Such primitives are added to the tell, get, nask and ask primitives in the definition of Anim-Bach.

(S) A | σ -→ A | σ A ; B | σ -→ A ; B | σ (P) A | σ -→ A | σ A || B | σ -→ A || B | σ B || A | σ -→ B || A | σ (C) A | σ -→ A | σ A + B | σ -→ A | σ B + A | σ -→ A | σ (Co) |= C, A | σ -→ A | σ C → A B | σ -→ A | σ !C → B A | σ -→ A | σ (Pc) P (x) = A, A[x/u | σ -→ A | σ P (u) | σ -→ A | σ
It is worth observing that the map constructs (introduced before) allow to declare coordinates in a symbolic manner making it easy to specify the position of images.

A fragment of temporal logic

Linear temporal logic is a logic widely used to reason on dynamic systems. The Scan workbench uses a fragment of PLTL [START_REF] Emerson | Temporal and Modal Logic[END_REF] with, as main goal, to check the reachability of states.

As usual, the logic employed relies on propositional state formulae. In our coordination context, these formulae are to be verified on the current contents of the store. Consequently, given a structured piece of information t, we introduce #t to denote the number of occurrences of t on the store and define as basic propositional formulae, equalities or inequalities combining algebraic expressions involving integers and number of occurrences of structured pieces of information. An example of such a basic formulae is #f ree(1, 1) = 1 which states that the cell of coordinates (1, 1) is free.

Propositional state formulae are built from these basic formulae by using the classical propositional connectors. As particular cases, we use true and false to denote propositional formulae that are respectively always true and false. Such formulae are in fact shorthands to denote respectively p ∨ ¬p and p ∧ ¬p, for some basic propositional formula p.

The fragment of temporal logic used in Scan is then defined by the following grammar :

T F ::

= P F | Next T F | P F Until T F
where P F is a propositional formula. As will be explained in the next section, it has been designed so as to allow for an efficient implementation.

As an example, if the red car indicates that it leaves the grid by placing out on the store, a solution to the rush problem is obtained by verifying the formula true Until (#out = 1)

Implementation

The Scan workbench has been implemented in Scala [START_REF] Odersky | Programming in Scala, A comprehensive step-by-step guide[END_REF] on top of the Processing library [START_REF] Reas | Processing: A Programming Handbook for Visual Designers[END_REF]. Scala is a programming language which combines the object-oriented and functional paradigms and benefits from strong static type systems. Scala source code is compiled to Java bytecode, which eases its interface with Java libraries. Moreover, Scala includes powerful parsing facilities. All these properties make it well-suited to interpret the Anim-Bach language, which as can be appreciated by the previous sections, can be easily described by recursive definitions.

Processing is a graphical library built to teach programming to artists in a visual context. Although it is generally used through a specific IDE, Processing can be employed as a Java library, which is the case for Scan. Processing is based on a key method, named draw, that is invoked several times per second (typically 60 times per second), which accordingly creates animations by modifying parameters such as the coordinates of images.

The page limit does not allow to enter deeply in the code of the implementation. However, the following subsections should allow the reader to understand the key elements of our implementation.

Internal representation of data

Scala case classes offer an elegant mechanism to represent data in an internal manner while keeping a close link to the textual representation in Anim-Bach. For instance, an abstract class AB AG has been introduced to represent agents of Anim-Bach. Case classes have then been defined to represent particular agents, such as AB AST Empty Agent() to represent the empty agent, AB AST Primitive(primitive: String, stinfo: AB SI ELM) to represent a primitive or AB AST Agent(op: String, agi: AB AG, agii: AB AG) to represent a composed agent using the operator op -for instance, || for the parallel composition -and two subagents agi and agii.

Other structures are used similarly to code sets, structured pieces of information, map equations, and temporal logic formulae.

As might be appreciated by this brief description, a close link is indeed made between the internal representation and the textual description in Anim-Bach. As a result, in contrast to tools such as mCRL2 [START_REF] Cranen | An Overview of the mCRL2 Toolset and Its Recent Advances[END_REF], it is quite easy to provide the user with messages directly connected to what he has written.

Parsing Anim-Bach constructs

As exposed in chapter 33 of [START_REF] Odersky | Programming in Scala, A comprehensive step-by-step guide[END_REF], Scala offers facilities to parse languages. The main ingredients to do so are, on the one hand, a library to define parsers, which basically allows to define the class AnimBachParsers as inherited from the class RegexParsers, parsing regular expressions, and the possibility of applying functions to the result of strings having been parsed.

The store

The store is implemented as a mutable map in Scala. Initially empty, it is enriched for each told structured piece of information by an association of it to a number representing the number of its occurrences on the store. The implementation of the primitives follows directly from this intuition. For instance, the execution of a tell primitive, say tell(t), consists in checking whether t is already in the map. If it is then the number of occurrences associated with it is simply incremented by one. Otherwise a new association (t,1) is added to the map. Dually, the execution of get(t) consists in checking whether t is in the map and, in this case, in decrementing by one the number of occurrences. In case one of these two conditions is not met then the get primitive cannot be executed.

The declaration of sets, map equations and procedure definitions are memorized similarly through maps or lists for equations.

The simulator

The simulator consists in repeatedly executing transition steps. In our implementation, this boils down to the definition of function run one, which assumes given an agent in a parsed form and which returns a pair composed of a boolean and an agent in parsed form. The boolean aims at specifying whether a transition step has taken place. In this case, the associated agent consists of the agent obtained by the transition step. Otherwise, failure is reported with the given agent as associated agent.

The function is defined inductively on the structure of its argument, say ag. If ag is a primitive, then the run one function simply consists in executing the primitive on the store. If ag is a sequentially composed agent ag i ; ag ii , then the transition step proceeds by trying to execute the first subagent ag i . Assume this succeeds and delivers ag as resulting agent. Then the agent returned is ag ; ag ii in case ag is not empty or more simply ag ii in case ag is empty. Of course, the whole computation fails in case ag i cannot perform a transition step, namely in case run one applied to ag i fails.

The case of an agent composed by a parallel or choice operator is more subtle. Indeed for both cases one should not always favor the first or second subagent. To avoid that behavior, we use a boolean variable, randomly assigned to 0 or 1, and depending upon this value we start by evaluating the first or second subagent. In case of failure, we then evaluate the other one and if both fails we report a failure. In case of success for the parallel composition we determine the resulting agent in a similar way to what we did for the sequentially composed agent. For a composition by the choice operator the tried alternative is simply selected.

The computation of a procedure call and of a conditional statement are performed similarly as one may expect.

The scene

The scene and its animation are implemented by means of Processing. The declaration of a scene induces dedicated declarations in the setup method used by Processing. Moving an image is obtained by an update in the draw method employed by Processing using a linear interpolation of the initial and final coordinates. Placing images and hiding or showing them is achieved by modifications of the corresponding variables and attributes.

Temporal formulae

Scan temporal formulae are verified by means of a home-made program inspired by the techniques proposed in [START_REF] Reynolds | A Traditional Tree-style Tableau for LTL[END_REF]. It essentially uses a limited depth-first search algorithm based on the simulator described in Subsection 4.4 with a recursive reasoning on the temporal formulae. More concretely, the key function check lts takes as arguments an integer I, a temporal formula F , an agent A and a trace T . The first argument is the length of the remaining search allowed. The second and third arguments are the temporal formula to be checked against the agent. The path consists of the trace prefix already computed. The function returns a boolean, stating whether the formula has been checked, together with a path, describing the last path explored. It provides an execution witness of the truth of the formula in case the return boolean is true.

The check lts function is coded by using a recursive reasoning on the formula F :

if F is a propositional formula, then the current contents of the store should verify it. If this is the case, true is returned together with the path P . Otherwise, false is returned together with P . if F is of the form Next T F and if I is strictly positive, then check lts is successively called on the list of next possible agents returned by run one with I -1 as integer, the agent produced by run one as agent, T F as formula and P augmented with a reference to the computation step as path. In case one of these calls succeed, namely returns true with the associated path, then this result is returned. Otherwise or in case I = 0, then false is returned together with the path P . the case where F is of the form PF Until TF is treated similarly. Either TF holds on the current store, in which case true is returned together with P , or PF holds in the current store and there is one successor agent (explored as for the above case) for which TF holds. In this latter case, true is returned together with the discovered path. In case none of the two situations holds, then false is returned with the path P .

It is worth noting that the algorithm is not complete. If it returns true then the considered formula has been established and the returned path provides a witness execution that can be replayed. Otherwise, because of the limited depthfirst search, false may be returned wrongly because the formula could have been proven by using a more exhaustive search. Nevertheless such a simple algorithm is in practice already useful to establish formulae.

Note also that, in case of success, the algorithm is sound because of the limited form of the temporal formulae considered in Scan, which in particular, does not involve negations.

Related work

Although many pieces of work in the coordination community have been devoted to the proposal of new languages, semantics and implementations, few articles have addressed the concerns of practically constructing programs in coordination languages, in particular in checking that what is described by programs actually corresponds to what has to be modeled. Notable exceptions include the Extensible Coordination Tools [START_REF] Kokash | Formal Design and Verification of Long-Running Transactions with Extensible Coordination Tools[END_REF], ReoLive [START_REF] Cruz | ReoLive: Analysing Connectors in Your Browser[END_REF], and TAPAs [START_REF] Calzolai | TAPAs: A Tool for the Analysis of Process Algebras[END_REF].

The Extensible Coordination Tools (ECT) has been developed for the controlbased coordination language Reo, a language quite different from Anim-Bach. ECT consists of a set of plug-ins for the Eclipse platform that provide graphical editing facilities of Reo connectors, the animation of these connectors as well as model checking based on constraint automata or a translation to the process algebra mCRL2 [START_REF] Cranen | An Overview of the mCRL2 Toolset and Its Recent Advances[END_REF]. Although it is certainly less elaborated, our work differs in several respects. First, it deals with tuple spaces instead of connectors. Second, it allows to grasp the modeling of real-life systems by connecting agents of Bach to animations at the application level. Consequently, although one may animate connectors in ECT, one cannot animate the modeling of the rush hour problem for instance, as we did with Anim-Bach. Finally, in contrast to our work, model checking in ECT does not preserve a one-to-one link with textual representations, in particular when mCRL2 is used.

ReoLive is also dedicated to Reo. It proposes similar tools but by means of a set of web-based tools using ScalaJS. As a consequence, the above comparison with ECT also applies to ReoLive.

TAPAs [START_REF] Calzolai | TAPAs: A Tool for the Analysis of Process Algebras[END_REF] is a tool developed essentially for CCSP with a plug-in for an extension of the Klaim coordination language. It allows to graphically specify systems and to verify their equivalence by means of bisimulations based equivalences (strong, weak and branching) or decorated trace equivalences (weak and strong variants of trace completed trace, divergence sensitive trace, must, testing). It also allows to model check systems by using formulae of the µ-calculus. The two main differences of our work with TAPAs are, on the one hand, our concern for tuple-based coordination languages, and, on the other hand, the facilities offered by Anim-Bach for animations. In contrast, as written above, model checking in Anim-Bach is quite simple and is much less elaborated than that of TAPAs. Future work will aim at improving this aspect.

Declarative invariant assertions are proposed in [START_REF] Kühn | Distributed Coordination Runtime Assertions for the Peer Model[END_REF] to detect inconsistencies in models expressed in the Peer model, a coordination model based on shared tuple spaces, messages and Petri nets. In addition to the fact that the Peer Model is quite different from Anim-Bach, our work differs in two main respects. On the one hand, assertions in [START_REF] Kühn | Distributed Coordination Runtime Assertions for the Peer Model[END_REF] are verified at runtime whereas our temporal formulae are checked statically. On the other hand, in contrast to our work, no animation facilities are provided.

Although it includes facilities to view the evolution of the shared space, TUCSON [START_REF] Omicini | Integrating Objective & Subjective Coordination in FIPA: A Roadmap to TuCSoN[END_REF] does not provide facilities to animate computations nor to modelcheck them.

Finally, a Linda workbench is presented in [START_REF] Dukielska | JavaSpaces NetBeans: a Linda Workbench for Distributed Programming Course[END_REF] with the goal of providing a simple tool that allows users to experiment with a Linda-inspired language. It is integrated with Netbeans and uses the JavaSpaces language, an extension of Java supporting Linda primitives. It is hence named JavaSpaces Netbeans. This workbench provides a tuple browser and a distributed debugger, including record facilities to replay a sequence of tuple space operations. Although our work provides facilities to explore and modify the tuple space, we do not provide debugging facilities. In contrast however we provide animation facilities as well as model checking facilities which are not included in JavaSpaces Netbeans.

Conclusion

The paper has introduced a workbench for reasoning on a Linda-like coordination language at three levels: (i) by executing in a step by step or automatic manner instructions while showing their impact on the shared space, (ii) by illustrating computations by animations and (iii) by model checking properties by means of temporal formulae.

The current version has been designed to be as simple as possible yet incorporating key ideas. As a result, it can be improved in many aspects, in particular, by refining the interfaces, by integrating it in IDE's, by improving the specification of animations and by handling more sophisticated temporal logics, like the µ-calculus [START_REF] Kozen | Results on the Propositional mu-Calculus[END_REF].

Fig. 3 .

 3 Fig. 3. Interacting with the blackboard

  Fig. 4. Animation

Fig. 6 .

 6 Fig. 6. Transition rules for the primitives

scene ( 6

 6 4 0 , 6 4 0 ) background = loadImage ( Images / t h e b a c k g r o u n d i m g . png ) . r e d c a r = loadImage ( Images / r c a r . j p g ) . y e l l o w t r u c k = loadImage ( Images / y t r u c k . g i f ) .

Fig. 7 .

 7 Fig. 7. Transition rules for the operators