Squawks

------------------------------- 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 ============================================================================

SPECIFICATION Spec CONSTANTS Variant = "gated" MaxHuman = 2 INVARIANTS TypeOK LiveResolver ResolverConsistent AtMostOnce LedgerComplete CHECK_DEADLOCK FALSE