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

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



Thanks a lot, Stephan.     I also want to know about  the latest version TLC's user guide, cause the  relevant command and input and output interface description I got from  chapter 14 of Specifying Systems, which is outdated. Although I can get the source code from Git, but it would cost much times to study. So is there some available reference documents about the latest version?

Best Regards   

在2020年12月9日星期三 UTC+8 下午4:32:19<Stephan Merz> 写道:
TLC is not checking these fairness conditions, since they are part of the specification and therefore assumed. Also, as long as you are only checking invariants it doesn't matter if you add the fairness assumptions to the spec or not as they do not influence whether a state is reachable or not.

Stephan

On 9 Dec 2020, at 09:16, Earnshaw <donglu...@xxxxxxxxx> wrote:

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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7de4a963-fd6f-4790-85c0-594973aa8d19n%40googlegroups.com.

--
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/a397cb78-2470-4802-9136-5c7f4510f9bcn%40googlegroups.com.