# Re: [tlaplus] Temporal operator leads to always (F ~> []G): misunderstanding?

• From: Shuhao Wu <shuhao@xxxxxxxxxxxx>
• Date: Tue, 29 Jun 2021 15:00:25 -0400
• Ironport-hdrordr: A9a23:3Usjjq/OJ5Pakca7rGxuk+HUdb1zdoMgy1knxilNoENuHr3hqyn+pplrrCMc1gx6KRcdcKO7SeW9qBLnhNNICOwqUotKMzOW8VdAQLsSmrcKhgeQUREXGIZmpP5dm4YXMqy3MbE4t7e53OGAe+xQh+VviZrY3ds2rE0dBj2D3spbnkRE42SgYztLrVJ9dNoE/fOnj6It1l7QAgVrH7jLdUXpR9Kz3eEj1qiWFSLuYSRXqTVmognI1FeQKWnr4v5xaUI7/V5vyxmMr+Q5jp/T1s1TCSW964YQ1fprcGuL8KoGOCVBsLl3FhzcziKFIL17XayT1QpF0N2H2RIPvJ30uBEwL4BY42/KcgiO0GrQ8jil9Bpr0HPpxV+GjXaLm72GeBsKT+5swbhUdRbU8CMbza5BOK8h5RPWi3KmZimw0xgVLuK4NWAMqmOE5UA6mepWpX1SW4kTZftwqsgw50VICf47bWfH1Lw=
• User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.11.0

Ah that makes perfect sense! I ended expanded the definition according to Specifying Systems (\A n \in Nat...) and I see why I was wrong earlier in this thread. I also spent a bit of time trying to write a temporal formula asserting that i = 2 will lead to i = 3 at least once[1]. This has also lead to me that I wasn't correctly applying the => operator in temporal formulas.

[1]: I think it should be <>((i = 2) /\ <>(i = 3))

Thanks again for all the help,
Shuhao

On 2021-06-28 4:13 p.m., Markus Kuppe wrote:

On 6/28/21 1:06 PM, Shuhao Wu wrote:

Thanks! Looking at the book a bit more, it says that F ~> G is equivalent to saying that exists a behavior following of F that satisfies G. I'm can kind of see that F ~> []G doesn't quite work, but my intuition is still a bit fuzzy.


That said, from Specifying Systems (page 89) I can see that if I want to check that G remains true after the initial transition, I can add a separate temporal property:

TwoRemainsTwo == []((i = 2) => [](i = 2))


I added this to the temporal properties and TLC indeed finds a violation. However, when I combined the two conditions:

(i = 1) ~> (i = 2) /\ []((i = 2) => [](i = 2))


and checked this in TLC, it appears to find no violations again? Am I doing something wrong again?


Careful, operator precedence!

M.



--
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/5c661d62-472b-09ac-4070-dfbb5ff873bf%40shuhaowu.com.



• References: