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

[tlaplus] Re: Trouble with describing the Fairness

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:

On Monday, November 1, 2021 at 10:04:52 AM UTC-4 uindc.st...@xxxxxxxxx wrote:

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/fa827fba-27c6-4447-8743-660e155dbac0n%40googlegroups.com.