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

[tlaplus] Trouble with describing the Fairness


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/a22e1f73-4964-4c01-ad53-40083913bd27n%40googlegroups.com.