Inbox

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

SPECIFICATION Spec CONSTANTS Users = {a, b} Msgs = {m1, m2} MaxWrites = 2 INVARIANTS TypeOK NoLostNotes RightRecipient NoWriteAfterAck CHECK_DEADLOCK FALSE