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

  var state1 : state_t;
  var state2 : state_t;

  init {
    state1 = RED;
    state2 = RED;
  }

  transition {
    if (state1 == RED && state2 == RED) {
      // Non-deterministic choice between which light turns green first
      if (nondet()) {
        state1' = GREEN;
        state2' = RED;
      } else {
        state1' = RED;
        state2' = GREEN;
      }
    } else if (state1 == GREEN && state2 == RED) {
      state1' = RED;
      state2' = GREEN;
    } else if (state1 == RED && state2 == GREEN) {
      state1' = GREEN;
      state2' = RED;
    }
  }
}
