Liveness and Safety properties fail in SpanTreeRandom.tla about examples

[muenchnerkindl]

How often does this happen for you? I ran TLC perhaps 20 times without getting a counter-example. Also, I tried to understand what part of the property is violated by the counter-example. The post-condition has three disjuncts for every node. In your counter-example, the second disjunct never applies because dist[n] # MaxCardinality for all nodes n. For the root n1 it is clear that the first disjunct holds. For all other nodes, the third disjunct has to hold, and indeed dist[n] \in 1 .. 5 is true for all nodes n2, ..., n6. It's also easy to check that dist[n] = dist[mom[n]] + 1 holds for all these nodes. So mom[n] \in Nbrs(n) has to fail for one of these nodes, which is not easy to check since we don't see the set Edges. However, Next ensures mom'[n] = m for some m \in Nbrs(n) whenever mom[n] is updated, so it's not clear how this could fail.

I am confused.

[ahelwer]

Try running it with -workers k for some k > 2. I had previously made (and closed) this bug report with the tools but maybe I should reopen it? tlaplus/tlaplus#866

Alternatively this seems like maybe multithreaded liveness checking doesn't play well with RandomElement.

[lemmy]

It is reproducible if you rerun TLC with the same seed and fingerprint? Also, is it still reproducible if Safety is reformulated as an invariant?

[ahelwer]

It still does fail if only checking Liveness and not Safety, so I think the []P hypothesis is a red herring. Will check the seed/fingerprint.

[ahelwer]

Got a reproducible failure with -fp 120 -seed -8286054000752913025. This occurs only with 2 or greater workers. It does not occur with only one worker. It also fails with the same fingerprint & seed when only checking Liveness, not Safety.

[lemmy]

Until somebody finds time to root cause, we should ASSUME TLCGet("config").worker = 1 in SpanningTreeRandom.

[ahelwer]

Perhaps, although I think it's better to just have a model not check those liveness properties so we can at least run a safety model on it in the CI.

[lemmy]

Does the CI have to run with multiple workers?

[ahelwer]

It runs quite a bit faster if it does, which I think is important. The CI machines have two cores. We can just have a comment in the model file pointing to the TLC bug. I could add some kind of option in the manifest.json to not use multithreaded workers on a per-model basis but that seems a bit much just to workaround this bug. I'll also just change Safety to be a safety property instead of a liveness property.

[ahelwer]

Oh actually this is quite bad. The Safety property fails as an invariant too, using only safety checking and not liveness, when running with two workers but not one!

With two workers:

[ahelwer@node SpanningTree]$ tlc SpanTreeRandom -fp 120 -seed -8286054000752913025 -workers 2
TLC2 Version 2.18 of Day Month 20?? (rev: a77ff3b)
Running breadth-first search Model-Checking with fp 120 and seed -8286054000752913025 with 2 workers on 8 cores with 3541MB heap and 64MB offheap memory [
pid: 210037] (Linux 6.6.10-arch1-1 amd64, N/A 21 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/SpanningTree/SpanTreeRandom.tla
Parsing file /tmp/tlc-12026332022650467513/Integers.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-12026332022650467513/FiniteSets.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla
)
Parsing file /tmp/tlc-12026332022650467513/TLC.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-12026332022650467513/Naturals.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-12026332022650467513/Sequences.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module SpanTreeRandom
Starting... (2024-01-26 14:26:24)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-01-26 14:26:24.
Error: Invariant Safety is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ mom = (n1 :> n1 @@ n2 :> n2 @@ n3 :> n3 @@ n4 :> n4 @@ n5 :> n5 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 6 @@ n3 :> 6 @@ n4 :> 6 @@ n5 :> 6 @@ n6 :> 6)

State 2: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n3 @@ n4 :> n4 @@ n5 :> n5 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 6 @@ n4 :> 6 @@ n5 :> 6 @@ n6 :> 6)

State 3: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n1 @@ n4 :> n4 @@ n5 :> n5 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 6 @@ n5 :> 6 @@ n6 :> 6)

State 4: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n1 @@ n4 :> n1 @@ n5 :> n5 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1 @@ n5 :> 6 @@ n6 :> 6)

State 5: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n1 @@ n4 :> n1 @@ n5 :> n1 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1 @@ n5 :> 1 @@ n6 :> 6)

State 6: <Next line 61, col 14 to line 64, col 53 of module SpanTreeRandom>
/\ mom = (n1 :> n1 @@ n2 :> n1 @@ n3 :> n1 @@ n4 :> n1 @@ n5 :> n1 @@ n6 :> n1)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 1 @@ n4 :> 1 @@ n5 :> 1 @@ n6 :> 1)

30689 states generated, 10811 distinct states found, 9649 states left on queue.
The depth of the complete state graph search is 6.
Finished in 00s at (2024-01-26 14:26:24)

With 1 worker:

[ahelwer@node SpanningTree]$ tlc SpanTreeRandom -fp 120 -seed -8286054000752913025 -workers 1
TLC2 Version 2.18 of Day Month 20?? (rev: a77ff3b)
Running breadth-first search Model-Checking with fp 120 and seed -8286054000752913025 with 1 worker on 8 cores with 3541MB heap and 64MB offheap memory [p
id: 210322] (Linux 6.6.10-arch1-1 amd64, N/A 21 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/ahelwer/src/tlaplus/examples/specifications/SpanningTree/SpanTreeRandom.tla
Parsing file /tmp/tlc-8521566003764952432/Integers.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-8521566003764952432/FiniteSets.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-8521566003764952432/TLC.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-8521566003764952432/Naturals.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-8521566003764952432/Sequences.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module SpanTreeRandom
Starting... (2024-01-26 14:28:27)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-01-26 14:28:28.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 1.0E-8
  based on the actual fingerprints:  val = 6.8E-11
1915931 states generated, 106664 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 6.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 31 and the 95th percentile is 9).
Finished in 03s at (2024-01-26 14:28:31)

Model:

CONSTANTS
  Nodes = {n1, n2, n3, n4, n5, n6}
  MaxCardinality = 6
  Root = n1
INVARIANTS TypeOK Safety
\* https://github.com/tlaplus/tlaplus/issues/866
\*PROPERTY Liveness
SPECIFICATION Spec
CHECK_DEADLOCK FALSE

[ahelwer]

Closing to limit conversation to TLC bug thread to reduce confusion