/*
 * Copyright (c) 2019 TAOS Data, Inc. <jhtao@taosdata.com>
 *
 * 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 <http://www.gnu.org/licenses/>.
 */

#include "syncRequestVote.h"

void requestVote(SRaft *pRaft, const SyncRequestVote *pMsg) {
  // TLA+ Spec
  // RequestVote(i, j) ==
  //    /\ state[i] = Candidate
  //    /\ j \notin votesResponded[i]
  //    /\ Send([mtype         |-> RequestVoteRequest,
  //             mterm         |-> currentTerm[i],
  //             mlastLogTerm  |-> LastTerm(log[i]),
  //             mlastLogIndex |-> Len(log[i]),
  //             msource       |-> i,
  //             mdest         |-> j])
  //    /\ UNCHANGED <<serverVars, candidateVars, leaderVars, logVars>>
}

void onRequestVote(SRaft *pRaft, const SyncRequestVote *pMsg) {
  // TLA+ Spec
  // HandleRequestVoteRequest(i, j, m) ==
  //    LET logOk == \/ m.mlastLogTerm > LastTerm(log[i])
  //                 \/ /\ m.mlastLogTerm = LastTerm(log[i])
  //                    /\ m.mlastLogIndex >= Len(log[i])
  //        grant == /\ m.mterm = currentTerm[i]
  //                 /\ logOk
  //                 /\ votedFor[i] \in {Nil, j}
  //    IN /\ m.mterm <= currentTerm[i]
  //       /\ \/ grant  /\ votedFor' = [votedFor EXCEPT ![i] = j]
  //          \/ ~grant /\ UNCHANGED votedFor
  //       /\ Reply([mtype        |-> RequestVoteResponse,
  //                 mterm        |-> currentTerm[i],
  //                 mvoteGranted |-> grant,
  //                 \* mlog is used just for the `elections' history variable for
  //                 \* the proof. It would not exist in a real implementation.
  //                 mlog         |-> log[i],
  //                 msource      |-> i,
  //                 mdest        |-> j],
  //                 m)
  //       /\ UNCHANGED <<state, currentTerm, candidateVars, leaderVars, logVars>>
}