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

Re: [tlaplus] Questions about TLA+ formula.


> On 25 Apr 2022, at 04:26, 宏黄 <wpkzxp@xxxxxxxxx> wrote:
> Hi all.
> I'm reading the TLA+ hyperbook ,And I met some questions.
> In Chapter 17 Temporal Logic Question 17.5
> How to prove []p=>p' is not equivalent to any legal TLA+ formula.

hint: all temporal formulas of TLA+ are insensitive to inserting or removing stuttering steps.

> and  in Chapter 17.4.1 lead to 
> How to understand  F~>false,i think it is nerver true,when F is true,false do not become true

F ~> FALSE asserts that if F ever becomes true, then FALSE must be true eventually. Since the latter is impossible, the formula expresses that F can never become true. You would normally write this as []~F, but the formulation using leads-to is more convenient in the context of reasoning about leads-to properties.

Hope this helps,

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/6210BB10-F79A-4FD2-B9A1-1A2D719181A9%40gmail.com.