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

*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=*References*: <16569f5a-d5fe-01d9-196a-c5e76adaaaed@shuhaowu.com> <7668376b-91f4-1caa-18e2-186585cd4835@lemmster.de> <4fc36b77-e942-2301-1beb-6c175725c88e@shuhaowu.com> <71c5ac02-083e-5afd-d39b-1acd10c27ad3@lemmster.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.11.0

[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 isequivalent to saying that exists a behavior following of F thatsatisfies G. I'm can kind of see that F ~> []G doesn't quite work, butmy intuition is still a bit fuzzy.That said, from Specifying Systems (page 89) I can see that if I wantto check that G remains true after the initial transition, I can add aseparate temporal property:TwoRemainsTwo == []((i = 2) => [](i = 2))I added this to the temporal properties and TLC indeed finds aviolation. 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 Idoing 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**:

- Prev by Date:
**Re: [tlaplus] Temporal operator leads to always (F ~> []G): misunderstanding?** - Next by Date:
**[tlaplus] Flattening a tuple of tuples** - Previous by thread:
**Re: [tlaplus] Temporal operator leads to always (F ~> []G): misunderstanding?** - Next by thread:
**[tlaplus] Flattening a tuple of tuples** - Index(es):