module trafficLightController {
    type lightState = enum { green, yellow, red, amber };

    var L1, L2, L3, L4 : lightState;

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

    next {
        case {
            L1 == green && L3 == green : {
                L1' = yellow;
                L3' = yellow;
            }
            L1 == yellow && L3 == yellow : {
                L1' = red;
                L3' = red;
                L2' = green;
            }
            L1 == red && L3 == red && L2 == green : {
                L2' = yellow;
            }
            L1 == red && L3 == red && L2 == yellow : {
                L2' = red;
                L4' = green;
            }
            L1 == red && L3 == red && L2 == red && L4 == green : {
                L4' = yellow;
            }
            L1 == red && L3 == red && L2 == red && L4 == yellow : {
                L4' = red;
                L1' = green;
                L3' = green;
            }
        }
    }
}
