/* * Copyright (c) 2019 TAOS Data, Inc. * * This program is free software: you can use, redistribute, and/or modify * it under the terms of the GNU Affero General Public License, version 3 * or later ("AGPL"), as published by the Free Software Foundation. * * This program is distributed in the hope that it will be useful, but WITHOUT * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or * FITNESS FOR A PARTICULAR PURPOSE. * * You should have received a copy of the GNU Affero General Public License * along with this program. If not, see . */ #ifndef _TD_LIBS_SYNC_REQUEST_VOTE_REPLY_H #define _TD_LIBS_SYNC_REQUEST_VOTE_REPLY_H #ifdef __cplusplus extern "C" { #endif #include "syncInt.h" // TLA+ Spec // HandleRequestVoteResponse(i, j, m) == // \* This tallies votes even when the current state is not Candidate, but // \* they won't be looked at, so it doesn't matter. // /\ m.mterm = currentTerm[i] // /\ votesResponded' = [votesResponded EXCEPT ![i] = // votesResponded[i] \cup {j}] // /\ \/ /\ m.mvoteGranted // /\ votesGranted' = [votesGranted EXCEPT ![i] = // votesGranted[i] \cup {j}] // /\ voterLog' = [voterLog EXCEPT ![i] = // voterLog[i] @@ (j :> m.mlog)] // \/ /\ ~m.mvoteGranted // /\ UNCHANGED <> // /\ Discard(m) // /\ UNCHANGED <> // int32_t syncNodeOnRequestVoteReply(SSyncNode* ths, const SRpcMsg* pMsg); #ifdef __cplusplus } #endif #endif /*_TD_LIBS_SYNC_REQUEST_VOTE_REPLY_H*/