
module traffic_light
{
  type state_t = enum { red, green, yellow, pending };

  var state : state_t;
  var count : int;
  input pedestrian : boolean;
  output sigG : boolean;
  output sigY : boolean;
  output sigR : boolean;

  init {
    state = red;
    count = 0;
    sigG = false;
    sigY = false;
    sigR = true;
  }

  next {
    count' = count + 1;

    if (state == red && count == 60) {
      state' = green;
      count' = 0;
    } else if (state == green) {
      if (pedestrian && count >= 60) {
        state' = yellow;
        count' = 0;
      } else {
        state' = pending;
      }
    } else if (state == yellow && count == 5) {
      state' = red;
      count' = 0;
    } else if (state == pending && count == 60) {
      state' = green;
      count' = 0;
    }

    sigG = (state == green);
    sigY = (state == yellow);
    sigR = (state == red || state == pending);
  }
}
