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

[Shuhao Wu]

Hello all:

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?

Thanks,
Shuhao

[Markus Kuppe]

Leads-to (P ~> Q) is "syntactic sugar" for [](P => <>Q) (see page 91
of Specifying Systems).

M.

[Shuhao Wu]

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

[Markus Kuppe]

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.

[Shuhao Wu]

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