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]