module TrafficLight {
    type phase_t = enum { RED, GREEN, YELLOW };
    var phase : phase_t;

    init {
        phase = RED;
    }

    next {
        case
            (phase == RED) : { phase' = GREEN; }
            (phase == GREEN) : { phase' = YELLOW; }
            (phase == YELLOW) : { phase' = RED; }
        esac
    }
}

module Main {
    var red, green, yellow : TrafficLight.phase_t;

    instance tl : TrafficLight(phase: (red));

    next {
        next(tl);
    }

    invariant red_preceded_by_yellow : (red == YELLOW);
}
