module main {
    // Declare state variables
    var x : boolean;
    var y : boolean;
    var r : boolean;

    // Define the initial states
    init {
        (x = false && r = false) || (x = true && r = false);
    }

    // Define the next state relations
    next(r) {
        r' = x || r; // next value of r is x OR current r
    }

    next(y) {
        y' = !(x ^ r); // y is the negation of (x XOR r)
    }

    next(x) {
        // Non-deterministic update of x, can be true or false
        x' = nondet_bool();
    }

    // LTL property to verify y is set to true infinitely often
    ltl infinitely_often_y {
        G F y
    }

    control {
        // Perform model checking
        check;
        print_results;
    }
}
