These are the exercises for week 3. During the exercise session we will try look at 1, 2, 3, 5a, 5c, 6c, 8, 9.1, 9.2, 10.1, 10.3, 11.1 and 11.3.

Channels

The solutions to exercises 1 -- 4 can be found here.

The slides used during the exercise session can be found here.

Exercise 1

Channels are useful when modelling distributed systems. In Promela a channel has a capacity and a message type.

chan myChan = [0] of { byte }

This simple example specifies a channel called myChan with 0 capacity, making it a rendezvous channel. The messagetype in this case is byte.

Now create two processes. The first process sends the numbers 0 through 9 onto the channel. The second process reads the values of the channel and outputs them.

Launch in web-interface

Exercise 2

Is it possible that process p does not read from the channel at all ?

chan com = [0] of {byte}
byte value = 0;

proctype p() {

  byte i = 0;

  do
  :: if
     :: i >= 5 -> break
     :: else   -> printf("Doing something else\n");
                  i ++
     fi
  :: com ? value ;
     printf("p received: %d\n",value)
  od

}

init {

  atomic {
    run p()
  }

  end:
  com ! 100;

}

Launch in web-interface

Exercise 3

Model a system having 5 clients and 2 servers where a client cannot send another request before his previous one was processed by a server. The suggested solution uses buffered channels and describes the behaviour of the server processes. Complete the solution for the client processes.

chan request = [2] of { byte, chan};
chan reply[5] = [2] of { byte };

active [2] proctype Server() {
  byte client;
  chan replyChannel;

  do
     :: request ? client, replyChannel ->
        printf("Client %d processed by server %d\n", client, _pid);
        replyChannel ! _pid
  od
}

proctype Client(byte id) {
  ...
}

init {
  ...
}

Launch in web-interface

Exercise 4

Model an office where two computer systems are hooked up to a single printer. Model the computer systems such that they have mutual exclusion on the printer. The printer can be modeled as the number of jobs it has. The two systems can communicate with each other via a rendezvous channel. Verify that it is never the case that both systems print at the same time.

Exercise 5

Example
F = (p & q)
Answer: I(p) = T, I(q) = T

5a
F = (p | q)
Answer: I(p) = F, I(q) = T OR I(p) = T, I(q) = T OR I(p) = T, I(q) = F

5b
F = !p
Answer: I(p) = F

5c
F = (p -> q)
Answer: I(p) = T, I(q) = T OR I(p) = F, I(q) = T OR I(p) = F, I(q) = F

Exercise 6

6a
p & !p
Answer: not satisfiable

6b
(p | q) -> (q & p)
Answer: I(p) = I(q) = T

6c
(p -> q) -> ! (q -> p)
Answer: I(p) = F, I(q) = T

Exercise 7

In earlier times there existed an island whose inhabitants were either knights or knaves. A knight always tells the truth, while a knave always lies. Hedwig and Katrin lived on that Island. A historian found in the archives the following statements:

Hedwig: I am a knave if and only iff Katrin is a knave.

Katrin: We are of different kind.

(after Raymond Smullyan, Knights and Knaves)

Answer:

H : Hedwig is a knight, K : Katrin is a knight

H <-> (!H <-> !K)

K <-> !(H <-> K)

Exercise 8

If a request occurs, then either it will eventually be acknowledged, or the requesting process will not ever be able to make progress.

Answer:

R : request is made, A : request is acknowledged

R->(<>A||[]!A)

Exercise 9

Consider a crossing of two streets with one traffic light (nr 1) controlling the north-to-south direction and one (nr 2) for the west-to-east direction. Assume you have the following propositional variables: R1 (traffic light 1 is red), G1 (traffic light 1 is green), R2 (traffic light 2 is red), G2 (traffic light 2 is green)

Give LTL formulas formalising the following properties:

1. Both traffic lights are never green at the same time.
2. Each traffic light will become eventually green at any time.
3. Traffic light 1 stays red until traffic light 2 has switched to red.
   Does the following run satisfy this last property: {R1, G2} → {R1, G2} → ..... (i.e., all states of the run interpret R1 as true and G2 as true and all others as false)?

Answer :

1. [](!G1 | !G2)
2. [](<>G1 & <>G2)
3. R1 U R2, no because R2 bever becomes true

Exercise 10

1. draw Büchi automata
2. generate a Büchi automaton from a temporal logic formula
3. check equivalence of two automata

1. you draw your own automaton (file->new->finite automaton->Büchi word automaton)
2. then you write down the formula it should represent (file->new->logic formula->qptl formula)
3. you create an automaton out of the formula (formula->translate qptl -> to NBW -> extendedLTL2AUT (both the extendedLTL2AUT and extendedLTL2AUT+ are ok))
4. tick simplify NBW
5. on a tab with the generated automaton, select Automaton->Equivalence->With an Automaton and pick the one you created.

1. 
   Answer : (b*a)^w
2. 
   Answer : (a+b)^w
3. 
   Answer : (authReq (reject + accept access* release))^w

Exercise 11

Consider the following LTL formulas and their corresponding Büchi automata. State whether these formulas accept the same language or not. If not, provide a counter-example in the form of a word which is accepted by the LTL formula but not by the automaton, or vice versa.

1. Liveness property: [](p-><>q)
2. Weak fairness: <>[]p->[]<>q
3. Strong fairness: []<>p->[]<>q

1. Incorrect, the automaton stays in q1 when p is false but q is true. A word that is accepted by the LTL formula is {p},{p,q},{},{},{},... but this is not accepted by the automaton.
2. Correct.
3. Incorrect, there is an unnecessary transition from q1 to q2. The automaton accepts the word {q},{p},{p},{p},{p},... but this is not accepted by the LTL formula.

Exercise 12

1. a appears a finite number of times
2. b appears infinitely often
3. a b cannot immediately follow an a

Answer: