module TrafficLightModule {
  var red: boolean;
  var green: boolean;
  var yellow: boolean;
  var previous_yellow: boolean;

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

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

  }
  invariant spec: (!red || previous_yellow);

}
