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

    var current_phase : phase_t;
    var previous_phase : phase_t;

    init {
        current_phase = GREEN;
        previous_phase = YELLOW;
    }

    next {
        previous_phase' = current_phase;
        if (current_phase == RED) {
            assert previous_phase == YELLOW;
        }
        if (current_phase == RED) {
            current_phase' = GREEN;
        } else {
            current_phase' = current_phase + 1;
        }
    }
}
