TLC2 Version 2026.09.12.025210 (rev: 867aefb)
Running breadth-first search Model-Checking with fp 79 and seed 6384382465359547601 with 4 workers on 6 cores with 1820MB heap and 64MB offheap memory [pid: 454399] (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-9576825824497595956/Naturals.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-9576825824497595956/FiniteSets.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-9576825824497595956/_TLCTrace.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-9576825824497595956/Sequences.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-9576825824497595956/TLC.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-9576825824497595956/TLCExt.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-9576825824497595956/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:27:41)
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:27:41.
Checking 2 branches of temporal properties for the current state space with 67892 total distinct states at (2026-10-12 03:27:44)
Finished checking temporal properties in 00s at 2026-10-12 03:27:45
Progress(7) at 2026-10-12 03:27:45: 83,505 states generated (83,505 s/min), 33,946 distinct states found (33,946 ds/min), 24,254 states left on queue.
Checking 2 branches of temporal properties for the current state space with 2296824 total distinct states at (2026-10-12 03:28:45)
Finished checking temporal properties in 11s at 2026-10-12 03:28:56
Progress(11) at 2026-10-12 03:28:56: 3,844,923 states generated (3,761,418 s/min), 1,148,414 distinct states found (1,114,468 ds/min), 564,779 states left on queue.
Checking 2 branches of temporal properties for the current state space with 4232766 total distinct states at (2026-10-12 03:29:56)
Finished checking temporal properties in 23s at 2026-10-12 03:30:20
Progress(12) at 2026-10-12 03:30:20: 7,295,182 states generated (3,450,259 s/min), 2,116,410 distinct states found (967,996 ds/min), 868,954 states left on queue.
Progress(12) at 2026-10-12 03:31:20: 9,432,689 states generated (2,137,507 s/min), 2,715,529 distinct states found (599,119 ds/min), 1,018,541 states left on queue.
Checking 2 branches of temporal properties for the current state space with 6398320 total distinct states at (2026-10-12 03:32:20)
Finished checking temporal properties in 40s at 2026-10-12 03:33:00
Progress(13) at 2026-10-12 03:33:00: 11,179,904 states generated (1,747,215 s/min), 3,199,173 distinct states found (483,644 ds/min), 1,100,290 states left on queue.
Progress(13) at 2026-10-12 03:34:00: 13,242,224 states generated (2,062,320 s/min), 3,774,722 distinct states found (575,549 ds/min), 1,180,376 states left on queue.
Checking 2 branches of temporal properties for the current state space with 8830246 total distinct states at (2026-10-12 03:35:00)
Finished checking temporal properties in 01min 10s at 2026-10-12 03:36:10
Progress(14) at 2026-10-12 03:36:10: 15,573,541 states generated (2,331,317 s/min), 4,415,123 distinct states found (640,401 ds/min), 1,232,421 states left on queue.
Progress(14) at 2026-10-12 03:37:10: 18,050,231 states generated (2,476,690 s/min), 5,097,340 distinct states found (682,217 ds/min), 1,247,815 states left on queue.
Progress(15) at 2026-10-12 03:38:10: 20,968,049 states generated (2,917,818 s/min), 5,884,657 distinct states found (787,317 ds/min), 1,191,462 states left on queue.
Progress(15) at 2026-10-12 03:39:10: 22,584,542 states generated (1,616,493 s/min), 6,322,914 distinct states found (438,257 ds/min), 1,147,623 states left on queue.
Progress(16) at 2026-10-12 03:40:10: 24,427,136 states generated (1,842,594 s/min), 6,809,332 distinct states found (486,418 ds/min), 1,043,135 states left on queue.
Checking 2 branches of temporal properties for the current state space with 14661498 total distinct states at (2026-10-12 03:41:10)
Finished checking temporal properties in 03min 58s at 2026-10-12 03:45:09
Progress(16) at 2026-10-12 03:45:09: 26,404,781 states generated (1,977,645 s/min), 7,330,754 distinct states found (521,422 ds/min), 907,912 states left on queue.
Progress(17) at 2026-10-12 03:46:10: 28,476,361 states generated (2,071,580 s/min), 7,855,569 distinct states found (524,815 ds/min), 680,401 states left on queue.
Progress(18) at 2026-10-12 03:47:10: 30,109,761 states generated (1,633,400 s/min), 8,254,190 distinct states found (398,621 ds/min), 444,499 states left on queue.
Progress(20) at 2026-10-12 03:48:10: 31,670,280 states generated (1,560,519 s/min), 8,602,432 distinct states found (348,242 ds/min), 114,910 states left on queue.
Progress(23) at 2026-10-12 03:48:24: 31,984,860 states generated, 8,656,832 distinct states found, 0 states left on queue.
Checking 2 branches of temporal properties for the complete state space with 17313664 total distinct states at (2026-10-12 03:48:24)
Finished checking temporal properties in 04min 03s at 2026-10-12 03:52:28
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 1.1E-5
  based on the actual fingerprints:  val = 6.2E-7
31984860 states generated, 8656832 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 23.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 12 and the 95th percentile is 3).
Finished in 24min 48s at (2026-10-12 03:52:29)

real	24m49.050s
user	37m56.:00s
sys	4m55.762s