If you download TLAPS (the TLA+ prover), you should find an examples directory containing a paxos directory that contains the spec (including a TLAPS-checked proof that it satisfies consensus).Leslie
On Wednesday, October 15, 2014 6:39:57 PM UTC-7, M T wrote:I am learning TLA+. Does anyone know where I can find an ASCII version of TLA+ spec for the original Paxos?(not fast Paxos) I heard it is only 40-line. I tried web searches but was not able to find one.Or I can use it as an exercise too :)