c
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 {
    if (state == RED) {
      count = count + 1;
      if (count == 60) {
        state = GREEN;
        count = 0;
      }
    }
    else if (state == GREEN) {
      if (pedestrian) {
        if (count >= 60) {
          state = YELLOW;
          count = 0;
        } else {
          state = PENDING;
        }
      } else {
        count = count + 1;
      }
    }
    else if (state == PENDING) {
      if (count == 60) {
        state = YELLOW;
        count = 0;
      } else {
        count = count + 1;
      }
    }
    else if (state == YELLOW) {
      count = count + 1;
      if (count == 5) {
        state = RED;
        count = 0;
      }
    }

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

}

module main
{
  var light : traffic_light;

  init {
    light.init;
  }

  next {
    light.next;
  }
}
