The Symphony IDE

Formal Modelling for Systems of Systems

Go to our GitHub Profile



This example is based on Bill Roscoe’s CSP specification of a level railroad crossing.


-- Based on Bill Roscoe's CSP specification

channels tock

-- The following are the communications between the controller process and the gate process

  gatestates = <godown> | <goup> | <up> | <down>

-- where we can think of the first two as being commands to it, and the
-- last two as being confirmations from a sensor that they are up or down.

  gate: gatestates

-- For reasons discussed below, we introduce a special error event:

channel error

-- To model the speed of trains, and also the separation of more than one train, we divide the track into
-- segments that the trains can enter or leave.

  TRAINS = <Thomas> | <Duncan>

  N = 5

-- Here, segment 0 represents the outside world, and 1-4 actual track segments including the crossing,
  TRACKS = nat
    inv t == t in set {0,...,N}

    inv t == t in set {1,...,N}

-- which is at

  GateSeg = N-1

-- To make modular arithmetic convenient, we define

  enter, leave: TRAINS * TRACKS

-- Trains are detected when they enter the first track segment by a sensor that drives the controller, 
-- and are also detected by a second sensor when they leave.

  sensorsig = <inseg> | <outseg>

  sensor: sensorsig

-- Untimed trains and tracks

-- The following gives an untimed description of Train A on track segment j. A train not currently in 
-- the domain of interest is given index 0.

process Trains =
    Train = A: TRAINS, j: TRACKS @
      enter.A.((j+1) mod (N+1)) -> leave.A.j -> Train(A,(j+1) mod (N+1))
  Train(<Thomas>,0) ||| Train(<Duncan>,0)

-- The real track segments can be occupied by one train at a time, and each time a train enters
-- segment 1 or leaves GateSeg the sensors fire.

process Track = j: TRACKS @
    Tracknf = j: TRACKS @
      if j=1 then
        enter?A!j -> sensor.<inseg> -> Trackf(A,j) 
        enter?A!j -> Trackf(A,j)

    Trackf = A: TRAINS, j: TRACKS @
      leave.A.j ->
        if j = GateSeg then
          sensor.<outseg> -> Tracknf(j)

-- Like the trains, the untimed track segments do not communicate with each other

process Tracks = ||| i: TRACKSEGS @ Track(i)

-- And we can put together the untimed network, noting that since there is
-- no process modelling the outside world there is no need to synchronise
-- on the enter and leave events for this area.

process Network =
  Trains [|({|enter,leave|} \ {|enter.A.0 | A: TRAINS|}) \ {|leave.A.0 | A: TRAINS|}|] Tracks

-- Speed assumptions on trains

-- We make assumptions about the speed of trains by placing (uniform)
-- upper and lower "speed limits" on the track segments:

  MinTocksPerSeg = 3

  MaxTocksPerSeg = 6

-- The speed regulators express bounds on the times between successive
-- enter events.

--  AlphaSR(j) = {tock,enter.A.j,enter.A.(j+1) mod (N+1) | A <- TRAINS}

process SpeedRegs = 
    SpeedReg = j: TRACKS @
      enter?A!j -> SpeedReg'(j,0)
      tock -> SpeedReg(j)

  SpeedReg' = j: TRACKS, n: int @
    [n < MaxTocksPerSeg] & tock -> SpeedReg'(j,n+1) 
    [n >= MinTocksPerSeg] & enter?A!((j+1) mod (N+1)) -> SpeedReg(j)
  || j: TRACKSEGS @ 
    [ {} | {tock}
      union {enter.A.j | A: TRAINS}
      union {enter.A.((j+1) mod (N+1)) | A: TRAINS}
    ] SpeedReg(j)

-- The following pair of processes express the timing contraint that
-- the two sensor events occur within one time unit of a train entering
-- or leaving the domain.

-- The timing constraints of the trains and sensors are combined into the
-- network as follows, noting that no speed limits are used outside the domain:

process SensorTiming = 
    InSensorTiming =
      tock -> InSensorTiming
      enter?A!1 -> sensor.<inseg> -> InSensorTiming

    OutSensorTiming = 
      tock -> OutSensorTiming
      leave?A!GateSeg -> sensor.<outseg> -> OutSensorTiming
  InSensorTiming [|{|tock|}|] OutSensorTiming

process NetworkTiming = SpeedRegs [|{tock} union {enter.A.1 | A: TRAINS}|] SensorTiming

process TimedNetwork =
  Network [|{|enter,sensor|} union {leave.A.GateSeg | A: TRAINS}|] NetworkTiming

-- Gate and controller

-- The last components of our system are a controller and the gate.
-- The duties of the controller
-- are to ensure that the gate is always down when there is a train on the
-- gate, and that it is up whenever prudent.

-- When the gate is up, the controller does nothing until the sensor
-- detects an approaching train.  
-- In this state, time is allowed to pass arbitrarily, except that the
-- signal for the gate to go down is sent immediately on the occurrence of
-- the sensor event.

process Controller =
    ControllerUp =
      sensor.<inseg> -> gate!<godown> -> ControllerGoingDown(1)
      sensor.<outseg> -> ERROR
      tock -> ControllerUp

    ControllerGoingDown = n: TRACKSEGS @
      ( if GateSeg < n then ERROR else sensor.<inseg> -> ControllerGoingDown(n+1) )
      []  gate.<down> -> ControllerDown(n)
      []  tock -> ControllerGoingDown(n)
      []  sensor.<outseg> -> ERROR

    ControllerDown = n: TRACKSEGS @
      ( if GateSeg < n then ERROR else sensor.<inseg> -> ControllerDown(n+1))
      [] sensor.<outseg> -> 
           ( if n=1 then gate!<goup> -> ControllerGoingUp else ControllerDown(n-1) )
      tock -> ControllerDown(n)

    ControllerGoingUp =
      gate!<up> -> ControllerUp
      [] tock -> ControllerGoingUp
      [] sensor.<inseg> -> gate!<godown> -> ControllerGoingDown(1)
      [] sensor.<outseg> -> ERROR

  ERROR = error -> Stop

-- The two states ControllerGoingDown and ControllerDown 
-- both keep a record of how many trains
-- have to pass before the gate may go up.  Each time the sensor event
-- occurs this count is increased.
-- The count should not get greater than the number of trains that
-- can legally be between the sensor and the gate (which equals the
-- number of track segments).
-- The ControllerGoingDown state comes to an end when the gate.down event occurs

-- When the gate is down, the occurrence of a train entering its sector
-- causes no alarm, and each time a train leaves the gate sector the
-- remaining count goes down, or the gate is signalled to go up, as appropriate.
-- Time is allowed to pass arbitrarily in this state, except that the
-- direction to the gate to go up is instantaneous when due.

-- When the gate is going up, the inward sensor may still fire, which means that
-- the gate must be signalled to go down again.
-- Otherwise the gate goes up after UpTime units.

-- Any process will be allowed to generate an error event, and since we will
-- be establishing that these do not occur, we can make the successor process
-- anything we please, in this case STOP.

-- The following are the times we assume here for the gate to go up
-- and go down.  They represent upper bounds in each case.

  DownTime = 5

  UpTime = 2

process Gate =
    GateUp =
      gate.<goup> -> GateUp
      [] gate.<godown> -> GateGoingDown(0)
      [] tock -> GateUp

    GateGoingDown = n: nat @
      gate.<godown> -> GateGoingDown(n)
      ( if n = DownTime then
          gate.<down> -> GateDown
          ( gate.<down> -> GateDown
            tock -> GateGoingDown(n+1) ) )

    GateDown =
      gate.<godown> -> GateDown
      gate.<goup> -> GateGoingUp(0)
      tock -> GateDown

    GateGoingUp = n: nat @
      gate.<goup> -> GateGoingUp(n)
      gate.<godown> -> GateGoingDown(0)
      [] ( if n = UpTime then
             gate.<up> -> GateUp
             ( gate.<up> -> GateUp
               tock -> GateGoingUp(n+1) ) )

process GateAndController = Controller [|{|tock,gate|}|] Gate

process System = TimedNetwork [|{|sensor,tock|}|] GateAndController