module TrafficLight {
    var red : boolean;
    var green : boolean;

    init {
        red = true;
        green = false;
    }

    next {
        if (red) {
            red' = false;
            green' = true;
        } else {
            red' = true;
            green' = false;
        }
    }

    invariant mutual_exclusion : (red != green);
}

module main {
    var red1, green1 : boolean;
    var red2, green2 : boolean;

    instance light1 : TrafficLight(red: red1, green: green1);
    instance light2 : TrafficLight(red: red2, green: green2);

    init {
        red1 = true;
        green1 = false;
        red2 = true;
        green2 = false;
    }

    next {
        if (*) {
            next(light1);
        } else {
            next(light2);
        }
    }

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