TLC2 Version 2026.10.20.183001 (rev: d2e1472) Running breadth-first search Model-Checking with fp 0 and seed 1 with 1 worker on 2 cores with 491MB heap and 64MB offheap memory [pid: 2415] (Linux 6.8.0-147-generic amd64, Ubuntu 21.0.12.1 64bit, MSBDiskFPSet, DiskStateQueue). Parsing file /tmp/formal-wiki-model-dlgclmeu/CommittedCompositionMC.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/ConnectedTimingMC.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/AdditionalContracts.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/SpecimenFactsB.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/FormalWikiTrace.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/ItemTimingMC.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/CompositionOracle.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/InspectionTimingMC.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/TraversalTimingMC.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/SchedulerChecksMC.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/AbilityContracts.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/SchedulerOracle.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/OperationContracts.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/InspectionContracts.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/TraversalContracts.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/TurnContracts.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/LocationContracts.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/TypeContracts.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/SchemaContracts.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/BasicContracts.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/SetupContracts.tla Parsing file /tmp/tlc-8591386325428978359/Integers.tla (jar:file:/tmp/formal-wiki-model-dlgclmeu/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /tmp/tlc-8591386325428978359/FiniteSets.tla (jar:file:/tmp/formal-wiki-model-dlgclmeu/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /tmp/tlc-8591386325428978359/Sequences.tla (jar:file:/tmp/formal-wiki-model-dlgclmeu/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /tmp/tlc-8591386325428978359/Naturals.tla (jar:file:/tmp/formal-wiki-model-dlgclmeu/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /tmp/tlc-8591386325428978359/TLCExt.tla (jar:file:/tmp/formal-wiki-model-dlgclmeu/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla) Parsing file /tmp/formal-wiki-model-dlgclmeu/AbilityProceduresMC.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/SpecimenFactsA.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/ObjectRuntime.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/ConnectionFacts.tla Parsing file /tmp/formal-wiki-model-dlgclmeu/SettlementFacts.tla Parsing file /tmp/tlc-8591386325428978359/TLC.tla (jar:file:/tmp/formal-wiki-model-dlgclmeu/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.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 BasicContracts Semantic processing of module SetupContracts Semantic processing of module SchemaContracts Semantic processing of module TypeContracts Semantic processing of module LocationContracts Semantic processing of module TurnContracts Semantic processing of module TraversalContracts Semantic processing of module InspectionContracts Semantic processing of module OperationContracts Semantic processing of module AbilityContracts Semantic processing of module SchedulerOracle Semantic processing of module SchedulerChecksMC Semantic processing of module TraversalTimingMC Semantic processing of module InspectionTimingMC Semantic processing of module ObjectRuntime Semantic processing of module ItemTimingMC Semantic processing of module CompositionOracle Semantic processing of module ConnectedTimingMC Semantic processing of module ConnectionFacts Semantic processing of module SettlementFacts Semantic processing of module AdditionalContracts Semantic processing of module SpecimenFactsB Semantic processing of module TLC Semantic processing of module TLCExt Semantic processing of module FormalWikiTrace Semantic processing of module SpecimenFactsA Semantic processing of module AbilityProceduresMC Semantic processing of module CommittedCompositionMC Linting of module BasicContracts Linting of module SetupContracts Linting of module SchemaContracts Linting of module TypeContracts Linting of module LocationContracts Linting of module TurnContracts Linting of module TraversalContracts Linting of module InspectionContracts Linting of module OperationContracts Linting of module AbilityContracts Linting of module SchedulerOracle Linting of module SchedulerChecksMC Linting of module TraversalTimingMC Linting of module InspectionTimingMC Linting of module ObjectRuntime Linting of module ItemTimingMC Linting of module CompositionOracle Linting of module ConnectedTimingMC Linting of module ConnectionFacts Linting of module SettlementFacts Linting of module AdditionalContracts Linting of module SpecimenFactsB Linting of module TLCExt Linting of module FormalWikiTrace Linting of module SpecimenFactsA Linting of module AbilityProceduresMC Linting of module CommittedCompositionMC Starting... (2026-10-29 03:52:14) Loading TraceEmit operator override from FormalWikiTrace with signature: . Implied-temporal checking--satisfiability problem has 1 branches. Computing initial states... Computed 2 initial states... Finished computing initial states: 4 distinct states generated at 2026-10-29 03:52:15. Progress(265) at 2026-10-29 03:52:17: 1,172 states generated, 1,048 distinct states found, 0 states left on queue. Checking temporal properties for the complete state space with 1048 total distinct states at (2026-10-29 03:52:17) Finished checking temporal properties in 00s at 2026-10-29 03:52:17 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 = 7.0E-15 1172 states generated, 1048 distinct states found, 0 states left on queue. The depth of the complete state graph search is 265. The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 1 and the 95th percentile is 1). Finished in 03s at (2026-10-29 03:52:17)