module TrafficLightController {
  var L1: enum { green, red, yellow };
  var L2: enum { green, red, yellow };
  var L3: enum { green, red, yellow };
  var L4: enum { green, red, yellow };
  var counter: bv2;

  procedure step()
    modifies counter;
    modifies L3;
    modifies L2;
    modifies L4;
    modifies L1;
  {
    counter = ((counter + 1bv2) % 16bv2);
    if (counter == 0bv2) {
      L1 = green;
      L3 = green;
      L2 = red;
      L4 = red;
    } else {
      if (counter == 3bv2) {
        L1 = yellow;
        L3 = yellow;
      } else {
        if (counter == 4bv2) {
          L1 = red;
          L3 = red;
        }
      }
    }
    if (counter == 4bv2) {
      L2 = green;
    } else {
      if (counter == 8bv2) {
        L2 = yellow;
      } else {
        if (counter == 9bv2) {
          L2 = red;
        }
      }
    }
    if (counter == 9bv2) {
      L4 = green;
    } else {
      if (counter == 13bv2) {
        L4 = yellow;
      } else {
        if (counter == 14bv2) {
          L4 = red;
        }
      }
    }
    if (counter == 15bv2) {
      L1 = red;
      L2 = red;
      L3 = red;
      L4 = red;
    }
  }

  next {
    call step();
  }
}
