TLA+ alarm clock spec where the Ring action is never enabled. Source: https://emptysqua.re/blog/interactive-tla-plus

AlarmClock.cfg

SPECIFICATION
HC

AlarmClock.tla

------------------------------ MODULE AlarmClock ------------------------------
EXTENDS Integers, Sequences

VARIABLES hr, alarmHr, alarmOn
vars == <<hr, alarmHr, alarmOn>>
HCini == 
    /\ hr \in (1 .. 12)
    /\ alarmHr \in (1..12)
    /\ alarmOn = FALSE 
AdvanceHour ==
    /\ hr' = IF hr # 12 THEN hr + 1 ELSE 1
    /\ UNCHANGED <<alarmHr, alarmOn>>
SetAlarm ==
    /\ alarmHr' \in (1..12)
    \* Oops, forgot to set alarmOn' = TRUE
    \* /\ alarmOn' = TRUE
    \* /\ UNCHANGED <<hr>>
    /\ UNCHANGED <<hr, alarmOn>>
Ring ==
    /\ alarmOn \* Oops, alarmOn is always FALSE
    /\ hr = alarmHr
    /\ alarmOn' = FALSE
    /\ UNCHANGED <<alarmHr, hr>>
HC == HCini /\ [][AdvanceHour \/ SetAlarm \/ Ring]_vars /\ SF_vars(Ring)

=============================================================================