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

datatype Location = A | B | C

datatype Color = red | green

nametype Train = {1..5}



------------------------------------------------------------------------
------------------------------------------------------------------------
-- 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


------------------------------------------------------------------------
------------------------------------------------------------------------
-- Finally, examples of their use  
-- Note:  DO NOT INCLUDE THESE PROPERTIES IN THE SOLUTIONS YOU TURN IN


--
-- Consider the following property:
--
--   There is never more than one train on the track.
--
--

-- Assume an initially empty track

EmptyTrack = enter?x?t -> leave.x.t -> EmptyTrack

------------------------------------------------------------------------
-- Now consider the following property:
--
--    Every train entering at location B must leave at location A
--

NoBC = enter.B?t -> leave.A.t -> NoBC

------------------------------------------------------------------------
-- Now, consider the following property:
--
--    No odd-numbered train enters at location C
--
-- What follows may not be the best way of specifying this property, but 
-- I want to point out a couple features that you may need or want to 
-- know.

-- First, we first create a parameterized process NotAtC(t), which represents 
-- the inability of Train t to enter at C
--
-- Note the use of "!" instead of "." -- it's necessary for indicating the
-- extent of the input pattern "?l" in "enter?l.t"

NotAtC(t) = enter?l:{A,B}!t -> leave.l.t -> NotAtC(t)

-- We then interleave copies for t=1,3,5
-- 
-- Note that the following is shorthand for
--  NoOddAtC = NotAtC(1) ||| NotAtC(2) ||| NotAtC(3) 

NoOddAtC = |||x:{1,3,5} @ NotAtC(x)