TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)
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 34 and seed 1229539742674362055 with 1 worker on 8 cores with 4002MB heap and 64MB offheap memory [pid: 480701] (Linux 6.12.94+ amd64, Eclipse Adoptium 21.0.13 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/tla-tutorial/Retry.tla
Semantic processing of module Retry
Starting... (2026-10-30 11:04:43)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-10-30 11:04:44.
Progress(3) at 2026-10-30 11:04:44: 4 states generated, 3 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 3 total distinct states at (2026-10-30 11:04:44)
Finished checking temporal properties in 00s at 2026-10-30 11:04:44
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.6E-19
4 states generated, 3 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 1 and the 95th percentile is 1).
Finished in 00s at (2026-10-30 11:04:44)
