Running as unit: run-p3318906-i74525162.scope; invocation ID: 1ecd398b675340d3a019050f723d417f 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 75 and seed -2255992561076427543 with 1 worker on 8 cores with 4096MB heap and 64MB offheap memory [pid: 3318906] (Linux 7.0.10-arch1-1 amd64, Arch Linux 26.0.1 x86_64, MSBDiskFPSet, DiskStateQueue). Parsing file /home/dylon/Workspace/f1r3fly.io/libdictenstein/formal-verification/tla+/LockFreeDurableCheckpoint.tla Parsing file /tmp/Naturals.tla Parsing file /tmp/FiniteSets.tla Parsing file /tmp/TLC.tla Parsing file /tmp/Sequences.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 LockFreeDurableCheckpoint Starting... (2026-06-07 07:44:56) Computing initial states... Finished computing initial states: 1 distinct state generated at 2026-06-07 07:44:56. 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-12 10021 states generated, 2810 distinct states found, 0 states left on queue. The depth of the complete state graph search is 16. The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 3). Finished in 00s at (2026-06-07 07:44:56)