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
|
940b
|
37 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
-- 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