Elementary Net Systems with Localities (ENL-systems) is a class of Petri nets introduced to model GALS (globally asynchronous locally synchronous) systems, where some of the components might be considered as logically or physically close and acting synchronously, while others might be considered as loosely connected or residing at distant locations and communicating with the rest of the system in an asynchronous way. The speci cation of the behaviour of a GALS system comes very often in the form of a transition system. The automated synthesis, based on regions, is an approach that allows to construct Petri net models from their transition system speci cations. While theory of regions is well developed, there is still lack of implemented tools capable of dealing with complex real-life system construction. In this paper we focus on developing algorithms and tool support for the synthesis of the ENL-systems from step transition systems, where arcs are labelled by steps (sets) of executed actions. The algorithms are implemented within the workcraft framework.
A number of computational systems exhibit behaviour that follows the
`globally asynchronous locally (maximally) synchronous' paradigm. Examples can
be found in hardware design, where a VLSI chip may contain multiple clocks
responsible for synchronising di erent subsets of gates [
distinct set of events which must be executed synchronously, i.e., in a maximally concurrent manner (often called local maximal concurrency ).
An attractive way of constructing complex computing systems is their
automated synthesis from behavioural speci cations given in terms of suitable
transition systems. In such a case, the synthesis procedure is often based on the
regions of a transition system, a notion introduced in [
The vast majority of results in the area of synthesis of Petri nets use the standard transition systems, where the arcs are labelled with single events/actions, as initial speci cations of systems' behaviour. In this paper, however, we follow the approach, used in [17{20, 24], employing step transition systems instead, where arcs are labelled with sets of executed events/actions.
This paper is concerned with nding e cient algorithms for deriving regions
for the synthesis of ENL-systems. The nets with localities, as already mentioned,
were rst introduced in [
To explain the basic idea behind ENL-systems, let us consider the net in Figure 1 modelling two co-located consumers and one producer residing in a remote location. In the initial state, the net can execute the singleton step fc4 g. Another enabled step is fp2 g which removes the token from b1 and puts a token in both b0 and b2 . In this new state, there are three enabled steps, viz. fp1 g, fc1 ; c4 g and fp1 ; c1 ; c4 g. The last one, fp1 ; c1 ; c4 g, corresponds to what is usually called maximal concurrency as no more activities can be added to it without violating the constrains imposed by the available resources (represented by tokens). However, the previously enabled step fc4 g which is still resource (or token) enabled is disallowed by the control mechanism of ENL-systems. It rejects a resource enabled step like fc4 g since we can add to it c1 co-located with c4 obtaining a step which is resource enabled. In other words, the control b1 b2 b5 b6 b3 b4 c2 c3 mechanism employed by ENL-systems (and PTL-nets) is that of local maximal concurrency as indeed postulated by the GALS systems execution rule.
b0 p1 p2 c1 c4
The paper is organised as follows. The next section recalls some basic notions concerning step transition systems, ENL-transition systems, ENL-systems and their synthesis. Section 3 introduces an algorithm for computing regions of a given step transition system (ENL-transition system) and provides theoretical results to support the algorithm. The paper ends with a conclusion that includes some directions for future work. 2
Let E be a xed nite non-empty set of events. A co-location relation on E is any equivalence relation l on the set of events. Moreover, for an event e and a non-empty set of events U (called a step), we will denote e l U whenever there is at least one event f 2 U satisfying e l f .
De nition 1. A step transition system on E is a triple ts =df (Q; A; q0) where Q is a non-empty nite set of states, A Q (2E n f?g) Q is a nite set of transitions (arcs), and q0 2 Q is the initial state. We will write q U! q0 (or simply q U!) whenever (q; U; q0) is a transition. We will call q the source of transition (q; U; q0) and q0 its target.
To ease the presentation, we will assume that each event of E occurs in at least one of the steps labelling the transitions of ts.
to q0, , in a step transition system ts = (Q; A; q0) if there are states q = q1; q2; : : : ; qk+1 = q0 such that (qi; Ui; qi+1) 2 A for i = 1; : : : ; k. We will denote
U1:::Uk this q ! q0 or q ! q0. We will say that a step sequence has no loops if all its states are distinct (adjacent to at most two transitions).
Let ts = (Q; A; q0) and ts0 = (Q0; A0; q00) be step transition systems. We say that ts and ts0 are isomorphic, ts = ts0, if there is a bijection f : Q ! Q0 such that f (q0) = q00 and (q; U; q0) 2 A , (f (q); U; f (q0)) 2 A0, for all q; q0 2 Q and U 2 2E n f?g.
In diagrams of bigger step transition systems we will write annotations of arcs for singleton steps without braces (e:g:; e instead of feg). Also, by thick arcs in a step transition system we will mean arcs labelled by non-singleton steps.
In the following sub-sections we gather de nitions introduced in [
De nition 3 ([
enl =df (B; E; F; l; c0) such that B is a nite set of conditions disjoint from the events, F (E B) is the ow relation, l is a co-location relation on E, and c0 initial case (in general, any subset of B is a case). (B
E) [ B is the
In diagrams, conditions (local states) are represented by circles, events (actions) by boxes, the ow relation by directed arcs, and each case (global state) by tokens (small black dots) placed inside those conditions which belong to this case. Moreover, boxes representing co-located events are shaded in the same way (see Figure 1).
For every event e, its pre-conditions and post-conditions are given respectively by
e =df fb j (b; e) 2 F g and e =df fb j (e; b) 2 F g (both sets are assumed non-empty and disjoint). Two events are in con ict (or con icting) if they share a pre-condition, or share a post-condition. The dotnotation extends to sets of events in the usual way, e.g., U =df Sf e j e 2 U g.
The semantics of enl is based on steps of simultaneously executed events. We rst de ne potential steps of enl as all non-empty sets of non-con icting events. A potential step U is then resource enabled at a case c if U c and U \ c = ?, and control enabled if, in addition, there is no event e 2= U such that e l U and the step U [ feg is resource enabled at c. A control enabled step U can be executed leading from c to the case c0 = (c n U ) [ U . We denote this by c[U ic0 (or c[U i). The step execution mechanism employed by ENL-systems can therefore be called local maximal concurrency.
tsenl =df C ; f(c; U; c0) 2 2B where C | the set of reachable cases | is the least set of cases containing c0 and closed w.r.t. the step execution relation. To ease the presentation, we will assume that enl does not have dead events, i.e., each event occurs in at least one of the steps labelling the arcs of the step transition system tsenl.
ENL-systems can be considered as Elementary Net Systems (EN-systems) equipped with an explicit notion of localities for their events. The local maximal semantics of their execution means that certain properties enjoyed by ENsystems do not hold for ENL-systems, like the following monotonicity property: Fact 1 The step monotonicity for EN-system states that: If c[U i and U 0 then c[U 0(U n U 0)i.
U 2.2
To link the nodes (global states) of a step transition system ts with the conditions (local states) of the hypothetical ENL-system corresponding to it, we use the notion of a region.
De nition 4 ([
(in = ? ^ out = ?) ) (r = Q _ r = ?) and for every transition q U! q0, the following hold: R1 R2 R3 R4
If q 2 r and q0 2= r then jU \ outj = 1.
If q 2= r and q0 2 r then jU \ inj = 1.
If U \ out 6= ? then q 2 r and q0 2= r.
If U \ in 6= ? then q 2= r and q0 2 r.
Each region is a triple: r = (in; r; out), where r is a subset of states of the
step transition system, in is a subset of its events E which are responsible for
entering r, and out is a subset of events E which are responsible for leaving r.
There are exactly two trivial regions satisfying r = ? or r = Q, viz. (?; ?; ?) and
(?; Q; ?). Moreover, (in; r; out) is a region i so is its complement (out; Qnr; in).
We will denote the complement of a region r by r. In general, a region, as de ned
above, cannot be identi ed only by its set of states; in other words, in and out
may not be recoverable from r. However, if the step transition system is thin,
i.e., for every event e 2 E there is a transition q f!eg q0 of ts, then di erent
regions are based on di erent sets of states [
The set of all non-trivial regions of ts will be denoted by Rts and, for every state q, Rq is the set of all non-trivial regions (in; r; out) containing q,
Rq =df fr 2 Rts j q 2 rg:
The sets of pre-regions, e, and post-regions, e , of an event e comprise all the
non-trivial regions (in; r; out) respectively satisfying e 2 out and e 2 in,
e =df fr 2 Rts j e 2 outg
and
e =df fr 2 Rts j e 2 ing: [
The set of potential steps of ts comprises all non-empty sets U of events such
that e \ f = e \ f = ?, for each pair of distinct events e; f 2 U . A potential
step U is then region enabled at state q if U Rq and U \ Rq = ? [
For all distinct states q and q0, Rq 6= Rq0 .
For every state q and step U , we have that q U! i U is region enabled at q and there is no event e 62 U such that e l U and the step U [ feg is region enabled at q.
One can show (see [
ENL-systems generate ENL-transition systems. The converse also is true, and the translation from ENL-transition systems to the corresponding ENL-systems is based on the regions of step transition systems.
Let ts = (Q; A; q0) be an ENL-transition system w.r.t. a (given) co-location
relation l. Then the net system associated with ts is de ned as [
relation l. Then enltls is an ENL-system and its step transition system is isomorphic to ts. Moreover, the isomorphism between ts and the step transition system of enltls is given by (q) =df Rq, for every state q of ts.
The enltls net system obtained from the synthesis of the step transition system
might contain many conditions which are redundant from the point of view of its
behaviour, i:e:; deletion of such conditions (and their adjacent arcs) would lead
to a net whose step transition system is still isomorphic to ts [
In this section, we present the approaches that have been used for designing and implementing algorithms to generate non-trivial regions of a given step transition system (ENL-transition system) as de ned in Section 2.2. We consider the execution time of the algorithms as the main measure to gauge their e ciency.
The initial idea was to focus on thin step transition systems, as in these
transition systems, for every event e 2 E, there is a transition q f!eg q0, for some
q; q0 2 Q. This, we believed, would allow us to ignore the thick arcs and base our
algorithm solely on singleton arcs, which in turn would enable us to use some of
the techniques used in the Petrify tool [
In the rst instance, we have implemented (starting with a brute-force approach)
an algorithm for extracting regions of ENL-transition systems as de ned in [
The approach for reducing the number of potential in and out sets of regions is based on the information about causality and concurrency embedded in the step transition systems. This approach is presented in section 3.3.
The approach for reducing the number of candidates for the sets of states (r)
for regions is based on source and targets sets. This idea was rst used in the
Petrify tool [
The question is: which of the thick arcs can be ignored without changing the set of non-trivial regions? The thin step transition systems would be the rst candidate of a class of systems to consider, because they contain the arcs labelled with all possible singleton steps, so all the events would be present in the set of steps labelling the remaining arcs of the step transition system after the removal of thick arcs. However, even in some of the thin transition systems removing thick arcs can be problematic as the Figure 4 shows. In that example removing the only thick arc, fe; f g, leads to the transition system being disconnected, meaning that previously ENL-transition system would not longer be classi ed as such on the grounds of not satisfying the axiom A1. The property of thinness is too weak to make a decision about the removal of thick arcs. We need to make much stronger assumptions as stated in the following proposition. Proposition 1. Let ts = (Q; A; q0) and ts0 = (Q; A0; q0) be two step transition systems, where ts0 is obtained from ts by deleting a thick arc (q; U; q0) 2 A labelled r1 p2 r2 r0 r0 r3 c1 r3 r4 r4 r9
r9 c2 c3 r8 r8
r5 r5 r6 r6 p1 c4 r7 r7 by step U that satis es: U = U1 ] : : : ] Uk and there exists in ts a step sequence = Ui1 : : : Uik , leading from q to q0, for any permutation of steps U1; : : : ; Uk. Then Rts = Rts0 .
Proof. The inclusion Rts Rts0 holds trivially. We need to prove that Rts0 Rts. Let r = (in; r; out) 2 Rts0 . We need to show that r 2 Rts, that means that for the arc (q; U; q0) of ts that was removed from ts to obtain ts0 and r the conditions R1 - R4 hold. We can assume, to the contrary, that one of the conditions does not hold for (q; U; q0).
Case 1: R1 does not hold for (q; U; q0) and r. That means we have that q 2 r and q0 2= r and jU \ outj 6= 1. From assumptions, it follows that there is a step sequence in ts0, = U1 : : : Uk, where (q1; U1; q2), (q2; U2; q3); : : : ; (qk; Uk; qk+1) 2 A0, q = q1 and q0 = qk+1. As r = (in; r; out) 2 Rts0 , q 2 r and q0 2= r, there exists a transition (qi; Ui; qi+1), 1 i k, such that qi 2 r and qi+1 2= r and for which R1 is satis ed in ts0. Hence jUi \ outj = 1. Suppose that there exists another step, Uj 6= Ui, in the step sequence such that (qj ; Uj ; qj+1) 2 A0 and qj 2 r and qj+1 2= r. From this and the assumptions it follows that there exists a permutation of steps of (which leads from q to q0), where Ui and Uj are consecutive steps, which is impossible as the sources of the arcs they label must belong to r and the targets must be outside r. We also cannot have a step Uj in labelling a transition (qj ; Uj ; qj+1), for which qj 2= r and qj+1 2 r, as in this case we would need to have either a loop in with two occurrences of Ui, or another step in , apart from Ui, which labels a transition exiting r, and we already proved that that is impossible. Hence, for all steps of apart from Ui, we have that they do not cross the border of r. As a consequence, from R3, which is satis ed for them, jUj \ outj = 0. As steps U1; : : : ; Uk are disjoint and U = U1 ] : : : ] Uk, we have jU \ outj = 1, a contradiction. So, R1 is satis ed for (q; U; q0) and r.
Case 2: R2 does not hold for (q; U; q0) and r. The proof is similar to the proof of Case 1 and also leads to a contradiction. So, R2 is satis ed for (q; U; q0) and r. Case 3: R3 does not hold for (q; U; q0) and r. That means jU \ outj 6= 0 and q 2= r or q0 2 r. We can assume, without the loss of generality, that q 2= r. We now need to consider two cases: 1. If q0 2 r and q 2= r, there is a step Ui in , labelling a transition (qi; Ui; qi+1) 2 A0, where 1 i k and qi 2= r and qi+1 2 r. Since R3 holds for this transition and r in ts0, we have jUi \ outj = 0. For other steps of , Uj 6= Ui, we must have jUj \outj = 0, as otherwise we would have a transition, labelled with step Uj , exiting r, but that would mean that either has a loop with two occurrences of Ui, or there is another transition, labelled with a step, di erent from Ui, entering r again, and this is impossible according to the argument used in Case 1. So, jUi \ outj = 0 for i = 1; : : : ; k, and as a consequence jU \ outj = 0, a contradiction. 2. If q0 2= r and q 2= r, then again we have, for all steps Ui in , labelling transitions (qi; Ui; qi+1), 1 i k, either qi; qi+1 2= r or we have at least one pair of transitions, with one transition entering r (labelled Ui, for example) and one transition exiting r (labelled Uj , for example). The latter can be ruled out as according to the assumptions, there would need to be a step sequence between q and q0 in ts0 with Uj and Ui being consecutive steps. However, that would mean that there must exist another two steps (di erent from Ui and Uj ) in one labelling a transition entering r and another labelling a transition exiting r and we already know that this must be excluded as two steps labelling exiting transitions and two steps labelling entering transitions cannot be part of any permutation of steps leading from q to q0. So, for all transition (qi; Ui; qi+1), 1 i k, we have qi; qi+1 2= r, and, by R3, which is satis ed for arcs of ts0, we have jUi \outj = 0 for i = 1 : : : k. As a consequence jU \ outj = 0, a contradiction.
So, R3 is satis ed for (q; U; q0) and r.
Case 4: R4 does not hold for (q; U; q0) and r. The proof is similar to the proof of Case 3 and also leads to a contradiction. So, R4 is satis ed for (q; U; q0) and r. tu
To check the conditions stated in Proposition 1 would be computationally expensive. However, there is a class of step transition systems, for which they are always satis ed as shown in the Theorem 2. But rst, we introduce a concept of co-located sequential events in the context of step transition systems.
U!.
De nition 6. Let ts = (Q; A; q0) be an ENL-transition system w.r.t. a colocation relation l and E be a set of events used in the steps labelling transitions from A. We say that l partitions the set of events E into sets of co-located sequential events, E = E1 ] : : : ] Em, if the following holds: for all i = 1; : : : ; m there is no q 2 Q and no step U in ts such that e; f 2 Ei and e; f 2 U and q Theorem 2. Let ts = (Q; A; q0) be an ENL-transition system w.r.t. a co-location relation l, which partitions its set of events E into sets of co-located sequential events (E = E1 ] : : : ] Em). Then all thick arcs in ts satisfy the conditions of
Proof. From the fact that l partitions the set of events into sets of co-located sequential events we have that every non-singleton step of ts can contain only one event from any individual sub-set Ei, i = 1; : : : ; m and therefore, there is no non-singleton step that can be executed as a consequence of the local maximal concurrency semantics (enforced concurrency). Hence, the sets of resource enabled steps and control enabled steps of ts are the same. That in turn means that ts, which is an ENL-transition system, is a step transition system of some EN-system and in this class of nets the step monotonicity property (see Fact 1) is satis ed for every (resource) enabled step. So, for every thick arc of ts the conditions of Proposition 1 are satis ed.
For a given step transition system ts = (Q; A; q0), nding its regions involve nding the in and out sets of events that are part of their de nition. To reduce the execution time of generating all the non-trivial regions we can look at the possibilities of minimising the number of in and out sets to be considered. For a transition system that has n events (jEj = n), the brute-force approach would consider 2n sets for in and out sets. However, looking at transitions of ts and their labels, we can eliminate safely many candidates for in and out sets as stated in the following propositions.
Proposition 2. Let r = (in; r; out) be a region in a step transition system ts = (Q; A; q0). If the target of any transition q U!0 q0 in ts, where e 2 U 0, is the source of another transition q0 U00
! q00 in ts, where f 2 U 00 and f 6= e, then the following hold:
Proof. 1. Assume, to the contrary, that we have two transitions in ts, q U!0 q0 and q0 U!00 q00 and two events e and f , such that e 6= f , e 2 U 0 and f 2 U 00, and fe; f g in for a region r = (in; r; out). Hence, since regional condition R4 is satis ed for both transitions and r, we have: q 62 r and q0 2 r and q0 62 r and q00 2 r. We obtained a contradiction and so fe; f g 6 in. 2. The proof is similar, but we use R3 regional condition here rather than R4. transition q0 ff!g q00 in ts, for f 6= e, then fe; f g 6 in and fe; f g 6 out. (Q; A; q0). If the target of any transition q f!eg q0 in ts is the source of another Proof. Follows directly from Proposition 2. tu Proposition 3. Let r = (in; r; out) be a region in a step transition system ts = (Q; A; q0), and let q U! q0 be a transition in ts, such that there are two events e; f 2 U . Then the following hold:
Proof. 1. Assume, to the contrary, that we have a transition q U! q0 in ts, where e; f 2 U and fe; f g in. Hence, since regional condition R2 is satis ed in ts for q U! q0 and r, we have that :(q 62 r and q0 2 r) is true, which means that either q 2 r or q0 62 r. However, as R4 regional condition is also satis ed for q U! q0 and r, we have q 62 r and q0 2 r, but this contradicts the previous conclusion. 2. The proof is similar, but we use R1 and R3 regional conditions here rather than R2 and R4.
After selecting the candidates for the sets in and out we need to turn our
attention to discovering the sets of states (r) for regions of the form: r = (in; r; out).
When doing so we need to look at the possibilities of reducing the number of
these sets (see Section 3.1). In the context of standard transition systems, where
arcs are labelled by single events, these sets would solely de ne regions. So,
although we are considering step transition systems in this paper rather than the
standard transition systems, some of the ideas developed earlier can be re-used
in our new setting. For this part of the algorithm, we use the ideas of excitation
and switching regions introduced in [
De nition 7. Let ts = (Q; A; q0) be a step transition system on E. We de ne the following two sets of states for every e 2 E: { The source set Se = fq 2 Q j 9q0 2 Q : (q; U; q0) 2 A ^ e 2 U g. { The target set Te = fq0 2 Q j 9q 2 Q : (q; U; q0) 2 A ^ e 2 U g. Proposition 4. Let r = (in; r; out) be a region in a step transition system on E, ts = (Q; A; q0), and let e 2 E. Then the following is satis ed: 1. If e 2 out then Se 2. If e 2 in then Te
r and Te \ r = ?.
r and Se \ r = ?.
Proof. Let (q; U; q0) 2 A be a transition in ts and e 2 U . Hence q 2 Se and q0 2 Te. 1. If e 2 out then e 2 U \ out and from the de nition of a region (R3) we have: q 2 r and q0 62 r. So, Se r and Te \ r = ?. 2. If e 2 in then then e 2 U \ in and from the de nition of a region (R4) we have: q 62 r and q0 2 r. So, Te r and Se \ r = ?. tu
If we want to combine the discovery of sets in, out and r, when searching for all non-trivial regions of step transition systems, we can use the results given in Corollary 2, Propositions 5 and Corollary 3.
Corollary 2. Let r = (in; r; out) be a region in a step transition system on E: ts = (Q; A; q0). Then
Se [ [ Te e2in r : Proof. Follows directly from Proposition 4.
From Corollary 2, we see that the set of states r of any region r = (in; r; out) in a step transition system ts = (Q; A; q0) can be represented as Corollary 3. Let r = (in; r; out) be a region in a step transition system ts = (Q; A; q0) and (q; U; q0) 2 A, where U E n (in [ out). Then the following hold: 1. If q 2 Sr [ T r and q0 62 Sr [ T r then q0 2 F r. 2. If q0 2 Sr [ T r and q 62 Sr [ T r then q 2 F r.
Proof. Follows from the representation of r (see Eq. (1)) and Proposition 5. r = where F r is a set of states we will call the ller set for r. We will use the following denotations: Sr = Se2out Se and T r = Se2in Te.
Proposition 5. Let r = (in; r; out) be a region in a step transition system ts = (Q; A; q0) and (q; U; q0) 2 A. Then the following hold: 1. If q 2 r and U \ out = ? then q0 2 r. 2. If q 62 r and U \ in = ? then q0 62 r.
Proof. 1. Follows directly from R1 of the de nition of a region. 2. Follows directly from R2 of the de nition of a region. tu (1) tu tu 3.5
Before we propose an algorithm for computing regions of ENL-transition systems, we summarise a few useful facts: 1. For every region r = (in; r; out) in a step transition system ts we have: in \ out = ?. This follows from R3 and R4 of the de nition of a region. 2. For any non-trivial region r = (in; r; out) in a step transition system ts we have: Sr [ T r 6= ?. This follows from the de nition of a region, which states that the sets in and out can only be both empty for trivial regions. 3. The set of potential in sets is the same as the one of out sets, as the in set of a region r is the out set of its complement, r, and the other way round.
Although the title of this section suggests that the input for the algorithm should be an ENL-transition system, the algorithm can take as its input just a step transition system as de ned in De nition 1, and it will compute regions as de ned in De nition 4. The de nition of a region that is used implies the target class of nets and the synthesis problem, in which the regions are later used as conditions to build the synthesised net. The algorithm does not check the axioms A1-A4 (see De nition 5) to decide whether the input step transition // |InOut| = n
*/ // (ini; outj ) is not valid // Initial states to consider Algorithm 1: Extract Rts 1 Function ExtractRts(Step transition system ts = (Q; A; q0)) 2 Initialise Rts to empty set 3 InOut = Generate All Potential in/out Sets(ts) ; 4 for i:= 1 to n do 5 for j:= 1 to n do 6 Initialise Sr and T r to empty sets 7 /* Consider (ini; outj) 2 InOut
(outj ; ini) 2 InOut InOut if ini \ outj = ? and ini [ outj 6= ? then for every event e 2 outj do
Generate set Se Add Se to Sr
InOut, and not for every event e 2 ini do
Generate set Te
Add Te to T r else
break ; Initialise S to Sr [ T r ; Initialise r to Sr [ T r for every q 2 S do
Initialise Fcurrent to empty set for every arc (q; U; q0) 2 A do if (ini [ outj ) \ U = ? and q0 62 r then
Add q0 to r
Add q0 to Fcurrent for every arc (q0; U; q) 2 A do if (ini [ outj ) \ U = ? and q0 62 r then
Add q0 to r
Add q0 to Fcurrent
Set S to Fcurrent Let r = (ini; r; outj) if r satis es regional axioms then
Add r to Rts
Add r = (outj ; Q n r; ini) to Rts 8 9 10 11 system is indeed an ENL-transition system and therefore synthesisable. In most of our experiments, however, we used ENL-transition systems as inputs for the algorithm for the testing purposes (see Section 3.6).
To explain the algorithm we can look at a step transition system of Figure 4(a). In the rst step of the algorithm we obtain all potential in and out sets using the techniques from Section 3.3. We can consider one such a pair: in = ? and out = fhg. This pair trivially satis es the validity constraints as stated in Section 3.3. The algorithm now discovers r for a candidate region r = (?; r; fhg). The set r is de ned as r = Sr [ T r [ F r = Se2out Se [ Se2in Te [ F r (see Equation (1)). First the algorithm computes the set Sr [ T r, in this case containing a single element q3. The most complex part of the algorithm is the one to compute the ller set F r (using Corollary 3). The set F r is initially empty. It does not feature in the algorithm explicitly. So, initially, r = S = Sr [ T r = fq3g. We start the for-loop at line 19 (see lines 19-29). Below we go through its iterations. 1. S = fq3g and Fcurrent = ? (this set records the states added to r during the current iteration of the loop). We consider all possible arcs adjacent to q3 that are not labelled by steps containing events from in [ out = fhg. We have two arcs to consider: { Arc q3 fg!g q4: we add q4 to r to `bury' this arc in r. Now we have:
Fcurrent = fq4g and r = fq3; q4g. { Arc q2 fe;fg q3: we add q2 to r to `bury' this arc in r. Now we have: !
Fcurrent = fq4; q2g and r = fq3; q4; q2g. 2. S = fq2; q4g and Fcurrent = ? and we consider all possible arcs adjacent to q2 and q4 that are not labelled by steps containing events from in[out = fhg and are not yet `buried' in r. We have two arcs to consider: { Arc q4 f!eg q5: we add q5 to r to `bury' this arc in r. Now we have:
Fcurrent = fq5g and r = fq2; q3; q4; q5g. { Arc q1 fg!g q2: we add q1 to r to `bury' this arc in r. Now we have:
Fcurrent = fq5; q1g and r = fq3; q4; q5; q2; q1g. 3. S = fq5; q1g and Fcurrent = ? and we consider all possible arcs adjacent to q1 and q5 that are not labelled by steps containing events from in[out = fhg and are not yet `buried' in r. We have one arc to consider: { Arc q0 f!eg q1: we add q0 to r to `bury' this arc in r. Now we have:
Fcurrent = fq0g and r = fq3; q4; q5; q2; q1; q0g. 4. S = fq0g and Fcurrent = ?. In this iteration we cannot add any more states to r that are not already there, so S is set to ? for the next iteration of the loop. The computation of r is completed.
The discovered candidate for a region is r = (?; fq0; q1; q2; q3; q4; q5g; fhg). The algorithm then checks the regional axioms for the candidate and, if they are satis ed, the region and its complement (in this case r = (fhg; fq6; q7g; ?)) are added to the set of discovered regions. These are two out of ten non-trivial regions of ts2 in Figure 4(a) discovered by Algorithm 1 (see the screenshot from workcraft, for this example, in Figure 7, in the Appendix). 3.6
The machine used in the experiments was PC with 3.20 GHz Intel Core i7 CPU and 12GB RAM, running Windows 10 Pro. The algorithms were implemented in Java (JDK 1.8.0) on top of the workcraft framework (version 3.2.6).
The average execution time of each algorithm was calculated on the basis of 20 runs. All experiments reported in this paper were conducted in isolation in order to prevent any side e ects caused by concurrently executing processes. We ran each of the experiments over approximately the same time period to ensure that the computer was placed under similar load. The same machine was used for conducting all the experiments to ensure fair performance comparisons.
Using an example of the ENL-transition system in Figure 2, ts3, we now compare the execution time taken to derive regions when applying ve di erent approaches described as follows: Approach 1: We generate all sets of 2Q and all sets of 2E ; we check regional axioms for all arcs of A.
Approach 2: We generate all sets of 2Q and all sets of 2E ; we check regional axioms for selected arcs of A, after ignoring the thick arcs (see Theorem 2). Approach 3: We generate all sets of 2Q; we consider only a selection of sets from 2E to generate potential in and out sets by using the results from Section 3.3; we check regional axioms for all arcs of A.
Approach 4: We generate only a selection of sets from 2Q by using the source and target sets; we consider only a selection of sets from 2E to generate potential in and out sets by using the results from Section 3.3; we check regional axioms for all arcs of A.
Approach 5: We generate only a selection of sets from 2Q by using the source and target sets; we consider only a selection of sets from 2E to generate potential in and out sets by using the results from Section 3.3; we check regional axioms for selected arcs of A, after ignoring the thick arcs.
All the algorithms, related to the ve approaches described above, produced the same non-trivial regions for ts3. Figure 5 shows the results of the comparison, where clearly the best savings are gained by reducing the number of potential in and out sets by using the results presented in Section 3.3.
To test Algorithm 1, we selected the following examples: ts1 in Figure 8 (2 states, 4 events), ts2 in Figure 4 (8 states, 4 events), ts3 in Figure 2 (16 states, 6 events), ts4 in Figure 9 (12 states, 6 events), the step transition system of an ENL-system in Figure 10 (ts5). The last transition system has 64 states and 9 events. The results of the experiments are shown in Figure 6.
When testing Algorithm 1, our rst aim was to check whether it generates correctly all the expected regions. We selected our examples for testing trying to consider ENL-transition systems representing nets with di erent characteristics: thin step transition systems (ts2, ts3, ts5) or not thin (ts1, ts4); step transition systems of nets with con icts (ts1, ts2) or without con icts (ts3, ts4, ts5); step transition systems of nets, where every locality represents a sequential subsystem (ts3, ts5) or not (ts1, ts2, ts4). For all the chosen examples the algorithm produced the expected results. The rst four examined transition systems were very small. The last step transition system, ts5, was bigger. As it has 64 states it was already too big to test the brute-force version of the algorithm on it, but Algorithm 1 produced its non-trivial regions in terms of milliseconds. We 20 s e u it n M 10 0 600 s d 4on00 c e s i l l i M 200 0
Approach 1
Approach 2
Approach 3 0.7 Fig. 6: A diagram showing the execution time taken to derive non-trivial regions of the ENL-transition systems: ts1, ts2, ts3, ts4 and ts5, when using Algorithm 1 without (or with) the removal of thick arcs, respectively tested Algorithm 1 on ENL-transition systems with up to 90 states and it still performed very well. We found this promising.
The removal of thick arcs, applicable to ts3, ts4 and ts5, gave the best results, in terms of execution time, for transition systems ts3 and ts5 as they satisfy the conditions of Theorem 2 allowing for the removal of all thick arcs. 4
In this paper we presented an algorithm for deriving non-trivial regions of ENLtransition systems. The algorithm was tested on a selection of small step transition systems. We plan to build a set of benchmarks to test its performance on bigger examples and see how it scales with the increasing sizes of inputs.
In the future, we plan to add new algorithms to our tool to produce a complete tool for the synthesis of ENL-systems, including algorithms for the minimization of the synthesised nets; and algorithms for synthesising ENL-systems with the assumption that the co-location relation is not known in advance and needs to be discovered as a part of solving the synthesis problem.
Acknowledgement The rst author is grateful to the National Transitional Council of Libya for funding her PhD studentship and research.
fe; gg fe; hg ff; gg ff; hg
q Fig. 8: An ENL-transition system ts1, where e, f , g and h are co-located events. fc4; c1g
p1
q11 fc2; c3g
fc2; c3g b10 b11 i b8 b12 Fig. 10: An ENL-system, where events a, b, c are sharing a location; events d, e, f are in the second location; and events g, h and i are in the third location. It generates ts5 step transition system considered in Figure 6.