module main {
    type state_t = enum { RED, GREEN, PENDING, YELLOW };
    var current_state : state_t;
    var count : integer;
    input pedestrian : boolean;
    output sigR, sigY, sigG : boolean;

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

    next {
        count' = (current_state == RED && count < 60) || (current_state == GREEN && (count < 60 || pedestrian)) || (current_state == PENDING && count < 60) || (current_state == YELLOW && count < 5) ? count + 1 : 0;
        current_state' = switch (current_state) {
            RED: count == 60 ? GREEN : RED,
            GREEN: pedestrian && count < 60 ? PENDING : (count >= 60 ? YELLOW : GREEN),
            PENDING: count == 60 ? YELLOW : PENDING,
            YELLOW: count == 5 ? RED : YELLOW
        };
        sigR' = current_state' == RED;
        sigY' = current_state' == YELLOW;
        sigG' = current_state' == GREEN;
    }

    invariant check_min_green_time : (current_state == GREEN) -> count >= 60;
}
