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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 25 Apr 2022 15:26:25 +0200*References*: <f53159ac-2f7c-4c02-9f61-64a2b11e1fean@googlegroups.com>

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

**Follow-Ups**:

**References**:

- Prev by Date:
**[tlaplus] Questions about TLA+ formula.** - Next by Date:
**Re: [tlaplus] Questions about TLA+ formula.** - Previous by thread:
**[tlaplus] Questions about TLA+ formula.** - Next by thread:
**Re: [tlaplus] Questions about TLA+ formula.** - Index(es):