GSPN REPRESENTATION OF PHASE-TYPE DISTRIBUTIONS - Modelling with Generalised Stochastic Petri Nets - page 156

Table 7.3: Specification of the transitions of the Central Server Model of
Fig. 7.3

transition rate semantics transition weight priority ECS

TERM 0.1 infinite-server getCPU 1 1 1

CPU 1.0 infinite-server stopI 1 1 1

DISK 0.8 infinite-server getDISK 1 1 2

INT 1.0 infinite-server complete 1 1 3

CPUbusy 1.0 infinite-server I/O 9 1 3

stopW 1 1 4

returnW 1 1 5

returnI 1 1 6

Table 7.4: Initial marking of the Central Server Model of Fig. 7.3

place initial marking

think 6

CPUidle 1

DISKidle 1

noINT 1

useCPU in the GSPNs of Figs. 7.1 and 7.2, obtaining the model of Fig.

7.3.
The structural analysis of this new GSPN system shows that all the places
are covered by P semi-flows, so that the net is bounded. These semi-flows
can also be conveniently used to prove several properties of this GSPN sys-
tem. The semi-flow useCPU + CPUidle + stoppedW + stoppedI reveals
that transitions stopW and stopI are mutually exclusive since, although
they share a common input place (place grabCPU), they cannot be simul-
taneously enabled due to the fact that the token count of the semi-flow is
one, and only one of the two places CPUidle and useCPU can be marked at
any given time. A similar argument (and in particular the same P semi-flow)
can be used to show that also transitions returnW and returnI are mutu-
ally exclusive. Finally, through the combined use of the semi-flows useCPU
+ CPUidle + stoppedW + stoppedI, useCPU + CPUidle + removeCPU +
releaseCPU and noINT + grabCPU + removeCPU + releaseCPU it can
be proved that once transition INT fires the token originally put in place
noINT inevitably returns in this same place. Indeed, if place grabCPU