In paper
vivaLaDifference which shows difference and similarity among VSR, ZAB and Paxos,
3.5 Passive Replication talks about making the generic spec support Primary Order:
"
To guarantee that a decision in slot is based on the
state decided in the prior slot, we add the following
precondition to transition certifySeq:
slot > 1 ⇒ ∃s :
cmd = (s, −) ∧
progrsum[cert] [slot − 1] = 〈rid , (−, (−, −, s))〉
"
* I added square bracket for cert to make it clear
I'm confused with the structure on the right side of formula, the paper says:
A command is "a pair of a client id and an operation to be performed"
A progress summary is a pair <rid , cmd > where rid is the identifier of a round and cmd
is a proposed command or ⊥
So at least cmd matches what it says, but progrsum is not.
Could you help to explain what it should be?
Has anyone tried to translate these code into TLA+?