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: 28090] (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.
Error: Invariant NoDoubleCommitment is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ sawFree = (R1 :> FALSE @@ R2 :> FALSE)
/\ committed = {}
/\ stage = (R1 :> "new" @@ R2 :> "new")

State 2: <Check line 9, col 13 to line 12, col 34 of module Commitments>
/\ sawFree = (R1 :> TRUE @@ R2 :> FALSE)
/\ committed = {}
/\ stage = (R1 :> "checked" @@ R2 :> "new")

State 3: <Check line 9, col 13 to line 12, col 34 of module Commitments>
/\ sawFree = (R1 :> TRUE @@ R2 :> TRUE)
/\ committed = {}
/\ stage = (R1 :> "checked" @@ R2 :> "checked")

State 4: <Commit line 13, col 14 to line 17, col 33 of module Commitments>
/\ sawFree = (R1 :> TRUE @@ R2 :> TRUE)
/\ committed = {R1}
/\ stage = (R1 :> "done" @@ R2 :> "checked")

State 5: <Commit line 13, col 14 to line 17, col 33 of module Commitments>
/\ sawFree = (R1 :> TRUE @@ R2 :> TRUE)
/\ committed = {R1, R2}
/\ stage = (R1 :> "done" @@ R2 :> "done")

13 states generated, 12 distinct states found, 3 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 1, the maximum 2 and the 95th percentile is 2).
Finished in 00s at (2026-10-03 20:10:53)
