Our requirement to do this is like this:

For this individual assignment, you will specify and verify the behavior of a software
system to be installed to control a traffic light system using model checker NuSMV. The
traffic light system services a four-way intersection. For each direction, there is a set of
lights which can give permission to go straight. Each set of lights contains three lights,
which includes a red one, a yellow one, and a green one. The red light indicates that the
cars should stop. The yellow light indicates caution and the red light will be on. The
green light indicates that the cars can proceed. N-S lights control the flow of traffic
arriving at the intersection from the north and the south and the E-W light controls traffic
arriving at the intersection from the east and the west.
The traffic light system works as follows: for the cars from the north and the south, they
are permitted to go straight by lights. Then, the cars are stopped by the lights and the cars
from the west and the east are permitted to go straight.
A green light shall stay green for exactly 30 seconds. Yellow lights will remain yellow
for 3 seconds and should be treated as part of the green light’s time duration. When lights
of one direction turn red, there will be a three second delay before the opposing set of
lights turn green. For example, if the N-S lights turn red, the E-W lights will remain red
for three seconds before turning green.
Generally, the traffic light system works iteratively without alteration. However, if
emergency happens, the system can be controlled manually with an Emergency Stop
control. If the Emergency Stop control is asserted, the normal sequence of lights proceeds
until all the lights are red and the lights are held red until the control is released.
The model should be represented using one module.
The variables are defined as:
LightSet_N_S --The traffic lights for the north and the south.
LightSet_E_W --The traffic lights for the east and the west.
timer --The timer controls the lights.
controller --The controller chooses which direction can proceed.
state --The state of the system.
emergency --The trigger of the emergency for system.
At the very least, you should make sure that the following properties hold in your system:
1. All the lights are reachable if no emergency happens.
2. Two sets of lights cannot be green or yellow at the same time.
3. When lights of one direction turn red, there will be a three second delay before the
opposing set of lights turn green.
4. If the Emergency Stop control is asserted, all the lights will turn red in the future. Bonus: Let’s take consideration of left turn lights.
For each direction, there are two set of lights. One set of lights can give permission to go
straight while the other set of lights can give permission to turn left. The N-S lights work
as follows: for the cars from the north, they are permitted to make left turn or go straight
by lights. Then, the left turn lights turn red but the cars are still permitted to go straight.
The cars from the south are also permitted to go straight. Next, the cars from the north are
stopped by the lights and the cars from the south are permitted to turn left. The E-W
lights work in the same way.
A left-protected light shall stay green for 15 seconds (including the yellow light). Also, if
a left-protected light goes from green to red there will be a three second delay before
oncoming traffic is allowed to proceed.
Deliverables
Every student shall send your two NuSMV models including all of the LTL formulae you
checked via email to Hui Shen on Thursday May 9th
.
Commands for NuSMV model checker:
NuSMV> read_model –i <file> --read model from the file
NuSMV> go --construct the model
NuSMV>check_ltlspec --check LTL properties against the model



need help...!!!