[tlaplus] Re: Model-checking the Raft spec

["A. Jesse Jiryu Davis" <jesse@xxxxxxxxxxxxxxx>]

There are obvious model-checking tricks like a SYMMETRY declaration, and additional state constraints, that I hope someone has already done for me. It looks like the current spec's state space is infinite.

On Thu, May 16, 2024 at 9:57 AM A. Jesse Jiryu Davis <jesse@xxxxxxxxxxxxxxx> wrote:

Hello! I was curious about the Raft TLA+ spec. I'd like to model-check it, enhance it with leader leases, and model-check it again. First step: model check Diego Ongaro's original spec.

In the repository README, Ongaro encourages us to use a version in an open pull request instead of the main-branch version:

https://github.com/ongardie/raft.tla

... but neither version has any invariants or temporal properties, and there's no config file. I suppose Ongaro just used this spec for description and perhaps proof, not model-checking.

So, has anyone model-checked a version of this Raft spec? Any tips or public code?

-- 
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 on the web visit https://groups.google.com/d/msgid/tlaplus/CAFRUCtYPwzPtuU8%3Dyzagvd3hg0%2BiMHPR%2Btork0x_6qZcygHyZA%40mail.gmail.com.