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

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

Have you tried emailing the authors with this question?

Andrew Helwer

On Friday, December 6, 2024 at 4:06:37 PM UTC-5 Anthony Lee wrote:

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/97d0501f-5edd-4d06-998f-9fe29eeea16an%40googlegroups.com.