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: 3128] (Linux 6.8.0-147-generic amd64, Ubuntu 21.0.12.1 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /tmp/formal-wiki-model-io2usaei/TypeOwnershipVariantMC.tla
Parsing file /tmp/formal-wiki-model-io2usaei/TypeChecksMC.tla
Parsing file /tmp/formal-wiki-model-io2usaei/FormalWikiTrace.tla
Parsing file /tmp/formal-wiki-model-io2usaei/TypeContracts.tla
Parsing file /tmp/formal-wiki-model-io2usaei/SchemaContracts.tla
Parsing file /tmp/formal-wiki-model-io2usaei/BasicContracts.tla
Parsing file /tmp/formal-wiki-model-io2usaei/SetupContracts.tla
Parsing file /tmp/tlc-10797295998421446145/Integers.tla (jar:file:/tmp/formal-wiki-model-io2usaei/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-10797295998421446145/FiniteSets.tla (jar:file:/tmp/formal-wiki-model-io2usaei/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-10797295998421446145/Sequences.tla (jar:file:/tmp/formal-wiki-model-io2usaei/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-10797295998421446145/Naturals.tla (jar:file:/tmp/formal-wiki-model-io2usaei/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-10797295998421446145/TLCExt.tla (jar:file:/tmp/formal-wiki-model-io2usaei/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-10797295998421446145/TLC.tla (jar:file:/tmp/formal-wiki-model-io2usaei/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 TypeChecksMC
Semantic processing of module TLC
Semantic processing of module TLCExt
Semantic processing of module FormalWikiTrace
Semantic processing of module TypeOwnershipVariantMC
Linting of module BasicContracts
Linting of module SetupContracts
Linting of module SchemaContracts
Linting of module TypeContracts
Linting of module TypeChecksMC
Linting of module TLCExt
Linting of module FormalWikiTrace
Linting of module TypeOwnershipVariantMC
Starting... (2026-10-29 03:53:30)
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...
Computed 2 initial states...
Error: Invariant Block3Assertions is violated by the initial state:
block3 = 4

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