java
module main {
    type phase_t = enum { RED, GREEN, YELLOW };

    var red, green, yellow : phase_t;

    init {
        red = RED;
        green = GREEN;
        yellow = YELLOW;
    }

    next {
        if (yellow == YELLOW) {
            red' = RED;
            green' = GREEN;
            yellow' = YELLOW;
        } else if (red == RED) {
            // Ensure every red phase is immediately preceded by a yellow phase
            assert yellow == YELLOW;
            red' = RED;
            green' = GREEN;
            yellow' = YELLOW;
        } else if (green == GREEN) {
            red' = RED;
            green' = GREEN;
            yellow' = YELLOW;
        }
    }
}
