Graphics Programs Reference
In-Depth Information
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.
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
Search WWH ::
Custom Search