module main {
    input x : boolean;
    output y : boolean;
    var r : boolean;

    next {
        r' = x | r;
        y' = ! (x ^ r);
    }
}

instantiate main;
next;

// LTL property
property always_y {
    always (y)
}
instantiate always_y;
next;
