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

    var red, green, yellow : phase_t;

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

    next {
        if (red == RED) {
            assert yellow == YELLOW;
        }
        if (green == GREEN) {
            // Add any specific transitions for the green phase here
        }
        if (yellow == YELLOW) {
            // Add any specific transitions for the yellow phase here
        }
    }
}
