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

    var red, green, yellow : phase_t;

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

    next {
        if (red == RED) {
            assert yellow == YELLOW; // Safety property: every red phase is immediately preceded by a yellow phase
        }

        if (red == RED) {
            yellow' = YELLOW;
        } else {
            yellow' = red;
        }

        if (yellow == YELLOW) {
            red' = RED;
        } else {
            red' = yellow;
        }

        if (green == GREEN) {
            yellow' = YELLOW;
        } else {
            yellow' = green;
        }

        if (yellow == YELLOW) {
            green' = GREEN;
        } else {
            green' = yellow;
        }
    }
}
