
module main
{
  type state_t = enum { RED, GREEN, YELLOW, PENDING };

  var state : state_t;
  var count : int;
  input pedestrian : boolean;
  output sigG : boolean; // Green light
  output sigY : boolean; // Yellow light
  output sigR : boolean; // Red light

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

  next {
    count' = count + 1;

    if (state == RED) {
      if (count == 60) {
        state' = GREEN;
        count' = 0;
      }
    } else if (state == GREEN) {
      if (pedestrian && count >= 60) {
        state' = YELLOW;
        count' = 0;
      }
    } else if (state == YELLOW) {
      if (count == 5) {
        state' = RED;
        count' = 0;
      }
    } else if (state == PENDING) {
      if (count == 60) {
        state' = YELLOW;
        count' = 0;
      }
    }

    sigG' = (state == GREEN);
    sigY' = (state == YELLOW);
    sigR' = (state == RED || state == PENDING);
  }
}
