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