COLOURED PETRI NETS 85

Figure 9.5: Modelling of anawait-statement.

fordo_12

Figure 9.6: Modelling of afor-statement.

whenycontains a⁾ -token, which corresponds to^* being ⁾ in Lamport’s Algorithm.

The goto-statements are modelled implicitly. Consider, e.g., the goto-statement immediately after theawait-statement in line 7. In the model, we have drawn an arc from the transition modelling the execution of theawait-statement to the placestart 1. Finally, we consider thefor-statement starting in line 12. It is modelled by the part of the CPN model shown in Fig. 9.6. For reasons to become clear later (in Sect. 9.6), we model a more general form of thefor-statement. In Lamport’s Algorithm, thefor -statement is used to test each of the entries in the¹ -array in turn starting from¹³²⁴⁶⁵. In the model, we do not impose an order in which the entries are tested.

When process⁺ enters thefor-statement by occurrence of the transitionfordo 12, the multi-set denoted+87:9<;>=!+@?

.BAC

+6DE$FHGEJIK9<;>=ML is put on the place wait, which contains the entries in the¹ -array that process⁺ still needs to test. The transition await 13models the execution of theawait-statement inside thefor-statement, and is only enabled when a^C ENDPORQ$SUTNVWF-token is present on theb-place. An occurrence of that transition will remove an^C+DEF -token fromwait and add it to the placedone, which contains the entries in the¹ -array that process⁺ has already tested. Process⁺ leaves the for-statement when the transitionforod 13 occurs. As it can be seen, this transition is only enabled when placedonecontains the multi-set+X7Y9Z;>=[+? , i.e., when all the entries in the¹ -array have been tested.

We have now explained how to model all the basic constructs of Lamport’s Al-gorithm. The creation of the complete model just consists of putting all the pieces together. The process might even be automated. No ingenuity is required — nor de-sired. This systematic strategy reduces the probability of accidental errors, and thus makes it unlikely that the constructed CP-net is not a proper model of the algorithm.

Lamport’s Algorithm is modelled in a similar way in [3].

9.2.2 Formal Definition of CP-nets

We now give a formal definition of CP-nets and their behaviour. The purpose of this section is twofold. First of all, to clear out any ambiguity that might be in the infor-mal introduction to CP-nets in the previous section, and second, to fix the notation to be used in this paper. The definitions and notation closely follow [66], and readers familiar with that reference may skip this section.

Structure of CP-nets

Before giving the formal definition of a CP-net, we fix some notation and terminol-ogy. The term net expressions refers to the expressions describing colour sets, initial markings, arc expressions, and guards. Related to net expressions, we introduce the following notation:

\J]

*^_V

C

Va`_^3bcF denotes the type of an expression<sup>Vd`e^3b</sup> .

\gf

QWb

C

Va`e^>bhF denotes the set of variables in an expression<sup>Vd`e^3b</sup> .

\J]

*^_V CUi

F denotes the type of a variableⁱ .

\J]

*^_V CUi

QWbcTjF , where^{i QkbcT} is a set of variables, denotes the set of types

A ]

*^_V CUi

FG i I i

QkbcTNL .

\glemon

denotes the set of multi-sets over a set^l .

\gprqsq

S denotes the set of booleans, i.e.,^{prqsq S .tA6u} bsvwVWDPORQ$SUTNVWL . We now formally define CP-nets. Explanation follows the definition.

Definition 1 A CP-net is a tuple ^{xZ9<? .yCaz DP9{D ]} DP| DP?}DPx@DP~<DPZDP;F satisfying the requirements below:

1. ^z is a finite set of non-empty types, called colour sets.

2. ⁹ is a finite set of places.

3. ^] is a finite set of transitions.

4. ^| is a finite set of arcs such that^{9g€ ] . 9g€| . ] €(| .ƒ‚} . 5. ^? is a node function. It is defined from^| into^{9K7 ]…„r] 7J9} . 6. ^x is a colour function. It is defined from⁹ into^z .

7. ^~ is a guard function. It is defined from^] into expressions such that:

† u I ]

: ^{2] *$^_V C ~ CUu FaF . prqsq S‡ ] *$^_V C f Qkb C ~ CUu FaFaF‰ˆ z 5}.

9.2. COLOURED PETRI NETS 87 8. ^ is an arc expression function. It is defined from^| into expressions such that:

†

9. ^; is an initialisation function. It is defined from⁹ into expressions without free variables such that:^{† ^MI-9t‹2] *$^_V C ; C ^_FaF . x C^_Fmon 5}. ^ Item 1 determines the set of colour sets and hence the colours which can be referred to in the net expressions. In the CPN model of Lamport’s Algorithm we have the following set of colour sets:^zŽ.tA 9<;>= )?}DP9<;=}D

prŠZ

DP9Z;>=‘7

prŠZ

DP9Z;>=’7

9<;=}L .

Items 2, 3, and 4 specify the places, transitions, and arcs. Item 5, the node func-tion, determines the source and destination of arcs. Note that an arc always connects a place and a transition. Item 6, the colour function, associates a colour set with each place. In the CPN model of Lamport’s Algorithm, the colour function maps the place

binto^{9<;=!7 prŠZ} , the placesxandyinto^{9<;= )?} , the placeswaitanddoneinto

9<;=7-9<;>= , and all other places into9<;>= . Item 7, the guard function, ensures that guards are expressions which evaluate to a boolean, and that the types of the variables in the guards are in^z . Likewise, items 8 and 9, the arc expression function and the ini-tialisation function, ensure similarly, appropriate type constraints. In the rest of this pa-per, we will assume that a CP-net^xZ9Z? is given,^{xŠ9<? .[Caz DP9{D ]} DP| DP?}DPx@DP~<DPZDP;F. Normally, a CP-net is created in terms of a CPN diagram, i.e., a graphical rep-resentation as in Fig. 9.2, and not by specifying a 9-tuple as in Def. 1. Figure 9.2 is created using the Design/CPN tool [16, 99], which supports construction and analy-sis of CP-nets. For declarations of colour sets, variables, and functions; and for net expressions, this tool uses CPN ML, which is an extension of the functional program-ming language Standard ML (SML) (see, e.g., [119]). The declarations for the CPN model of Lamport’s Algorithm can be seen in Fig. 9.7.

In line 2, the number of processes^? is specified. In this case,^{? .K“} . Lines 8-12 declare the colour sets. Lines 15-17 declare the variables and their type. Finally, the function9Z;>=”7Y•Z|

l

 , used to specify the initial marking on the placeb, and the function+X7-9<;= , used in the modelling of thefor-statement, are declared. Both are typical SML-style recursive functions.

Behaviour of CP-nets

We now turn to the formal definition of behaviour of CP-nets. First, we fix some more notation.

\gf

QWb CUu

F , for a transition^{u I ]} , denotes the set of variables of^u present in either the guard ^{~ CUu F} or in an arc expression of one of the surrounding arcs denoted

|

7ž9 denotes the set of connecting arcs.

Formally:

1: (* Number of processes – in this case 3 *)

2: val N = 3;

3:

4: (* non-zero predicate *)

5: fun nonzero i = (i ^<¡ 0);

6:

7: (* Declarations of the colour sets *)

8: color PID 0N = int with 0..N declare ms;

9: color BOOL = bool;

10: color PID = subset PID 0N by nonzero declare ms;

11: color PIDxPID = product PID * PID;

12: color PIDxBOOL = product PID * BOOL;

13:

14: (* Declaration of the variables *)

15: var x,y : PID 0N;

16: var i,j : PID;

17: var bi : BOOL;

18:

19: (* Function used to specify the initial marking on b *)

20: fun PIDxFALSE 0 = empty

21: ^G PIDxFALSE i = 1‘(i,false) + (PIDxFALSE (i-1));

22:

23: (* Function used in the for-statement *)

24: fun ixPID i 0 = empty

25: ^G ixPID i j = 1‘(i,j)+(ixPID i (j-1));

Figure 9.7: Declarations for the CPN model of Lamport’s Algorithm.

As a consequence, if^{`Ÿ™</sup> and<sup>`_›} are not connected,^{| C`w™šD`œ›3F .t‚} .

\  C

`w™šD`œ›3F for ^C`Ÿ™šD`_›3F<IK97 ]K„M]

7ž9 denotes the expression of^{C `w™šD`_›3F} . Formally:

 C

`w™šD`œ›3F

. ¢N£k¤w¥§¦¨ª©¦3«ª¬

 C Q$F .

It should be noted that the sum in the definition of^{ C`Ÿ™šD`_›3F} is well-defined be-cause of item 8 in Def. 1, which ensures that all terms in the sum are of the same multi-set type. Having fixed the notation, we define the concept of a binding. Vd`e^3bŒ­U1š®

denotes the result of evaluating an expression^{Vd`e^3b} , whose variables are bound to val-ues as determined by¹ .

Definition 2 A binding of a transition^{u I ]} is a function¹ defined on^{f QWb CUu F} such that:

1. ^{† i I f Qkb CUu F{‹h1 CUi FI ] *^œV CUi F}. 2. ^{~ CUu FW­U1š®}.

B(t) denotes the set of all bindings for t. ^

9.2. COLOURED PETRI NETS 89

In document View of State Space Methods for Coloured Petri Nets (Sider 99-103)