A traffic light controller

Now we'll consider a slightly more complex example that uses some additional features of SMV's language. The example is a controller that operates the traffic lights at an intersection where two-way street running north and south intersects a one-way street running east. The goals are to design the controller so that collisions are avoided, and no traffic waits at a red light forever.

The controller has three traffic sensor inputs, N_Sense, S_Sense and E_Sense, indicating when a car is present at the intersection traveling in the north, south and east directions respectively. There are three outputs, N_Go, S_Go and E_Go, indicating that a green light should be given to traffic in each of the three directions.

module main(N_Sense,S_Sense,E_Sense,N_Go,S_Go,E_Go){
  input N_Sense,S_Sense,E_Sense : boolean;
  output N_Go,S_Go,E_Go : boolean;

In addition, there are four internal registers. The register NS_Lock is set when traffic is enabled in the north or south directions, and prevents east-going traffic from being enabled. The three bits N_Req, S_Req, E_Req are used to latch the traffic sensor inputs.

  NS_Lock, N_Req, S_Req, E_Req : boolean;

The registers are initialized as follows:

  init(N_Go) := 0;
  init(S_Go) := 0;
  init(E_Go) := 0;
  init(NS_Lock) := 0;
  init(N_Req) := 0;
  init(S_Req) := 0;
  init(E_Req) := 0;

In modeling the traffic light controller's behavior, we will use two new SMV statements. The case statement is a conditional form. The sequence:

  case{
    cond1 : {block1}
    cond2 : {block2}
    cond3 : {block3}
  }

is equivalent to

  if (cond1) {block1}
  else if (cond2) {block2}
  else if (cond3) {block3}

In addition, we will use the default construct to indicate that certain assignments are to be used as defaults when the given signals are not assigned in the code that follows. In a sequence like this:

  default {block1}
  in {block2}

assignments in block2 take precedence over assignments in block1. SMV enforces a ``single assignment rule'', meaning that only one assignment to a given signal can be active at any time. Thus, if we have more than one assignment to a signal, we must indicate which of the two takes precedence in case both apply.

Now, returning to the traffic controller, if any of the sense bits are true, we set the corresponding request bit:

  default{
    if(N_Sense) next(N_Req) := 1;
    if(S_Sense) next(S_Req) := 1;
    if(E_Sense) next(E_Req) := 1;
  }

The code to operate the north-going light is then as follows:

  in default case{
    N_Req & ~N_Go & ~E_Req : {
      next(NS_Lock) := 1;
      next(N_Go) := 1;
    }
    N_Go & ~N_Sense : {
      next(N_Go) := 0;
      next(N_Req) := 0;
      if(~S_Go) next(NS_Lock) := 0; 
    }
  }

This says that if a north request is latched, and the north light is not green and there is no east request, then switch on the north light and set the lock (in effect, we give priority to the east traffic). If the north light is on, and there is no more north traffic, switch off the light, clear the request, and switch off the lock. Note however, that if the south light is on, we don't switch the lock off. This is to prevent south and east traffic from colliding. The south light code is similar:

  in default case{
    S_Req & ~S_Go & ~E_Req : {
      next(NS_Lock) := 1;
      next(S_Go) := 1;
    }
    S_Go & ~S_Sense : {
      next(S_Go) := 0;
      next(S_Req) := 0;
      if(~N_Go) next(NS_Lock) := 0;
    }
  }

Finally, the east light is switched on whenever there is an east request, and the lock is off. When the east sense input goes off, we switch off the east light and reset the request bit:

  in case{
    E_Req & ~NS_Lock & ~E_Go : next(E_Go) := 1;
    E_Go & ~E_Sense : {
      next(E_Go) := 0;
      next(E_Req) := 0;
    }
  }

There are two kinds of specification we would like to make about the traffic light controller. The first is a ``safety'' specification that say that lights in cross directions are never on at the same time:

  safety: assert G ~(E_Go & (N_Go | S_Go));

The second is a ``liveness'' specification, for each direction, which says that is the traffic sensor is on for a given direction, then the corresponding light is eventually on, thus no traffic waits forever at a read light:

  N_live: assert G (N_Sense -> F N_Go);
  S_live: assert G (S_Sense -> F S_Go);
  E_live: assert G (E_Sense -> F E_Go);

Note, however, that our traffic light controller is designed so that it depends on drivers not waiting forever at a green light. We want to verify the above properties given that this assumption holds. To do this, we write some ``fairness constraints'', as follows:

  N_fair: assert G F ~(N_Sense & N_Go);
  S_fair: assert G F ~(S_Sense & S_Go);
  E_fair: assert G F ~(E_Sense & E_Go);

Each of these assertions states that, always eventually, it is not the case that a car is at a green light. To tell SMV to assume these ``fairness'' properties when proving the ``liveness'' properties, we say:

  using N_fair, S_fair, E_fair prove N_live, S_live, E_live;
  assume E_fair, S_fair, N_fair;
}

Because of the assume statement, the fairness constraints themselves will simply be left unproved. Now, open this file and try to verify the property safety. The result should be ``false'', and in the ``Trace'' panel, you should see a counterexample trace in which the south light goes off exactly at the time when the north light goes on. The result is that the lock bit is cleared. This is because the code for the south light takes precedence over the code for the north light, due to our use of default. With the north light on and the lock cleared, the east light can now go on, violating the safety property.

To fix this problem, let's change the south light code so that it tests to see whether that north light is about to go on before clearing the lock. Here is the revised code for the south light:

  in default case{
    S_Req & ~S_Go & ~E_Req : {
      next(NS_Lock) := 1;
      next(S_Go) := 1;
    }
    S_Go & ~S_Sense : {
      next(S_Go) := 0;
      next(S_Req) := 0;
      if(~(N_Go | N_Req & ~N_Go & ~E_Req)) next(NS_Lock) := 0;
    }
  }

Open this new version and verify the property safety. It should be true. Now try to verify N_live. It should come up false, with a counterexample showing a case where both the north and south lights are going off at exactly the same time. In this case neither the north code nor the south code clears the lock, because each thinks that the other light is still on. As a result, the lock remains on, which prevents an east request from being served. Since the east request takes priority over north and south requests, the controller is deadlocked, and remains in the same state indefinitely (note the ``repeat signs'' on the last state).

To fix this problem, we'll give the north light controller the responsibility to turn off the lock when both lights are going off. Here's the new north light code:

  in default case{
    N_Req & ~N_Go & ~E_Req : {
      next(NS_Lock) := 1;
      next(N_Go) := 1;
    }
    N_Go & ~N_Sense : {
      next(N_Go) := 0;
      next(N_Req) := 0;
      if(~S_Go | ~S_Sense) next(NS_Lock) := 0; 
    }
  }

Open this new version and verify the properties safety, N_live, S_live and E_live. They should all be true. Note that if you try to verify the fairness constraints N_fair, S_fair and E_fair, they will come up false. These are unprovable assumptions that we made in designing the controller. However, if we used the controller module in a larger circuit, we could (and should) verify that the environment we put the controller into actually satisfies these properties. In general, it's best to avoid unproved assumptions if possible, since if any of these assumptions is actually false, all the properties we ``proved'' are invalid.