-
Notifications
You must be signed in to change notification settings - Fork 0
/
correct_coaster.lts
30 lines (24 loc) · 1.16 KB
/
correct_coaster.lts
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
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
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]
).
// 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). //Need to seperate the actions
// system with two coaster cars with capacity two and three
||ROLLERCOASTER = (PASSENGERS
|| car[1..2]::(CONTROLLER || PLATFORMACCESS )
|| car[1]:COASTERCAR(2)
|| car[2]:COASTERCAR(3)
)
/{newPassenger/car[1..2].newPassenger}.