TLC2 Version 2026.08.21.155922 (rev: 9787e65) 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 10 and seed -1487851184821070843 with 12 workers on 12 cores with 3972MB heap and 64MB offheap memory [pid: ] (Linux 7.1.9-arch1-2 amd64, Arch Linux 17.0.20.1 64bit, MSBDiskFPSet, DiskStateQueue). Parsing file ./GovernanceMCV6.tla Parsing file ./GovernanceV6.tla Parsing file ./GovernanceInvariantsV6.tla Parsing file ./GovernanceTransitionsV6.tla Parsing file /_TLCTrace.tla (jar:file:/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla) Parsing file /Naturals.tla (jar:file:/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /FiniteSets.tla (jar:file:/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /Sequences.tla (jar:file:/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /TLC.tla (jar:file:/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) Parsing file /TLCExt.tla (jar:file:/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla) Parsing file /Integers.tla (jar:file:/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 GovernanceV6 Semantic processing of module GovernanceInvariantsV6 Semantic processing of module GovernanceTransitionsV6 Semantic processing of module TLC Semantic processing of module Integers Semantic processing of module TLCExt Semantic processing of module _TLCTrace Semantic processing of module GovernanceMCV6 Linting of module GovernanceV6 Linting of module GovernanceInvariantsV6 Linting of module GovernanceTransitionsV6 Linting of module TLCExt Linting of module _TLCTrace Linting of module GovernanceMCV6 Starting... (2026-09-18 16:24:05) Computing initial states... Finished computing initial states: 1 distinct state generated at 2026-09-18 16:24:05. Progress(11) at 2026-09-18 16:24:08: 258,104 states generated (258,104 s/min), 233,132 distinct states found (233,132 ds/min), 85,539 states left on queue. 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 = 5.4E-10 based on the actual fingerprints: val = 3.9E-9 373933 states generated, 345322 distinct states found, 0 states left on queue. The depth of the complete state graph search is 11. The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 17 and the 95th percentile is 3). Finished in 05s at (2026-09-18 16:24:10)