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

  var L1, L2, L3, L4 : state_t;
  var green, yellow, red, amber : state_t;

  init {
    L1 = RED;
    L2 = RED;
    L3 = RED;
    L4 = RED;
    green = GREEN;
    yellow = YELLOW;
    red = RED;
    amber = AMBER;
  }

  procedure controller()
    modifies L1;
    modifies L2;
    modifies L3;
    modifies L4;
  {
    if (L1 == GREEN && L3 == GREEN) {
      L1' = YELLOW;
      L3' = YELLOW;
    } else if (L2 == GREEN) {
      L2' = YELLOW;
    } else if (L4 == GREEN) {
      L4' = YELLOW;
    } else {
      L1' = GREEN;
      L3' = GREEN;
    }
  }

  next {
    controller();
  }
}
