module TrafficLight {
  var red: boolean;
  var green: boolean;
  var yellow: boolean;

  init {
    red = false;
    green = false;
    yellow = true;

  }
  next {
    if (red) {
      assert yellow;
      red' = false;
      green' = true;
      yellow' = false;
    } else {
      if (green) {
        red' = true;
        green' = false;
        yellow' = false;
      } else {
        if (yellow) {
          red' = false;
          green' = false;
          yellow' = true;
        }
      }
    }

  }
  invariant spec: (red || green);

}
