[tlaplus] How to translate this piece of pseudocode to TLA+?

[Anthony Lee <anthonynlee@xxxxxxxxx>]

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/407c8e3e-d260-47c9-9b32-27c2e1ed2b1dn%40googlegroups.com.