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

    // Initialize the state
    init {
        r = false;
    }

    // Define the transition relation
    next(r) {
        // next_r = x OR r
        r' = x || r;
    }

    // Define the output logic
    next(y) {
        // y = !(x XOR r)
        y' = !(x ^ r);
    }

    // Define the initial states
    init {
        // S1: x = 0, r = 0
        // S2: x = 1, r = 0
        (x = false && r = false) || (x = true && r = false);
    }

    // Define the LTL property
    ltl y_is_set_infinitely_often {
        G F y
    }

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