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

    var current_state : state_t;
    var count : int;
    input pedestrian : boolean;

    output sigR : boolean;
    output sigG : boolean;
    output sigY : boolean;

    init {
        current_state = RED;
        count = 0;
        sigR = true;
        sigG = false;
        sigY = false;
    }

    next {
        match (current_state) {
            RED: {
                if (count == 60) {
                    current_state' = GREEN;
                    count' = 0;
                    sigR' = false;
                    sigG' = true;
                } else {
                    count' = count + 1;
                }
            }
            GREEN: {
                if (pedestrian && count >= 60) {
                    current_state' = PENDING;
                }
                count' = count + 1;
            }
            PENDING: {
                if (count == 60) {
                    current_state' = YELLOW;
                    count' = 0;
                    sigG' = false;
                    sigY' = true;
                } else {
                    count' = count + 1;
                }
            }
            YELLOW: {
                if (count == 5) {
                    current_state' = RED;
                    count' = 0;
                    sigY' = false;
                    sigR' = true;
                } else {
                    count' = count + 1;
                }
            }
        }
    }

    invariant check_single_light_on : (sigR ? 1 : 0) + (sigG ? 1 : 0) + (sigY ? 1 : 0) == 1;
}
