Write a spec for a clock that cycles through the hours 1 through 12 — Lamport's classic first example from Specifying Systems.
Requirements:
hr holding the current hour.TypeOK: hr is always in 1..12.Init: hr may start at any value in 1..12.Next: advances hr by one, wrapping from 12 back to 1.Spec: Init conjoined with [][Next]_hr (the clock is always allowed to
stutter — that is, to take no step at all — which is why we use [Next]_hr
rather than bare Next).Fill in starter.tla where marked, then click Run Model Checker. TLC
should report no invariant violations. If [][Next]_hr looks unfamiliar,
Chapter 1.3 covers exactly what the box and the subscript are each doing.