------------------------ MODULE WebSessionRenewal ------------------------
EXTENDS Naturals, FiniteSets, TLC

\* This protocol covers one WebSession refresh-token generation. Provider refresh
\* is external and cannot observe or honor the store's ownership fence.

CONSTANTS
    Replicas, NoReplica,
    AllowTakeover, AllowAmbiguousRelease, ObserverDestroysOwned

ASSUME
    /\ Replicas # {}
    /\ NoReplica \notin Replicas
    /\ AllowTakeover \in BOOLEAN
    /\ AllowAmbiguousRelease \in BOOLEAN
    /\ ObserverDestroysOwned \in BOOLEAN

Active    == "Active"
Renewed   == "Renewed"
Destroyed == "Destroyed"
SessionStates == {Active, Renewed, Destroyed}

Up   == "Up"
Down == "Down"
ReplicaStates == {Up, Down}

Idle            == "Idle"
Submitted       == "Submitted"
ProviderUnknown == "ProviderUnknown"
Returned        == "Returned"
CommitUnknown   == "CommitUnknown"
Committed       == "Committed"
RequestStates ==
    {Idle, Submitted, ProviderUnknown, Returned, CommitUnknown, Committed}

AccessValid   == "AccessValid"
AccessExpired == "AccessExpired"
AccessStates == {AccessValid, AccessExpired}

NoObservation   == "NoObservation"
UsedCurrent     == "UsedCurrent"
Unavailable     == "Unavailable"
ObservedSignout == "ObservedSignout"
Observations ==
    {NoObservation, UsedCurrent, Unavailable, ObservedSignout}

VARIABLES
    sessionState, owner, replicaState, requestState, committedBy,
    accessState, observation, observerDestroyedOwned

vars ==
    <<sessionState, owner, replicaState, requestState, committedBy,
      accessState, observation, observerDestroyedOwned>>

Init ==
    /\ sessionState = Active
    /\ owner = NoReplica
    /\ replicaState = [r \in Replicas |-> Up]
    /\ requestState = [r \in Replicas |-> Idle]
    /\ committedBy = NoReplica
    /\ accessState = AccessValid
    /\ observation = NoObservation
    /\ observerDestroyedOwned = FALSE

Acquire(r) ==
    /\ sessionState = Active
    /\ owner = NoReplica
    /\ replicaState[r] = Up
    /\ requestState[r] = Idle
    /\ owner' = r
    /\ UNCHANGED
        <<sessionState, replicaState, requestState, committedBy,
          accessState, observation, observerDestroyedOwned>>

Submit(r) ==
    /\ sessionState = Active
    /\ owner = r
    /\ replicaState[r] = Up
    /\ requestState[r] = Idle
    /\ requestState' = [requestState EXCEPT ![r] = Submitted]
    /\ UNCHANGED
        <<sessionState, owner, replicaState, committedBy,
          accessState, observation, observerDestroyedOwned>>

ProviderOutcomeUnknown(r) ==
    /\ requestState[r] = Submitted
    /\ requestState' = [requestState EXCEPT ![r] = ProviderUnknown]
    /\ UNCHANGED
        <<sessionState, owner, replicaState, committedBy,
          accessState, observation, observerDestroyedOwned>>

Return(r) ==
    /\ requestState[r] = Submitted
    /\ replicaState[r] = Up
    /\ requestState' = [requestState EXCEPT ![r] = Returned]
    /\ UNCHANGED
        <<sessionState, owner, replicaState, committedBy,
          accessState, observation, observerDestroyedOwned>>

CommitOutcomeUnknown(r) ==
    /\ sessionState = Active
    /\ owner = r
    /\ requestState[r] = Returned
    /\ requestState' = [requestState EXCEPT ![r] = CommitUnknown]
    /\ UNCHANGED
        <<sessionState, owner, replicaState, committedBy,
          accessState, observation, observerDestroyedOwned>>

Commit(r) ==
    /\ sessionState = Active
    /\ owner = r
    /\ requestState[r] = Returned
    /\ sessionState' = Renewed
    /\ owner' = NoReplica
    /\ requestState' = [requestState EXCEPT ![r] = Committed]
    /\ committedBy' = r
    /\ UNCHANGED
        <<replicaState, accessState, observation, observerDestroyedOwned>>

ExpireOwnership(r) ==
    /\ AllowTakeover
    /\ sessionState = Active
    /\ owner = r
    /\ requestState[r] # Idle
    /\ owner' = NoReplica
    /\ UNCHANGED
        <<sessionState, replicaState, requestState, committedBy,
          accessState, observation, observerDestroyedOwned>>

ReleaseAfterAmbiguousOutcome(r) ==
    /\ AllowAmbiguousRelease
    /\ sessionState = Active
    /\ owner = r
    /\ requestState[r] \in {ProviderUnknown, CommitUnknown}
    /\ owner' = NoReplica
    /\ UNCHANGED
        <<sessionState, replicaState, requestState, committedBy,
          accessState, observation, observerDestroyedOwned>>

Crash(r) ==
    /\ replicaState[r] = Up
    /\ replicaState' = [replicaState EXCEPT ![r] = Down]
    /\ UNCHANGED
        <<sessionState, owner, requestState, committedBy,
          accessState, observation, observerDestroyedOwned>>

DestroyAfterOwnerCrash(r) ==
    /\ sessionState = Active
    /\ owner = r
    /\ replicaState[r] = Down
    /\ sessionState' = Destroyed
    /\ owner' = NoReplica
    /\ UNCHANGED
        <<replicaState, requestState, committedBy,
          accessState, observation, observerDestroyedOwned>>

ConfirmRenewalFailure(r) ==
    /\ sessionState = Active
    /\ owner = r
    /\ requestState[r] \in
        {Submitted, ProviderUnknown, Returned, CommitUnknown}
    /\ sessionState' = Destroyed
    /\ owner' = NoReplica
    /\ UNCHANGED
        <<replicaState, requestState, committedBy,
          accessState, observation, observerDestroyedOwned>>

ExpireAccessToken ==
    /\ sessionState = Active
    /\ accessState = AccessValid
    /\ accessState' = AccessExpired
    /\ UNCHANGED
        <<sessionState, owner, replicaState, requestState, committedBy,
          observation, observerDestroyedOwned>>

ObserveValidToken ==
    /\ sessionState = Active
    /\ accessState = AccessValid
    /\ observation' = UsedCurrent
    /\ UNCHANGED
        <<sessionState, owner, replicaState, requestState, committedBy,
          accessState, observerDestroyedOwned>>

ObserveExpiredOwnedRenewal ==
    /\ sessionState = Active
    /\ accessState = AccessExpired
    /\ owner # NoReplica
    /\ observation' = Unavailable
    /\ UNCHANGED
        <<sessionState, owner, replicaState, requestState, committedBy,
          accessState, observerDestroyedOwned>>

ObserveExpiredAndDestroy ==
    /\ sessionState = Active
    /\ accessState = AccessExpired
    /\ \/ owner = NoReplica
       \/ ObserverDestroysOwned
    /\ sessionState' = Destroyed
    /\ owner' = NoReplica
    /\ observation' = ObservedSignout
    /\ observerDestroyedOwned' = (owner # NoReplica)
    /\ UNCHANGED
        <<replicaState, requestState, committedBy, accessState>>

Logout ==
    /\ sessionState = Active
    /\ sessionState' = Destroyed
    /\ owner' = NoReplica
    /\ UNCHANGED
        <<replicaState, requestState, committedBy,
          accessState, observation, observerDestroyedOwned>>

ExpireSession ==
    /\ sessionState = Active
    /\ sessionState' = Destroyed
    /\ owner' = NoReplica
    /\ UNCHANGED
        <<replicaState, requestState, committedBy,
          accessState, observation, observerDestroyedOwned>>

Next ==
    \/ \E r \in Replicas : Acquire(r)
    \/ \E r \in Replicas : Submit(r)
    \/ \E r \in Replicas : ProviderOutcomeUnknown(r)
    \/ \E r \in Replicas : Return(r)
    \/ \E r \in Replicas : CommitOutcomeUnknown(r)
    \/ \E r \in Replicas : Commit(r)
    \/ \E r \in Replicas : ExpireOwnership(r)
    \/ \E r \in Replicas : ReleaseAfterAmbiguousOutcome(r)
    \/ \E r \in Replicas : Crash(r)
    \/ \E r \in Replicas : DestroyAfterOwnerCrash(r)
    \/ \E r \in Replicas : ConfirmRenewalFailure(r)
    \/ ExpireAccessToken
    \/ ObserveValidToken
    \/ ObserveExpiredOwnedRenewal
    \/ ObserveExpiredAndDestroy
    \/ Logout
    \/ ExpireSession

Spec == Init /\ [][Next]_vars
FairSpec == Spec /\ WF_vars(ExpireSession)

TypeOK ==
    /\ sessionState \in SessionStates
    /\ owner \in Replicas \cup {NoReplica}
    /\ replicaState \in [Replicas -> ReplicaStates]
    /\ requestState \in [Replicas -> RequestStates]
    /\ committedBy \in Replicas \cup {NoReplica}
    /\ accessState \in AccessStates
    /\ observation \in Observations
    /\ observerDestroyedOwned \in BOOLEAN

SubmittedRefreshes ==
    {r \in Replicas : requestState[r] # Idle}

ProviderRefreshSerialized ==
    Cardinality(SubmittedRefreshes) <= 1

CommitIsOwnerFenced ==
    committedBy # NoReplica =>
        /\ sessionState = Renewed
        /\ requestState[committedBy] = Committed

ObserverPreservesOwnedRenewal ==
    ~observerDestroyedOwned

TerminalSessionAction ==
    sessionState \in {Renewed, Destroyed} =>
        sessionState' = sessionState

TerminalSessionIsPermanent == [][TerminalSessionAction]_vars

EventuallyTerminal ==
    <>(sessionState \in {Renewed, Destroyed})

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