Raft is a consensus algorithm designed for understandability. Please see the official Raft web page for more information.
Apalache is a tool for TLA+ model checking.
Before running the script, install Apalache according to the instructions.
Run the script:
apalache check --config=MC.cfg MC- Election Safety
- Multiple leaders are not in the same term.
The TLA+ document is originally created by Diego Ongaro, under Creative Commonse Attribution-4.0.
My revision is described in Raft.tla as comments.
Copyright 2014 Diego Ongaro
Copyright 2022 Yuya Shiratori