TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)
Running breadth-first search Model-Checking with fp 119 and seed -3933734229481669942 with 1 worker on 10 cores with 3641MB heap and 64MB offheap memory [pid: 56938] (Mac OS X 26.4.1 aarch64, Homebrew 17.0.18 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /Users/jfields/Desktop/TerraVault/spec/knox_anchor_chain.tla
Parsing file /private/var/folders/n0/cmxj9dr11g7fkbrbkjcqb4d40000gn/T/Naturals.tla
Parsing file /private/var/folders/n0/cmxj9dr11g7fkbrbkjcqb4d40000gn/T/Sequences.tla
Parsing file /private/var/folders/n0/cmxj9dr11g7fkbrbkjcqb4d40000gn/T/TLC.tla
Parsing file /private/var/folders/n0/cmxj9dr11g7fkbrbkjcqb4d40000gn/T/FiniteSets.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 knox_anchor_chain
Starting... (2026-04-18 16:10:05)
Implied-temporal checking--satisfiability problem has 4 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-04-18 16:10:05.
Progress(9) at 2026-04-18 16:10:05: 1,425 states generated, 633 distinct states found, 0 states left on queue.
Checking 4 branches of temporal properties for the complete state space with 2532 total distinct states at (2026-04-18 16:10:05)
Finished checking temporal properties in 00s at 2026-04-18 16:10:05
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 = 2.7E-14
1425 states generated, 633 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 9.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 4).
Finished in 00s at (2026-04-18 16:10:05)