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

*From*: Shuhao Wu <shuhao@xxxxxxxxxxxx>*Date*: Mon, 28 Jun 2021 16:06:54 -0400*References*: <16569f5a-d5fe-01d9-196a-c5e76adaaaed@shuhaowu.com> <7668376b-91f4-1caa-18e2-186585cd4835@lemmster.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.11.0

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

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

Thanks, Shuhao On 2021-06-28 3:33 p.m., Markus Kuppe wrote:

On 6/28/21 12:01 PM, Shuhao Wu wrote:I've been trying to write a temporal property to check in TLC where Iwant to know that some condition F leads to G, and G remain true forthe rest of time. This lead me to using the temporal operators ~> and[] together, in a statement in the form of F ~> []G. I'm likelymisunderstanding one of these operators, as when I used TLC to checkthe following simple spec, the nothing was found to be violated:--fair algorithm leadstoalways variables i = 1; define \* This is the temporal property to check OneLeadsToTwo == (i = 1) ~> [](i = 2) end define; begin step1: i := 2; step2: i := 3; step3: i := 2; end algorithm;My understanding is that (i = 1) ~> (i = 2) would be true for theabove program (which is true in TLC). In the same understanding, (i =1) ~> [](i = 2) would not be true, as the variable i changed from 1 to2, then away from 2, and then back to 2. This means that i = 2 is notalways true following the initial transition from i = 1 to i = 2.What am I missing?Leads-to (P ~> Q) is "syntactic sugar" for [](P => <>Q) (see page 91of Specifying Systems).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/4fc36b77-e942-2301-1beb-6c175725c88e%40shuhaowu.com.

**References**:

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