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

Re: [tlaplus] Confusions about setting variant to NAT then getting it overriden



So I am wondering what the reasons are that to design `Ballot` in this way. Why not just setting it something like `Ballot == 0..10` in the first place?
>> Because nowhere in https://lamport.azurewebsites.net/pubs/paxos-simple.pdf does the paper
say that ballot has to be in 0..10. The paper also doesn't say that it has to be Nat, but Nat is
(1) a totally ordered set (therefore any pair of elements are comparable---something that Paxos wants),
(2) infinite (so, more general than 0..10). This is the main reason. If the authors had written 0..10 to begin with,
     I would assume that this specification/algorithm does not handle ballot 11 and may therefore be useless to me.
(3) defined in Naturals along with operators like >, <, etc and their arithmetic. So, we do not have to specify that.

So Nat serves the purpose as a high level abstraction of Ballots (but not as a practical executable one because
if Ballots is Nat, then the first conjunct of Phase2a would itself require consensus). Note that 0..10 satisfies (1) and (3)
but not (2).

Also, while with Nat we cannot do model checking, we can do theorem proving.
As is done in https://github.com/tlaplus/v1-tlapm/blob/master/examples/paxos/Paxos.tla
and https://github.com/sachand/HistVar
But that requires much more human effort than model checking.

Hope this helps,
Saksham


On Fri, Aug 23, 2019 at 11:29 AM Yanchen SHI <shiyc@xxxxxxxxxx> wrote:
Hi,

Recently I were viewing Paxos implementation in https://github.com/tlaplus/Examples/blob/master/specifications/Paxos/Paxos.tla

, in which there is a statement as
`Ballot == Nat`.

Since `Nat` is non-enumerable, the toolbox would raise an error if I didn't override `Ballot`.

So I am wondering what the reasons are that to design `Ballot` in this way. Why not just setting it something like `Ballot == 0..10` in the first place?

Thanks!

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/271200e7-db86-44dc-aa35-0ad64dabbac2%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJSuO-9Ce3hxU9v2UZ%3DrJBO13-YW3h-ihyfjTS_%2BkbzQUC9RKQ%40mail.gmail.com.