---------------------------- MODULE Applications ----------------------------
(***************************************************************************)
(* Lifecycle of fee-paying applications in a government services portal.   *)
(*                                                                         *)
(* The backend is a single SQLite-style table `applications`.  Every       *)
(* request is exactly ONE SQL statement, so each applies atomically, but   *)
(* requests may be duplicated (client retry, double-click) and interleave  *)
(* arbitrarily.  The DB is modelled as a SET of rows so that "one row per  *)
(* id" is a real property of INSERT OR IGNORE, not of the representation.  *)
(*                                                                         *)
(*   create(id,u): INSERT OR IGNORE (id, user_id=u, status=awaiting_payment)*)
(*   pay(id,u):    UPDATE SET status=complete, reference=<fresh>           *)
(*                 WHERE id=? AND user_id=u AND status=awaiting_payment    *)
(*   cancel(id,u): UPDATE SET status=cancelled                             *)
(*                 WHERE id=? AND user_id=u AND status=awaiting_payment    *)
(*                                                                         *)
(* Because a request reads nothing before its single statement, an         *)
(* in-flight request is fully described by (kind, id, user); every         *)
(* interleaving of in-flight requests is some ordering of atomic applies,  *)
(* so each step below issues-and-applies one request.  Duplicates are      *)
(* modelled by allowing the same request up to MaxPerKind times per id.    *)
(*                                                                         *)
(* References are a monotonically allocated counter (fresh per winning    *)
(* transition).  The fee is a pure function of the application kind and is *)
(* not modelled.                                                           *)
(***************************************************************************)
EXTENDS Naturals, FiniteSets

CONSTANTS
  Users,        \* set of user ids (model values)
  Ids,          \* set of client-generated application ids (model values)
  Refs,         \* finite set of naturals available as references
  MaxPerKind,   \* how many requests of each kind may be applied per id
  NoRef         \* sentinel: no reference assigned

ASSUME NoRef \notin Refs
ASSUME Cardinality(Refs) >= Cardinality(Ids)   \* references never run out

Kinds    == {"create", "pay", "cancel"}
Statuses == {"awaiting_payment", "complete", "cancelled"}
Terminal == {"complete", "cancelled"}
Ops      == [kind: Kinds, id: Ids, user: Users]
Rows     == [id: Ids, owner: Users, status: Statuses, ref: Refs \cup {NoRef}]

MinRef == CHOOSE r \in Refs : \A s \in Refs : r <= s
MaxRef == CHOOSE r \in Refs : \A s \in Refs : r >= s

VARIABLES
  db,        \* set of rows in the applications table
  nextRef,   \* next reference to allocate
  applied    \* Ids x Kinds -> how many requests of that kind were applied

vars == <<db, nextRef, applied>>

RowsFor(i) == {r \in db : r.id = i}

Init ==
  /\ db = {}
  /\ nextRef = MinRef
  /\ applied = [x \in Ids \X Kinds |-> 0]

(* Budget: the same request may arrive again (retry, double-click). *)
Budget(o) ==
  /\ applied[<<o.id, o.kind>>] < MaxPerKind
  /\ applied' = [applied EXCEPT ![<<o.id, o.kind>>] = @ + 1]

(* INSERT OR IGNORE keyed on id. *)
Create(o) ==
  /\ o.kind = "create"
  /\ Budget(o)
  /\ IF RowsFor(o.id) = {}
       THEN db' = db \cup {[id |-> o.id, owner |-> o.user,
                            status |-> "awaiting_payment", ref |-> NoRef]}
       ELSE UNCHANGED db
  /\ UNCHANGED nextRef

(* Rows matched by the WHERE clause of pay/cancel. *)
Matching(o) ==
  {r \in db : r.id = o.id /\ r.owner = o.user /\ r.status = "awaiting_payment"}

(* Conditional UPDATE; the server learns whether it won from changes(). *)
Pay(o) ==
  /\ o.kind = "pay"
  /\ Budget(o)
  /\ IF Matching(o) = {}
       THEN UNCHANGED <<db, nextRef>>
       ELSE /\ db' = (db \ Matching(o)) \cup
                     {[r EXCEPT !.status = "complete", !.ref = nextRef]
                        : r \in Matching(o)}
            /\ nextRef' = nextRef + 1

Cancel(o) ==
  /\ o.kind = "cancel"
  /\ Budget(o)
  /\ IF Matching(o) = {}
       THEN UNCHANGED db
       ELSE db' = (db \ Matching(o)) \cup
                  {[r EXCEPT !.status = "cancelled"] : r \in Matching(o)}
  /\ UNCHANGED nextRef

Next == \E o \in Ops : Create(o) \/ Pay(o) \/ Cancel(o)

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

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

TypeOK ==
  /\ db \subseteq Rows
  /\ nextRef \in MinRef..(MaxRef + 1)
  /\ applied \in [Ids \X Kinds -> 0..MaxPerKind]

(* At most one row per id: a duplicated create never inserts twice. *)
NoDuplicateCreate ==
  \A r1, r2 \in db : r1.id = r2.id => r1 = r2

(* A reference is present exactly on complete applications. *)
RefIffComplete ==
  \A r \in db : (r.status = "complete") <=> (r.ref \in Refs)

(* No two applications share a reference. *)
UniqueRefs ==
  \A r1, r2 \in db : (r1.ref \in Refs /\ r1.ref = r2.ref) => r1 = r2

(* Exactly one reference was allocated per transition to complete:
   repeated/concurrent pay calls on one application cannot allocate twice. *)
OneRefPerTransition ==
  Cardinality({r \in db : r.status = "complete"}) = nextRef - MinRef

-----------------------------------------------------------------------------
(* Action properties, checked as PROPERTY *)

(* Once complete or cancelled, the row (status, reference, owner) is
   never touched again. *)
TerminalStatesFrozen ==
  [][\A r \in db : r.status \in Terminal => r \in db']_vars

(* The owner is the creating user and never changes; a pay/cancel by any
   other user leaves the database untouched. *)
OwnerOnly ==
  [][ /\ \A r \in db : \E r2 \in db' : r2.id = r.id /\ r2.owner = r.owner
      /\ \A o \in Ops :
           (Pay(o) \/ Cancel(o)) =>
             \A r \in db : r.owner # o.user => r \in db' ]_vars

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