module main {
    // Define the boolean variables
    var x : boolean;
    var r : boolean;
    var y : boolean;

    // Initial states
    init {
        (x = false && r = false) || (x = true && r = false);
    }

    // Transition relation
    next(r) {
        // Register r updates to 'x OR r'
        r' = x || r;
    }

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

    // LTL property to check if 'y' is set to true infinitely often
    ltl GF_y { G F y }

    // Control block to check properties
    control {
        check;
        print_results;
    }
}
