I don't think you mean deadlock. Deadlock is when you reach a state where no non-stuttering steps are enabled out of that state. I'm assuming you mean your system runs in a loop and thus will never satisfy some temporal property ⋄P, since P is not true of any state in that loop. This loop constitutes a valid counterexample to ⋄P. What you want to do is assert weak fairness of specific actions and strong fairness of others, so as to selectively disallow counterexamples to the temporal properties you're trying to show. Remember, fairness assertions are the assumptions of your system. You want to assume as little as possible - the more you assume, the less the property you're validating translates to reality (garbage in, garbage out). As a rule of thumb:
- Assert weak fairness for actions that are ordinary steps for your system to take
- Assert strong fairness for successful actions that have a fail/retry alternative, like sending messages over a lossy network - so you would assert strong fairness for successful delivery
- Make no fairness assertion for failure actions - so make no fairness assertion about the failed message delivery step
AndrewOn Monday, November 1, 2021 at 10:04:52 AM UTC-4 uindc.st...@xxxxxxxxx wrote: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/ SFIf 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 cyclesIf 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