MODELLING FLEXIBLE MANUFACTURING SYSTEMS - Modelling with Generalised Stochastic Petri Nets - page 178

is idle”, while a token in place busyM i represents the condition “machine
M i is busy”. The transitions represent the possible events that can cause
the movement of parts and/or cards in the cell. An n-cell Kanban system
is obtained by composing n such submodels by simply merging transition
exitCell i and enterCell i+1 as shown in Fig. 8.3. In the GSPN model of
Fig. 8.3, an unlimited source of raw parts and an unlimited sink for finished
products is implicitly assumed. For this reason places BB 1 and OB n are
never marked in any tangible marking.

8.2.1 Structural analysis of the GSPN model of the Kanban

system

In this section we show how structural analysis methods can be used to
check whether the GSPN model correctly represents the studied system and
whether the system behaviour is correct.
P-semiflow analysis allows us to conclude that the GSPN model in Fig. 8.3
is bounded, since it is covered by P-semiflows.
The n-cell Kanban model of Fig. 8.3 has 2n minimal P-semiflows, whose

associated P-invariants are:

∀ i, 1 ≤ i ≤ n:
M(BB i ) + M(IB i ) + M(busyM i ) + M(OB i ) = K i

M(idleM i ) + M(busyM i ) = 1

The former kind of P-invariant ensures that the number of parts in cell i
is at most K i , the number of cards in the cell; the latter instead ensures
that each machine can process only one part at a time, and that places
idleM i and busyM i are mutually exclusive, consistently with their intended
interpretation.
All the transitions of the GSPN model are covered by a unique minimal
T-semiflow. It represents the deterministic flow of the unique type of parts
processed by the system. Observe that the net behaviour is deterministic:
indeed, no structural conflicts exist, hence effective conflicts can never arise.
Since confusion is a situation related to conflict resolution, this net surely is
confusion-free.
Using P-invariants it is easy to prove that the GSPN model is live. Let us
consider the model of cell i in isolation: it is trivial to show that due to the
P-invariant

M(BB i ) + M(IB i ) + M(busyM i ) + M(OB i ) = K i

at least one of the four transitions is enabled. Using the net structure it
is possible to show that from any marking where at least one transition is
enabled, markings in which any other transition in the cell model is enabled
can be eventually reached.