Objective:
- Practice specification and refinement of CSP processes in FDR
- Practice the specification and refinement of safety properties
- The dining philosophers problem
Five philosophers dine together at the round table, and each one has one plate of spaghetti. One fork is placed between any adjacent philosophers, and a philosopher must hold two nearby forks to eat. A fork can be held by one philosopher only anytime.
We consider the most simple case in which three events, pickup, putdown and eat, are used. We use a number to name a philosopher or a fork. For example, pickup.0.0 means that the 0th philosopher picks up the 0th fork. We assume all the philosophers pick up the left-side fork first, then pick up the right-side fork and put down the right one, and finally put down the left one. The left-side fork has the same number with the philosopher, and the right-side fork is i+1. For example, the 4th philosopher picks up the right side fork, which is modelled as pickup.4.0
Please exercise the following FDR script.
N = 5
channel pickup, putdown:{0..N-1}.{0..N-1}
channel eat:{0..N-1}
PHIL(i) = pickup.i.i->pickup.i.((i+1)%N)->eat.i->
putdown.i.((i+1)%N)->putdown.i.i->PHIL(i)
FORK(i) = pickup.i.i->putdown.i.i->FORK(i) []
pickup.((i-1)%N).i->putdown.((i-1)%N).i->FORK(i)
PHILS = |||i:{0..N-1}@PHIL(i)
FORKS = |||i:{0..N-1}@FORK(i)
SYSTEM = PHILS [|{|pickup, putdown|}|] FORKS
The safety property for the system is that each philosopher should not eat consecutively if any philosopher has not eaten yet. To denote all the philosophers haven finished eating, we introduce a new event done and make it happen when all have finished. We also introduce an event error to label the ‘bad’ traces in which two eat.i have happened but other philosophers may not eat yet.
The process, which can identify the ‘bad’ behaviour, is described by the following transition diagram, and is represented in FDR like
channel done, error
CE(i) = eat.i -> CE1(i)
CE1(i) = done -> CE(i) [] eat.i -> CE2(i)
CE2(i) = error -> CE2(i) [] eat.i-> CE2(i)
| 0 |
| eat.0 |
| done |
| eat.0 |
| error |
| eat.0 |
We make this process synchronised with PHILS and FORKS, and refine it again.
CES = [|{done}|]x:{0..N-1}@CE(x)
S1 = SYSTEM [| {|eat|} |] CES
assert SKIP [T= S1 \{|pickup, putdown,eat,done|}
Now, we restrict the behaviour of a philosopher to use the event done to force all to finish together. This constraint enables the system to satisfy the safety property.
SPHIL(i) = pickup.i.i->pickup.i.((i+1)%N)->eat.i->
putdown.i.((i+1)%N)->putdown.i.i->done->SPHIL(i)
SPHILS = [|{done}|]i:{0..N-1}@SPHIL(i)
SSYSTEM = SPHILS [|{|pickup, putdown|}|] FORKS
S2 = SSYSTEM [| {|eat, done|} |] CES
assert SKIP [T= S2 \{|pickup, putdown,eat,done|}
- The railway crossing problem
Three processes in the system: a train or a car can approach, enter and leave the crossing, the gate can be raised and lowered and is initially raised. Obviously, the car can enter only if the gate is raised, and the train has no interaction.
The safety property is the car and the train cannot enter the crossing at the same time. Therefore, we need a process to capture the ‘bad’ behaviour (traces) which can violate the property.
Obviously, the ‘raw’ system cannot satisfy the safety property and therefore we introduce a control system to make sure the car cannot enter the cross when the gate is lowered.
Please read and exercise the following script to understand the modelling and refinement.
datatype LOC = approach | enter | leave
datatype POS = raise | lower
channel car,train:LOC
channel gate:POS
channel crash
Trains = train.approach -> train.enter -> train.leave -> Trains
Cars = car.approach -> car.enter -> car.leave -> Cars
Gates = gate.lower -> gate.raise -> Gates [] car.enter -> Gates
System = Trains ||| (Cars [|{car.enter}|] Gates)
CR = car.enter ->C [] train.enter -> T
C = car.leave -> CR [] train.enter -> CT
T = train.leave -> CR [] car.enter -> CT
CT = crash -> STOP
A = {car.enter, car.leave, train.enter, train.leave}
SYS = System [|A|] CR
X = {|car, train, gate|}
SPEC = []x:X@x-> SPEC
assert SPEC [T= SYS
— we introduce a controller
CONTROL = gate.lower -> train.enter -> train.leave -> gate.raise -> CONTROL []
car.enter -> car.leave -> CONTROL
SAFE_SYS = SYS [|union(A, {|gate|})|] CONTROL
assert SPEC [T= SAFE_SYS
- The simulation of a Queue
A queue is a data structure which has the property FIFO (first in first out). Here we use two events in and out to simulate the operations, enqueue and dequeue, respectively.
We assume there are five numbers (well, you can set up an any number later), and the queue can input these numbers unrepeatedly, and output these numbers with the input order. The queue can input the numbers if there are left, and output these numbers anytime as long as there is at least one number in the queue.
The following script models the operations of the queue. Please pay attention to the operations of sets and sequences in FDR. Please use FDR/Probe to check it.
N = 5
Range = {0..N-1}
channel in,out:Range
Queue(X, S) = in?x:X -> Queue(diff(X,{x}), S^<x> ) []
(not null(S)) & out.head(S) -> Queue(X, tail(S))
P = Queue(Range, <>)
