TLAPlusExamples/specifications/diskpaxos at master · sr-murthy/TLAPlusExamples

Name	Name	Last commit message	Last commit date
parent directory ..
DiskSynod.tla	DiskSynod.tla
HDiskSynod.tla	HDiskSynod.tla
MC_HDiskSynod.cfg	MC_HDiskSynod.cfg
MC_HDiskSynod.tla	MC_HDiskSynod.tla
README.md	README.md
Synod.tla	Synod.tla
manifest.json	manifest.json

Name

Last commit message

Last commit date

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

Navigation Menu