TLC2 Version 2026.03.19.000345 (rev: 30a4862)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 128 and seed -6586072359393911742 with 1 worker on 10 cores with 16384MB heap and 64MB offheap memory [pid: 60337] (Mac OS X 26.5.2 aarch64, Eclipse Adoptium 25 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tmp.QT71S2J9VU/C.tla
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-12900470724610432484/Naturals.tla (jar:file:/private/tmp/claude-501/-Users-eric/9a44bd6f-81c9-4566-8526-5d5e1337a2df/scratchpad/vscode-tlaplus/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-12900470724610432484/_TLCTrace.tla (jar:file:/private/tmp/claude-501/-Users-eric/9a44bd6f-81c9-4566-8526-5d5e1337a2df/scratchpad/vscode-tlaplus/tools/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-12900470724610432484/TLC.tla (jar:file:/private/tmp/claude-501/-Users-eric/9a44bd6f-81c9-4566-8526-5d5e1337a2df/scratchpad/vscode-tlaplus/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-12900470724610432484/TLCExt.tla (jar:file:/private/tmp/claude-501/-Users-eric/9a44bd6f-81c9-4566-8526-5d5e1337a2df/scratchpad/vscode-tlaplus/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-12900470724610432484/Sequences.tla (jar:file:/private/tmp/claude-501/-Users-eric/9a44bd6f-81c9-4566-8526-5d5e1337a2df/scratchpad/vscode-tlaplus/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-12900470724610432484/FiniteSets.tla (jar:file:/private/tmp/claude-501/-Users-eric/9a44bd6f-81c9-4566-8526-5d5e1337a2df/scratchpad/vscode-tlaplus/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-12900470724610432484/Integers.tla (jar:file:/private/tmp/claude-501/-Users-eric/9a44bd6f-81c9-4566-8526-5d5e1337a2df/scratchpad/vscode-tlaplus/tools/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 _TLCTrace
Semantic processing of module C
Linting of module TLCExt
Linting of module _TLCTrace
Linting of module C
Starting... (2026-08-07 13:41:06)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-08-07 13:41:06.
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 = 2.2E-19
The coverage statistics at 2026-08-07 13:41:06 (see https://explain.tlapl.us/module-coverage-statistics for how to interpret the following statistics).
<x line 3, col 10 to line 3, col 10 of module C>: 3
<Init line 4, col 1 to line 4, col 4 of module C>: 1:1
  line 4, col 9 to line 4, col 13 of module C: 1
<Bump line 5, col 1 to line 5, col 4 of module C>: 3:4
  line 5, col 12 to line 5, col 16 of module C: 4
  line 5, col 23 to line 5, col 32 of module C: 3
  line 5, col 39 to line 5, col 44 of module C: 1
<Never line 6, col 1 to line 6, col 5 of module C>: 0:0
  line 6, col 10 to line 6, col 15 of module C: 4
  line 6, col 20 to line 6, col 25 of module C: 0
<Inv line 9, col 1 to line 9, col 3 of module C>
  line 9, col 8 to line 9, col 13 of module C: 4
End of statistics.
5 states generated, 4 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 4.
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 (2026-08-07 13:41:06)
