Trouble with describing the Fairness

[Paulina Maurer]

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

[Andrew Helwer]

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

Andrew

[Paulina Maurer]

Thank you for your answer. Actually I want to check if it has deadlocks with TLC. And to assert some additional properties. All actions are ordinary actions. And yes for the weak fairness is the problem that the system runs in a loop and does not take any action outside of the loop. And I want to avoid this.

[Andrew Helwer]

Fairness assertions don't affect deadlock in any way. If you want to assert that your system cannot run in a loop forever you need to assert strong fairness on an action that breaks out of that loop.

Andrew