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