/* model of a railroad crossing. The scenario is a train track with a
   gate along it.  There is a sensor 1 km before the gate which signals
   the approach of the train, and sends a message to the gate asking it
   to close.  Another sensor is 100 m after the gate, and sends a signal 
   to the gate to open.  There is a delay of 5 s between the time a 
   signal comes from the sensor and the siganl reaching the gate.
*/
    
always Train = (ipos, vel)[pos]{
    pos = ipos,
    always pos' = vel
},

Sensor = (pos, Sig)[]{
    always forall Train(N) do if N.pos = pos then Sig
},

/* controller for the gate.  Enforces the delays. Also if there is
   a signal to lower the gate while the controller is waiting to 
   signal the gate to open, then the lowering is preempted */
Controller = (App, Lower, Exit, Raise){
    always {
        if App then wait 5 do Lower,
        if Exit then do wait 5 do Raise watching App
    }
},

Gate = (){
    g = 90,
    always {
        cont(g),
        if (g=0 || g=90) then
            do always g' = 0 watching (Raise || Lower),
        if Raise then
            do always g' = 10 watching (Lower || g=90),
        if Lower then
            do always g' = -10 watching (Raise || g=0)
    }
},

/* scenario */
Gate(),
Sensor(S1, 1000, App),
Sensor(S2, -100, Exit),
Controller(App, Lower, Exit, Raise),
Train(T1, 10000, -50),
wait 220 do Train(T2, 10000, -50)