[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*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):