История

Markus Alexander Kuppe 483d1c10a0 Remove unused variable votesSent. (#4439 )		2022-11-01 21:50:22 +00:00
..
.gitignore	Another subset of small improvements of TLA+ specification listed in #4264 (#4411 )	2022-10-31 23:34:10 +00:00
MCccfraft.cfg	Rename currentConfigurations to configurations and model value as `[ Servers -> [ Nat -> SUBSET Servers ] ]` instead of `[ Servers -> Seq(<<Nat, SUBSET Server>>)`. (#4438 )	2022-11-01 21:30:55 +00:00
MCccfraft.tla	Another subset of small improvements of TLA+ specification listed in #4264 (#4411 )	2022-10-31 23:34:10 +00:00
MCccfraftWithReconfig.tla	Another subset of small improvements of TLA+ specification listed in #4264 (#4411 )	2022-10-31 23:34:10 +00:00
README.md	TLA+ at the push of a button (#4420 )	2022-10-28 11:17:15 +01:00
ccfraft.tla	Remove unused variable votesSent. (#4439 )	2022-11-01 21:50:22 +00:00
download_or_update_tla.sh	Subset of small improvements of TLA+ specification listed in #4264 (#4363 )	2022-10-24 19:57:17 +01:00
tlc.sh	Subset of small improvements of TLA+ specification listed in #4264 (#4363 )	2022-10-24 19:57:17 +01:00

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.

If your Github account supports it, you can also interact with this specification using codespaces: