From 02dc3b2ba23403854886765881f364b78c9ce065 Mon Sep 17 00:00:00 2001
From: Arseny Sher <sher-ars@yandex.ru>
Date: Thu, 14 Nov 2024 13:22:36 +0300
Subject: [PATCH] remove obsolete nextentry

---
 safekeeper/spec/ProposerAcceptorStatic.tla | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla
index 6a6f16fd5d..c3f1c7a3a1 100644
--- a/safekeeper/spec/ProposerAcceptorStatic.tla
+++ b/safekeeper/spec/ProposerAcceptorStatic.tla
@@ -62,14 +62,6 @@ IsEmptyF(f) == DOMAIN f = {}
 \* Set of values (image) of the function f. Apparently no such builtin.
 Range(f) == {f[x] : x \in DOMAIN f}
 
-\* Next entry proposer p will push to acceptor a or NULL.
-NextEntry(p, a) ==
-  IF Len(prop_state[p].wal) >= prop_state[p].next_send_lsn[a] THEN
-    CHOOSE r \in Range(prop_state[p].wal) : r.lsn = prop_state[p].next_send_lsn[a]
-  ELSE
-    NULL
-
-
 \*****************
 
 NumAccs == Cardinality(acceptors)