How to perform exhaustive state checking in TLA+?

Question

Is it possible to check that each legal state in a model is reached? And if it is possible, how should the property be written?

Consider the module below where a 24 hour clock is modulated. I am able to check that hour is not in a illegal state, i.e. that its between 0 and 23. But if I write a bad Next predicate e.g. hour' = (hour + 1) % 23, not all states is reached but the properties does not catch this error.

----------------------------- MODULE Clock -----------------------------
EXTENDS Naturals
VARIABLE hour

Init ==
    hour \in 0..23

Next == 
    hour' = (hour + 1) % 24

Spec == 
    /\ Init
    /\ [][Next]_hour

\* Properties
hourMinBound == [](hour >= 0)
hourMaxBound == [](hour <= 23)
=============================================================================

Answer 1

Try

ReachesAllStates == \A h \in 0..23: <>(hour = h)

This will check that it reaches each state at least once. To check that it continually reaches every state, you need

KeepsReachingAllStates == \A h \in 0..23: []<>(hour = h)