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 112 and seed -9209802301750629620 with 1 worker on 10 cores with 16064MB heap and 64MB offheap memory [pid: 236107] (Linux 6.12.88+deb13-amd64 amd64, Debian 21.0.11 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/user/workspace/apps/safeatomic/formal/SafeAtomicLock.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Naturals.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 SafeAtomicLock
Starting... (2026-05-19 06:07:22)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-05-19 06:07:22.
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 = 8.7E-18
28 states generated, 8 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 4.
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-05-19 06:07:22)
