module main {
    type color_t = enum { red, green };

    var traffic_light1 : color_t;
    var traffic_light2 : color_t;

    init {
        traffic_light1 = red;
        traffic_light2 = green;
    }

    next {
        if (traffic_light1 == red && traffic_light2 == green) {
            traffic_light1' = green;
            traffic_light2' = red;
        } else if (traffic_light1 == green && traffic_light2 == red) {
            traffic_light1' = red;
            traffic_light2' = green;
        }
    }

    invariant no_deadlock : !(traffic_light1 == red && traffic_light2 == red) && !(traffic_light1 == green && traffic_light2 == green);

    control {
        v = unroll(5);
        check;
        print_results;
    }
}
