TLC2 Version 2026.09.12.025210 (rev: 867aefb)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 46 and seed 5909712261916727237 with 1 worker on 6 cores with 1024MB heap and 64MB offheap memory [pid: 525898] (Linux 7.0.0-38-generic amd64, Ubuntu 25.0.4.1 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /root/cain-studio-platform/ihvrk/formal/IHVRK.tla
Parsing file /tmp/tlc-5755819240141627888/Naturals.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-5755819240141627888/FiniteSets.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-5755819240141627888/_TLCTrace.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-5755819240141627888/Sequences.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-5755819240141627888/TLC.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-5755819240141627888/TLCExt.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-5755819240141627888/Integers.tla (jar:file:/root/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 TLC
Semantic processing of module Integers
Semantic processing of module TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module IHVRK
Linting of module TLCExt
Linting of module _TLCTrace
Linting of module IHVRK
Starting... (2026-10-12 03:38:10)
Implied-temporal checking--satisfiability problem has 2 branches.
Computing initial states...
Computed 2 initial states...
Finished computing initial states: 4 distinct states generated at 2026-10-12 03:38:11.
Checking 2 branches of temporal properties for the current state space with 6478 total distinct states at (2026-10-12 03:38:14)
Finished checking temporal properties in 00s at 2026-10-12 03:38:14
Progress(5) at 2026-10-12 03:38:15: 5,935 states generated (5,935 s/min), 3,239 distinct states found (3,239 ds/min), 2,561 states left on queue.
Error: Invariant NoDoubleExecution is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ state = (r1 :> "NONE" @@ r2 :> "NONE")
/\ approvedBy = ( r1 :> [r |-> "none", d |-> "none", dec |-> "none", auth |-> FALSE] @@
  r2 :> [r |-> "none", d |-> "none", dec |-> "none", auth |-> FALSE] )
/\ execCount = (r1 :> 0 @@ r2 :> 0)
/\ action = (r1 :> a1 @@ r2 :> a1)
/\ used = {}
/\ permitDigest = (r1 :> "none" @@ r2 :> "none")
/\ sent = {}
/\ permit = (r1 :> "NONE" @@ r2 :> "NONE")
/\ execDigest = (r1 :> "none" @@ r2 :> "none")
/\ nonce = (r1 :> 0 @@ r2 :> 0)
/\ clock = 0
/\ deadline = (r1 :> 0 @@ r2 :> 0)
/\ verifierUp = TRUE

State 2: <Propose(r1) line 71, col 3 to line 77, col 113 of module IHVRK>
/\ state = (r1 :> "AWAITING" @@ r2 :> "NONE")
/\ approvedBy = ( r1 :> [r |-> "none", d |-> "none", dec |-> "none", auth |-> FALSE] @@
  r2 :> [r |-> "none", d |-> "none", dec |-> "none", auth |-> FALSE] )
/\ execCount = (r1 :> 0 @@ r2 :> 0)
/\ action = (r1 :> a1 @@ r2 :> a1)
/\ used = {}
/\ permitDigest = (r1 :> "none" @@ r2 :> "none")
/\ sent = {}
/\ permit = (r1 :> "NONE" @@ r2 :> "NONE")
/\ execDigest = (r1 :> "none" @@ r2 :> "none")
/\ nonce = (r1 :> 1 @@ r2 :> 0)
/\ clock = 0
/\ deadline = (r1 :> 2 @@ r2 :> 0)
/\ verifierUp = TRUE

State 3: <VerifierSend(r1,a1,"APPROVE") line 82, col 3 to line 86, col 39 of module IHVRK>
/\ state = (r1 :> "AWAITING" @@ r2 :> "NONE")
/\ approvedBy = ( r1 :> [r |-> "none", d |-> "none", dec |-> "none", auth |-> FALSE] @@
  r2 :> [r |-> "none", d |-> "none", dec |-> "none", auth |-> FALSE] )
/\ execCount = (r1 :> 0 @@ r2 :> 0)
/\ action = (r1 :> a1 @@ r2 :> a1)
/\ used = {}
/\ permitDigest = (r1 :> "none" @@ r2 :> "none")
/\ sent = {[r |-> r1, d |-> a1, dec |-> "APPROVE"]}
/\ permit = (r1 :> "NONE" @@ r2 :> "NONE")
/\ execDigest = (r1 :> "none" @@ r2 :> "none")
/\ nonce = (r1 :> 1 @@ r2 :> 0)
/\ clock = 0
/\ deadline = (r1 :> 2 @@ r2 :> 0)
/\ verifierUp = TRUE

State 4: <Receive(r1,a1,"APPROVE",TRUE,1) line 91, col 3 to line 103, col 112 of module IHVRK>
/\ state = (r1 :> "AUTHORIZED" @@ r2 :> "NONE")
/\ approvedBy = ( r1 :> [r |-> r1, d |-> a1, dec |-> "APPROVE", auth |-> TRUE] @@
  r2 :> [r |-> "none", d |-> "none", dec |-> "none", auth |-> FALSE] )
/\ execCount = (r1 :> 0 @@ r2 :> 0)
/\ action = (r1 :> a1 @@ r2 :> a1)
/\ used = {1}
/\ permitDigest = (r1 :> "none" @@ r2 :> "none")
/\ sent = {[r |-> r1, d |-> a1, dec |-> "APPROVE"]}
/\ permit = (r1 :> "NONE" @@ r2 :> "NONE")
/\ execDigest = (r1 :> "none" @@ r2 :> "none")
/\ nonce = (r1 :> 1 @@ r2 :> 0)
/\ clock = 0
/\ deadline = (r1 :> 2 @@ r2 :> 0)
/\ verifierUp = TRUE

State 5: <IssuePermit(r1) line 106, col 3 to line 111, col 108 of module IHVRK>
/\ state = (r1 :> "PERMIT_ISSUED" @@ r2 :> "NONE")
/\ approvedBy = ( r1 :> [r |-> r1, d |-> a1, dec |-> "APPROVE", auth |-> TRUE] @@
  r2 :> [r |-> "none", d |-> "none", dec |-> "none", auth |-> FALSE] )
/\ execCount = (r1 :> 0 @@ r2 :> 0)
/\ action = (r1 :> a1 @@ r2 :> a1)
/\ used = {1}
/\ permitDigest = (r1 :> a1 @@ r2 :> "none")
/\ sent = {[r |-> r1, d |-> a1, dec |-> "APPROVE"]}
/\ permit = (r1 :> "ISSUED" @@ r2 :> "NONE")
/\ execDigest = (r1 :> "none" @@ r2 :> "none")
/\ nonce = (r1 :> 1 @@ r2 :> 0)
/\ clock = 0
/\ deadline = (r1 :> 2 @@ r2 :> 0)
/\ verifierUp = TRUE

State 6: <Consume(r1,a1) line 116, col 3 to line 123, col 99 of module IHVRK>
/\ state = (r1 :> "EXECUTING" @@ r2 :> "NONE")
/\ approvedBy = ( r1 :> [r |-> r1, d |-> a1, dec |-> "APPROVE", auth |-> TRUE] @@
  r2 :> [r |-> "none", d |-> "none", dec |-> "none", auth |-> FALSE] )
/\ execCount = (r1 :> 1 @@ r2 :> 0)
/\ action = (r1 :> a1 @@ r2 :> a1)
/\ used = {1}
/\ permitDigest = (r1 :> a1 @@ r2 :> "none")
/\ sent = {[r |-> r1, d |-> a1, dec |-> "APPROVE"]}
/\ permit = (r1 :> "CONSUMED" @@ r2 :> "NONE")
/\ execDigest = (r1 :> a1 @@ r2 :> "none")
/\ nonce = (r1 :> 1 @@ r2 :> 0)
/\ clock = 0
/\ deadline = (r1 :> 2 @@ r2 :> 0)
/\ verifierUp = TRUE

State 7: <Consume(r1,a1) line 116, col 3 to line 123, col 99 of module IHVRK>
/\ state = (r1 :> "EXECUTING" @@ r2 :> "NONE")
/\ approvedBy = ( r1 :> [r |-> r1, d |-> a1, dec |-> "APPROVE", auth |-> TRUE] @@
  r2 :> [r |-> "none", d |-> "none", dec |-> "none", auth |-> FALSE] )
/\ execCount = (r1 :> 2 @@ r2 :> 0)
/\ action = (r1 :> a1 @@ r2 :> a1)
/\ used = {1}
/\ permitDigest = (r1 :> a1 @@ r2 :> "none")
/\ sent = {[r |-> r1, d |-> a1, dec |-> "APPROVE"]}
/\ permit = (r1 :> "CONSUMED" @@ r2 :> "NONE")
/\ execDigest = (r1 :> a1 @@ r2 :> "none")
/\ nonce = (r1 :> 1 @@ r2 :> 0)
/\ clock = 0
/\ deadline = (r1 :> 2 @@ r2 :> 0)
/\ verifierUp = TRUE

59184 states generated, 25308 distinct states found, 18409 states left on queue.
The depth of the complete state graph search is 7.
Finished in 10s at (2026-10-12 03:38:20)
Trace exploration spec path: ./IHVRK_TTrace_1791776289.tla
exit=12