Objective:

• Practice specification and refinement of CSP processes in FDR
• Practice the specification and refinement of safety properties
1. 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)

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, <>)

All papers are written by ENL (US, UK, AUSTRALIA) writers with vast experience in the field. We perform a quality assessment on all orders before submitting them.

Do you have an urgent order?  We have more than enough writers who will ensure that your order is delivered on time.

We provide plagiarism reports for all our custom written papers. All papers are written from scratch.