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

[Shuhao Wu <shuhao@xxxxxxxxxxxx>]

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[1]. This has also lead to me that I wasn't correctly applying the 
=> operator in temporal formulas.

[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 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!
>
> 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.