Hello,
I try to check for deadlocks and other properties in my system.
Since I had problems with stuttering I tried to fixe them with WF/ SF
If using WF for all actions a in the Next statement like:
SPEC = Init /\ [] [Next]_vars /\ WF_vars(a)
The execution stops if it runs in cycles
If I use SF no deadlock is anymore detected.
Is there a way to forbid infinite stuttering in only one state. But still allows iterating between a subset of states?
Thanks a lot