[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: ASCII version of TLA+ spec for Paxos?



Found it. With other useful examples. Thanks!

On Thursday, October 16, 2014 1:54:47 AM UTC-7, Leslie Lamport wrote:
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 :)