------------------------------- MODULE Keep -------------------------------
EXTENDS Naturals, Sequences

\* Each connection serializes RPCs; one abandoned write may finish after reconnect. Epochs audit explicit intent only.
\* Human controls and successful agent blocks form an append-only input stream; progress assumes eventual connectivity, usage recovery, and fair finite work.
CONSTANTS Mode, GoalBound, EditBound, StampBound, TurnBound, FailBound

GoalStates == {"active", "blocked", "paused", "complete", "cleared",
               "budgetLimited", "usageLimited"}
TurnStates == {"inProgress", "failed", "completed", "interrupted"}
Reads == {"pollGoal", "pollTurn", "thread", "check", "attach", "usage"}
Events == {"goal", "start", "done"}
Episodes == (1..GoalBound) \X (1..TurnBound)
StopType == [id : 0..GoalBound, status : GoalStates, epoch : 0..EditBound]

ASSUME /\ Mode \in {"Baseline", "Local", "Observe", "Unordered", "BarrierOld", "Filtered", "BlindUsage", "Reconcile"}
       /\ GoalBound \in Nat \ {0} /\ EditBound \in Nat \ {0}
       /\ StampBound \in Nat /\ TurnBound \in Nat \ {0}
       /\ FailBound \in Nat \ {0}

Recon == Mode \in {"Observe", "Unordered", "BarrierOld", "Filtered", "BlindUsage", "Reconcile"}
Durable == Mode \in {"Unordered", "BarrierOld", "Filtered", "BlindUsage", "Reconcile"}
Ordered == Mode \in {"BarrierOld", "Filtered", "BlindUsage", "Reconcile"}

AllFailures == Mode \in {"BlindUsage", "Reconcile"}
Waiting == {"blocked"} \cup (IF AllFailures THEN {"usageLimited"} ELSE {})
Running == {"active"} \cup Waiting

\* Error classes are observationally equivalent in the current recovery policy.
Failures == IF AllFailures THEN {FALSE} ELSE BOOLEAN

GoalType == [id : 0..GoalBound, stamp : 0..StampBound,
             status : GoalStates]
TurnType == [id : 0..(TurnBound + 1), status : TurnStates, api : BOOLEAN]
LiveType == [edits : 0..EditBound, gen : 1..GoalBound, goal : GoalType, turn : TurnType]
WatchType == [cut : 0..EditBound, cursor : 0..EditBound, fence : 0..EditBound, goal : GoalType, turn : TurnType, armed : BOOLEAN,
              fails : 0..FailBound, due : {"none", "waiting", "ready"},
              hold : GoalStates \cup {"none"}, pending : BOOLEAN, known : BOOLEAN, echo : GoalType, seed : GoalType]
TicketType == [expired : BOOLEAN, status : GoalStates, quota : BOOLEAN]
MsgType == [kind : Events \cup Reads \cup {"set"}, goal : GoalType,
            turn : TurnType, truth : 0..EditBound, busy : BOOLEAN, ok : BOOLEAN]
ActType == [sent : BOOLEAN, view : [goal : 0..GoalBound, turn : 0..(TurnBound + 1)], expected : TicketType,
            origin : {"user", "automatic"}, evidence : BOOLEAN, recover : BOOLEAN, usage : BOOLEAN]

VARIABLES late, inputs, sample, attached, live, w, wire, online, phase, req, invalid,
          ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed

vars == <<late, inputs, sample, attached, live, w, wire, online, phase, req, invalid,
          ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>

EmptyGoal == [id |-> 0, stamp |-> 0, status |-> "cleared"]

Message(kind, state, ok) ==
    [kind |-> kind, goal |-> state.goal, turn |-> state.turn,
     truth |-> state.edits, busy |-> state.turn.status = "inProgress", ok |-> ok]

Stop(x) == [x EXCEPT !.armed = FALSE, !.due = "none"]
Increment(x) == [x EXCEPT !.fails = IF @ < FailBound THEN @ + 1 ELSE @]
Retry(t) == t.api \/ AllFailures
Eligible(x) == x.armed /\ x.goal.id # 0 /\ x.goal.status \in Waiting
               /\ x.turn.status = "failed" /\ Retry(x.turn)
Schedule(x) == IF Eligible(x) /\ x.due = "none"
               THEN IF Mode = "Reconcile" /\ x.goal.status = "usageLimited"
                    THEN [x EXCEPT !.due = "ready"]
                    ELSE [Increment(x) EXCEPT !.due = "waiting"] ELSE x
KnownAfter(g) == IF g.id # 0 /\ g.status = "active" THEN known \cup {g.id} ELSE known

BaseGoal(x, g) ==
    LET same == g.id # 0 /\ x.goal.id = g.id
        cancel == ~same \/ g.status \notin Running
                  \/ (g.status = "active" /\ x.goal.status # "active")
                  \/ (g.status \in Waiting /\ x.due # "none"
                      /\ x.goal.stamp # g.stamp)
        base == [x EXCEPT !.goal = g, !.fails = IF same THEN @ ELSE 0,
                  !.armed = @ /\ ~cancel, !.due = IF cancel THEN "none" ELSE @]
    IN IF g.status = "active" /\ x.turn.status = "inProgress"
       THEN [base EXCEPT !.armed = TRUE] ELSE base

GoalUpdate(x, g, fresh) ==
    IF ~Recon THEN BaseGoal(x, g) ELSE
    IF ~fresh /\ g.status = "active" /\ x.hold = "none" /\ g.id = x.goal.id THEN x ELSE
    LET same == g.id # 0 /\ g.id = x.goal.id
        holding == x.hold # "none" /\ same
        stopped == g.id # 0 /\ g.status \notin Running
        base == IF ~same THEN [Stop(x) EXCEPT !.fails = 0, !.hold = "none", !.known = FALSE] ELSE x
        active == g.id # 0 /\ g.status = "active"
        transition == (active /\ (~same \/ x.goal.status # "active"))
                      \/ (Mode = "Reconcile" /\ g.status = "usageLimited" /\ (~same \/ x.goal.status # g.status))
        updated == [base EXCEPT !.goal = g, !.known = @ \/ active,
                     !.armed = IF active THEN @ \/ transition ELSE IF stopped \/ g.id = 0 THEN FALSE ELSE @,
                     !.due = IF transition \/ stopped \/ g.id = 0 THEN "none" ELSE @,
                     !.hold = IF (stopped /\ (Durable \/ x.pending))
                                  \/ (~same /\ g.status \in Waiting /\ x.pending) THEN g.status ELSE @]
    IN IF holding
       THEN IF ~fresh THEN IF g.status \in Running THEN x ELSE [Stop(x) EXCEPT !.goal = g, !.hold = g.status]
            ELSE IF g.status = x.hold /\ x.echo.id = 0
                 THEN [Stop(x) EXCEPT !.goal = g, !.hold = IF Durable /\ g.status # "active" THEN @ ELSE "none",
                        !.armed = g.status = "active",
                        !.known = @ \/ g.status = "active"] ELSE x
       ELSE updated

TurnUpdate(x, t) ==
    LET fresh == t.id # x.turn.id
        base == [x EXCEPT !.turn = t,
                  !.armed = IF fresh /\ ~Recon THEN FALSE ELSE @,
                  !.due = IF fresh THEN "none" ELSE @]
        started == [base EXCEPT !.armed = (Recon /\ x.armed)
                                         \/ (t.status = "inProgress" /\ x.goal.id # 0 /\ x.goal.status = "active")]
        terminal == t.status = "interrupted"
                    \/ (t.status = "failed" /\ ~Retry(t))
                    \/ (t.status = "completed" /\ ~Recon)
        settled == IF terminal THEN Stop(base) ELSE base
        result == IF fresh /\ t.status = "inProgress" THEN started ELSE
                  IF Recon /\ (fresh \/ x.turn.status = "inProgress")
                     /\ t.status = "failed" /\ Retry(t)
                     /\ x.known /\ x.hold = "none"
                  THEN [settled EXCEPT !.armed = TRUE] ELSE settled
        held == IF Recon /\ t.status = "interrupted" /\ x.goal.id # 0 /\ x.pending
                THEN [Stop(result) EXCEPT !.goal.status = "paused", !.hold = "paused"]
                ELSE IF x.hold # "none" THEN Stop(result) ELSE result
    IN IF t.status = "completed" /\ (Mode # "Baseline" \/ ~fresh)
       THEN [held EXCEPT !.fails = 0, !.due = "none"] ELSE held

ApplyInput(x, status) ==
    IF status = "cleared" THEN [Stop(x) EXCEPT !.hold = "none", !.known = FALSE] ELSE
    IF x.goal.id = 0 THEN x ELSE
    IF status = "active" /\ x.goal.status \in Running
    THEN [x EXCEPT !.hold = "none", !.known = TRUE, !.armed = TRUE, !.due = "none"]
    ELSE [Stop(x) EXCEPT !.goal.status = status, !.hold = status, !.known = status = "active"]

InputEnd(x) == IF Ordered THEN x.cut ELSE Len(inputs)
NewInput(x) == Recon /\ InputEnd(x) > x.cursor /\ InputEnd(x) > x.fence
SyncInput(x) ==
    IF ~Recon THEN x ELSE
    LET updated == IF NewInput(x) THEN ApplyInput(x, inputs[InputEnd(x)]) ELSE x
    IN [updated EXCEPT !.cursor = InputEnd(x)]

Init ==
    /\ late = "none"
    /\ inputs = <<>>
    /\ attached = TRUE
    /\ live = [edits |-> 0, gen |-> 1,
                goal |-> [id |-> 1, stamp |-> 0,
                           status |-> "active"],
                turn |-> [id |-> 1, status |-> "inProgress", api |-> FALSE]]
    /\ sample = live.goal
    /\ w = [cut |-> 0, cursor |-> 0, fence |-> 0, goal |-> live.goal, turn |-> live.turn,
             armed |-> TRUE, fails |-> 0, due |-> "none", hold |-> "none", pending |-> FALSE, known |-> TRUE, echo |-> EmptyGoal, seed |-> EmptyGoal]
    /\ wire = <<>> /\ online = TRUE /\ phase = "idle" /\ req = "none"
    /\ invalid = FALSE
    /\ ticket = [expired |-> FALSE, status |-> "active", quota |-> FALSE]
    /\ lastAct = [sent |-> FALSE, view |-> [goal |-> w.goal.id, turn |-> w.turn.id], expected |-> ticket,
                   origin |-> "automatic", evidence |-> TRUE, recover |-> TRUE, usage |-> FALSE]
    /\ known = {1} /\ need = {} /\ resumed = {} /\ cancelled = {}
    /\ stopWant = [id |-> 0, status |-> "paused", epoch |-> 0] /\ stopNeed = FALSE

CancelGoal(id) == {e \in Episodes : e[1] = id}
FutureGoal(id) == {e \in Episodes : e[1] = id /\
                   (e[2] > live.turn.id \/ (e[2] = live.turn.id /\ live.turn.status = "inProgress"))}

IntentChange(status, stamp) ==
    /\ live.goal.id # 0 /\ live.edits < EditBound
    /\ LET g == [live.goal EXCEPT !.stamp = stamp,
                  !.id = IF status = "cleared" THEN 0 ELSE @,
                  !.status = status]
           state == [live EXCEPT !.goal = g, !.edits = @ + 1]
       IN /\ live' = state
          /\ wire' = IF online THEN Append(wire, Message("goal", state, TRUE)) ELSE wire
    /\ inputs' = Append(inputs, status)
    /\ cancelled' = IF status = "active" THEN cancelled \ FutureGoal(live.goal.id)
                    ELSE cancelled \cup CancelGoal(live.goal.id)
    /\ stopNeed' = FALSE
    /\ UNCHANGED <<late, sample, attached, w, online, phase, req, invalid,
                   ticket, lastAct, known, need, resumed, stopWant>>

ReplaceGoal(stamp) ==
    /\ live.gen < GoalBound /\ live.edits < EditBound
    /\ LET g == [id |-> live.gen + 1, stamp |-> stamp, status |-> "active"]
           state == [live EXCEPT !.goal = g, !.gen = @ + 1, !.edits = @ + 1]
       IN /\ live' = state
          /\ wire' = IF online THEN Append(wire, Message("goal", state, TRUE)) ELSE wire
    /\ inputs' = Append(inputs, "active")
    /\ cancelled' = cancelled \cup CancelGoal(live.goal.id)
    /\ stopNeed' = FALSE
    /\ UNCHANGED <<late, sample, attached, w, online, phase, req, invalid,
                   ticket, lastAct, known, need, resumed, stopWant>>

StartTurn ==
    /\ live.goal.id # 0 /\ live.goal.status = "active"
    /\ live.turn.status # "inProgress" /\ live.turn.id <= TurnBound
    /\ LET state == [live EXCEPT !.turn = [id |-> @.id + 1,
                                          status |-> "inProgress", api |-> FALSE]]
       IN /\ live' = state
          /\ wire' = IF online THEN Append(wire, Message("start", state, TRUE)) ELSE wire
    /\ resumed' = resumed \cup {e \in need : e[1] = live.goal.id /\ e[2] <= live.turn.id}
    /\ UNCHANGED <<late, inputs, sample, attached, w, online, phase, req, invalid,
                   ticket, lastAct, known, need, cancelled, stopWant, stopNeed>>

FinishTurn(status) ==
    /\ live.turn.status = "inProgress"
    /\ LET state == [live EXCEPT !.turn.status = status, !.turn.api = FALSE]
       IN /\ live' = state
          /\ wire' = IF online THEN Append(wire, Message("done", state, TRUE)) ELSE wire
    /\ cancelled' = IF status = "interrupted" THEN cancelled \cup CancelGoal(live.goal.id) ELSE cancelled
    /\ UNCHANGED <<late, inputs, sample, attached, w, online, phase, req, invalid,
                   ticket, lastAct, known, need, resumed, stopWant, stopNeed>>

FailTurn(isApi, status, stamp) ==
    /\ live.turn.status = "inProgress" /\ live.turn.id <= TurnBound
    /\ LET g == IF live.goal.status = "active"
                 THEN [live.goal EXCEPT !.status = status,
                        !.stamp = stamp]
                 ELSE live.goal
           state == [live EXCEPT !.goal = g, !.turn.status = "failed", !.turn.api = isApi]
           events == IF live.goal.status = "active"
                      THEN Append(wire, Message("goal", state, TRUE)) ELSE wire
       IN /\ live' = state
          /\ wire' = IF online THEN Append(events, Message("done", state, TRUE)) ELSE wire
    /\ need' = IF live.goal.status = "active" /\ live.goal.id \in known
               THEN need \cup {<<live.goal.id, live.turn.id>>} ELSE need
    /\ UNCHANGED <<late, inputs, sample, attached, w, online, phase, req, invalid,
                   ticket, lastAct, known, resumed, cancelled, stopWant, stopNeed>>

StampUpdate(stamp) ==
    /\ live.goal.id # 0 /\ stamp > live.goal.stamp
    /\ LET state == [live EXCEPT !.goal.stamp = stamp]
       IN /\ live' = state
          /\ wire' = IF online THEN Append(wire, Message("goal", state, TRUE)) ELSE wire
    /\ UNCHANGED <<late, inputs, sample, attached, w, online, phase, req, invalid, ticket, lastAct,
                   known, need, resumed, cancelled, stopWant, stopNeed>>

Poll ==
    /\ online /\ phase = "idle" /\ req = "none"
    /\ phase' = "pollGoal" /\ req' = "pollGoal" /\ invalid' = FALSE
    /\ UNCHANGED <<late, inputs, sample, attached, live, w, wire, online, ticket, lastAct,
                   known, need, resumed, cancelled, stopWant, stopNeed>>

ServeRead ==
    /\ req \in Reads \ {"usage"}
    /\ wire' = IF ~online THEN wire ELSE
               IF req = "attach" THEN Append(Append(wire, Message(req, live, TRUE)), Message("goal", live, TRUE))
               ELSE Append(wire, Message(req, live, TRUE))
    /\ req' = "none"
    /\ UNCHANGED <<late, inputs, sample, attached, live, w, online, phase, invalid, ticket, lastAct,
                   known, need, resumed, cancelled, stopWant, stopNeed>>

ServeUsage(allowed) ==
    /\ req = "usage"
    /\ wire' = IF ~online THEN wire ELSE
               Append(wire, Message(req, live, allowed))
    /\ req' = "none"
    /\ UNCHANGED <<late, inputs, sample, attached, live, w, online, phase, invalid, ticket, lastAct,
                   known, need, resumed, cancelled, stopWant, stopNeed>>

ReadWatch(m) ==
    IF invalid /\ ~(Mode = "BarrierOld" /\ m.kind = "attach")
    THEN IF Ordered /\ m.kind = "attach"
         THEN [w EXCEPT !.seed = [id |-> 1, stamp |-> 0, status |-> "active"]] ELSE w
    ELSE
    CASE m.kind = "pollGoal" ->
           LET updated == GoalUpdate(w, m.goal, TRUE)
               base == IF Recon THEN [updated EXCEPT !.pending = FALSE] ELSE updated
           ready == IF Recon /\ base.hold = m.goal.status /\ base.echo.id = 0
                        /\ (~Durable \/ m.goal.status = "active")
                        THEN [base EXCEPT !.hold = "none", !.armed = m.goal.status = "active"] ELSE base
           IN IF Recon /\ ~attached /\ m.goal.id # 0
              THEN [ready EXCEPT !.seed = IF Ordered THEN EmptyGoal ELSE m.goal, !.echo = EmptyGoal] ELSE ready
      [] m.kind = "attach" -> IF Ordered THEN [w EXCEPT !.seed = [id |-> 1, stamp |-> 0, status |-> "active"]] ELSE w
      [] m.kind = "usage" -> w
      [] m.kind = "pollTurn" -> Schedule(TurnUpdate(w, m.turn))
      [] m.kind = "thread" -> IF ~m.busy THEN w ELSE
                               IF Recon THEN [w EXCEPT !.due = "none",
                                  !.turn = [id |-> 0, status |-> "inProgress", api |-> FALSE]] ELSE Stop(w)
      [] OTHER -> LET updated == GoalUpdate(w, m.goal, TRUE)
                  IN IF Eligible(updated)
                     THEN [updated EXCEPT !.due = "waiting"] ELSE updated

ReadPhase(m, updated) ==
    IF invalid /\ ~(Mode = "BarrierOld" /\ m.kind = "attach") THEN "idle" ELSE
    CASE m.kind = "pollGoal" -> IF m.goal.id = 0 THEN "idle" ELSE IF ~attached \/ Ordered THEN "attach" ELSE IF Recon THEN "inputs" ELSE "pollTurn"
      [] m.kind = "attach" -> IF Recon THEN "inputs" ELSE "pollTurn"
      [] m.kind = "pollTurn" -> IF Eligible(updated) /\ updated.due = "ready" /\ updated.echo.id = 0 /\ updated.seed.id = 0
                                THEN "thread" ELSE "idle"
      [] m.kind = "thread" -> IF m.busy THEN "idle" ELSE "check"
      [] m.kind = "usage" -> IF m.ok /\ Eligible(updated) THEN "send" ELSE "idle"
      [] OTHER -> IF ~Eligible(updated) THEN "idle" ELSE
                  IF Mode = "Reconcile" /\ updated.goal.status = "usageLimited" THEN "usage" ELSE "send"

ReceiveRead ==
    /\ online /\ Len(wire) > 0 /\ Head(wire).kind \in Reads
    /\ phase = Head(wire).kind
    /\ LET m == Head(wire)
           updated == ReadWatch(m)
           next == ReadPhase(m, updated)
       IN /\ w' = [updated EXCEPT !.cut = IF Ordered /\ m.kind = "pollGoal" /\ next = "attach" THEN Len(inputs) ELSE @]
          /\ phase' = next
          /\ req' = IF next \in Reads THEN next ELSE "none"
          /\ ticket' = IF m.kind = "usage" THEN [ticket EXCEPT !.quota = m.ok]
                        ELSE IF next \in {"send", "usage"}
                             THEN [expired |-> w.due = "ready", status |-> "active", quota |-> FALSE]
                             ELSE ticket
          /\ known' = IF ~invalid /\ m.kind \in {"pollGoal", "check"}
                       THEN KnownAfter(m.goal) ELSE known
    /\ sample' = IF Head(wire).kind = "pollGoal" /\ ~invalid THEN Head(wire).goal ELSE sample
    /\ invalid' = IF Mode = "BarrierOld" /\ Head(wire).kind = "attach" THEN invalid ELSE FALSE
    /\ wire' = Tail(wire)
    /\ attached' = (attached \/ Head(wire).kind = "attach")
    /\ LET m == Head(wire)
           stopped == ~invalid /\ m.kind = "pollGoal" /\ m.goal.id # 0
                       /\ m.goal.status \notin Running
                       /\ (ReadWatch(m)).goal.status = m.goal.status
       IN /\ stopWant' = IF stopped THEN [id |-> m.goal.id, status |-> m.goal.status, epoch |-> m.truth] ELSE stopWant
          /\ stopNeed' = (stopNeed \/ stopped)
    /\ UNCHANGED <<late, inputs,  live, online, lastAct, need, resumed, cancelled>>


ReadInput ==
    /\ online /\ phase = "inputs" /\ req = "none"
    /\ LET updated == SyncInput(w)
           blocked == updated.hold = "active" /\ sample.status \in Waiting
           ready == IF blocked THEN [updated EXCEPT !.hold = "none", !.goal = sample,
                                      !.known = TRUE, !.armed = TRUE] ELSE updated
       repair == ready.hold # "none" /\ ready.hold # sample.status
       IN /\ invalid' = (Mode = "BarrierOld" /\ invalid /\ repair)
          /\ w' = ready
          /\ phase' = IF repair
                        THEN IF ready.echo.id = 0 /\ (Ordered \/ ready.seed.id = 0) THEN "repair" ELSE "idle"
                        ELSE "pollTurn"
          /\ req' = IF ~repair THEN "pollTurn" ELSE "none"
    /\ sample' = IF Ordered THEN EmptyGoal ELSE sample
    /\ stopNeed' = IF NewInput(w) THEN FALSE ELSE stopNeed
    /\ UNCHANGED <<late, inputs, attached, live, wire, online, ticket, lastAct,
                   known, need, resumed, cancelled, stopWant>>

ReceiveEvent ==
    /\ online /\ phase \notin {"send", "repair", "inputs"} /\ Len(wire) > 0 /\ Head(wire).kind \in Events
    /\ LET m == Head(wire)
           seed == Recon /\ m.kind = "goal" /\ w.seed.id # 0
           snapshot == seed /\ (Ordered \/ (m.goal.id = w.seed.id /\ m.goal.status = w.seed.status /\ m.goal.stamp = w.seed.stamp))
           echo == Recon /\ m.kind = "goal" /\ w.echo.id # 0
                   /\ m.goal.id = w.echo.id /\ m.goal.status = w.echo.status /\ m.goal.stamp = w.echo.stamp
           ignore == snapshot \/ echo \/ (m.kind = "done" /\ m.turn.id # w.turn.id)
           seal == ~ignore /\ ((~Ordered /\ m.kind = "goal" /\ m.goal.status \notin Running)
                     \/ (m.kind = "done" /\ m.turn.status = "interrupted"))
           base == IF seal /\ Recon THEN [w EXCEPT !.fence = Len(inputs)]
                   ELSE IF Ordered \/ (ignore /\ ~echo /\ ~snapshot) THEN w ELSE SyncInput(w)
           updated == IF ignore THEN w ELSE
                      IF m.kind = "goal" THEN GoalUpdate(base, m.goal, FALSE)
                      ELSE TurnUpdate(base, m.turn)
       IN /\ w' = [IF echo THEN [base EXCEPT !.echo = EmptyGoal] ELSE IF snapshot THEN base
                 ELSE IF ignore THEN w ELSE Schedule(updated)
                 EXCEPT !.seed = IF seed THEN EmptyGoal ELSE @]
          /\ known' = IF m.kind = "goal" THEN KnownAfter(m.goal) ELSE known
          /\ stopWant' = IF ~echo /\ ~snapshot /\ m.kind = "goal" /\ m.goal.id # 0 /\ m.goal.status \notin Running
                         THEN [id |-> m.goal.id, status |-> m.goal.status, epoch |-> m.truth]
                         ELSE IF ~ignore /\ m.kind = "done" /\ m.turn.status = "interrupted" /\ w.goal.id # 0 /\ w.pending
                              THEN [id |-> w.goal.id, status |-> "paused", epoch |-> m.truth] ELSE stopWant
          /\ stopNeed' = ((stopNeed /\ ~(~seal /\ NewInput(w)))
                         \/ (~echo /\ ~snapshot /\ m.kind = "goal" /\ m.goal.id # 0 /\ m.goal.status \notin Running)
                         \/ (~ignore /\ m.kind = "done" /\ m.turn.status = "interrupted" /\ w.goal.id # 0 /\ w.pending))
          /\ invalid' = (invalid \/ ((~ignore \/ (~Ordered /\ (echo \/ snapshot) /\ NewInput(w))) /\ phase # "idle"))
    /\ wire' = Tail(wire)
    /\ UNCHANGED <<late, inputs, sample, attached, live, online, phase, req,
                   ticket, lastAct, need, resumed, cancelled>>

SendSet ==
    /\ online /\ phase \in {"send", "repair"} /\ req = "none" /\ w.echo.id = 0 /\ (Ordered \/ w.seed.id = 0)
    /\ IF phase = "send" THEN Eligible(w) ELSE w.hold # "none"
    /\ phase' = "set" /\ req' = "set" /\ invalid' = FALSE     /\ w' = [w EXCEPT !.pending = TRUE]
    /\ ticket' = IF phase = "repair"
                  THEN [expired |-> FALSE, status |-> w.hold, quota |-> FALSE] ELSE ticket
    /\ lastAct' = [sent |-> TRUE, view |-> [goal |-> w.goal.id, turn |-> w.turn.id],
                     expected |-> IF phase = "send" THEN ticket ELSE [ticket EXCEPT !.status = w.hold],
                     origin |-> IF Mode = "Baseline" THEN "user" ELSE "automatic",
                     evidence |-> Eligible(w), recover |-> phase = "send", usage |-> w.goal.status = "usageLimited"]
    /\ UNCHANGED <<late, inputs, sample, attached, live, wire, online, known, need, resumed, cancelled, stopWant, stopNeed>>

ServeSet(stamp) ==
    /\ req = "set"
    /\ LET allowed == live.goal.id # 0
           state == IF allowed THEN [live EXCEPT !.goal.status = ticket.status,
                                      !.goal.stamp = stamp] ELSE live
           replies == Append(wire, Message("set", state, allowed))
       IN /\ live' = state
          /\ wire' = IF online
                      THEN IF allowed THEN Append(replies, Message("goal", state, TRUE))
                           ELSE replies
                      ELSE wire
    /\ req' = "none"
    /\ UNCHANGED <<late, inputs, sample, attached, w, online, phase, invalid, ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>

ReceiveSet ==
    /\ online /\ phase = "set" /\ Len(wire) > 0 /\ Head(wire).kind = "set"
    /\ LET m == Head(wire)
           base == [w EXCEPT !.pending = FALSE, !.echo = IF m.ok /\ Recon THEN m.goal ELSE @]
       IN /\ w' = IF m.ok
                   THEN IF invalid THEN base ELSE GoalUpdate(base, m.goal, TRUE)
                   ELSE IF Mode = "Baseline" \/ (~invalid /\ Eligible(w)
                        /\ (Mode # "Reconcile" \/ w.goal.status # "usageLimited"))
                        THEN Increment(base) ELSE base
          /\ known' = IF m.ok /\ ~invalid THEN KnownAfter(m.goal) ELSE known
    /\ phase' = "idle" /\ invalid' = FALSE /\ wire' = Tail(wire)
    /\ UNCHANGED <<late, inputs, sample, attached, live, online, req, ticket, lastAct, need, resumed, cancelled, stopWant, stopNeed>>

Receive == ReceiveEvent \/ ReceiveRead \/ ReceiveSet

Clock ==
    /\ w.due = "waiting"
    /\ w' = [w EXCEPT !.due = "ready"]
    /\ UNCHANGED <<late, inputs, sample, attached, live, wire, online, phase, req, invalid,
                   ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>

Disconnect ==
    /\ online /\ (req # "set" \/ late = "none") /\ online' = FALSE /\ attached' = FALSE /\ wire' = <<>> /\ phase' = "idle"
    /\ req' = "none"
    /\ late' = IF req = "set" THEN ticket.status ELSE late
    /\ invalid' = FALSE
    /\ w' = [IF phase = "set" /\ (Mode = "Baseline" \/ (~invalid /\ Eligible(w)
                   /\ (Mode # "Reconcile" \/ w.goal.status # "usageLimited")))
              THEN Increment(w) ELSE w EXCEPT !.echo = EmptyGoal, !.seed = EmptyGoal]
    /\ UNCHANGED <<inputs, sample,  live, ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>

ServeLate(stamp) ==
    /\ late # "none"
    /\ LET state == IF live.goal.id # 0 THEN [live EXCEPT !.goal.status = late,
                       !.goal.stamp = stamp] ELSE live
       IN /\ live' = state
          /\ wire' = IF online /\ attached /\ live.goal.id # 0 THEN Append(wire, Message("goal", state, TRUE)) ELSE wire
    /\ late' = "none"
    /\ UNCHANGED <<inputs, sample, attached, w, online, phase, req, invalid,
                   ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>

Reconnect ==
    /\ ~online /\ online' = TRUE
    /\ UNCHANGED <<late, inputs, sample, attached, live, w, wire, phase, req, invalid,
                   ticket, lastAct, known, need, resumed, cancelled, stopWant, stopNeed>>

HonourStop ==
    /\ stopNeed /\ req # "set"
    /\ (live.goal.id # stopWant.id \/ live.edits > stopWant.epoch)
    /\ stopNeed' = FALSE
    /\ UNCHANGED <<late, inputs, sample, attached, live, w, wire, online, phase, req, invalid,
                   ticket, lastAct, known, need, resumed, cancelled, stopWant>>

Next ==
    \/ \E status \in GoalStates, stamp \in live.goal.stamp..StampBound : IntentChange(status, stamp)
    \/ \E stamp \in live.goal.stamp..StampBound : ReplaceGoal(stamp)
    \/ StartTurn
    \/ \E status \in {"completed", "interrupted"} : FinishTurn(status)
    \/ \E isApi \in Failures, status \in Waiting, stamp \in live.goal.stamp..StampBound : FailTurn(isApi, status, stamp)
    \/ Poll \/ ServeRead \/ ServeUsage(TRUE) \/ ServeUsage(FALSE) \/ Receive \/ SendSet \/ ReadInput
    \/ \E stamp \in live.goal.stamp..StampBound : ServeSet(stamp)
    \/ (\E stamp \in live.goal.stamp..StampBound : ServeLate(stamp))
    \/ Clock \/ Disconnect \/ Reconnect \/ HonourStop
    \/ \E stamp \in (live.goal.stamp + 1)..StampBound : StampUpdate(stamp)

TypeOK ==
    /\ late \in GoalStates \cup {"none"}
    /\ inputs \in Seq(GoalStates) /\ Len(inputs) <= EditBound /\ sample \in GoalType
    /\ attached \in BOOLEAN
    /\ live \in LiveType /\ w \in WatchType /\ wire \in Seq(MsgType)
    /\ online \in BOOLEAN /\ invalid \in BOOLEAN
    /\ phase \in {"idle", "send", "repair", "set", "inputs"} \cup Reads
    /\ req \in {"none", "set"} \cup Reads
    /\ ticket \in TicketType /\ lastAct \in ActType
    /\ known \subseteq 1..GoalBound
    /\ need \subseteq Episodes /\ resumed \subseteq Episodes /\ cancelled \subseteq Episodes
    /\ stopWant \in StopType /\ stopNeed \in BOOLEAN

FreshRepair == phase # "repair" \/ ~invalid
FailureEvidence == ~lastAct.sent \/ ~lastAct.recover \/ lastAct.evidence
AutoProvenance == ~lastAct.sent \/ lastAct.origin = "automatic"
SuccessReset == w.turn.status # "completed" \/ w.fails = 0
UsageEvidence == ~lastAct.sent \/ ~lastAct.recover \/ ~lastAct.usage \/ lastAct.expected.quota
NoEarlyResume == ~lastAct.sent \/ ~lastAct.recover \/ lastAct.expected.expired
StopCancels == w.hold = "none" \/ (~w.armed /\ w.due = "none")
HumanStops == (w.goal.status \notin Running \/ w.turn.status = "interrupted")
              => (~Eligible(w) /\ w.due = "none")


StopWins == <>[](~stopNeed \/ live.goal.id # stopWant.id
                      \/ live.edits > stopWant.epoch \/ live.goal.status = stopWant.status)

EventuallyResume == \A e \in Episodes :
    (e \in need) ~> (e \in resumed \cup cancelled)

RecoveryProgress == (<>[]online) => EventuallyResume
StopProgress == (<>[]online) => StopWins
HoldProgress == (<>[]online) => (w.hold # "none" ~> (w.hold = "none" \/ live.goal.id # w.goal.id \/ live.goal.status = w.hold))

FairLate == \E stamp \in live.goal.stamp..StampBound : ServeLate(stamp)
FairSet == \E stamp \in live.goal.stamp..StampBound : ServeSet(stamp)
Fairness == WF_vars(Poll) /\ WF_vars(ServeRead) /\ WF_vars(Receive)
        /\ WF_vars(SendSet) /\ WF_vars(FairSet) /\ WF_vars(Clock) /\ WF_vars(StartTurn)
        /\ WF_vars(FairLate) /\ WF_vars(HonourStop) /\ WF_vars(ReadInput)
        /\ SF_vars(ServeUsage(TRUE))
Spec == Init /\ [][Next]_vars /\ Fairness
=============================================================================