Failing clocks example

[fgmarand]

On the TLA+ page https://www.learntla.com/core/tla.html the basic clock example and the second one work, but I had to stop the non-deterministic example at https://www.learntla.com/_downloads/148bdcbbec03267f2a9e389fc05ff863/hourclock.tla after 250M states found.

Here is a trace of a shorter TLC run:

$ tlc core11_3_clock_with.tla
TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)
Running breadth-first search Model-Checking with fp 109 and seed 5122784111867585607 with 1 worker on 11 cores with 4096MB heap and 64MB offheap memory [pid: 26303] (Mac OS X 15.3.1 aarch64, Homebrew 23.0.2 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /<redacted>/core11_3_clock_with.tla
Parsing file /private/var/folders/_n/tb20d08d6p327llpm9yjvs1w0000gn/T/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module core11_3_clock_with
Starting... (2025-02-11 12:57:54)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2025-02-11 12:57:54.
Progress(3648672) at 2025-02-11 12:57:57: 14,594,664 states generated (14,594,664 s/min), 7,297,282 distinct states found (7,297,282 ds/min), 1 states left on queue.

AFAICT the problem is expected: in that version of the spec, x will be equal to 2 in some traces and, starting from 1, it will never reach 12 but will skip from 11 to 13.

Changing the code from if hr = 12 then to if hr >= 12 then fixes the problem because it restarts on 13 too.