remove obsolete nextentry

This commit is contained in:
Arseny Sher
2024-11-18 14:06:13 +03:00
parent 9ab6a89b5c
commit 02dc3b2ba2
@@ -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)