// This is a description of the UCLID5 model for the example in the README.

module main {
    input x : boolean;
    var r : boolean;
    var y : boolean;

    init {
        case
        (r == false && x == false) : { assume false; }
        (r == false && x == true)  : { assume false; }
        esac
    }

    next {
        next_r : r = x | r;
        next_y : y = !(x ^ r);
    }

    control {
        check_liveness("output_y_infinitely_often", G(F(y)));
    }
}
