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

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


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?


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.