
module traffic_light
{
  var red : boolean;
  var green : boolean;
  var yellow : boolean;
  var prev_yellow : boolean;

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

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

  safety_property red_preceded_by_yellow {
    assert !(red && !prev_yellow);
  }
}
