COMPUTER-AIDED ANALYSIS OF PARALLEL SYSTEMS

Michael Yoeli, Prof. Emeritus, CS Dept., Technion

LECTURE 3

CADP

In this lecture you will learn how to go from Blot descriptions to the corresponding LOTOS specifications, and how to apply the toolbox CADP to convert such LOTOS specifications into corresponding LTSs.

At this stage it is important that you get access to CADP, so that you can actively participate in the exercises we are about to discuss. Once you are enrolled in this Course, you will have easy access to CADP.

Throughout this Course we will mainly be concerned with Basic LOTOS, which deals with control aspects only, disregarding any data-processing.

We now assume that you have access to CADP and are thus in a position to actively follow our instructions.

3.1 Getting Started with CADP

To get started with CADP, open a dedicated directory, and into this directory copy the following LOTOS file exa3.1.lotos

File exa3.1.lotos

specification exa[a,b]:exit behaviour

a;b;exit

endspec

If two processes are strongly equivalent, we say that they have the same behaviour. A LOTOS program, such as the above, specifies a behaviour by means of a representative process.

The above LOTOS-file specifies the behaviour of the Blot process a;b;$ (see Fig. 2.1). The process is described in the second line of the file, with ‘$’ replaced by ‘exit’. We name this process now ‘exa’; this name appears in the heading, together with the (observable) actions involved. The term ‘exit’ in the heading indicates that the process is terminating (no recursion is involved).

Now issue the following CADP command:

caesar -aldebaran exa3.1.lotos

The outcome is a file exa3.1.aut, representing an extended version of the above LTS 2.1 , which is strongly equivalent to the process specified by exa3.1.lotos. File exa3.1.aut is shown below.

File exa3.1.aut

des (0,3,4)

(0,A,1)

(1,B,2)

(2,exit,3)

This file differs from the LTS 2.1 by the addition of a heading, and a transition labeled ‘exit’. The heading ‘des (0,3,4)’ indicates that the initial state is 0, the number of the following lines is 3, and the number of states is 4. The transition labeled ‘exit’ connects the terminal state of LTS 2.1 (state 2) to a new terminal state (state 3). This may be viewed as an indication that state 2 is a proper terminal state of the basic (non-augmented) LTS 2.1, and not a “deadlock” state. We will return to this distinction later on.

3.2 Equivalences

You may use Aldebaran to check strong and observation equivalences. To do so, issue the command ‘aldebaran’ followed by

-bequ to compare two LTSs with respect to strong equivalence

-oequ to compare two LTSs with respect to obs. equivalence.

To illustrate, copy the following file into your dedicated directory.

File exa3.2.lotos

specification exa[a,b]:exit behaviour

i;a;b;exit

endspec

Now use the command

caesar –aldebaran exa3.2.lotos

to obtain the file exa3.2.aut.

You may now verify that the processes specified in files exa9.1.lotos and exa9.2.lotos are obs. equivalent by using the command

aldebaran –oequ exa3.1.aut exa3.2.aut

You will get the outcome ‘TRUE’.

On the other hand, if you replace in the above command ‘-oequ’ by ‘-bequ’, you will get an explanation, why the two processes are not strongly equivalent.

You may also use Aldebaran to reduce a given LTS modulo observation equivalence; i.e., to get a minimal LTS, obs. equivalent to the original one. The relevant command is:

aldebaran –omin file.aut

E.g., if you apply this command to exa3.2.aut you will get exa3.1.aut (with changed state names).

3.3 Recursion

The following file pud.lotos illustrates how recursion is dealt with in LOTOS.

File pud.lotos

specification pud[up,down]:noexit behaviour

P[up,down]

where

process P[up,down]:noexit:=

up;down;P[up,down]

endproc

endspec

Thus, when specifying the behaviour of pud[up,down], the relevant recursive process (here denoted P[up,down]) has to be suitably defined. If we use CADP, to convert pud[up,down] into an LTS , the outcome is shown below.

File pud.aut

des(0,2,2)

(0,UP,1)

(1,DOWN,0)

We may also use mutual recursion, as illustrated in Section 2.5.

Below is the corresponding LOTOS file pud1.lotos.

File pud1.lotos

specification pud1[up,down]:noexit behaviour

Pup[up,down[

where

process Pup[up,down]:noexit:=

up;Pdown[up,down]

endproc

process Pdown[up,down]:noexit:=

down;Pup[up,dow]

endproc

endspec

We can now prove that processes pud and pud1 have equal behaviour. Namely, we convert pud1 into the corresponding LTS, which turns out to be equal to pud.aut.

3.4 Choice

If P and Q are processes, then P[]Q denotes a process that behaves either like P or like Q (see Section 2.6). To illustrate, consider the following LOTOS-file choice.lotos.

File choice.lotos

specification choice[a,b]:exit behaviour

(i;a;exit) [] (b;exit)

endspec

Copy this file and generate the relevant choice.aut file. You should get:

File choice.aut

des (0,4,4)

(0,i,1)

(1,A,2)

(0,B,2)

(2,exit,3)

The last line of this file again augments the basic LTS, as explained in Section 3.1.

3.5 From LTS to LOTOS

It is rather easy to convert a given LTS into an obs.equivalent process. To illustrate, consider the LTS shown in the file lts.aut below.

File lts.aut

des (0,6,4)

(0,A,1)

(1,B,0)

(1,C,3)

(0,D,2)

(2,E,3)

(3,F,0)

To obtain an obs.equivalent process we associate a process with each state, which has more than one incoming transition and/or more than one outgoing transition. The corresponding lotos.file is shown below.

File lts.lotos

specification lts[a,b,c,d,e,f]:noexit behaviour

P0[a,b,c,d,e,f[

where

process P0[a,b,c,d,e,f]:noexit:=

a;P1[a,b,c,d,e,f] [] d;e;P3[a,b,c,d,e,f]

endproc

process P1[a,b,c,d,e,f]:noexit:=

b;P0[a,b,c,d,e,f] [] c;P3[a,b,c,d,e,f[

endproc

process P3[a,b,c,d,e,f]:noexit:=

f;P0[a,b,c,d,e,f[

endproc

endspec

Here, process Pj represents state ‘j’ of the above LTS.

I suggest that you now verify that the above process P0 and the LTS specified in lts.aut are strongly equivalent by converting file lts.lotos into an aut-file. I assume that you can do this without any problems.

3.6 Parallel Operators

LOTOS provides a variety of facilities to represent processes which operate concurrently.

The Interleaving Operator |||

If P and Q are processes, P|||Q represents their parallel execution without any “synchronization”, i.e., each process proceeds independently of the other. Using Blot, we have ,e.g.,

a;b;$ ||| c;$ ≡ c;a;b;$ [] a;(c;b;$ [] b;c;$)

where ‘≡’ denotes strong equivalence.

The Selective Composition Operator |[…]|

If A1,…,An are some observable actions common to processes P and Q, then P|[A1,…,An]|Q represents the parallel execution of P and Q, provided they synchronize on (perform simultaneously) the listed actions A1,…,An. Using Blot, we have, e.g.,

a;b;c;$ |[b]| d;b;$ ≡ a;d;b;c;$ [] d;a;b;c;$

Formally, P|[L]|Q, where L is a set of observable actions common to P and Q, may be defined as follows.

(1) If P[a>P’ and ‘a’ is not in L then P|[L]|Q [a>P’|[L]|Q

(2) If Q[b>Q’ and ‘b’ is not in L then P|[L]|Q [b> P|[L]|Q’

(3) If P[a>P’ , Q[a>Q’, and ‘a’ is in L then P|[L]|Q [a> P’|[L]|Q’

The Full Synchronization Operator ||

Let P and Q be processes which have all their observable actions in common. Let this common set of actions be L. Then

P||Q = P|[L]|Q .

The operator ‘||’ is referred to as the full synchronization operator. Thus, the composite process P||Q requires that processes P and Q synchronize on all their observable actions, but not on ‘i’. It might be possible that this cooperation of P and Q stops at some state, before both processes have completed their tasks. Such a state is referred to as deadlock. In Blot we will use ‘stop’ to refer to such a deadlock state.

Let us now look at illustrating examples, formulated in Blot.

Example Syn1 a;i;i;b;$ || i;a;i;b;$ == a;b;$

Here, ‘==’ denotes obs. equivalence. Note that the two component processes do not synchronize on ‘i’.

Example Syn2 Let syn2 = a;b;$ || a;b;a;$ .

This process will encounter a deadlock state, after performing the sequence a;b. Using Blot, we may state that the process syn2 equals a;b;stop.

The corresponding aut-file is shown below.

File syn2.aut

des (0,2,3)

(0,A,1)

(1,B,2)

As compared with file exa3.1.aut (Section 3.1) no transition labeled ‘exit’ appears. This is an indication that state 2 is now a deadlock state. You may confirm this by issuing the command:

aldebaran –dead syn2.aut

The outcome is the statement:

“state 2 is a deadlock state” .

3.7 Hiding

The hiding facility of LOTOS allows us to transform some observable actions of a process into unobservable ones. This facility will be illustrated in the next lecture.

3.8 Solved Exercises

[to be completed]

3.9 Additional Exercises

[to be completed]

3.10 References

[to be completed]