home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
cs.rhul.ac.uk
/
www.cs.rhul.ac.uk.zip
/
www.cs.rhul.ac.uk
/
pub
/
CS375
/
crossing1.fdr2
< prev
next >
Wrap
Text File
|
1999-11-01
|
2KB
|
81 lines
-- The level crossing.
-- Originator: Simon Gay, Royal Holloway, January 1999
-- Adapted by Steve Schneider, Royal Holloway, May 1999
-- The purpose of these datatype and channel declarations is to give
-- us events car.enter, gate.raise etc
datatype UD = raise | lower
datatype ELA = enter | leave | approach
channel car:ELA
channel train:ELA
channel gate:UD
channel crash
-- A supply of cars
CARS = car.approach -> car.enter -> car.leave -> CARS
-- ... and trains
TRAINS = train.approach -> train.enter -> train.leave -> TRAINS
-- The behaviour of the crossing, unconstrained by any sensible
-- restrictions on when the gate should be raised. The only
-- thing not allowed is a car crossing when the gate is down.
CR = car.approach -> car.enter -> C
[] train.approach -> train.enter -> T
C = car.leave -> CR
[] train.approach -> train.enter -> CT
T = train.leave -> CR
[] car.approach -> car.enter -> CT
CT = crash -> STOP
GATE = gate.lower -> gate.raise -> GATE
[] car.enter -> GATE
ET = {| train |}
EC = {| car |}
EGC = { gate.raise, gate.lower, car.enter }
EX = {| crash |}
ES = {| train, car, gate, crash |}
ETCC = {| train, car, crash |}
ETCG = {| train, car, gate |}
SYSTEM = ((CR [ETCC||EGC] GATE) [ES||EC] CARS) [ES||ET] TRAINS
-- Define RUN(A)
RUN(A) = [] x:A @ x -> RUN(A)
-- The specification allows all events except crash
SPEC = RUN(ETCG)
assert SPEC [T= SYSTEM
-- Using hiding to express the specification differently
assert STOP [T= (SYSTEM \ ETCG)
-- Introducing the controller to restrict the use of the gate
CONTROL = train.approach -> gate.lower -> train.enter ->
train.leave -> gate.raise -> CONTROL
[] car.approach -> car.enter -> car.leave -> CONTROL
-- Using the controller should make the system safe
SAFE_SYSTEM = SYSTEM [ES||ETCG] CONTROL
-- which can be checked, again in two ways
assert SPEC [T= SAFE_SYSTEM
assert STOP [T= (SAFE_SYSTEM \ ETCG)