-
Notifications
You must be signed in to change notification settings - Fork 1
/
correct_coaster.lts
36 lines (30 loc) · 1.19 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
31
32
33
34
35
36
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).
// 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}.