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

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

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

  next {
    if (current_state == RED && count == 60) {
      current_state' = GREEN;
      count' = 0;
    } else if (current_state == GREEN && pedestrian && count >= 60) {
      current_state' = YELLOW;
      count' = 0;
    } else if (current_state == GREEN && pedestrian && count < 60) {
      current_state' = PENDING;
      count' = count + 1;
    } else if (current_state == PENDING && count == 60) {
      current_state' = YELLOW;
      count' = 0;
    } else if (current_state == YELLOW && count == 5) {
      current_state' = RED;
      count' = 0;
    } else {
      count' = count + 1;
    }
  }

  next {
    sigR = (current_state == RED);
    sigG = (current_state == GREEN || current_state == PENDING);
    sigY = (current_state == YELLOW);
  }
}
