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

    var state1 : state_t;
    var state2 : state_t;

    init {
        state1 = RED;
        state2 = RED;
    }

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