MODELLING AND ANALYSIS OF CONCURRENT PROGRAMS - Modelling with Generalised Stochastic Petri Nets - page 242

need two places if a variable can assume also negative values. If the variable
can assume an infinite number of values we still have a Petri net with a finite
number of places, but now the net may be unbounded. Testing the value
of a variable is simple, while the assignment of a value requires extra arcs,
places and transitions.
A simple modification of the GSPN of Fig. 10.9 is shown in Fig. 10.10. Tags
of places and transitions not shown in this figure are the same as in Fig. 10.9.
The three control variables x, n and k are modelled by places p x , p n and p k
respectively. After communication on Chan 1 (Chan 2 ) the variables p x and
p k (p n ) are initialized with the same constant value k (n); at each for itera-
tion the transition that enters the loop decrements by one the corresponding
control variable; the end of loop is deterministically implemented with a test
for zero on the control variable place. In this net we have assumed that the
values of n and k are known and are represented in the GSPN by assigning
the corresponding multiplicity from T 5 (T 6 ) to p k (p n ) and p x . In this case
we can notice that the actual value of k (n) is not essential for capturing
all the important aspects of the qualitative behaviour of the net. It follows
that the value of k (n) can be randomly generated each time the for loop
starts (to mimic the variability of real messages that have different lengths),
or be kept constant to a “typical value”.
The structural analysis of the model of Fig. 10.10 reveals the same three
P-semiflows obtained for the model of Fig. 10.9: places representing control
variables are, of course, not included in any invariant.
No deadlock states are identified, i.e. the static analysis performed on this
modified model of the program does not detect any nonfault. Indeed, by
modelling the control variables we have forced the model to choose deter-
ministically whether to enter or exit a loop, and this choice is not done
independently by the processes (as in the previous model), but it is based
on information exchanged between Spooler and the two processes P 1 and
P 2 . Moreover all transitions are live, meaning that we have not modelled
impossible events.
The results are independent of the actual values of k (n). The size of the
state space of the model of Fig. 10.10, however, grows linearly with the
sum of n and k. The reason for introducing the control variables into the
model was that of limiting the number of detected anomalies which are
actually nonfaults. The price paid for obtaining such a result is an increasing
complexity of the graphical layout of the net as well as of its state space.

10.5 Stochastic Analysis

The previous subsections discuss how to translate a program into a GSPN
system. But a complete definition of a GSPN system also requires that rates
are associated with timed transition and weights are assigned to immediate