docs(Reply): model local versus remote deletion

Per <https://stackoverflow.com/q/47115185>, we still need Reply = NULL as the "dead and gone" sentinel state/value, because we can't remove it from from the range of the function [DOMAIN pool -> Reply] once we've added it.
freedomofpress · Apr 13, 2023 · 4772cb8 · 4772cb8
1 parent a6958f2
commit 4772cb8
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 27 deletions.
diff --git a/docs/tla/Reply.cfg b/docs/tla/Reply.cfg
@@ -8,4 +8,5 @@ CONSTANTS
     JOB_RETRIES = 0
     InReplies = {0}
     OutReplies = {1}
-    ToDelete = {0}
+    ForLocalDeletion = {}
+    ForRemoteDeletion = {}
diff --git a/docs/tla/Reply.tla b/docs/tla/Reply.tla
@@ -4,7 +4,8 @@ CONSTANTS
     JOB_RETRIES,
     InReplies,
     OutReplies,
-    ToDelete
+    ForLocalDeletion,
+    ForRemoteDeletion
 
 Replies == InReplies \union OutReplies
 
@@ -21,19 +22,14 @@ Contains(q, id) == \E el \in Range(q): el.id = id
 
 \* Reply model:
 Id == Nat
-Deletion == {
-    "DeletePending",
-    "Deleting",
-    "DeletedLocally"
-}
+Deletion == {"DeletedLocally"}
 SharedStates == {"Ready"} \union Deletion
 TerminalStates == {
     "Ready",
     "DownloadFailed",
     "DecryptionFailed",
-    "SendFailed",
-    "DeletedLocally"
-    }
+    "SendFailed"
+    } \union Deletion
 NULL == [type: {"NULL"}]
 InReply ==
     [
@@ -61,6 +57,18 @@ Reply ==
     OutReply
 VARIABLES pool, deleting
 
+CheckAlive(id) ==
+    /\ id \in DOMAIN pool
+    /\ pool[id] \notin NULL
+
+CheckState(id, from) ==
+    /\ CheckAlive(id)
+    /\ pool[id].state = from
+
+Set(id, to) == pool' = [pool EXCEPT ![id].state = to]
+
+Delete(id) == pool' = [pool EXCEPT ![id] = [type |-> "NULL"]]
+
 \* RunnableQueue, sans prioritization.  Current = Head(queue).
 DeleteJob == [id: Id, type: {"Delete"}, ttl: Nat]  \* FIXME: DeleteConversationJob
 DownloadReplyJob == [id: Id, type: {"DownloadReply"}, ttl: Nat]
@@ -88,7 +96,7 @@ TypeOK ==
 
 \* ---- QUEUE ACTIONS ----
 
-Delete(id) ==
+LocalDelete(id) ==
     /\ id \in DOMAIN pool
     /\ id \notin deleting
     /\ deleting' = deleting \union {id}
@@ -99,6 +107,11 @@ Delete(id) ==
        ])
     /\ UNCHANGED<<done, pool>>
 
+RemoteDelete(id) ==
+    /\ CheckAlive(id)
+    /\ Delete(id)
+    /\ UNCHANGED<<deleting, done, queue>>
+
 Enqueue(id) ==
     LET
         dir == IF id \in InReplies THEN "in" ELSE "out"
@@ -135,30 +148,22 @@ QueueNext ==
 
 \* --- REPLY STATES ---
 
-Check(id, from) == pool[id].state = from
-
-Set(id, to) == pool' = [pool EXCEPT ![id].state = to]
-
 Trans(id, from, to) ==
-    /\ Check(id, from)
+    /\ CheckState(id, from)
     /\ Set(id, to)
 
 DeleteInterrupt(job) ==
     /\ pool[job.id].state \notin Deletion
-    /\ Set(job.id, "DeletePending")
-    /\ UNCHANGED<<done, queue>>
-
-DeletePending(job) ==
-    /\ Trans(job.id, "DeletePending", "Deleting")
+    /\ Set(job.id, "DeletedLocally")
     /\ UNCHANGED<<done, queue>>
 
-Deleting(job) ==
-    \/ /\ pool' = [pool EXCEPT ![job.id] = [type |-> "NULL"]]
+DeletedLocally(job) ==
+    \/ /\ Delete(job.id)
        /\ QueueNext
     \/ Retry(job)
     \/ /\ Failed(job)
-       /\ Trans(job.id, "Deleting", "DeletedLocally")
        /\ QueueNext
+       /\ UNCHANGED pool
 
 DownloadPending(job) ==
     /\ Trans(job.id, "DownloadPending", "Downloading")
@@ -200,6 +205,7 @@ vars == <<
 ProcessJob ==
     LET job == Head(queue)
     IN
+        IF CheckAlive(job.id) THEN
         \/ /\ job \in DownloadReplyJob
            /\ \/ DownloadPending(job)
               \/ Downloading(job)
@@ -209,8 +215,10 @@ ProcessJob ==
               \/ Sending(job)
         \/ /\ job \in DeleteJob
            /\ \/ DeleteInterrupt(job)
-              \/ DeletePending(job)
-              \/ Deleting(job)
+              \/ DeletedLocally(job)
+        ELSE
+        /\ QueueNext
+        /\ UNCHANGED pool
 
 QueueRun ==
     \/ /\ Len(queue) > 0
@@ -233,7 +241,8 @@ Next ==
         /\ Enqueue(id)
         /\ UNCHANGED deleting
     \/ QueueRun
-    \/ \E id \in ToDelete: Delete(id)
+    \/ \E id \in ForLocalDeletion: LocalDelete(id)
+    \/ \E id \in ForRemoteDeletion: RemoteDelete(id)
 
 Spec == Init /\ [][Next]_vars /\ WF_vars(Next)