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

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



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.