From cd24f119985306b63f1f92481044ee2317822cc8 Mon Sep 17 00:00:00 2001 From: Arup Chauhan Date: Sun, 15 Feb 2026 22:22:48 -0600 Subject: [PATCH] sync self vote in FastLeaderElection TLA receiveVotes Signed-off-by: Arup Chauhan --- .../system-spec/zk-3.7/FastLeaderElection.tla | 32 ++++++++++++++----- 1 file changed, 24 insertions(+), 8 deletions(-) diff --git a/zookeeper-specifications/system-spec/zk-3.7/FastLeaderElection.tla b/zookeeper-specifications/system-spec/zk-3.7/FastLeaderElection.tla index cdff66ad225..b9e1cef4b51 100644 --- a/zookeeper-specifications/system-spec/zk-3.7/FastLeaderElection.tla +++ b/zookeeper-specifications/system-spec/zk-3.7/FastLeaderElection.tla @@ -188,11 +188,22 @@ RvClear(i) == receiveVotes' = [receiveVotes EXCEPT ![i] = [v \in Server |-> [v RvPut(i, id, mvote, mround, mstate) == receiveVotes' = CASE receiveVotes[i][id].round < mround -> [receiveVotes EXCEPT ![i][id].vote = mvote, ![i][id].round = mround, ![i][id].state = mstate, - ![i][id].version = 1] + ![i][id].version = 1, + ![i][i].vote = currentVote'[i], + ![i][i].round = mround, + ![i][i].state = LOOKING, + ![i][i].version = @ + 1] [] receiveVotes[i][id].round = mround -> [receiveVotes EXCEPT ![i][id].vote = mvote, ![i][id].state = mstate, - ![i][id].version = @ + 1] - [] receiveVotes[i][id].round > mround -> receiveVotes + ![i][id].version = @ + 1, + ![i][i].vote = currentVote'[i], + ![i][i].round = mround, + ![i][i].state = LOOKING, + ![i][i].version = @ + 1] + [] receiveVotes[i][id].round > mround -> [receiveVotes EXCEPT ![i][i].vote = currentVote'[i], + ![i][i].round = mround, + ![i][i].state = LOOKING, + ![i][i].version = @ + 1] Put(i, id, rcvset, mvote, mround, mstate) == CASE rcvset[id].round < mround -> [rcvset EXCEPT ![id].vote = mvote, ![id].round = mround, @@ -203,11 +214,16 @@ Put(i, id, rcvset, mvote, mround, mstate) == CASE rcvset[id].round < mround -> [ ![id].version = @ + 1] [] rcvset[id].round > mround -> rcvset -RvClearAndPut(i, id, vote, round) == receiveVotes' = LET oneVote == [vote |-> vote, - round |-> round, - state |-> LOOKING, - version |-> 1] - IN [receiveVotes EXCEPT ![i] = [v \in Server |-> IF v = id THEN oneVote +RvClearAndPut(i, id, vote, round) == receiveVotes' = LET oneVote == [vote |-> vote, + round |-> round, + state |-> LOOKING, + version |-> 1] + selfVote == [vote |-> currentVote'[i], + round |-> round, + state |-> LOOKING, + version |-> 1] + IN [receiveVotes EXCEPT ![i] = [v \in Server |-> IF v = i THEN selfVote + ELSE IF v = id THEN oneVote ELSE [vote |-> InitialVote, round |-> 0, state |-> LOOKING,