- TLA+ specification's authors: Leslie Lamport
- Pluscal specification's authors: Giuliano Losa
- Pluscal files
- First, Lamport wrote the TLA+ specifications in his paper. Because we could not find Lamport's TLA files, we translated his writing in PDF format to TLA+ and pushed them in this repository. Later, Losa wrote another specification for this algorithm in Pluscal.
- Original paper: Gafni, Eli, and Leslie Lamport. Disk paxos. Distributed Computing 16.1 (2003): 1-20.
- Extended modules: Int
- Computation models: crashes, inaccessibility
- Some properties checked with TLC: SynodSpec