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

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

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

    init {
        L1 = GREEN;
        L2 = RED;
        L3 = GREEN;
        L4 = RED;
    }

    next {
        switch_lights();
    }

}
