Graphics Programs Reference
In-Depth Information
analysis doesn't include any variable, the exit from the for is probabilisti-
cally controlled. The Spooler code consists of a while true, an ALT and
two fors, one on each branch of the ALT. Communications statements have
been translated as immediate transitions whose tags are obtained from the
concatenation of the name of the channel with the type of input/output
operation (? or !).
Fig.
10.9
presents the results of the complete translation of the program of
Fig.
10.7.
The centre portion of the net represents the spooler process, while
the left and right portions represent processes P
1
and P
2
, respectively. The
ALT, which is represented in the translation rule as a free-choice subnet,
after the inclusion of the complete model of communications becomes a non-
free-choice conflict among communications on the two channels Chan
1
and
Chan
2
.
The structural analysis applied to the net of Fig.
10.9
indicates three minimal
P-semiflows, all with a token count of one: each P-semiflow identifies one
of the three processes.
The three P-semiflows originate the following P-
invariants.
M(while
1
)
+ M(rv
1
)
+ M(c
1
)
+ M(for
1
)
+
+ M(infor
1
)
+ M(c
3
)
+ M(ec
3
)
=
1
M(while
2
)
+ M(rv
2
)
+ M(c
2
)
+ M(for
2
)
+
+ M(infor
2
)
+ M(c
4
)
+ M(ec
4
)
=
1
M(whileSpAlt)
+ M(c
1
)
+ M(for
1
Sp)
+
+ M(infor
1
Sp)
+ M(c
3
)
+ M(prt
1
)
+
+ M(c
2
)
+ M(for
2
Sp)
+
+ M(infor
2
Sp)
+ M(c
4
)
+ M(prt
2
)
=
1
The token position inside each process represents the current state of the
process. Observe that places c
1
,c
3
(c
2
,c
4
) are common to P
1
(P
2
) and to
Spooler, as they represent the action of communicating after the rendez-
vous.
The analysis shows also that all transitions are covered by some T-semiflow,
and that there are four minimal T-semiflows that represent the four possible
behaviours of the loops. The following two minimal T-semiflows refer to the
processes Spooler and P
1
, and represent a run on the outer loop without
entering the inner loop, and a single run of the inner loop respectively.
T
1
+ Chan
1
+ T
5
+ t
1
+ t
7
t
2
+ t
3
+ P
1
Sp + T
7
+ t
7
+ T
3
Other two specular minimal T-invariants exists for processes Spooler and
P
1
.
The reachability graph analysis detects the following five deadlock states
expressed as (P
1
+ Spooler + P
2
): (while
1
+ infor
1
Sp + while
2
), (while
1
+ infor
2
Sp + while
2
), (while
1
+ infor
1
Sp + infor
2
), (infor
1
+ infor
2
Sp
Search WWH ::
Custom Search