234
M. Bozga et al.
– S
def
=
N
k=1 S
k
× U. That is, the net has a place (s, u) for each state s of each component type, and for each node u.
– For each minimal model I = (U,ι) of a clause C of Γ, the set T contains a transition
t ι ∈ T , and the set E contains edges ((s, u), t ι ) and (t ι , (s , u)) for every s
p
−
→ s ∈
N
k=1 Δ
k
such that u ∈ ι(p). Nothing else is in T or E. Intuitively, t ι “synchronizes”
all the transitions s
p
−
→ s of the different components occurring in the interaction.
– For each 1 ≤ k ≤ N, each s ∈ S
k and each u ∈ U, m 0 ((s, u)) = 1 if s = s 0
k and
m 0 ((s, u)) = 0, otherwise. That is, m 0 contains the places (s, u) such that s is an
initial state.
It follows immediately from this definition that N U
S
is a 1-safe Petri Net. Indeed, for
every u ∈ U, for every component-type C
k , and for every reachable marking m, we have
s∈S k m((s, u)) = 1. This reflects that the instance of C
k at u is always in exactly one of
the states of S
k ; if s is that state, then (s, u) is the place carrying the token.
Example 2. Consider our running example, with U = {0, 1,..., n−1}, i.e., n philosophers
and n forks. Since the interaction formula (1) has no constants, its models are pairs
(U,ι), where ι gives the interpretation of the free variable i and the predicates g, t, etc.
The first disjunct of (1) is [g(i) ∧ t(i) ∧ t(succ(i))]. It has a minimal model for each k ∈ U,
namely the model with ι(i) = k, ι(g) = {k} and ι(t) = {k, (k + 1) mod n}. In the interaction
produced by this model, the k-th philosopher executes transition g(et), the forks with
numbers k and (k + 1) mod n execute transition t(ake), and all other philosophers and
forks remain idle. The second disjunct yields the interactions in which a philosopher
puts down its forks. Fig. 2 shows the Petri Net N U
S
for universe U = {0, 1, 2}. For clarity,
(w, 0)
(w, 1)
(w, 2)
(e, 0)
(e, 1)
(e, 2)
( f, 0)
(b, 0)
( f, 1)
(b, 1)
( f, 2)
(b, 2)
( f, 0)
(b, 0)
i 1
i 2
i 3
i 4
i 5
i 6
Fig. 2: Petri Net of the dining philosophers for the universe U = {0, 1, 2}. In reality, the
two pink and green places are only one place.
the places ( f, 0) and (b, 0) have been duplicated; in reality the two copies are merged.
The places of each philosopher are {(w, i), (e, i)} for i = 0, 1, 2. For example, transition
M. Bozga et al.
– S
def
=
N
k=1 S
k
× U. That is, the net has a place (s, u) for each state s of each component type, and for each node u.
– For each minimal model I = (U,ι) of a clause C of Γ, the set T contains a transition
t ι ∈ T , and the set E contains edges ((s, u), t ι ) and (t ι , (s , u)) for every s
p
−
→ s ∈
N
k=1 Δ
k
such that u ∈ ι(p). Nothing else is in T or E. Intuitively, t ι “synchronizes”
all the transitions s
p
−
→ s of the different components occurring in the interaction.
– For each 1 ≤ k ≤ N, each s ∈ S
k and each u ∈ U, m 0 ((s, u)) = 1 if s = s 0
k and
m 0 ((s, u)) = 0, otherwise. That is, m 0 contains the places (s, u) such that s is an
initial state.
It follows immediately from this definition that N U
S
is a 1-safe Petri Net. Indeed, for
every u ∈ U, for every component-type C
k , and for every reachable marking m, we have
s∈S k m((s, u)) = 1. This reflects that the instance of C
k at u is always in exactly one of
the states of S
k ; if s is that state, then (s, u) is the place carrying the token.
Example 2. Consider our running example, with U = {0, 1,..., n−1}, i.e., n philosophers
and n forks. Since the interaction formula (1) has no constants, its models are pairs
(U,ι), where ι gives the interpretation of the free variable i and the predicates g, t, etc.
The first disjunct of (1) is [g(i) ∧ t(i) ∧ t(succ(i))]. It has a minimal model for each k ∈ U,
namely the model with ι(i) = k, ι(g) = {k} and ι(t) = {k, (k + 1) mod n}. In the interaction
produced by this model, the k-th philosopher executes transition g(et), the forks with
numbers k and (k + 1) mod n execute transition t(ake), and all other philosophers and
forks remain idle. The second disjunct yields the interactions in which a philosopher
puts down its forks. Fig. 2 shows the Petri Net N U
S
for universe U = {0, 1, 2}. For clarity,
(w, 0)
(w, 1)
(w, 2)
(e, 0)
(e, 1)
(e, 2)
( f, 0)
(b, 0)
( f, 1)
(b, 1)
( f, 2)
(b, 2)
( f, 0)
(b, 0)
i 1
i 2
i 3
i 4
i 5
i 6
Fig. 2: Petri Net of the dining philosophers for the universe U = {0, 1, 2}. In reality, the
two pink and green places are only one place.
the places ( f, 0) and (b, 0) have been duplicated; in reality the two copies are merged.
The places of each philosopher are {(w, i), (e, i)} for i = 0, 1, 2. For example, transition