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 117 and seed -3849947353514573439 with 1 worker on 8 cores with 4002MB heap and 64MB offheap memory [pid: 481141] (Linux 6.12.94+ amd64, Eclipse Adoptium 21.0.13 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/tla-tutorial/pstack-PickWorker/PickWorker.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.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 PickWorker
Starting... (2026-10-30 11:05:01)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-10-30 11:05:01.
Progress(2) at 2026-10-30 11:05:01: 3 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:05:01)
Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
picked = {}

State 2: <Pick line 6, col 12 to line 6, col 39 of module PickWorker>
picked = {w2}

State 3: Stuttering
Finished checking temporal properties in 00s at 2026-10-30 11:05:01
3 states generated, 3 distinct states found, 0 states left on queue.
Finished in 00s at (2026-10-30 11:05:01)
