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

*From*: Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>*Date*: Thu, 18 Oct 2018 18:45:13 -0700*References*: <8e248a82-1a42-4b42-9775-dbf992dbe6e7@googlegroups.com>

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

**Follow-Ups**:**Re: [tlaplus] Possible TLC false positives bug***From:*Hillel Wayne

**References**:**Possible TLC false positives bug***From:*Hillel Wayne

- Prev by Date:
**Practical TLA+ now out** - Next by Date:
**Evaluating Complex Constant Expressions in TLA+ Toolbox** - Previous by thread:
**Possible TLC false positives bug** - Next by thread:
**Re: [tlaplus] Possible TLC false positives bug** - Index(es):