---------------------------- MODULE Inbox ----------------------------
(* Delivery of a message to a device: a sent note is written to the      *)
(* recipient's device and acknowledged to the server exactly once, with   *)
(* the device write strictly before the ack. The client may crash at any *)
(* point during a pull; the server's ack is a single conditional update,  *)
(* so a duplicate ack is a no-op.                                         *)
EXTENDS Naturals, FiniteSets

CONSTANTS Users, Msgs, MaxWrites

VARIABLES
  sent,       \* set of msgs the server holds
  to,         \* msg -> recipient
  delivered,  \* set of msgs the server has marked delivered
  device,     \* user -> bag of msgs written on their device (count per msg)
  pulling     \* user -> msg currently mid-pull (fetched, maybe written), or 0

vars == <<sent, to, delivered, device, pulling>>

None == 0

Init ==
  /\ sent = {}
  /\ to = [m \in Msgs |-> CHOOSE u \in Users : TRUE]
  /\ delivered = {}
  /\ device = [u \in Users |-> [m \in Msgs |-> 0]]
  /\ pulling = [u \in Users |-> None]

Send(m, u) ==
  /\ m \notin sent
  /\ sent' = sent \cup {m}
  /\ to' = [to EXCEPT ![m] = u]
  /\ UNCHANGED <<delivered, device, pulling>>

PullFetch(u, m) ==
  /\ pulling[u] = None
  /\ m \in sent /\ to[m] = u /\ m \notin delivered
  /\ pulling' = [pulling EXCEPT ![u] = m]
  /\ UNCHANGED <<sent, to, delivered, device>>

PullWrite(u) ==
  /\ pulling[u] # None
  /\ device[u][pulling[u]] < MaxWrites
  /\ device' = [device EXCEPT ![u][pulling[u]] = @ + 1]
  /\ UNCHANGED <<sent, to, delivered, pulling>>

PullAck(u) ==
  /\ pulling[u] # None
  /\ device[u][pulling[u]] > 0
  /\ delivered' = delivered \cup {pulling[u]}
  /\ pulling' = [pulling EXCEPT ![u] = None]
  /\ UNCHANGED <<sent, to, device>>

Crash(u) ==
  /\ pulling[u] # None
  /\ pulling' = [pulling EXCEPT ![u] = None]
  /\ UNCHANGED <<sent, to, delivered, device>>

Next ==
  \/ \E m \in Msgs, u \in Users : Send(m, u)
  \/ \E u \in Users, m \in Msgs : PullFetch(u, m)
  \/ \E u \in Users : PullWrite(u) \/ PullAck(u) \/ Crash(u)

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

-----------------------------------------------------------------------------
TypeOK ==
  /\ sent \subseteq Msgs
  /\ delivered \subseteq sent
  /\ \A u \in Users : pulling[u] \in Msgs \cup {None}

NoLostNotes ==
  \A m \in delivered : device[to[m]][m] >= 1

RightRecipient ==
  \A u \in Users, m \in Msgs : device[u][m] > 0 => (m \in sent /\ to[m] = u)

NoWriteAfterAck ==
  \A u \in Users : pulling[u] # None => pulling[u] \notin delivered

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