Confusions about setting variant to NAT then getting it overriden

[Yanchen SHI]

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!

[Saksham Chand]

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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/271200e7-db86-44dc-aa35-0ad64dabbac2%40googlegroups.com.