[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Model-checking the Raft spec

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:


... 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.