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: 2896] (Linux 6.8.0-147-generic amd64, Ubuntu 21.0.12.1 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /tmp/formal-wiki-model-bkz62351/CostClampVariantMC.tla
Parsing file /tmp/formal-wiki-model-bkz62351/DefinitionChecksMC.tla
Parsing file /tmp/formal-wiki-model-bkz62351/FormalWikiTrace.tla
Parsing file /tmp/formal-wiki-model-bkz62351/BasicContracts.tla
Parsing file /tmp/formal-wiki-model-bkz62351/SetupContracts.tla
Parsing file /tmp/tlc-1465594686982313628/Integers.tla (jar:file:/tmp/formal-wiki-model-bkz62351/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-1465594686982313628/FiniteSets.tla (jar:file:/tmp/formal-wiki-model-bkz62351/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-1465594686982313628/Sequences.tla (jar:file:/tmp/formal-wiki-model-bkz62351/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-1465594686982313628/Naturals.tla (jar:file:/tmp/formal-wiki-model-bkz62351/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-1465594686982313628/TLCExt.tla (jar:file:/tmp/formal-wiki-model-bkz62351/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-1465594686982313628/TLC.tla (jar:file:/tmp/formal-wiki-model-bkz62351/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 DefinitionChecksMC
Semantic processing of module TLC
Semantic processing of module TLCExt
Semantic processing of module FormalWikiTrace
Semantic processing of module CostClampVariantMC
Linting of module BasicContracts
Linting of module SetupContracts
Linting of module DefinitionChecksMC
Linting of module TLCExt
Linting of module FormalWikiTrace
Linting of module CostClampVariantMC
Starting... (2026-10-29 03:53:25)
Loading TraceEmit operator override from FormalWikiTrace with signature: <Java Method: public static tlc2.value.impl.Value FormalWikiTrace.TraceEmit(tlc2.value.impl.Value) throws java.lang.Exception>.
Computing initial states...
Error: Invariant AllAssertions is violated by the initial state:
done = TRUE

Finished in 00s at (2026-10-29 03:53:25)