История

Markus Alexander Kuppe 3000670a64 Allow sending empty AppendEntries message. (#5150 )		2023-03-30 07:38:18 +01:00
..
.gitignore	Bias random simulation to forward-progress actions. (#4658 )	2022-12-01 18:21:49 +00:00
MCccfraft.cfg	A pending node that becomes part of any configuration immediately transitions to Follower state. (#4928 )	2023-02-03 17:26:49 +00:00
MCccfraft.tla	(Raft) Node without configuration can become primary/leader #4806 (#4807 )	2023-02-27 08:14:43 +00:00
MCccfraftWithReconfig.tla	(Raft) Node without configuration can become primary/leader #4806 (#4807 )	2023-02-27 08:14:43 +00:00
README.md	Fix bug fetching deps for TLA and call during dev container setup (#4523 )	2022-11-14 12:08:03 +00:00
SIMCoverageccfraft.R	Bias random simulation to forward-progress actions. (#4658 )	2022-12-01 18:21:49 +00:00
SIMCoverageccfraft.cfg	Bias random simulation to forward-progress actions. (#4658 )	2022-12-01 18:21:49 +00:00
SIMCoverageccfraft.tla	Bias random simulation to forward-progress actions. (#4658 )	2022-12-01 18:21:49 +00:00
SIMccfraft.cfg	A pending node that becomes part of any configuration immediately transitions to Follower state. (#4928 )	2023-02-03 17:26:49 +00:00
SIMccfraft.tla	Nodes may not rejoin a configuration. (#4868 )	2023-01-30 17:35:12 +00:00
ccfraft.tla	Allow sending empty AppendEntries message. (#5150 )	2023-03-30 07:38:18 +01:00
install_deps.py	Install wget if install_deps.py script is executed in default codespace. (#4802 )	2023-01-06 10:15:28 +00:00
tlc.sh	Subset of small improvements of TLA+ specification listed in #4264 (#4363 )	2022-10-24 19:57:17 +01:00

README.md

TLA+ specification

This directory contains a formal specification of CCF's variant of Raft in TLA+. For more information, please refer to the CCF documentation: https://microsoft.github.io/CCF/main/architecture/raft_tla.html.

You can also interact with this specification using codespaces:

You can also manually run install_deps.py to install or update the dependencies required to interact with the spec. Run with --help to see all available options