Traffic light with NuSMV

NuSMV

• NuSMV 2.6.0 (binary) 
• NuSMV User Manual
• NuSMV Tutorial

Simple traffic light

Note : NuSMV accepts only Mealy Machines !

The system has three actors:

1. tick: this is a discrete input signal that models the (logical discrete) time at which the system evolves. Each time tick occurs, the system evolves.
2. carLight: this is the actual car light seen by the car drivers. It can be red, yellow or green.
3. pedestrianLight: this is the actual pedestrian light seen by the pedestrians willing to cross the street. It can be either red or green.

The traffic light controller is in charge of computing the behavior of the car and pedestrian lights:

• Control of the car light: 

Initially the car light is red.

5 ticks after turning red, the car light turns green.  

It remains green during ten ticks before going to yellow.

It remains yellow during 2 ticks before turning red again.

• Control of the pedestrian light:

The control of the pedestrian light does not directly depend on the time (tick). It must be done in a way that is safe for the pedestrians to cross the street. 

P1 [Safety]: The pedestrians must not be able to cross when the car light is either green or yellow.

P2 [Liveness]: The pedestrians must be able to cross the street at some point: the pedestrian light turns green infinitely often assuming that ticks occur infinitely often.

Traffic Light extension

Instead of having the car light turning back to yellow and red automatically after some ticks, we would like to build a smart light controller that goes back to red only when a pedestrian has pushed a button.

To avoid having the cars being interrupted too frequently, the car light must remain green at least 10 successive ticks, whether there is a pedestrian or not.

1. Modify your model to take that new specification into account
2. Are the safety and liveness properties still verified ?
3. If not what kind of additional assumption do we need ?