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

[Shuhao Wu <shuhao@xxxxxxxxxxxx>]

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?

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 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/4fc36b77-e942-2301-1beb-6c175725c88e%40shuhaowu.com.