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

  var state1, state2 : state_t;

  init {
    state1 = RED;
    state2 = RED;
  }

  next {
    case
      state1 == RED && state2 == RED : { state1' = GREEN; state2' = RED; }
      state1 == RED && state2 == GREEN : { state1' = GREEN; state2' = GREEN; }
      state1 == GREEN && state2 == RED : { state1' = RED; state2' = GREEN; }
      state1 == GREEN && state2 == GREEN : { state1' = RED; state2' = GREEN; }
    esac
  }
}
