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 88 and seed 2711346771946957776 with 1 worker on 6 cores with 1024MB heap and 64MB offheap memory [pid: 525893] (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-15442621045473289217/Naturals.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-15442621045473289217/FiniteSets.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-15442621045473289217/_TLCTrace.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-15442621045473289217/Sequences.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-15442621045473289217/TLC.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-15442621045473289217/TLCExt.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-15442621045473289217/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.
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: <Receive(r1,a1,"APPROVE",FALSE,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 |-> FALSE] @@
  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 = {}
/\ 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: <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 |-> FALSE] @@
  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 = {}
/\ 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 5: <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 |-> FALSE] @@
  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 = {}
/\ permit = (r1 :> "CONSUMED" @@ r2 :> "NONE")
/\ execDigest = (r1 :> a1 @@ r2 :> "none")
/\ nonce = (r1 :> 1 @@ r2 :> 0)
/\ clock = 0
/\ deadline = (r1 :> 2 @@ r2 :> 0)
/\ verifierUp = TRUE

4384 states generated, 2213 distinct states found, 1842 states left on queue.
The depth of the complete state graph search is 5.
Finished in 04s at (2026-10-12 03:38:13)
Trace exploration spec path: ./IHVRK_TTrace_1791776289.tla
exit=12