Graphics Programs Reference

In-Depth Information

t
a

p
a

T
w

N

p
r

T
a

p
w

S

p
q

t
q

p
s

T
s

t
s

Figure 9.8: Abstract GSPN model obtained from that of Fig.
9.7
by elimi-

nating one immediate transition and one vanishing place

ing in models that, although easier to solve, are more di
cult to understand

or to reason about.

Before applying the reduction algorithm, we can observe that in the GSPN

model of Fig.
9.7
two immediate transitions always fire in a row: the firing

of transition t
q
is indeed always followed by that of transition t, because t
q

is enabled only if p
q
is marked (although the firing of t
q
does not modify

the marking of p
q
), so that t is always enabled after the firing of t
q
. As

(the transition resulting from the combination was named t
q
) and place p
p

has been removed.

N is the P-invariant that represents the conservation of queues (a queue can

be either empty [p
a
], or waiting for service [p
q
], or in service [p
s
]). The P-

invariant M(p
s
)+M(p
w
)+M(p
r
) = S represents the conservation of servers

(a server may be either serving [p
s
], or walking [p
w
], or deciding which queue

Search WWH ::

Custom Search