[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Does WF and SF statements applicable in distributed Mode?
From ToolBox help, we can get that when run in distributed mode, TLC cannot check liveness properties.
For my spec, I just check the invariants for each states instead of liveness properties
for every possible behavior.
But I also need to add Weak Fairness statements for sevral key actions to make sure
they will eventaully always enabled.
TCFSFairSpec == TCFSSpec /\ WF_vars(TCFSClientNext) /\ WF_vars(Server_Down) /\ WF_vars(Server_Reboot)
Because according to TLA+'s grammar, WF and SF statements are also some kind of liveness expressions, so I wonder if they can work properly as in stand-alone mode?
Thanks in advance
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/7de4a963-fd6f-4790-85c0-594973aa8d19n%40googlegroups.com.