Traffic light with NuSMV

De $1

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 redyellow 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.

A - Functional verification

  1. Propose two Mealy machines to specify the behavior of the car and pedestrian controllers.
  2. Propose two LTL and CTL formulae to specify the two properties P1 and P2.
  3. Implement the two Mealy machines within three modules NuSMV
    1. One module for the car light state machine
    2. One module for the pedestrian light state machine
    3. One main module to put the two other modules together and include the two CTL properties
  4. Run the NuSMV model-checker to verify that the two properties are satisfied

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 ?