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

    var L1, L2, L3, L4 : state_t;
    var green, yellow, red, amber : state_t;

    init {
        L1 = GREEN;
        L2 = RED;
        L3 = GREEN;
        L4 = RED;
        green = GREEN;
        yellow = RED;
        red = RED;
        amber = RED;
    }

    procedure controller()
        modifies L1;
        modifies L2;
        modifies L3;
        modifies L4;
    {
        if (L1 == GREEN && L3 == GREEN) {
            L1' = YELLOW;
            L3' = YELLOW;
        } else if (L2 == GREEN) {
            L2' = YELLOW;
        } else if (L4 == GREEN) {
            L4' = YELLOW;
        } else {
            L1' = GREEN;
            L3' = GREEN;
            L2' = RED;
            L4' = RED;
        }
    }

    next {
        controller();
    }
}
