Possible TLC false positives bug

[Hillel Wayne]

I think this is a TLC bug, but since it involves fairness and somewhat-unusual temporal properties I want to confirm it's actually a bug and not me misunderstanding temporal logic.

---- MODULE main ----

EXTENDS Naturals
VARIABLE x

A == x' = (x + 1) % 3
B == x' \in 0..2

Init == x = 0
Next == (A \/ B)

Spec == Init /\ [][Next]_x /\ WF_x(A)
====

There are three temporal properties I checked: Spec, WF_x(A), and []<><<A>>_x. The first two should be tautologically true, the last should be true for this spec. Each of the three fails with the same error trace:

In the first step, both A and B are true. In the second step, A is false and B is true. If we go back to state one, we have an infinite number of steps where A is true, so all three properties should be satisfied. Replacing  B with x' \in {0, 1} does not cause a spec failure, even though in the existing spec failure x is never 2.

It seems like it could be one of three things:

1. TLC is finding a false positive.
2. TLC is finding a true positive, but not outputting the correct error trace.
3. I'm misunderstanding how fairness works.
   

This should be machine-closed (A is a subaction of Next) but there could be another subtle issue I don't know about.

Hillel

[Markus Kuppe]

On 17.10.18 12:39, Hillel Wayne wrote:
> I /think/ this is a TLC bug, but since it involves fairness and
> somewhat-unusual temporal properties I want to confirm it's /actually/ a

> bug and not me misunderstanding temporal logic.
>
> ---- MODULE main ----
> EXTENDS Naturals
> VARIABLE x
>
> A == x' = (x + 1) % 3
> B == x' \in 0..2
>
> Init == x = 0
> Next == (A \/ B)
>
> Spec == Init /\ [][Next]_x /\ WF_x(A)
> ====
>
> There are three temporal properties I checked: Spec, WF_x(A), and
> []<><<A>>_x. The first two should be tautologically true, the last
> should be true for this spec. Each of the three fails with the same
> error trace:
>
>

> In the first step, both A and B are true. In the second step, A is false
> and B is true. If we go back to state one, we have an infinite number of
> steps where A is true, so all three properties should be satisfied.

> Replacing  B with x' \in {0, 1} does /not/ cause a spec failure, even

> though in the existing spec failure x is never 2.
>
> It seems like it could be one of three things:
>

> 1. TLC is finding a false positive.
> 2. TLC is finding a true positive, but not outputting the correct error
> trace.
> 3. I'm misunderstanding how fairness works.
>
> This /should/ be machine-closed (A is a subaction of Next) but there

> could be another subtle issue I don't know about.
>
> Hillel

Hi Hillel,

can you please open up an issue at GitHub?

Thanks
Markus

[Hillel Wayne]

Done! https://github.com/tlaplus/tlaplus/issues/201

Thanks
Markus