module main {
    type state_t = enum { RED, GREEN, PENDING, YELLOW };
    var state : state_t;
    var count : integer;
    input pedestrian : boolean;

    var sigR : boolean;
    var sigG : boolean;
    var sigY : boolean;

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

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

    control {
        v = unroll(120);
        check;
        print_results;
    }
}
