TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)
Running breadth-first search Model-Checking with fp 0 and seed 1 with 1 worker on 14 cores with 245MB heap and 64MB offheap memory [pid: 28215] (Mac OS X 27.0.1 aarch64, Amazon.com Inc. 21.0.11 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /private/var/folders/69/dwg4b48n54l79z0hv04311bw0000gn/T/modeling-e03-y6beq7wu/Commitments.tla
Parsing file /private/var/folders/69/dwg4b48n54l79z0hv04311bw0000gn/T/Naturals.tla
Parsing file /private/var/folders/69/dwg4b48n54l79z0hv04311bw0000gn/T/FiniteSets.tla
Parsing file /private/var/folders/69/dwg4b48n54l79z0hv04311bw0000gn/T/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module Commitments
Starting... (2026-10-03 20:10:53)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-10-03 20:10:53.
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 = 3.8E-18
19 states generated, 14 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 5.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 2 and the 95th percentile is 2).
Finished in 00s at (2026-10-03 20:10:53)
