How to translate this piece of pseudocode to TLA+?

[Anthony Lee]

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+?

[Anthony Lee]

For anyone who has interest in this I added answer here: https://www.reddit.com/r/compsci/comments/1iiwezh/a_question_about_paper_vive_la_diff_erence_paxos/.

In short for Passive Replication the cmd is no longer <client, op> (the one mentioned in paper for Active Replication) but < oldState, <cmd, result, newState> >.