PETRI NETS AND THEIR PROPERTIES - Modelling with Generalised Stochastic Petri Nets - page 20

2.3.1 Enabling and firing rules

An “enabling rule” and a “firing rule” are associated with transitions. The
enabling rule states the conditions under which transitions are allowed to
fire. The firing rule defines the marking modification induced by the transi-
tion firing. Informally, we can say that the enabling rule defines the condi-
tions that allow a transition t to fire, and the firing rule specifies the change
of state produced by the transition.
Both the enabling and the firing rule are specified through arcs. In particu-
lar, the enabling rule involves input and inhibitor arcs, while the firing rule
depends on input and output arcs. Note that input arcs play a double role,
since they are involved both in enabling and in firing.
A transition t is enabled if and only if (i) each input place contains a number
of tokens greater or equal than a given threshold, and (ii) each inhibitor
place contains a number of tokens strictly smaller than a given threshold.
These thresholds are defined by the multiplicities of arcs. In the example in
Fig. 2.2, t is enabled if the number of tokens in place p 1 is greater than or
equal to n, and the number of tokens in place p 2 is less than m.
We can now give the following definition:

Definition 2.3.1 (Enabling) Transition t is enabled in marking M if and
only if

•∀ p ∈ • t,M(p) ≥ O(t,p) and

•∀ p ∈ ◦ t,M(p) < H(t,p)

When transition t fires, it deletes from each place in its input set • t as many
tokens as the multiplicity of the arc connecting that place to t, and adds to
each place in its output set t • as many tokens as the multiplicity of the arc
connecting t to that place.

Definition 2.3.2 (Firing) The firing of transition t, enabled in marking
M produces marking M 0 such that

M 0 = M + O(t) − I(t)

This statement is usually indicated in a compact way as M[t i M 0 , and we
say that M 0 is directly reachable from M. Referring to Fig. 2.2, we may
observe that the firing of t changes the marking by deleting n tokens from
p 1 and by adding k tokens to p 3 ; place p 2 is unaffected by the firing of t. Of
course, for t to remove n tokens from p 1 , at least n need to be there, and
this is precisely part of the condition tested by the enabling rule.
It is interesting to interpret the enabling conditions and the effect of firing
for some of the transitions of the readers & writers model of Fig. 2.1. Tran-
sitions t 4 and t 5 represent the beginning of a read access and a write access,