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: 97] (Linux 6.8.0-147-generic amd64, Ubuntu 21.0.12.1 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /tmp/formal-wiki-model-51o1nbx2/PriorityMC.tla
Parsing file /tmp/formal-wiki-model-51o1nbx2/PriorityProtocol.tla
Parsing file /tmp/formal-wiki-model-51o1nbx2/FormalWikiTrace.tla
Parsing file /tmp/tlc-3235760673819970455/Naturals.tla (jar:file:/tmp/formal-wiki-model-51o1nbx2/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-3235760673819970455/FiniteSets.tla (jar:file:/tmp/formal-wiki-model-51o1nbx2/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-3235760673819970455/Sequences.tla (jar:file:/tmp/formal-wiki-model-51o1nbx2/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-3235760673819970455/TLCExt.tla (jar:file:/tmp/formal-wiki-model-51o1nbx2/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-3235760673819970455/TLC.tla (jar:file:/tmp/formal-wiki-model-51o1nbx2/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-3235760673819970455/Integers.tla (jar:file:/tmp/formal-wiki-model-51o1nbx2/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module PriorityProtocol
Semantic processing of module TLC
Semantic processing of module Integers
Semantic processing of module TLCExt
Semantic processing of module FormalWikiTrace
Semantic processing of module PriorityMC
Linting of module PriorityProtocol
Linting of module TLCExt
Linting of module FormalWikiTrace
Linting of module PriorityMC
Starting... (2026-10-28 22:19:22)
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...
Finished computing initial states: 1 distinct state generated at 2026-10-28 22:19:22.
Error: Invariant ReturnStaysWithActor is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
state = [ phase |-> "NeedCheckpoint",
  nextReceipt |-> 1,
  nextCall |-> 1,
  childComplete |-> FALSE,
  call |-> 0,
  busyActor |-> "None",
  holder |-> "A",
  previousPass |-> FALSE,
  reception |-> 1,
  consecutivePasses |-> 0,
  usedCalls |-> {},
  usedReceipts |-> {},
  lastEvent |-> "Open",
  lastActor |-> "None",
  returnAudit |->
      [ expectedWindow |-> 0,
        actualWindow |-> 0,
        expectedCall |-> 0,
        actualCall |-> 0,
        expectedChild |-> 0,
        actualChild |-> 0,
        expectedTransaction |-> 0,
        actualTransaction |-> 0,
        expectedReception |-> 0,
        actualReception |-> 0 ],
  lastReturn |->
      [ call |-> 0,
        reception |-> 0,
        id |-> 0,
        window |-> 0,
        child |-> 0,
        transaction |-> 0,
        actor |-> "None",
        complete |-> FALSE,
        childrenReturned |-> FALSE,
        drained |-> FALSE ],
  child |-> 0,
  transaction |-> 0,
  checkpoint |-> 0 ]

State 2: <Checkpoint line 9, col 5 to line 10, col 40 of module PriorityMC>
state = [ phase |-> "Ready",
  nextReceipt |-> 2,
  nextCall |-> 1,
  childComplete |-> FALSE,
  call |-> 0,
  busyActor |-> "None",
  holder |-> "A",
  previousPass |-> FALSE,
  reception |-> 1,
  consecutivePasses |-> 0,
  usedCalls |-> {},
  usedReceipts |-> {1},
  lastEvent |-> "Checkpoint",
  lastActor |-> "None",
  returnAudit |->
      [ expectedWindow |-> 0,
        actualWindow |-> 0,
        expectedCall |-> 0,
        actualCall |-> 0,
        expectedChild |-> 0,
        actualChild |-> 0,
        expectedTransaction |-> 0,
        actualTransaction |-> 0,
        expectedReception |-> 0,
        actualReception |-> 0 ],
  lastReturn |->
      [ call |-> 0,
        reception |-> 0,
        id |-> 0,
        window |-> 0,
        child |-> 0,
        transaction |-> 0,
        actor |-> "None",
        complete |-> FALSE,
        childrenReturned |-> FALSE,
        drained |-> FALSE ],
  child |-> 0,
  transaction |-> 0,
  checkpoint |-> 1 ]

State 3: <Act line 13, col 5 to line 14, col 34 of module PriorityMC>
state = [ phase |-> "Resolving",
  nextReceipt |-> 2,
  nextCall |-> 2,
  childComplete |-> FALSE,
  call |-> 1,
  busyActor |-> "A",
  holder |-> "None",
  previousPass |-> FALSE,
  reception |-> 1,
  consecutivePasses |-> 0,
  usedCalls |-> {1},
  usedReceipts |-> {1},
  lastEvent |-> "Begin",
  lastActor |-> "None",
  returnAudit |->
      [ expectedWindow |-> 0,
        actualWindow |-> 0,
        expectedCall |-> 0,
        actualCall |-> 0,
        expectedChild |-> 0,
        actualChild |-> 0,
        expectedTransaction |-> 0,
        actualTransaction |-> 0,
        expectedReception |-> 0,
        actualReception |-> 0 ],
  lastReturn |->
      [ call |-> 0,
        reception |-> 0,
        id |-> 0,
        window |-> 0,
        child |-> 0,
        transaction |-> 0,
        actor |-> "None",
        complete |-> FALSE,
        childrenReturned |-> FALSE,
        drained |-> FALSE ],
  child |-> 0,
  transaction |-> 1,
  checkpoint |-> 1 ]

State 4: <Suspend line 15, col 12 to line 15, col 74 of module PriorityMC>
state = [ phase |-> "Paused",
  nextReceipt |-> 2,
  nextCall |-> 2,
  childComplete |-> FALSE,
  call |-> 1,
  busyActor |-> "A",
  holder |-> "None",
  previousPass |-> FALSE,
  reception |-> 1,
  consecutivePasses |-> 0,
  usedCalls |-> {1},
  usedReceipts |-> {1},
  lastEvent |-> "ChildSuspend",
  lastActor |-> "None",
  returnAudit |->
      [ expectedWindow |-> 0,
        actualWindow |-> 0,
        expectedCall |-> 0,
        actualCall |-> 0,
        expectedChild |-> 0,
        actualChild |-> 0,
        expectedTransaction |-> 0,
        actualTransaction |-> 0,
        expectedReception |-> 0,
        actualReception |-> 0 ],
  lastReturn |->
      [ call |-> 0,
        reception |-> 0,
        id |-> 0,
        window |-> 0,
        child |-> 0,
        transaction |-> 0,
        actor |-> "None",
        complete |-> FALSE,
        childrenReturned |-> FALSE,
        drained |-> FALSE ],
  child |-> 1,
  transaction |-> 1,
  checkpoint |-> 1 ]

State 5: <ChildComplete line 17, col 5 to line 18, col 36 of module PriorityMC>
state = [ phase |-> "Paused",
  nextReceipt |-> 2,
  nextCall |-> 2,
  childComplete |-> TRUE,
  call |-> 1,
  busyActor |-> "A",
  holder |-> "None",
  previousPass |-> FALSE,
  reception |-> 1,
  consecutivePasses |-> 0,
  usedCalls |-> {1},
  usedReceipts |-> {1},
  lastEvent |-> "ChildComplete",
  lastActor |-> "None",
  returnAudit |->
      [ expectedWindow |-> 0,
        actualWindow |-> 0,
        expectedCall |-> 0,
        actualCall |-> 0,
        expectedChild |-> 0,
        actualChild |-> 0,
        expectedTransaction |-> 0,
        actualTransaction |-> 0,
        expectedReception |-> 0,
        actualReception |-> 0 ],
  lastReturn |->
      [ call |-> 0,
        reception |-> 0,
        id |-> 0,
        window |-> 0,
        child |-> 0,
        transaction |-> 0,
        actor |-> "None",
        complete |-> FALSE,
        childrenReturned |-> FALSE,
        drained |-> FALSE ],
  child |-> 1,
  transaction |-> 1,
  checkpoint |-> 1 ]

State 6: <Return line 20, col 5 to line 26, col 35 of module PriorityMC>
state = [ phase |-> "NeedCheckpoint",
  nextReceipt |-> 3,
  nextCall |-> 2,
  childComplete |-> FALSE,
  call |-> 0,
  busyActor |-> "None",
  holder |-> "B",
  previousPass |-> FALSE,
  reception |-> 2,
  consecutivePasses |-> 0,
  usedCalls |-> {1},
  usedReceipts |-> {1, 2},
  lastEvent |-> "Return",
  lastActor |-> "A",
  returnAudit |->
      [ expectedWindow |-> 1,
        actualWindow |-> 1,
        expectedCall |-> 1,
        actualCall |-> 1,
        expectedChild |-> 1,
        actualChild |-> 1,
        expectedTransaction |-> 1,
        actualTransaction |-> 1,
        expectedReception |-> 1,
        actualReception |-> 1 ],
  lastReturn |->
      [ call |-> 1,
        reception |-> 1,
        id |-> 2,
        window |-> 1,
        child |-> 1,
        transaction |-> 1,
        actor |-> "A",
        complete |-> TRUE,
        childrenReturned |-> TRUE,
        drained |-> TRUE ],
  child |-> 0,
  transaction |-> 0,
  checkpoint |-> 0 ]

11 states generated, 11 distinct states found, 1 states left on queue.
The depth of the complete state graph search is 6.
Finished in 00s at (2026-10-28 22:19:22)