type state_t = {green, yellow, red, amber};

var L1, L2, L3, L4 : state_t;

init {
    L1 = green;
    L2 = red;
    L3 = green;
    L4 = red;
}

next(L1) = if (L1 == green) then yellow
           else if (L1 == yellow) then red
           else if (L1 == red) then amber
           else green;

next(L2) = if (L2 == green) then yellow
           else if (L2 == yellow) then red
           else if (L2 == red) then amber
           else green;

next(L3) = if (L3 == green) then yellow
           else if (L3 == yellow) then red
           else if (L3 == red) then amber
           else green;

next(L4) = if (L4 == green) then yellow
           else if (L4 == yellow) then red
           else if (L4 == red) then amber
           else green;

procedure control_lights() {
    if (L1 == green && L3 == green) {
        L1 = yellow;
        L3 = yellow;
    } else if (L1 == red && L3 == red && L2 == red) {
        L2 = green;
    } else if (L2 == red && L4 == red) {
        L4 = green;
    }
}

invariant !(L1 == green && L2 == green);
invariant !(L3 == green && L4 == green);

module main {
    init;
    next;
    control_lights();
}

control {
    check;
    print_results;
}
