------------------------------------------------------------------------
------------------------------------------------------------------------
-- First introduce some new types for convenience

datatype Location = A | B | C

datatype Color = red | green

-- nametype Train = {1..5}

nametype Train = {1..2}



------------------------------------------------------------------------
------------------------------------------------------------------------
-- Now, introduce the necessary channels


-- signal.X.Y represents that the signal at location X has color Y

channel signal: Location . Color

-- point.X represents that the points connect A to location X

channel point: {B,C}

-- enter.X.t represents that train t has entered at location X
-- leave.X.t represents that train t has left at location X

channel enter, leave: Location . Train



-- Method 1: Keep track of number of trains

NumOnTrack(n) = if n == 5 then leave?X.t -> NumOnTrack(4) else
                if n == 0 then
                   signal?X!green -> NumOnTrack(0) 
                  [] enter?X?t -> NumOnTrack(1)
                else
                   enter?X?t -> NumOnTrack(n+1)
                  [] leave?X?t -> NumOnTrack(n-1)

-- Not specifically specified, but it makes sense that a train has to 
-- enter before leaving the track

TRAIN(t) = enter?X!t -> leave?Y!t -> TRAIN(t)

TRAINS = (|||t:Train @ TRAIN(t)) [| {|enter,leave|} |] NumOnTrack(0)



 
                   


-- Method 2: let each train keep track of itself

Beta = { signal.x.green | x <- Location }

GreenOkay(t) = enter?X!t -> leave?Y!t -> GreenOkay(t)
              [] signal?X!green -> GreenOkay (t)

GreenSignal = [| Beta |] t:Train @ GreenOkay(t)



assert TRAINS [T= GreenSignal
assert GreenSignal [T= TRAINS