with_go_coaster.lts

const Max  = 9
const MCar = 4

// Models passenger arrival at the platform
PASSENGERS = (newPassenger -> PASSENGERS).

// Limits passengers on platfrom to Max & allocates passengers to cars
// while allowing a car to leave the platform if there is at least one
// passenger in it
CONTROLLER        
    = CONTROL[0][0],
CONTROL[count:0..Max][carSize:0..MCar]  
    = (when (count < Max) 
            newPassenger  -> CONTROL[count+1][carSize]
      |requestPassenger[n:1..MCar] -> CONTROL[count][n]
      |when (carSize > 0 && count >= carSize) 
            getPassenger[carSize] -> CONTROL[count-carSize][0] 
      |when (carSize > 0 && count > 0 && count < carSize)
            goNow -> getPassenger[count] -> CONTROL[0][0]
      ).

// The coaster car requests N passengers and departs when the
// Controller responds with getPassenger
COASTERCAR(N=MCar) 
    = (arrive -> requestPassenger[N] -> getPassenger[i:1..MCar] -> 
         if (i > N) then ERROR else (depart -> COASTERCAR))
      +{{requestPassenger,getPassenger}[1..MCar]}.

// Controls access to the platform
PLATFORMACCESS = (arrive -> depart -> PLATFORMACCESS).

// Allows a car to leave the platform if there is at least one passenger in it
BUTTON = (goNow -> BUTTON).

// System with two coaster cars with capacity two and three
||ROLLERCOASTER
         = (PASSENGERS 
           || car[1..2]::(CONTROLLER || PLATFORMACCESS || BUTTON) 
           || car[1]:COASTERCAR(2) 
           || car[2]:COASTERCAR(3)
           || BUTTON
           )
           /{newPassenger/car[1..2].newPassenger, goNow/car[1..2].goNow}.