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 >
Text File  |  1999-11-01  |  940b  |  37 lines
  1. -- The level crossing.
  2. -- Originator: Simon Gay, Royal Holloway, January 1999
  3. -- Adapted by Steve Schneider, Royal Holloway, May 1999
  4.  
  5. -- The purpose of these datatype and channel declarations is to give
  6. -- us events car.enter, gate.raise etc
  7.  
  8. datatype UD = raise | lower
  9. datatype ELA = enter | leave | approach
  10.  
  11. channel car:ELA
  12. channel train:ELA
  13. channel gate:UD
  14.  
  15. -- A supply of cars
  16.  
  17. CARS = car.approach -> car.enter -> car.leave -> CARS
  18.  
  19. -- ... and trains
  20.  
  21. TRAINS = train.approach -> train.enter -> train.leave -> TRAINS
  22.  
  23. -- The behaviour of the crossing, unconstrained by any sensible
  24. -- restrictions on when the gate should be raised. The only
  25. -- thing not allowed is a car crossing when the gate is down.
  26.  
  27. CR = car.approach -> car.enter -> C
  28.      [] train.approach -> train.enter -> T
  29.  
  30. C  = car.leave -> CR
  31.      [] train.approach -> train.enter -> CT
  32.  
  33. T  = train.leave -> CR
  34.      [] car.approach -> car.enter -> CT
  35.  
  36. CT = crash -> Stop
  37.