module TrafficLight {
  var count: integer;
  var pedestrian: boolean;
  var sigG: boolean;
  var sigR: boolean;
  var sigY: boolean;
  var state: integer;

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

  }
  procedure step()
    modifies sigG;
    modifies sigY;
    modifies count;
    modifies state;
    modifies sigR;
  {
    if (state == 0) {
      sigG = false;
      sigY = false;
      sigR = true;
      count = 0;
      if (count < 60) {
        count = (count + 1);
      } else {
        state = 1;
      }
    } else {
      if (state == 1) {
        sigR = false;
        sigY = false;
        sigG = true;
        if (pedestrian) {
          if (count >= 60) {
            state = 2;
          } else {
            state = 3;
          }
        }
      } else {
        if (state == 2) {
          sigG = false;
          sigR = false;
          sigY = true;
          if (count < 5) {
            count = (count + 1);
          } else {
            state = 0;
          }
        } else {
          if (state == 3) {
            sigG = false;
            sigY = false;
            sigR = false;
            if (count < 60) {
              count = (count + 1);
            } else {
              state = 0;
            }
          }
        }
      }
    }
  }

  next {
    call step();
  }
}
