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: 391] (Linux 6.8.0-147-generic amd64, Ubuntu 21.0.12.1 64bit, MSBDiskFPSet, DiskStateQueue). Parsing file /tmp/formal-wiki-model-w39bnoc5/AtomicPayment.tla Parsing file /tmp/formal-wiki-model-w39bnoc5/CostAlgebra.tla Parsing file /tmp/formal-wiki-model-w39bnoc5/FormalWikiTrace.tla Parsing file /tmp/tlc-16427848890853399872/Integers.tla (jar:file:/tmp/formal-wiki-model-w39bnoc5/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) Parsing file /tmp/tlc-16427848890853399872/FiniteSets.tla (jar:file:/tmp/formal-wiki-model-w39bnoc5/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) Parsing file /tmp/tlc-16427848890853399872/Sequences.tla (jar:file:/tmp/formal-wiki-model-w39bnoc5/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) Parsing file /tmp/tlc-16427848890853399872/Naturals.tla (jar:file:/tmp/formal-wiki-model-w39bnoc5/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) Parsing file /tmp/tlc-16427848890853399872/TLCExt.tla (jar:file:/tmp/formal-wiki-model-w39bnoc5/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla) Parsing file /tmp/tlc-16427848890853399872/TLC.tla (jar:file:/tmp/formal-wiki-model-w39bnoc5/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 CostAlgebra Semantic processing of module TLC Semantic processing of module TLCExt Semantic processing of module FormalWikiTrace Semantic processing of module AtomicPayment Linting of module CostAlgebra Linting of module TLCExt Linting of module FormalWikiTrace Linting of module AtomicPayment Starting... (2026-10-28 22:19:26) Loading TraceEmit operator override from FormalWikiTrace with signature: . Computing initial states... Finished computing initial states: 1 distinct state generated at 2026-10-28 22:19:26. Error: Invariant UseRecorded is violated. Error: The behavior up to this point is: State 1: /\ pending = FALSE /\ available = 3 /\ paid = FALSE /\ declined = FALSE State 2: /\ pending = TRUE /\ available = 1 /\ paid = FALSE /\ declined = FALSE 2 states generated, 2 distinct states found, 0 states left on queue. The depth of the complete state graph search is 2. Finished in 00s at (2026-10-28 22:19:26)