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

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

valid=={e\in entries:e[2][1]/=−1}
IN IF valid={⋅} THEN −1 ELSE Max({e[1]:e\in valid})
Merge(b)==/\\E Q\in Quorums:
/\\A a\in Q:\E m\in 1bMsgs(b,Q):m[3]=a
/\leaderVote′=[leaderVote EXCEPT ![b]=[i\in Instances6
IF (/\i\in 0..lastInstance(b,Q)
/\leaderVote[b][i][1]=−1)
THEN 〈〈b,MaxVote(b,i,Q)〉〉
ELSE leaderVote[b][i]]]
/\UNCHANGED 〈〈vote,ballot,1amsgs,1bmsgs,2amsgs〉〉

Propose(b,i)==/\leaderVote[b][i][1]=−1
/\\E Q\in Quorums:
/\\A a\in Q:\E m\in 1bMsgs(b,Q):m[3]=a
/\LET maxV==MaxVote(b,i,Q)
safe==IF maxV/=Nil THEN {maxV} ELSE
Value \cup {Nil}
IN \E v\in safe: leaderVote′=[leaderVote EXCEPT
![b][i]=〈〈b,v〉〉]
/\UNCHANGED 〈〈vote,ballot,1amsgs,1bmsgs,2amsgs〉〉

Phase2a(b,i)==
/\leaderVote[b][i][1]=b
/\2amsgs′=2amsgs\cup {〈〈b,i,leaderVote[b][i]〉〉}
/\UNCHANGED 〈〈ballot,vote,leaderVote,1amsgs,1bmsgs〉〉

Vote(a,b,i)==
/\ballot[a]\leq b
/\ballot′=[ballot EXCEPT ![a]=b]
/\\E m\in 2amsgs:
/\m[2]=i/\m[1]=b
/\vote′=[vote EXCEPT ![a][i][b]=m[3][2]]
/\UNCHANGED 〈〈leaderVote,1amsgs,1bmsgs,2amsgs〉〉
-----------------------------------------------------------------------------------------------------------------
Next 定义了次态关系,Spec 定义了完整的行为规约.
-----------------------------------------------------------------------------------------------------
Next==
\/\E a\in Acceptors,b\in Ballots:IncreaseBallot(a,b)
\/\E b\in Ballots:Phase1a(b)
\/\E a\in Acceptors,b\in Ballots:Phase1b(a,b)
\/\E b\in Ballots:Merge(b)
\/\E b\in Ballots,i\in Instances:Propose(b,i)