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-02-10  |  2KB  |  76 lines
  1. -- The level crossing.
  2.  
  3. -- The purpose of these datatype and channel declarations is to give
  4. -- us events car.enter, gate.raise etc
  5.  
  6. datatype UD = raise | lower
  7. datatype ELA = enter | leave | approach
  8.  
  9. channel car:ELA
  10. channel train:ELA
  11. channel gate:UD
  12.  
  13. -- A supply of cars
  14.  
  15. CARS = car.approach -> car.enter -> car.leave -> CARS
  16.  
  17. -- ... and trains
  18.  
  19. TRAINS = train.approach -> train.enter -> train.leave -> TRAINS
  20.  
  21. -- The behaviour of the crossing, unconstrained by any sensible
  22. -- restrictions on when the gate should be raised. The only
  23. -- thing not allowed is a car crossing when the gate is down.
  24.  
  25. CR_UP =  car.approach -> CR_UP
  26.       [] car.enter -> CR_UP
  27.       [] car.leave -> CR_UP
  28.       [] train.approach -> CR_UP
  29.       [] train.enter -> CR_UP
  30.       [] train.leave -> CR_UP
  31.       [] gate.lower -> CR_DOWN
  32.  
  33. CR_DOWN =  car.approach -> CR_DOWN
  34.       [] car.leave -> CR_DOWN
  35.       [] train.approach -> CR_DOWN
  36.       [] train.enter -> CR_DOWN
  37.       [] train.leave -> CR_DOWN
  38.       [] gate.raise -> CR_UP
  39.  
  40. -- The crossing, cars and trains - still no restrictions on the gate
  41. -- Notice that we only have to put the channel names, not all the 
  42. -- individual events, in the alphabets for [ || ]
  43.  
  44. SYSTEM = (CR_UP [ {|train,car,gate|} || {|car|} ] CARS)
  45.           [ {|train,car,gate|} || {|train|} ] TRAINS
  46.  
  47. -- The safety specification doesn't allow a car and a train to enter
  48. -- the crossing simultaneously.
  49.  
  50. SPEC =  train.enter -> train.leave -> SPEC
  51.      [] car.enter -> car.leave -> SPEC
  52.  
  53. -- Define RUN(A)
  54.  
  55. RUN(A) = [] x:A @ x -> RUN(A)
  56.  
  57. -- The assertion is best written with hiding
  58.  
  59. assert SPEC [T= SYSTEM \ {|gate,car.approach,train.approach|}
  60.  
  61. -- Now we can restrict the use of the gate
  62.  
  63. CONTROL =  train.approach -> gate.lower -> train.enter -> 
  64.            train.leave -> gate.raise -> CONTROL
  65.         [] car.approach -> car.enter -> car.leave -> CONTROL
  66.  
  67. -- The system with control added
  68.  
  69. SAFE_SYSTEM = SYSTEM 
  70.                 [ {|train,car,gate|} || {|train,car,gate|} ]
  71.               CONTROL 
  72.  
  73. -- and a new assertion
  74.  
  75. assert SPEC [T= SAFE_SYSTEM \ {|gate,car.approach,train.approach|}
  76.