-
Notifications
You must be signed in to change notification settings - Fork 0
/
traffic-lights2.smv
180 lines (153 loc) · 9.9 KB
/
traffic-lights2.smv
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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
-- START Scope
-- Traffic light controller system manages the intersection of cars-pedestrians, cars-cars,
-- pedestrians-pedestrians and cars-pedestrians-emergency in a two way direction.
-- Drive Signals follow the color order - Red (Stop), Yellow (About to stop) and Green (Good to go).
-- The pedestrians raise a request to walk by pressing a request button and loop sensors sense the
-- presence of vehicles.
-- System provides higher priority for emergency vehicles by switching the traffic lights to Green in
-- the direction of emergency.
-- END Scope
-- START Requirements
-- 1. The traffic lights shall not be green for both the directions at the same time.
-- 2. Pedestrian light shall be Red if the traffic light is Green on the crossing direction.
-- 3. If the traffic light is Green, it shall eventually in the future turn Yellow.
-- 4. If there is an emergency in a particular direction, then the traffic light of that respective direction shall immediately turn Green.
-- 5. If there is an emergency in a particular direction, then the traffic light shall eventually turn Yellow once the emergency vehicle is allowed to pass through the intersection.
-- 6. If the pedestrian light is Green, then it shall eventually turn Red.
-- 7. If there is an emergency then the pedestrian lights shall immediately turn Red.
-- END Requirements
-- Assumptions
-- 1. There are no emergency vehicles at the same time on both the roads.
-- 2. Pedestrian and Drive signal can be green at the same time in the same direction.
-- 3. Traffic and Pedestrian lights will be Green on one of the directions for 30 seconds.
-- END Assumptions
-- START Traffic Light Module
-- The traffic light module which models the traffic lights across two directions NS and EW.
-- Inputs:
-- 1. turnInProgress
-- 2. direction
-- 3. currentAllowedDirection
-- 4. light_timer - Timer which counts down the number of seconds left before the traffic signal changes state.
MODULE trafficLightModule(turnInProgress, direction, currentAllowedDirection, light_timer)
VAR
-- Traffic lights can be Red, Yellow and Green.
current_traffic_light : {Red, Yellow, Green};
ASSIGN
-- Setting initial traffic light to Red.
init(current_traffic_light) := Red;
next(current_traffic_light) :=
case
direction != currentAllowedDirection : current_traffic_light;
current_traffic_light = Red & turnInProgress & light_timer = 0 : Red;
current_traffic_light = Red & !turnInProgress & light_timer = 0 : Green;
current_traffic_light = Green & light_timer = 0 : Yellow;
current_traffic_light = Yellow : Red;
TRUE : current_traffic_light;
esac;
-- END Traffic Light Module
-- START Pedestrian Light Module
-- The pedestrian light module which models the pedestrian crossing signals across two directions, NS and EW.
-- Inputs:
-- 1. trafficLight
-- 2. light_timer
MODULE pedestrianLightModule(trafficLight, light_timer)
VAR
-- Pedestrian lights can be Dont_Walk (Red), Alert, Walk
current_walk_light : {Dont_Walk, Alert, Walk};
ASSIGN
init(current_walk_light) := Dont_Walk;
next(current_walk_light) :=
case
current_walk_light = Dont_Walk & trafficLight.current_traffic_light = Green : Walk;
-- Start alerting if the light countdown timer is less than 10s.
trafficLight.current_traffic_light = Green & light_timer < 10 & light_timer > 0 : Alert;
(light_timer = 0) | (current_walk_light = Alert & trafficLight.current_traffic_light = Red) : Dont_Walk;
TRUE : current_walk_light;
esac;
-- END Pedestrian Light Module
-- START Main Module
MODULE main
VAR
turnInProgress : boolean;
-- Direction in which the traffic lights are allowed to turn Green.
allowedDirection : {NS, EW};
NSDriving : trafficLightModule(turnInProgress, NS, allowedDirection, light_timer);
EWDriving : trafficLightModule(turnInProgress, EW, allowedDirection, light_timer);
NSPedestrian : pedestrianLightModule(NSDriving, light_timer);
EWPedestrian : pedestrianLightModule(EWDriving, light_timer);
light_timer : 0..30;
emergency : {NS,EW,none};
ASSIGN
init(turnInProgress) := FALSE;
init(allowedDirection) := NS;
init(light_timer) := 0;
init(emergency) := none;
next(turnInProgress) :=
case
(NSDriving.current_traffic_light = Red) &
(EWDriving.current_traffic_light = Red) : FALSE;
(NSDriving.current_traffic_light = Green) |
(EWDriving.current_traffic_light = Green) : TRUE;
(NSDriving.current_traffic_light = Yellow) |
(EWDriving.current_traffic_light = Yellow) : TRUE;
TRUE : turnInProgress;
esac;
next(allowedDirection) :=
case
(allowedDirection = NS & !turnInProgress) : EW;
(allowedDirection = EW & !turnInProgress) : NS;
TRUE : allowedDirection;
esac;
next(light_timer) :=
case
(EWDriving.current_traffic_light = Green & emergency=NS)|(NSDriving.current_traffic_light = Green & emergency=EW) : 0;
(light_timer > 0) : light_timer - 1;
(light_timer = 0 & (next(NSDriving.current_traffic_light = Yellow) |
next(EWDriving.current_traffic_light = Yellow))) : 3;
(light_timer = 0 & (next(NSDriving.current_traffic_light = Green) |
next(EWDriving.current_traffic_light = Green))) : 27;
(light_timer = 0 & (next(NSDriving.current_traffic_light = Red) |
next(EWDriving.current_traffic_light = Red))) : 30;
TRUE : light_timer;
esac;
-- END Main Module
-- START CTL Specificaitons
-- Sanity checks: To make sure all the traffic and pedestrian lights shall turn Green eventually.
SPEC EF (NSDriving.current_traffic_light = Green)
SPEC EF (EWDriving.current_traffic_light = Green)
SPEC EF (NSPedestrian.current_walk_light = Walk)
SPEC EF (EWPedestrian.current_walk_light = Walk)
SPEC EF (emergency = NS | emergency = EW | emergency = none)
-- Another sanity check stated differently: Negative property we expect to
-- be false. We can never get into the critical state.
-- SPEC AG !(NSDriving.current_traffic_light = Green)
-- SPEC AG !(EWDriving.current_traffic_light = Green)
-- SPEC AG !(NSPedestrian.current_walk_light = Walk)
-- SPEC AG !(EWPedestrian.current_walk_light = Walk)
-- Safety Properties.
-- 1: If traffic light on NS direction is Green then traffic light on EW shall not be Green. (Ref Req 1)
SPEC AG !(NSDriving.current_traffic_light = Green & EWDriving.current_traffic_light = Green)
-- 2: If traffic light on NS direction is Green then traffic light on EW shall not be Yellow.
SPEC AG !(NSDriving.current_traffic_light = Green & EWDriving.current_traffic_light = Yellow)
-- 3: If traffic light on NS direction is Green then the Pedestrian signal on EW direction shall not be Walk. (Ref Req 2)
SPEC AG !(NSDriving.current_traffic_light = Green & EWPedestrian.current_walk_light = Walk)
-- 4: If traffic light on EW direction is Green then the Pedestrian signal on NS direction shall not be Walk.
SPEC AG !(EWDriving.current_traffic_light = Green & NSPedestrian.current_walk_light = Walk)
-- Liveness Properties.
-- 5: If traffic light on NS direction is Green then it will switch to Yellow in the future. (Ref Req 3)
SPEC AG (NSDriving.current_traffic_light = Green -> AF NSDriving.current_traffic_light = Yellow)
-- 6: If traffic light on EW direction is Green then it will switch to Yellow in the future.
SPEC AG (EWDriving.current_traffic_light = Green -> AF EWDriving.current_traffic_light = Yellow)
-- 7: If traffic light on NS (or EW) direction is Red and there is an emergency in NS (or EW) direction then the traffic light on NS (or EW) direction will switch to Green. (Ref Req 4)
SPEC AG (NSDriving.current_traffic_light = Red & emergency=NS -> AF NSDriving.current_traffic_light = Green)
SPEC AG (EWDriving.current_traffic_light = Red & emergency=EW -> AF EWDriving.current_traffic_light = Green)
-- 8: If traffic light on NS direction is Green and there in an emergency on EW direction then the traffic light on NS direction will turn Yellow. (Ref Req 5)
SPEC AG (NSDriving.current_traffic_light = Green & emergency=EW -> AF NSDriving.current_traffic_light = Yellow)
-- 9: If traffic light on EW direction is Green and there in an emergency on NS direction then the traffic light on EW direction will turn Yellow.
SPEC AG (EWDriving.current_traffic_light = Green & emergency=NS -> AF EWDriving.current_traffic_light = Yellow)
-- 10: If the NS pedestrian light is 'Walk', then it shall eventually turn 'Do not Walk'.
SPEC AG (NSPedestrian.current_walk_light = Walk -> AF NSPedestrian.current_walk_light = Dont_Walk)
-- 11: If the EW pedestrian light is 'Walk', then it shall eventually turn 'Do not Walk'.
SPEC AG (EWPedestrian.current_walk_light = Walk -> AF EWPedestrian.current_walk_light = Dont_Walk)
-- 12: If there is an emergency in NS direction then pedestrian lights in both directions shall immediately turn 'Don't Walk'.
SPEC AG (emergency=NS -> AF(EWPedestrian.current_walk_light = Dont_Walk & NSPedestrian.current_walk_light = Dont_Walk))