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 49 and seed 7887559279028691461 with 1 worker on 6 cores with 1024MB heap and 64MB offheap memory [pid: 525896] (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-14955714711130021206/Naturals.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-14955714711130021206/FiniteSets.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-14955714711130021206/_TLCTrace.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-14955714711130021206/Sequences.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-14955714711130021206/TLC.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-14955714711130021206/TLCExt.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-14955714711130021206/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 11108 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:14: 10,640 states generated (10,640 s/min), 5,554 distinct states found (5,554 ds/min), 4,322 states left on queue.
Error: Invariant NoUnauthorizedExecution 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,a2,"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 |-> a2, 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,a2,"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 |-> a2, 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 |-> a2, 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 |-> a2, 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 |-> a2, 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 |-> a2, 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 |-> a2, 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

14008 states generated, 7074 distinct states found, 5457 states left on queue.
The depth of the complete state graph search is 6.
Finished in 06s at (2026-10-12 03:38:15)
Trace exploration spec path: ./IHVRK_TTrace_1791776289.tla
exit=12