[tlaplus] Trouble with describing the Fairness

[Paulina Maurer <uindc.student.kit@xxxxxxxxx>]

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