------------------------------- MODULE Squawks -------------------------------
(***************************************************************************)
(* Squawk (discrepancy) tracking against maintenance logs on D1 (SQLite).  *)
(* A squawk has a status in {open, deferred, resolved} and a `log` column   *)
(* naming the maintenance log that resolved it ("none" when unresolved or  *)
(* resolved by hand).  Every request runs as one D1 `batch`, so each       *)
(* action below is a single atomic step.                                   *)
(*                                                                         *)
(* Requests:                                                               *)
(*   LogAdd(l)     mx_log_add: INSERT OR IGNORE the log row (the client    *)
(*                 may RETRY with the same log id), then UPDATE each       *)
(*                 targeted squawk to resolved with log = l.               *)
(*   DeleteLog(l)  soft-delete the log and reopen every squawk it resolved *)
(*                 (status open, log none) in the same batch.              *)
(*   Reopen(s)     human reopens a resolved squawk.                        *)
(*   Resolve(s)    human resolves a non-resolved squawk by hand (log none).*)
(*   Defer(s)      human defers an open squawk.                            *)
(*                                                                         *)
(* Variant = "gated" (the real design): a `ledger` of <<squawk, log>>      *)
(* pairs (table squawk_resolutions).  A LogAdd resolves a squawk only if   *)
(* it is not already resolved AND the pair is not yet in the ledger; the   *)
(* pair is then recorded regardless, so a retry of the same request is a   *)
(* no-op on the squawk.                                                    *)
(* Variant = "naive": the same UPDATE without the ledger condition.  The   *)
(* INSERT OR IGNORE makes the log row idempotent, but the UPDATE is not:   *)
(* a retry that lands after the log was deleted re-resolves the squawk    *)
(* and points it at a deleted log (LiveResolver, AtMostOnce).              *)
(***************************************************************************)
EXTENDS Naturals, FiniteSets

CONSTANTS
  Variant,   \* "gated" (real design) or "naive" (no resolution ledger)
  MaxHuman   \* bound on human actions, keeps the model finite

ASSUME Variant \in {"gated", "naive"}

(* Small fixed world: two logs, one squawk targeted by both.  L1 is       *)
(* delivered twice (a client retry reusing the same log id), L2 once.     *)
Logs     == {"L1", "L2"}
Squawks  == {"S"}
Targets  == [l \in Logs |-> Squawks]
Attempts == [l \in Logs |-> IF l = "L1" THEN 2 ELSE 1]
MaxAttempts == 2

Statuses  == {"open", "deferred", "resolved"}
LogStates == {"absent", "live", "deleted"}
Pairs     == Squawks \X Logs

VARIABLES
  status,       \* per squawk: open | deferred | resolved
  log,          \* per squawk: the log that resolved it, or "none"
  logState,     \* per log: absent (never inserted) | live | deleted
  ledger,       \* rows of squawk_resolutions: set of <<squawk, log>>
  attemptsLeft, \* per log: remaining mx_log_add deliveries (incl. retries)
  resolvedBy,   \* history: per <<squawk, log>>, times the log flipped the
                \* squawk to resolved
  humanLeft     \* budget for Reopen / Resolve / Defer

vars == <<status, log, logState, ledger, attemptsLeft, resolvedBy, humanLeft>>

Init ==
  /\ status       = [s \in Squawks |-> "open"]
  /\ log          = [s \in Squawks |-> "none"]
  /\ logState     = [l \in Logs |-> "absent"]
  /\ ledger       = {}
  /\ attemptsLeft = Attempts
  /\ resolvedBy   = [p \in Pairs |-> 0]
  /\ humanLeft    = MaxHuman

(* The UPDATE's WHERE clause.  The ledger conjunct is the gated design.   *)
Flips(s, l) ==
  /\ s \in Targets[l]
  /\ status[s] # "resolved"
  /\ Variant = "naive" \/ <<s, l>> \notin ledger

(* mx_log_add, one batch: INSERT OR IGNORE the log, conditional UPDATE of *)
(* each targeted squawk, INSERT OR IGNORE of the ledger pairs.            *)
LogAdd(l) ==
  /\ attemptsLeft[l] > 0
  /\ attemptsLeft' = [attemptsLeft EXCEPT ![l] = @ - 1]
  /\ logState' = [logState EXCEPT ![l] = IF @ = "absent" THEN "live" ELSE @]
  /\ status' = [s \in Squawks |-> IF Flips(s, l) THEN "resolved" ELSE status[s]]
  /\ log'    = [s \in Squawks |-> IF Flips(s, l) THEN l ELSE log[s]]
  /\ resolvedBy' = [p \in Pairs |->
                      IF p[2] = l /\ Flips(p[1], l) THEN resolvedBy[p] + 1
                      ELSE resolvedBy[p]]
  /\ ledger' = ledger \cup {<<s, l>> : s \in Targets[l]}
  /\ UNCHANGED humanLeft

(* Soft delete: mark the log deleted and reopen everything it resolved.   *)
DeleteLog(l) ==
  /\ logState[l] = "live"
  /\ logState' = [logState EXCEPT ![l] = "deleted"]
  /\ status' = [s \in Squawks |-> IF log[s] = l THEN "open" ELSE status[s]]
  /\ log'    = [s \in Squawks |-> IF log[s] = l THEN "none" ELSE log[s]]
  /\ UNCHANGED <<ledger, attemptsLeft, resolvedBy, humanLeft>>

Human ==
  /\ humanLeft > 0
  /\ humanLeft' = humanLeft - 1
  /\ UNCHANGED <<logState, ledger, attemptsLeft, resolvedBy>>

Reopen(s) ==
  /\ Human
  /\ status[s] = "resolved"
  /\ status' = [status EXCEPT ![s] = "open"]
  /\ log'    = [log EXCEPT ![s] = "none"]

Resolve(s) ==
  /\ Human
  /\ status[s] # "resolved"
  /\ status' = [status EXCEPT ![s] = "resolved"]
  /\ log'    = [log EXCEPT ![s] = "none"]

Defer(s) ==
  /\ Human
  /\ status[s] = "open"
  /\ status' = [status EXCEPT ![s] = "deferred"]
  /\ UNCHANGED log

Next ==
  \/ \E l \in Logs : LogAdd(l) \/ DeleteLog(l)
  \/ \E s \in Squawks : Reopen(s) \/ Resolve(s) \/ Defer(s)

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

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

TypeOK ==
  /\ status       \in [Squawks -> Statuses]
  /\ log          \in [Squawks -> Logs \cup {"none"}]
  /\ logState     \in [Logs -> LogStates]
  /\ ledger       \subseteq Pairs
  /\ attemptsLeft \in [Logs -> 0..MaxAttempts]
  /\ resolvedBy   \in [Pairs -> 0..MaxAttempts]
  /\ humanLeft    \in 0..MaxHuman

\* A squawk never points at a deleted (or never-inserted) log.
LiveResolver ==
  \A s \in Squawks : log[s] # "none" => logState[log[s]] = "live"

\* A squawk that names a resolving log is resolved.
ResolverConsistent ==
  \A s \in Squawks : log[s] # "none" => status[s] = "resolved"

\* A given log resolves a given squawk at most once, however often the
\* request is retried.
AtMostOnce ==
  \A p \in Pairs : resolvedBy[p] <= 1

\* Every log-resolved squawk has its pair in the ledger (gated design).
LedgerComplete ==
  \A s \in Squawks : log[s] # "none" => <<s, log[s]>> \in ledger

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