// Define the main module
module main {
    // Input variable
    input x : boolean;

    // State variable
    var r : boolean;

    // Output variable
    output y : boolean;

    // Initialize the state
    init {
        // Initial state S1 and S2
        (r = false);
    }

    // Define the next state logic
    next {
        r' = x | r;  // r updates to x OR r
        y' = !(x ^ r);  // y is the negation of x XOR r
    }

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

    // Control block for model checking
    control {
        v = unroll(10); // Unroll the transition system 10 steps
        check;
        print_results;
        v.print_cex();
    }
}
