TLC2 Version 2026.07.31.184830 (rev: 30cc360)
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 65 and seed 8650960643930312358 with 1 worker on 10 cores with 16384MB heap and 64MB offheap memory [pid: 27061] (Mac OS X 26.5.2 aarch64, Eclipse Adoptium 25 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /private/tmp/lasso_test/Stutter2.tla
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-15305675934526204073/Naturals.tla (jar:file:/private/tmp/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-15305675934526204073/_TLCTrace.tla (jar:file:/private/tmp/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-15305675934526204073/TLC.tla (jar:file:/private/tmp/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-15305675934526204073/TLCExt.tla (jar:file:/private/tmp/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-15305675934526204073/Sequences.tla (jar:file:/private/tmp/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-15305675934526204073/FiniteSets.tla (jar:file:/private/tmp/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /private/var/folders/2q/79m85_bj1qlbkz3sts_bdfl00000gn/T/tlc-15305675934526204073/Integers.tla (jar:file:/private/tmp/tla2tools.jar!/tla2sany/StandardModules/Integers.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 Integers
Semantic processing of module TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module Stutter2
Linting of module TLCExt
Linting of module _TLCTrace
Linting of module Stutter2
Starting... (2026-08-07 20:59:45)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-08-07 20:59:45.
Progress(3) at 2026-08-07 20:59:45: 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-08-07 20:59:45)
Error: Temporal property Live was violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
x = 0

State 2: <Next line 5, col 9 to line 5, col 39 of module Stutter2>
x = 1

State 3: <Next line 5, col 9 to line 5, col 39 of module Stutter2>
x = 2

State 4: Stuttering
Warning: The stuttering counterexample above may be caused by the absence of a fairness constraint in the behavior specification Spec defined at line 6, col 1 to line 6, col 26 of module Stutter2. To rule out such counterexamples, conjoin a suitable fairness constraint to Spec (compare Chapter 8, page 87ff of Specifying Systems at https://lamport.azurewebsites.net/tla/book.html).
Finished checking temporal properties in 00s at 2026-08-07 20:59:45
4 states generated, 3 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.
Finished in 00s at (2026-08-07 20:59:45)
Trace exploration spec path: ./Stutter2_TTrace_1786154385.tla
