module main {
    // Define the input, output, and register variables.
    input x : boolean;
    output y : boolean;
    var r : boolean;

    // Initial states
    init {
        // Initialize r to 0
        r = false;
        // Initialize y based on the initial value of x and r
        y = !(x ^ r);
    }

    // Next state logic
    next {
        // Update the register based on the current input and register value
        r' = x | r;
        // Update the output based on the new input and register value
        y' = !(x ^ r');
    }

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

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

    // Control block for model checking
    control {
        check;
        print_results;
    }
}
