[tlaplus] Does WF and SF statements applicable in distributed Mode?

[Earnshaw <dongluming77@xxxxxxxxx>]

Dear all

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.