TLC2 Version 2026.09.12.025210 (rev: 867aefb)
Running breadth-first search Model-Checking with fp 26 and seed 2285626784705943520 with 3 workers on 6 cores with 2731MB heap and 64MB offheap memory [pid: 855048] (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-17395211252142132174/Naturals.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-17395211252142132174/FiniteSets.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-17395211252142132174/_TLCTrace.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-17395211252142132174/Sequences.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-17395211252142132174/TLC.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-17395211252142132174/TLCExt.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/tlc-17395211252142132174/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 04:24:33)
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 04:24:33.
Checking 2 branches of temporal properties for the current state space with 57840 total distinct states at (2026-10-12 04:24:36)
Finished checking temporal properties in 00s at 2026-10-12 04:24:37
Progress(7) at 2026-10-12 04:24:37: 76,119 states generated (76,119 s/min), 28,920 distinct states found (28,920 ds/min), 20,869 states left on queue.
Checking 2 branches of temporal properties for the current state space with 2241230 total distinct states at (2026-10-12 04:25:37)
Finished checking temporal properties in 11s at 2026-10-12 04:25:48
Progress(11) at 2026-10-12 04:25:48: 4,277,668 states generated (4,201,549 s/min), 1,120,615 distinct states found (1,091,695 ds/min), 555,211 states left on queue.
Checking 2 branches of temporal properties for the current state space with 4192120 total distinct states at (2026-10-12 04:26:48)
Finished checking temporal properties in 21s at 2026-10-12 04:27:10
Progress(12) at 2026-10-12 04:27:10: 8,173,145 states generated (3,895,477 s/min), 2,096,072 distinct states found (975,457 ds/min), 864,884 states left on queue.
Progress(13) at 2026-10-12 04:28:10: 11,339,677 states generated (3,166,532 s/min), 2,891,065 distinct states found (794,993 ds/min), 1,060,778 states left on queue.
Checking 2 branches of temporal properties for the current state space with 7194942 total distinct states at (2026-10-12 04:29:10)
Finished checking temporal properties in 43s at 2026-10-12 04:29:53
Progress(13) at 2026-10-12 04:29:53: 14,076,253 states generated (2,736,576 s/min), 3,597,471 distinct states found (706,406 ds/min), 1,156,975 states left on queue.
Progress(14) at 2026-10-12 04:30:53: 17,065,047 states generated (2,988,794 s/min), 4,358,950 distinct states found (761,479 ds/min), 1,230,748 states left on queue.
Progress(14) at 2026-10-12 04:31:53: 19,664,934 states generated (2,599,887 s/min), 5,026,187 distinct states found (667,237 ds/min), 1,249,525 states left on queue.
Checking 2 branches of temporal properties for the current state space with 11337316 total distinct states at (2026-10-12 04:32:53)
Finished checking temporal properties in 01min 20s at 2026-10-12 04:34:14
Progress(15) at 2026-10-12 04:34:14: 22,155,613 states generated (2,490,679 s/min), 5,668,661 distinct states found (642,474 ds/min), 1,218,677 states left on queue.
Progress(15) at 2026-10-12 04:35:14: 24,898,541 states generated (2,742,928 s/min), 6,373,663 distinct states found (705,002 ds/min), 1,144,011 states left on queue.
Progress(16) at 2026-10-12 04:36:14: 27,574,253 states generated (2,675,712 s/min), 7,057,131 distinct states found (683,468 ds/min), 979,527 states left on queue.
Progress(17) at 2026-10-12 04:37:14: 30,131,635 states generated (2,557,382 s/min), 7,700,671 distinct states found (643,540 ds/min), 749,247 states left on queue.
Progress(18) at 2026-10-12 04:38:14: 32,641,612 states generated (2,509,977 s/min), 8,312,229 distinct states found (611,558 ds/min), 407,521 states left on queue.
Progress(23) at 2026-10-12 04:39:09: 34,282,716 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 04:39:09)
Finished checking temporal properties in 03min 04s at 2026-10-12 04:42:13
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.2E-5
  based on the actual fingerprints:  val = 2.6E-6
34282716 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 17min 41s at (2026-10-12 04:42:14)