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

*From*: Hillel Wayne <hwa...@xxxxxxxxx>*Date*: Fri, 19 Oct 2018 11:32:31 -0700 (PDT)*References*: <8e248a82-1a42-4b42-9775-dbf992dbe6e7@googlegroups.com> <084220d5-856f-82a2-00d7-d366927619e1@lemmster.de>

On Thursday, 18 October 2018 20:45:20 UTC-5, Markus Alexander Kuppe wrote:

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?

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

Thanks

Markus

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

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

- Prev by Date:
**Re: [tlaplus] Evaluating Complex Constant Expressions in TLA+ Toolbox** - Next by Date:
**TLC crashes with "File too large" IOException while writing MC.st file** - Previous by thread:
**Re: [tlaplus] Possible TLC false positives bug** - Next by thread:
**Practical TLA+ now out** - Index(es):