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

*From*: 宏黄 <wpkzxp@xxxxxxxxx>*Date*: Mon, 25 Apr 2022 18:06:43 -0700 (PDT)*References*: <f53159ac-2f7c-4c02-9f61-64a2b11e1fean@googlegroups.com> <6210BB10-F79A-4FD2-B9A1-1A2D719181A9@gmail.com>

thanks very much for your answer.

在2022年4月25日星期一 UTC+8 21:26:30<Stephan Merz> 写道：

Hello,

> On 25 Apr 2022, at 04:26, 宏黄 <wpk...@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,

Stephan

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/cf01ea89-f953-4748-b1cf-9b2708c05693n%40googlegroups.com.

**References**:**[tlaplus] Questions about TLA+ formula.***From:*宏黄

**Re: [tlaplus] Questions about TLA+ formula.***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Questions about TLA+ formula.** - Next by Date:
**Re: [tlaplus] How to read a liveness dot dump** - Previous by thread:
**Re: [tlaplus] Questions about TLA+ formula.** - Next by thread:
**Re: [tlaplus] How to read a liveness dot dump** - Index(es):