home *** CD-ROM | disk | FTP | other *** search
/ cs.rhul.ac.uk / www.cs.rhul.ac.uk.zip / www.cs.rhul.ac.uk / pub / CS375 / crossing.fdr2 < prev    next >
Text File  |  1999-12-02  |  2KB  |  81 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. channel crash
  15.  
  16. -- A supply of cars
  17.  
  18. CARS = car.approach -> car.enter -> car.leave -> CARS
  19.  
  20. -- ... and trains
  21.  
  22. TRAINS = train.approach -> train.enter -> train.leave -> TRAINS
  23.  
  24. -- The behaviour of the crossing, unconstrained by any sensible
  25. -- restrictions on when the gate should be raised. The only
  26. -- thing not allowed is a car crossing when the gate is down.
  27.  
  28. CR = car.approach -> car.enter -> C
  29.      [] train.approach -> train.enter -> T
  30.  
  31. C  = car.leave -> CR
  32.      [] train.approach -> train.enter -> CT
  33.  
  34. T  = train.leave -> CR
  35.      [] car.approach -> car.enter -> CT
  36.  
  37. CT = crash -> STOP
  38.  
  39. GATE = gate.lower -> gate.raise -> GATE
  40.        [] car.enter -> GATE
  41.  
  42. ET   = {| train |}
  43. EC   = {| car |}
  44. EGC  = { gate.raise, gate.lower, car.enter }
  45. EX   = {| crash |}
  46. ES   = {| train, car, gate, crash |}
  47. ETCC = {| train, car, crash |}
  48. ETCG = {| train, car, gate |}
  49.  
  50. SYSTEM = ((CR [ETCC||EGC] GATE) [ES||EC] CARS) [ES||ET] TRAINS
  51.  
  52. -- Define RUN(A)
  53.  
  54. RUN(A) = [] x:A @ x -> RUN(A)
  55.  
  56. -- The specification allows all events except crash
  57.  
  58. SPEC = RUN(ETCG)
  59.  
  60. assert SPEC [T= SYSTEM
  61.  
  62. -- Using hiding to express the specification differently
  63.  
  64. assert STOP [T= (SYSTEM \ ETCG)
  65.  
  66. -- Introducing the controller to restrict the use of the gate
  67.  
  68. CONTROL =  train.approach -> gate.lower -> train.enter -> 
  69.            train.leave -> gate.raise -> CONTROL
  70.            [] car.approach -> car.enter -> car.leave -> CONTROL
  71.  
  72. -- Using the controller should make the system safe
  73.  
  74. SAFE_SYSTEM = SYSTEM [ES||ETCG] CONTROL
  75.  
  76. -- which can be checked, again in two ways
  77.  
  78. assert SPEC [T= SAFE_SYSTEM
  79.  
  80. assert STOP [T= (SAFE_SYSTEM \ ETCG)
  81.