ScreenBlank

---- 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 ====

SPECIFICATION Spec CONSTANTS MaxTime = 5 Timeout = 2 INVARIANTS TypeOK NoBlankWhilePrinting PROPERTY NoBlindPrint CHECK_DEADLOCK FALSE