-
Notifications
You must be signed in to change notification settings - Fork 66
/
traffic.tla
71 lines (53 loc) · 1.73 KB
/
traffic.tla
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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
------------------------------ MODULE traffic ------------------------------
Color == {"red", "green"}
NextColor(c) == CASE c = "red" -> "green"
[] c = "green" -> "red"
(*--algorithm traffic
variables
at_light = TRUE,
light = "red";
fair process light = "light"
begin
Cycle:
while at_light do
light := NextColor(light);
end while;
end process;
fair+ process car = "car"
begin
Drive:
when light = "green";
at_light := FALSE;
end process;
end algorithm;*)
\* BEGIN TRANSLATION
\* Process light at line 14 col 1 changed to light_
VARIABLES at_light, light, pc
vars == << at_light, light, pc >>
ProcSet == {"light"} \cup {"car"}
Init == (* Global variables *)
/\ at_light = TRUE
/\ light = "red"
/\ pc = [self \in ProcSet |-> CASE self = "light" -> "Cycle"
[] self = "car" -> "Drive"]
Cycle == /\ pc["light"] = "Cycle"
/\ IF at_light
THEN /\ light' = NextColor(light)
/\ pc' = [pc EXCEPT !["light"] = "Cycle"]
ELSE /\ pc' = [pc EXCEPT !["light"] = "Done"]
/\ light' = light
/\ UNCHANGED at_light
light_ == Cycle
Drive == /\ pc["car"] = "Drive"
/\ light = "green"
/\ at_light' = FALSE
/\ pc' = [pc EXCEPT !["car"] = "Done"]
/\ light' = light
car == Drive
Next == light_ \/ car
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
=============================================================================