From d7ad70f26b8a5c9f6548c640ea70868ba4fc2f85 Mon Sep 17 00:00:00 2001
From: Graham Hay <grahamrhay@gmail.com>
Date: Tue, 23 Jan 2024 15:01:43 +0000
Subject: [PATCH] Update refcount, when conflicts are resolved

---
 syn.tla | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/syn.tla b/syn.tla
index 7a7922c..8178337 100644
--- a/syn.tla
+++ b/syn.tla
@@ -220,10 +220,14 @@ AckSync(n) ==
     /\ inbox' = [inbox EXCEPT![n] = Tail(inbox[n])]
     /\ LET message == Head(inbox[n])
         l == MergeRegistries(locally_registered[n], message.local_data, n, message.from)
+        conflicts == DOMAIN locally_registered[n][n] \intersect DOMAIN message.local_data
+        c1 == [c \in { r \in conflicts : message.local_data[r] > locally_registered[n][n][r] } |-> registered[c] - 1]
+        c2 == [c \in { r \in conflicts : locally_registered[n][n][r] > message.local_data[r] } |-> registered[c]]
         IN locally_registered' = [locally_registered EXCEPT![n] = l]
+        /\ registered' = c1 @@ c2 @@ [r \in (DOMAIN registered \ conflicts) |-> registered[r]]
         /\ states' = Append(states, <<"AckSync", n, message.from>>)
     /\ time' = time + 1
-    /\ UNCHANGED <<registered, names, visible_nodes, disconnections>>
+    /\ UNCHANGED <<names, visible_nodes, disconnections>>
 
 Down(n) ==
     /\ Len(inbox[n]) > 0