---- MODULE Lease ----
EXTENDS Naturals

\* Equal clocks and urgent local steps project the bounded synthetic child fixture.
\* The invariant counts live processes; it makes no claim about kernel SA cleanup.
CONSTANTS LeaseSpan, ReplyMax
ASSUME LeaseSpan \in Nat \ {0} /\ ReplyMax \in 0..20

Retry == 5
Renew == 20
StopWait == 10
PollLow == 5
PollHigh == 11
Limit == LeaseSpan + 2 * PollHigh + ReplyMax + Retry + Renew + StopWait

VARIABLES now, version, seen, age, committed, leader, remaining,
          signalled, oldAlive, standby, pollLeft, newAlive
vars == <<now, version, seen, age, committed, leader, remaining,
          signalled, oldAlive, standby, pollLeft, newAlive>>

TypeOK ==
    /\ now \in 0..Limit
    /\ version \in 0..2 /\ seen \in 0..2 /\ age \in 0..LeaseSpan
    /\ leader \in {"Pending", "Retry", "Renew", "Stopping", "Done"}
    /\ standby \in {"Poll", "Check", "Acquired", "Callback", "Running"}
    /\ remaining \in 0..Renew /\ pollLeft \in 0..PollHigh
    /\ \A value \in {committed, signalled, oldAlive, newAlive} : value \in BOOLEAN

\* The incumbent is running; one final renewal commits before later requests fail.
Init ==
    /\ now = 0 /\ version = 0 /\ seen = 0 /\ age = 0
    /\ committed = FALSE /\ leader = "Pending" /\ remaining = 0
    /\ signalled = FALSE /\ oldAlive = TRUE
    /\ standby = "Poll" /\ pollLeft = 0 /\ newAlive = FALSE

Commit ==
    /\ ~committed
    /\ committed' = TRUE /\ version' = 1
    /\ UNCHANGED <<now, seen, age, leader, remaining, signalled, oldAlive,
                   standby, pollLeft, newAlive>>

\* RenewDeadline bounds this successful response; the next retry starts afterward.
Reply ==
    /\ committed /\ leader = "Pending" /\ now <= ReplyMax
    /\ leader' = "Retry" /\ remaining' = Retry
    /\ UNCHANGED <<now, version, seen, age, committed, signalled, oldAlive,
                   standby, pollLeft, newAlive>>

BeginRenew ==
    /\ leader = "Retry" /\ remaining = 0
    /\ leader' = "Renew" /\ remaining' = Renew
    /\ UNCHANGED <<now, version, seen, age, committed, signalled, oldAlive,
                   standby, pollLeft, newAlive>>

Cancel ==
    /\ leader = "Renew" /\ remaining = 0
    /\ leader' = "Stopping" /\ remaining' = StopWait
    /\ UNCHANGED <<now, version, seen, age, committed, signalled, oldAlive,
                   standby, pollLeft, newAlive>>

Signal ==
    /\ leader = "Stopping" /\ ~signalled
    /\ signalled' = TRUE
    /\ UNCHANGED <<now, version, seen, age, committed, leader, remaining,
                   oldAlive, standby, pollLeft, newAlive>>

Reap ==
    /\ leader = "Stopping" /\ signalled /\ oldAlive
    /\ oldAlive' = FALSE
    /\ UNCHANGED <<now, version, seen, age, committed, leader, remaining,
                   signalled, standby, pollLeft, newAlive>>

Return ==
    /\ leader = "Stopping" /\ ~oldAlive
    /\ leader' = "Done" /\ remaining' = 0
    /\ UNCHANGED <<now, version, seen, age, committed, signalled, oldAlive,
                   standby, pollLeft, newAlive>>

\* An unchanged Lease does not reset the contender's local observation age.
Observe ==
    /\ standby = "Poll" /\ pollLeft = 0
    /\ age' = IF seen = version THEN age ELSE 0
    /\ seen' = version /\ standby' = "Check"
    /\ UNCHANGED <<now, version, committed, leader, remaining,
                   signalled, oldAlive, pollLeft, newAlive>>

Defer ==
    /\ standby = "Check" /\ (age < LeaseSpan \/ seen /= version)
    /\ standby' = "Poll" /\ pollLeft' \in PollLow..PollHigh
    /\ UNCHANGED <<now, version, seen, age, committed, leader, remaining,
                   signalled, oldAlive, newAlive>>

Acquire ==
    /\ standby = "Check" /\ age = LeaseSpan /\ seen = version
    /\ version' = 2 /\ seen' = 2 /\ age' = 0
    /\ standby' = "Acquired"
    /\ UNCHANGED <<now, committed, leader, remaining,
                   signalled, oldAlive, pollLeft, newAlive>>

Start ==
    /\ standby = "Acquired"
    /\ standby' = "Callback"
    /\ UNCHANGED <<now, version, seen, age, committed, leader, remaining,
                   signalled, oldAlive, pollLeft, newAlive>>

Spawn ==
    /\ standby = "Callback"
    /\ standby' = "Running" /\ newAlive' = TRUE
    /\ UNCHANGED <<now, version, seen, age, committed, leader, remaining,
                   signalled, oldAlive, pollLeft>>

Done == leader = "Done" /\ standby = "Running"

\* Deadlines and local callbacks run before the next one-second clock step.
Urgent ==
    \/ ~committed
    \/ (leader = "Pending" /\ now = ReplyMax)
    \/ (leader \in {"Retry", "Renew"} /\ remaining = 0)
    \/ (leader = "Stopping" /\ (~signalled \/ ~oldAlive \/ remaining = 0))
    \/ (standby = "Poll" /\ pollLeft = 0)
    \/ standby \in {"Check", "Acquired", "Callback"}

Tick ==
    /\ ~Done /\ ~Urgent
    /\ now' = now + 1
    /\ remaining' = IF leader \in {"Retry", "Renew", "Stopping"}
                    THEN remaining - 1 ELSE remaining
    /\ age' = IF standby = "Poll" /\ age < LeaseSpan THEN age + 1 ELSE age
    /\ pollLeft' = IF standby = "Poll" THEN pollLeft - 1 ELSE pollLeft
    /\ UNCHANGED <<version, seen, committed, leader, signalled,
                   oldAlive, standby, newAlive>>

Next == Commit \/ Reply \/ BeginRenew \/ Cancel \/ Signal \/ Reap \/ Return
        \/ Observe \/ Defer \/ Acquire \/ Start \/ Spawn \/ Tick
        \/ (Done /\ UNCHANGED vars)

Spec ==
    /\ Init /\ [][Next]_vars
    /\ WF_vars(Commit) /\ WF_vars(Reply) /\ WF_vars(BeginRenew)
    /\ WF_vars(Cancel) /\ WF_vars(Signal) /\ WF_vars(Reap) /\ WF_vars(Return)
    /\ WF_vars(Observe) /\ WF_vars(Defer) /\ WF_vars(Acquire)
    /\ WF_vars(Start) /\ WF_vars(Spawn) /\ WF_vars(Tick)

ProcessExclusion == ~(oldAlive /\ newAlive)
Handoff == <>Done
====