[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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=
- References: <email@example.com> <firstname.lastname@example.org> <email@example.com> <firstname.lastname@example.org>
- 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. This has also lead to me that I wasn't correctly applying the
=> operator in temporal formulas.
: I think it should be <>((i = 2) /\ <>(i = 3))
Thanks again for all the help,
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!
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.