[tlaplus] How to understand onTimeOutxxx in this TenderMint spec's?

[Anthony Lee <anthonynlee@xxxxxxxxx>]

In paper "The latest gossip on BFT consensus"  Tendermint algorithm is descried in pseudocode, and here is a TLA+ spec for it.

I'm confused in how the timer for step Propose/Prevote/PreCommit is scheduled.

OnTimeoutPropose action condition shows that when step is propose but Proposer is not p

then it is timeout. Each round has its own proposer, so I searched to see where a new round can be started, I found that UponQuorumOfPrecommitsAny(p) and OnRoundCatchup(p) trigger StartRound(p,r);

For UponQuorumOfPrecommitsAny, there is comment saying that it should be called in onTimeoutPrecommit, but there is no onTimeoutPrecommit in the TLA.

 I don't understand how timeout is implemented in this TLA and why there is no need to define onTimeoutPrevote or onTimeoutPrecommit.

Please help to explain.

Thanks.

Anthony

 

-- 
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/1bd42a42-9e22-408f-8c53-293ce699f136n%40googlegroups.com.