Model-Checking/trafficLight.tla at master · Amithabh-A/Model-Checking · GitHub

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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
---------------------------- MODULE trafficLight ----------------------------

EXTENDS Integers

VARIABLES light1, light2, counter, pc0, pc1

TypeOK == /\ light1 \in 0..1
          /\ light2 \in 0..1
          /\ counter \in 0..20

Init1 == /\ light1 = 1
        /\ counter = 20
        /\ pc0 = 0

Init2 == /\ light2 = 0
         /\ pc1 = 0
         /\ counter = 20

Init == (Init1 /\ Init2)

(* --------------------------------------------------- *)

l01 == /\ pc0 = 0
       /\ pc0' = 1
       /\ UNCHANGED << counter, light1 >>

l12 == /\ pc0 = 1
       /\ pc0' = 2
       /\ counter = 0
       /\ UNCHANGED << counter, light1 >>

l14 == /\ pc0 = 1
       /\ pc0' = 4
       /\ counter /= 0
       /\ UNCHANGED << counter, light1 >>

l23 == /\ pc0 = 2
       /\ pc0' = 3
       /\ light1' = 1-light1
       /\ UNCHANGED << counter >>

l35 == /\ pc0 = 3
       /\ pc0' = 5
       /\ counter' = 20
       /\ UNCHANGED << light1 >>

l45 == /\ pc0 = 4
       /\ pc0' = 5
       /\ counter' = counter - 1
       /\ UNCHANGED << light1 >>

l50 == /\ pc0 = 5
       /\ pc0' = 0
       /\ UNCHANGED << counter, light1 >>

(* ----------------------------------------------------- *)

Next1 ==   (\/ l01
            \/ l12
            \/ l14
            \/ l23
            \/ l35
            \/ l45
            \/ l50)

(* --------------------------------------------------- *)

m01 == /\ pc1 = 0
       /\ pc1' = 1
       /\ UNCHANGED << counter, light2 >>

m12 == /\ pc1 = 1
       /\ pc1' = 2
       /\ counter = 0
       /\ UNCHANGED << counter, light2 >>

m14 == /\ pc1 = 1
       /\ pc1' = 4
       /\ counter /= 0
       /\ UNCHANGED << counter, light2 >>

m23 == /\ pc1 = 2
       /\ pc1' = 3
       /\ light2' = 1-light2
       /\ UNCHANGED << counter >>

m35 == /\ pc1 = 3
       /\ pc1' = 5
       /\ counter' = 20
       /\ UNCHANGED << light2 >>

m45 == /\ pc1 = 4
       /\ pc1' = 5
       /\ counter' = counter - 1
       /\ UNCHANGED << light2 >>

m50 == /\ pc1 = 5
       /\ pc1' = 0
       /\ UNCHANGED << counter, light2 >>

(* ----------------------------------------------------- *)

Next2 ==    (\/ m01
             \/ m12
             \/ m14
             \/ m23
             \/ m35
             \/ m45
             \/ m50)

(* ----------------------------------------------------- *)


Next == (Next1 /\ Next2)

Invariant == ~(light1 = 0 /\ light2 = 0)


=============================================================================
\* Modification History
\* Last modified Tue Feb 13 18:29:06 IST 2024 by amithabh_a
\* Created Tue Feb 13 16:39:24 IST 2024 by amithabh_a