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

Re: [tlaplus] Questions about TLA+ formula.



 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.