Page 198 - 《软件学报》2021年第6期

1772 Journal of Software 软件学报 Vol.32, No.6, June 2021

• ClientRequest(i):i 为主节点时,可以响应用户的请求,将用户的命令插入到日志中.
----------------------------------------------------------------------------
BecomeLeader(i)==
/\currentState[i]=LeaderCandidate
/\\E Q\in Quorums:\A q\in Q:(q=i\/syncTrack[i][q]=currentTerm[i])
/\elections′=elections\union
{[eterm6currentTerm[i],
esync6sync[i],
eleader6i,
evotes6Q,
evoterLog6{log[k]:k\in Q},
elog6log[i]]}
/\sync′=[sync EXCEPT ![i]=currentTerm[i]]
/\currentState′=[currentState EXCEPT ![i]=Leader]
/\log′=[log EXCEPT ![i]=[n\in Index6
IF log[i][n].term=sync[i] THEN
log[i][n].committed6TRUE]
ELSE log[i][n]]]
/\UNCHANGED 〈〈messages,currentTerm,votedFor,end,syncTrack,halfElections〉〉

ClientRequest(i,v)==
LET nextIndex==logTail(log[i])+1
entry==[term6currentTerm[i],
date6currentTerm[i],
value6v,
committed6FALSE]
IN
/\currentState[i]=Leader
/\log′=[log EXCEPT ![i][nextIndex]=entry]
/\UNCHANGED 〈〈messages,serverVars,electionVars,syncTrack〉〉
-------------------------------------------------------------------------------------------------
Next 定义了次态关系.Spec 定义了完整的行为规约.
---------------------------------------------------------------------------------------
Next==\/\E i\in Server:Restart(i)
\/\E i\in Server:Timeout(i)
\/\E i\in Server:UpdateTerm(i)
\/\E i\in Server:RequestVote(i)
\/\E i\in Server:HandleRequestVoteRequest(i)
\/\E i\in Server:BecomeLeaderCandidate(i)
\/\E i\in Server:BecomeLeader(i)
\/\E i\in Server,v\in Value:ClientRequest(i,v)