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

*From*: Hillel Wayne <hwa...@xxxxxxxxx>*Date*: Wed, 17 Oct 2018 12:39:29 -0700 (PDT)

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)

====

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:

- TLC is finding a false positive.
- TLC is finding a true positive, but not outputting the correct error trace.
- 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

**Follow-Ups**:**Re: [tlaplus] Possible TLC false positives bug***From:*Markus Kuppe

- Prev by Date:
**[Dr. TLA+ Series] TLA+ specifications of the consistency guarantees provided by Cosmos DB (Murat Demirbas)** - Next by Date:
**Practical TLA+ now out** - Previous by thread:
**[Dr. TLA+ Series] TLA+ specifications of the consistency guarantees provided by Cosmos DB (Murat Demirbas)** - Next by thread:
**Re: [tlaplus] Possible TLC false positives bug** - Index(es):