module main {
  type state_t = enum { RED, GREEN, PENDING, YELLOW };
  var current_state : state_t;
  var count : integer;
  input pedestrian : boolean;
  output sigG, sigY, sigR : boolean;

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

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

    sigG' = (current_state' == GREEN);
    sigY' = (current_state' == YELLOW);
    sigR' = (current_state' == RED);
  }

  control {
    v = simulate 1;
    print_results;
  }
}
