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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 6/28/21 12:01 PM, Shuhao Wu wrote:
> I've been trying to write a temporal property to check in TLC where I 
> want to know that some condition F leads to G, and G remain true for the 
> rest of time. This lead me to using the temporal operators ~> and [] 
> together, in a statement in the form of F ~> []G. I'm likely 
> misunderstanding one of these operators, as when I used TLC to check the 
> 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 the above 
> 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 to 2, then 
> away from 2, and then back to 2. This means that i = 2 is not always 
> 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 91 
of 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/7668376b-91f4-1caa-18e2-186585cd4835%40lemmster.de.