---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/HourClock.tla
---
------------------------------- MODULE HourClock -------------------------------
EXTENDS Naturals
VARIABLE hr
HCini == hr \in (1..12)
HCnxt == hr' = IF hr /= 12 THEN hr + 1 ELSE 1
HC == HCini /\ [][HCnxt]_hr
--------------------------------------------------------------------------------
THEOREM HC => []HCini
================================================================================