[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Trouble with describing the Fairness



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

On Monday, November 1, 2021 at 11:11:17 AM UTC-4 uindc.st...@xxxxxxxxx wrote:
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...@xxxxxxxxx schrieb am Montag, 1. November 2021 um 15:30:41 UTC+1:
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

On 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/ 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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0af6d0f5-3e38-45fe-afd1-c9abf42f927an%40googlegroups.com.