Advanced Programming - Concurrency, Lab 3

Aims

Understanding parallel composition of processes.

  1. (3.1) Show that S1 and S2 describe the same behaviour

    P = (a->b->P).
    Q = (c->b->Q).
    ||S1 = (P||Q).

    S2 = (a->c->b->S2 | c->a->b->S2).
    Hint: load the definitions of P, Q, S1 into LTSA; do Compose and see that the result is equivalent to S2.

    Why isn't S2 exactly the same as S1? How come and S1 is "optimised"?

  2. (3.3) Extend the model of the client-server system described in section 3.1.4 (slide 16) copied below, such that more than one client can use the server. 
    CLIENT = (call->wait->continue->CLIENT).
SERVER = (request->service->reply->SERVER).

||CLIENT_SERVER = (CLIENT || SERVER)
                 /{call/request, reply/wait}.

  3. (3.4) Modify the model of the client-server system in exercise 3.3 such that the call may terminate with a timeout action rather than a response from the server. What happens to the server in this situation?

  4. Run some of the examples from Chapter 3 for the LTSA.