module ParallelTrafficLights {
  type Bit = integer;

  var nondet_1: boolean;
  var state: integer;
  var red1: Bit;
  var green1: Bit;
  var red2: Bit;
  var green2: Bit;

  init {
    state = 0;
    red1 = 1;
    green1 = 0;
    red2 = 1;
    green2 = 0;

  }
  next {
    havoc nondet_1;
    if (state == 0) {
      if (nondet_1) {
        state' = 1;
        green1' = 1;
        red1' = 0;
      } else {
        state' = 2;
        green2' = 1;
        red2' = 0;
      }
    } else {
      if (state == 1) {
        state' = 0;
        green1' = 0;
        red1' = 1;
      } else {
        if (state == 2) {
          state' = 0;
          green2' = 0;
          red2' = 1;
        }
      }
    }

  }
}
