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: 3243] (Linux 6.8.0-147-generic amd64, Ubuntu 21.0.12.1 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /tmp/formal-wiki-model-thtmqdb8/TurnHandoffVariantMC.tla
Parsing file /tmp/formal-wiki-model-thtmqdb8/TurnChecksMC.tla
Parsing file /tmp/formal-wiki-model-thtmqdb8/FormalWikiTrace.tla
Parsing file /tmp/formal-wiki-model-thtmqdb8/TurnContracts.tla
Parsing file /tmp/formal-wiki-model-thtmqdb8/LocationContracts.tla
Parsing file /tmp/formal-wiki-model-thtmqdb8/TypeContracts.tla
Parsing file /tmp/formal-wiki-model-thtmqdb8/SchemaContracts.tla
Parsing file /tmp/formal-wiki-model-thtmqdb8/BasicContracts.tla
Parsing file /tmp/formal-wiki-model-thtmqdb8/SetupContracts.tla
Parsing file /tmp/tlc-10745528289690849002/Integers.tla (jar:file:/tmp/formal-wiki-model-thtmqdb8/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-10745528289690849002/FiniteSets.tla (jar:file:/tmp/formal-wiki-model-thtmqdb8/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-10745528289690849002/Sequences.tla (jar:file:/tmp/formal-wiki-model-thtmqdb8/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-10745528289690849002/Naturals.tla (jar:file:/tmp/formal-wiki-model-thtmqdb8/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-10745528289690849002/TLCExt.tla (jar:file:/tmp/formal-wiki-model-thtmqdb8/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-10745528289690849002/TLC.tla (jar:file:/tmp/formal-wiki-model-thtmqdb8/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 TurnChecksMC
Semantic processing of module TLC
Semantic processing of module TLCExt
Semantic processing of module FormalWikiTrace
Semantic processing of module TurnHandoffVariantMC
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 TurnChecksMC
Linting of module TLCExt
Linting of module FormalWikiTrace
Linting of module TurnHandoffVariantMC
Starting... (2026-10-29 03:53:32)
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 Block5Assertions is violated by the initial state:
block5 = 1

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