weird stutter-sensitive feedback
Received from Victor Khomenko:
I've been playing with the online tool, and noticed that for the formula
G( {x} |-> ({x[+]} <>-> ( {Y1[+]} <>=> Y2)) )
the tool says that it's stutter-sensitive, with the witness traces
Accepted word: !Y1 & !Y2 & x; cycle{Y1 & Y2 & x} Rejected word: cycle{!Y1 & !Y2 & x; Y1 & Y2 & x}
However, these two traces are not stutter-equivalent: In both traces, always x=1 and Y1=Y2. So if one ignores x and Y2, the traces become:
Accepted word: !Y1; cycle{Y1} Rejected word: cycle{!Y1; Y1}