---- MODULE ScreenBlank ----
(* Backlight-timeout (screen blank) state machine for a device main loop.
   The loop processes input events (Key, PrintButton) and a monotonically
   advancing clock. After Timeout ticks with no input the screen blanks.
   When the screen is off, any input wakes it and is SWALLOWED (it never
   reaches the UI). While Printing the loop is blocked: no events are
   processed and no blanking occurs; completion resets the activity clock. *)
EXTENDS Naturals

CONSTANTS MaxTime,  \* bound on the model clock (keeps the state space finite)
          Timeout   \* ticks of inactivity before the screen blanks

VARIABLES now,          \* model time, 0..MaxTime
          screenOn,     \* backlight state
          lastActivity, \* time of last input (or print completion)
          ui            \* "Idle" or "Printing"

vars == <<now, screenOn, lastActivity, ui>>

TypeOK ==
    /\ now \in 0..MaxTime
    /\ lastActivity \in 0..MaxTime
    /\ lastActivity <= now
    /\ screenOn \in BOOLEAN
    /\ ui \in {"Idle", "Printing"}

Init ==
    /\ now = 0
    /\ screenOn = TRUE
    /\ lastActivity = 0
    /\ ui = "Idle"

\* Time advances (bounded).
Tick ==
    /\ now < MaxTime
    /\ now' = now + 1
    /\ UNCHANGED <<screenOn, lastActivity, ui>>

\* Inactivity blanking. Never fires while Printing (the loop is blocked).
Blank ==
    /\ screenOn
    /\ ui = "Idle"
    /\ now - lastActivity >= Timeout
    /\ screenOn' = FALSE
    /\ UNCHANGED <<now, lastActivity, ui>>

\* A keyboard event. If the screen is off it only wakes it (swallowed);
\* either way the UI state is untouched and the activity clock resets.
Key ==
    /\ ui = "Idle"
    /\ screenOn' = TRUE
    /\ lastActivity' = now
    /\ UNCHANGED <<now, ui>>

\* The print button. Screen off: wake and swallow (no print starts).
\* Screen on: the print begins.
PrintButton ==
    /\ ui = "Idle"
    /\ lastActivity' = now
    /\ IF screenOn
       THEN /\ ui' = "Printing"
            /\ UNCHANGED <<now, screenOn>>
       ELSE /\ screenOn' = TRUE
            /\ UNCHANGED <<now, ui>>

\* Printing completes; activity clock resets so the screen does not blank
\* immediately after a long print.
PrintDone ==
    /\ ui = "Printing"
    /\ ui' = "Idle"
    /\ lastActivity' = now
    /\ UNCHANGED <<now, screenOn>>

Next == Tick \/ Blank \/ Key \/ PrintButton \/ PrintDone

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

\* A print implies the backlight is on (blanking never overlaps printing).
NoBlankWhilePrinting == ui = "Printing" => screenOn

\* A print never starts in the very step that wakes the screen: any step
\* that enters Printing must begin with the screen already on.
NoBlindPrint == [][(ui = "Idle" /\ ui' = "Printing") => screenOn]_vars
====