Refactor Network!DropMessage to be orders of magnitude faster to eval…

…uate.
microsoft · Oct 9, 2023 · 71ca039 · 71ca039
1 parent 0960ab8
commit 71ca039
Showing 1 changed file with 6 additions and 17 deletions.
diff --git a/tla/Network.tla b/tla/Network.tla
@@ -98,15 +98,8 @@ LOCAL OrderOneMoreMessage(m) ==
     \/ Len(SelectSeq(messages[m.dest], LAMBDA e: m = e)) < Len(SelectSeq(messages'[m.dest], LAMBDA e: m = e))
 
 LOCAL OrderDropMessages(server) ==
-    \* messages' is in the set of of all functions mapping from servers to the set of all subsequences.
-    /\ messages' \in [ Servers -> UNION { SubSeqs(messages[s]) : s \in Servers } ]
-    \* Filter those values where messages appear in other inboxes.
-    /\ \A s \in Servers \ {server}:
-        messages'[s] = messages[s]
-    /\ \A m \in Range(messages'[server]) : m.dest = server
-    \* /\ \A s \in Servers:
-    \*     /\ messages'[s] \in SubSeqs(messages[s]) 
-    \*     /\ \A m \in Range(messages'[s]) : m.dest = s
+    \E subSeq \in SubSeqs(messages[server]):
+        messages' = [ messages EXCEPT ![server] = subSeq ]
 
 ----------------------------------------------------------------------------------
 \* Point-to-Point Ordering and no duplication of messages:
@@ -135,13 +128,9 @@ LOCAL OrderNoDupOneMoreMessage(m) ==
     \/ /\ m \in OrderMessages
        /\ m \in OrderMessages'
 
-LOCAL OrderNoDupDropMessages ==
-    \* messages' is in the set of of all functions mapping from servers to the set of all subsequences.
-    /\ messages' \in [ Servers -> { SubSeqs(messages[s]) : s \in Servers } ]
-    \* Filter those values where messages appear in other inboxes.
-    /\ \A s \in Servers:
-        /\ messages'[s] \in SubSeqs(messages[s]) 
-        /\ messages'[s].dest = s
+LOCAL OrderNoDupDropMessages(server) ==
+    \E subSeq \in SubSeqs(messages[server]):
+        messages' = [ messages EXCEPT ![server] = subSeq ]
 
 ----------------------------------------------------------------------------------
 
@@ -186,7 +175,7 @@ OneMoreMessage(msg) ==
       [] Guarantee = Reordered      -> ReorderDupOneMoreMessage(msg)
 
 DropMessages(server) ==
-    CASE Guarantee = OrderedNoDup   -> OrderNoDupDropMessages
+    CASE Guarantee = OrderedNoDup   -> OrderNoDupDropMessages(server)
       [] Guarantee = Ordered        -> OrderDropMessages(server)
       [] Guarantee = ReorderedNoDup -> ReorderNoDupDropMessages
       [] Guarantee = Reordered      -> ReorderDupDropMessages