-------------------------- MODULE PwaUpdate --------------------------
(***************************************************************************)
(* Service-worker update flow for an installed PWA in "prompt" mode.       *)
(*                                                                         *)
(* A server holds a deployed app version, bumped by deploys up to          *)
(* MaxVersion.  Each client runs an `active` service worker version and    *)
(* optionally holds a `waiting` worker (NoSW when absent).  An update      *)
(* check (periodic or on visibilitychange) installs the server version     *)
(* into `waiting` when it is newer than `active` and not already waiting.  *)
(*                                                                         *)
(* A waiting worker lets the UI show an "Update available" prompt.  The    *)
(* user may dismiss it (the waiting worker remains and the prompt can be   *)
(* re-shown) or accept it, which sends skipWaiting: the waiting worker     *)
(* activates, the page reloads, and `active` becomes the previously        *)
(* waiting version.  The key property versus silent auto-update: the       *)
(* active version changes ONLY through explicit user acceptance, modeled   *)
(* by an `accepted` flag that alone gates the activate/reload step.        *)
(***************************************************************************)
EXTENDS Naturals

CONSTANTS
    Clients,      \* set of client (browser/installed-PWA) ids, model values
    MaxVersion    \* bound on the number of deployed versions

NoSW == 0        \* "no waiting worker" (versions are 1..MaxVersion)

VARIABLES
    serverVersion, \* currently deployed app version on the server
    active,        \* active[c]   : SW version client c is running
    waiting,       \* waiting[c]  : installed waiting SW version, or NoSW
    prompt,        \* prompt[c]   : "Update available" prompt is shown
    accepted       \* accepted[c] : user accepted; gates activate/reload

vars == <<serverVersion, active, waiting, prompt, accepted>>

-----------------------------------------------------------------------------

Init ==
    /\ serverVersion = 1
    /\ active   = [c \in Clients |-> 1]
    /\ waiting  = [c \in Clients |-> NoSW]
    /\ prompt   = [c \in Clients |-> FALSE]
    /\ accepted = [c \in Clients |-> FALSE]

\* A deploy bumps the server's app version.
Deploy ==
    /\ serverVersion < MaxVersion
    /\ serverVersion' = serverVersion + 1
    /\ UNCHANGED <<active, waiting, prompt, accepted>>

\* Periodic or visibilitychange-driven update check: a strictly newer
\* server version, not already installed as waiting, installs into
\* `waiting`.  Suppressed once the user has accepted, since skipWaiting
\* is already in flight for the current waiting worker.
CheckForUpdate(c) ==
    /\ ~accepted[c]
    /\ serverVersion > active[c]
    /\ serverVersion # waiting[c]
    /\ waiting' = [waiting EXCEPT ![c] = serverVersion]
    /\ UNCHANGED <<serverVersion, active, prompt, accepted>>

\* The UI surfaces the "Update available" prompt for a waiting worker.
ShowPrompt(c) ==
    /\ waiting[c] # NoSW
    /\ ~prompt[c]
    /\ ~accepted[c]
    /\ prompt' = [prompt EXCEPT ![c] = TRUE]
    /\ UNCHANGED <<serverVersion, active, waiting, accepted>>

\* User dismisses the prompt.  The waiting worker remains installed and
\* the prompt may be re-shown later by ShowPrompt.
Dismiss(c) ==
    /\ prompt[c]
    /\ prompt' = [prompt EXCEPT ![c] = FALSE]
    /\ UNCHANGED <<serverVersion, active, waiting, accepted>>

\* User accepts the update: the prompt closes and skipWaiting is sent.
Accept(c) ==
    /\ prompt[c]
    /\ waiting[c] # NoSW
    /\ accepted' = [accepted EXCEPT ![c] = TRUE]
    /\ prompt'   = [prompt EXCEPT ![c] = FALSE]
    /\ UNCHANGED <<serverVersion, active, waiting>>

\* controllerchange + reload: the waiting worker activates and the page
\* reloads on the new version.  Enabled only after user acceptance.
ActivateReload(c) ==
    /\ accepted[c]
    /\ waiting[c] # NoSW
    /\ active'   = [active EXCEPT ![c] = waiting[c]]
    /\ waiting'  = [waiting EXCEPT ![c] = NoSW]
    /\ accepted' = [accepted EXCEPT ![c] = FALSE]
    /\ UNCHANGED <<serverVersion, prompt>>

Next ==
    \/ Deploy
    \/ \E c \in Clients:
           \/ CheckForUpdate(c)
           \/ ShowPrompt(c)
           \/ Dismiss(c)
           \/ Accept(c)
           \/ ActivateReload(c)

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

-----------------------------------------------------------------------------
(* Invariants *)

TypeOK ==
    /\ serverVersion \in 1..MaxVersion
    /\ active   \in [Clients -> 1..MaxVersion]
    /\ waiting  \in [Clients -> {NoSW} \cup 1..MaxVersion]
    /\ prompt   \in [Clients -> BOOLEAN]
    /\ accepted \in [Clients -> BOOLEAN]

\* (1) A client only ever runs a version the server actually deployed.
ActiveDeployed ==
    \A c \in Clients: active[c] \in 1..serverVersion

\* (2) The prompt is never shown without a waiting worker.
PromptImpliesWaiting ==
    \A c \in Clients: prompt[c] => waiting[c] # NoSW

\* (3) A waiting worker, when present, is a deployed version strictly
\* newer than the one running.
WaitingNewer ==
    \A c \in Clients:
        waiting[c] # NoSW =>
            /\ waiting[c] > active[c]
            /\ waiting[c] <= serverVersion

\* (4) An accepted update always has a waiting worker to activate.
AcceptedImpliesWaiting ==
    \A c \in Clients: accepted[c] => waiting[c] # NoSW

-----------------------------------------------------------------------------
(* Action property: no silent update.  Across every step, a client's
   active version changes only when the user had accepted, and only to
   the previously waiting version, which is then cleared. *)

NoSilentActivation ==
    \A c \in Clients:
        active'[c] # active[c] =>
            /\ accepted[c]
            /\ active'[c] = waiting[c]
            /\ waiting'[c] = NoSW

Safety == [][NoSilentActivation]_vars

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