search

tlaplus / tlaplus

TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
https://lamport.azurewebsites.net/tla/tla.html
MIT License
2.3k stars 192 forks source link

Using RandomElement with multiple workers may result in bogus counterexample #866

Closed ahelwer closed 3 months ago

ahelwer commented 8 months ago

Description

Something useful has come out of the work in https://github.com/tlaplus/Examples/pull/110! In the tlaplus/examples repo, model-checking specifications/SpanningTree/SpanTreeRandom.tla with the below model will sometimes produce a liveness failure and sometimes terminate successfully, if TLC is run in multithreaded mode (-workers k with k > 1; the rate of failure seems to increase as k increases, k = 2 rarely fails):

CONSTANTS
  Nodes = {n1, n2, n3, n4, n5, n6}
  MaxCardinality = 6
  Root = n1
INVARIANT TypeOK
PROPERTIES Liveness Safety
SPECIFICATION Spec
CHECK_DEADLOCK FALSE

This will not occur if -workers k is omitted so TLC runs in single-threaded mode; TLC will always succeed. It's worth noting that the property being checked is of the form []P, so basically a property that could have been checked as a regular invariant but is now being checked by the liveness code (so it's likely this liveness checking code isn't exercised as often as other paths). Also of note is that the model has high variance in runtime, taking between 1 second and 40 seconds to complete.

Expected Behavior

I expected TLC to always return the same result on the same inputs when running exhaustive checking, and in this particular case always return success.

Actual Behavior

TLC sometimes returns success and sometimes outputs the following:

tlc SpanTreeRandom
TLC2 Version 2.18 of Day Month 20?? (rev: a77ff3b)
Running breadth-first search Model-Checking with fp 116 and seed 2350910532224203137 with 8 workers on 8 cores with 3541MB heap and 64MB offheap memory [p
id: 187405] (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-9076410093698049487/Integers.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-9076410093698049487/FiniteSets.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-9076410093698049487/TLC.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-9076410093698049487/Naturals.tla (jar:file:/home/ahelwer/.local/share/java/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-9076410093698049487/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 08:12:58)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-01-26 08:12:58.
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 :> n3 @@ n4 :> n2 @@ n5 :> n5 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 6 @@ n4 :> 2 @@ 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 :> n3 @@ n4 :> n2 @@ n5 :> n1 @@ n6 :> n6)
/\ dist = (n1 :> 0 @@ n2 :> 1 @@ n3 :> 6 @@ n4 :> 2 @@ n5 :> 1 @@ n6 :> 6)

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

21742 states generated, 4063 distinct states found, 2041 states left on queue.
The depth of the complete state graph search is 6.
Finished in 01s at (2024-01-26 08:12:59)

Steps to Reproduce

  1. Clone tlaplus/examples repo
  2. Save above model to specifications/SpanningTree directory as SpanTreeRandom.cfg
  3. cd to specifications/SpanningTree directory
  4. Run java -cp $PATH_TO_TLA2TOOLS_JAR tlc2.TLC -workers 4 SpanTreeRandom

Steps Taken to Fix

N/A

Possible Fix

N/A

Your Environment

I reproduced this on a few different commits:

I also reproduced this on both Linux and macOS.

ahelwer commented 8 months ago

Actually this nondeterminism is almost definitely because the spec is using RandomElement, not nondeterminism in TLC itself! Oops.

ahelwer commented 8 months ago

Reopening here because it turns out this is in fact a TLC bug. It can be reproduced with -fp 120 -seed -8286054000752913025 and -workers k where k >= 2. This is an issue with liveness checking generally and not just formulas of the form []P.

lemmy commented 8 months ago

What happens if you combine -fp 120, -seed -8286054000752913025, -workers 2 with -lncheck final?

ahelwer commented 8 months ago

Should have specified, I'm already using -lncheck final. Here is the expansion of my tlc alias: alias tlc='java -XX:+UseParallelGC tlc2.TLC -noGenerateSpecTE -workers 8 -lncheck final -fpmem 0.65'

ahelwer commented 8 months ago

(Copying from other thread and closing that one to limit confusion)

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

I changed the definition of Safety to remove the [] operator in the .tla file.

FedericoPonzi commented 4 months ago

Moved to https://github.com/tlaplus/tlaplus/issues/971

I'm looking into this one. I found this (still open) issue: https://github.com/tlaplus/tlaplus/issues/790#issuecomment-1425320966 and by checking the "predecessor commit" https://github.com/tlaplus/tlaplus/commit/ca5ad64d836ae157c0101d04752e740d550e7a83 and running against SpanningTreeRandom, the single worker fails right away with the same state trace. I feel like the faulty commit (as mentioned there) worked for the single worker, but it's still having issues with multiple workers, maybe?

As a check, if I run the same spec (Github710a, introduced in the fix) with multiple workers, it still fails. I've tested the matrix: old commit against single and multiple worker and fix commit against single and multiple workers, multiple workers still fails and single worker passes with the fix. I'm still researching, so maybe it's not related at all I could get some hint.

lemmy commented 3 months ago

This (incompleteness) issue is less serious because it involves RandomElement. It would be serious if the issue could be reproduced without involving randomization.

FedericoPonzi commented 3 months ago

Moved to https://github.com/tlaplus/tlaplus/issues/971

Here's a another example without randomization: https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/test-model/Github710a.tla (I first had to copy Github710.cfg to Github710a.cfg)

I'm running it with:

alias tlc="java -cp /home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar -XX:+UseParallelGC tlc2.TLC -noGenerateSpecTE -lncheck final -fpmem 0.65"
tlc -workers 2 -fp 120 -seed -8286054000752913025 Github710a

and sometimes it is able to succeed.

tlc -workers 2 -fp 120 -seed -8286054000752913025 Github710a
TLC2 Version 2.18 of Day Month 20?? (rev: ${git.shortRevision})
Running breadth-first search Model-Checking with fp 120 and seed -8286054000752913025 with 2 workers on 8 cores with 3529MB heap and 64MB offheap memory [pid: 1113596] (Linux 6.5.0-35-generic amd64, Ubuntu 11.0.23 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /tmp/genereto/Github710a.tla
Parsing file /tmp/tlc-12832920167823912074/TLC.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-12832920167823912074/TLCExt.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-12832920167823912074/Naturals.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-12832920167823912074/Sequences.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-12832920167823912074/FiniteSets.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-12832920167823912074/Integers.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Integers
Semantic processing of module TLCExt
Semantic processing of module Github710a
Starting... (2024-06-18 17:24:40)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-06-18 17:24:40.
Error: Assumption line 24, col 9 to line 59, col 55 of module Github710a is false.
Progress(2) at 2024-06-18 17:24:40: 5 states generated, 2 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 2 total distinct states at (2024-06-18 17:24:40)
Finished checking temporal properties in 00s at 2024-06-18 17:24:40
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 = 3.3E-19
5 states generated, 2 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 2.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 1 and the 95th percentile is 1).
Finished in 00s at (2024-06-18 17:24:40)

Not sure why the Assumption line 24 fails. Removing the PostCondition altogether still leads to the same behavor:

tlc -workers 2 -fp 120 -seed -8286054000752913025 Github710a
TLC2 Version 2.18 of Day Month 20?? (rev: ${git.shortRevision})
Running breadth-first search Model-Checking with fp 120 and seed -8286054000752913025 with 2 workers on 8 cores with 3529MB heap and 64MB offheap memory [pid: 1114082] (Linux 6.5.0-35-generic amd64, Ubuntu 11.0.23 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /tmp/genereto/Github710a.tla
Parsing file /tmp/tlc-4654616207224023195/TLC.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-4654616207224023195/TLCExt.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-4654616207224023195/Naturals.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-4654616207224023195/Sequences.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-4654616207224023195/FiniteSets.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-4654616207224023195/Integers.tla (jar:file:/home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Integers
Semantic processing of module TLCExt
Semantic processing of module Github710a
Starting... (2024-06-18 17:25:18)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-06-18 17:25:18.
Progress(2) at 2024-06-18 17:25:18: 5 states generated, 2 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 2 total distinct states at (2024-06-18 17:25:18)
Finished checking temporal properties in 00s at 2024-06-18 17:25:18
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 = 3.3E-19
5 states generated, 2 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 2.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 1 and the 95th percentile is 1).
Finished in 00s at (2024-06-18 17:25:18)

For reference, this is the spec and model:

---- MODULE Github710a ----
EXTENDS TLC, TLCExt
VARIABLE x
vars == <<x>>

Init == x = FALSE

Next == x' \in BOOLEAN 

Spec == 
    /\ Init
    /\ [][Next]_vars
    \* /\ WF_x(Next)

StateConstraint ==
    TRUE

\* This is property to check
AtMostOnce == [](x => [](~x => []~x)) \* G(x => G(~x => G~x))

AtMostOnceEquiv == [](~x \/ [](x \/ []~x)) \* G(~x \/ G(x \/ G~x))

====
SPECIFICATION Spec
PROPERTY AtMostOnce
CONSTRAINT StateConstraint
POSTCONDITION PostCondition

Sidenote: apparently there is no error if Postcondition is not defined like in this case...

lemmy commented 3 months ago

Moved to https://github.com/tlaplus/tlaplus/issues/971

Not sure why the Assumption line 24 fails. Removing the PostCondition altogether still leads to the same behavor: [...] Sidenote: apparently there is no error if Postcondition is not defined like in this case...

The config file has POSTCONDITION PostCondition, but Github710a.tla does not define PostCondition. Can you please confirm that the bug happens without a post condition?

FedericoPonzi commented 3 months ago

Moved to https://github.com/tlaplus/tlaplus/issues/971

Yes, confirmed. To be clear, Github710a.tla has a postcondition defined but I've not pasted in the comment above because I can reproduce the issue wihtout it. With "there is no error", I meant that tlc is not complaining even though I've forgot to remove from the .cfg file the postcondition after removing it from the .tla file. Even after removing the superflous definition in the .cfg file, the bug is still reproducible. Sorry for any confusion!

I'll try to dig into this one a little more, though I feel like it might be too challenging for me to root cause.

lemmy commented 3 months ago

This is a serious issue and has highest priority.

lemmy commented 3 months ago

Root cause: TLC reevaluates RandomElement for each worker during spec processing:

https://github.com/tlaplus/tlaplus/blob/90245f32b67b8928eab46ec92294a9a6936b140d/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/WorkerValue.java#L116-L135

In total, TLC evaluates RandomElement 6*N where N is the number of workers.

lemmy commented 3 months ago

Fixed with https://github.com/tlaplus/tlaplus/pull/973