Search code examples
modelingpaxostla+

How to model Paxos in TLA+ Toolbox?

I try to model Paxos (Paxos example) in TLA+ Toolbox (toolbox). What numbers should I put in the model to make it work? Or are there other ways a confirmation of this algorithm in this toolbox?

Base on this code:

CONSTANT Value,     \* The set of choosable values.
     Acceptor,  \* A set of processes that will choose a value.
     Quorum     \* The set of "quorums", where a quorum" is a 
                \*   "large enough" set of acceptors

I try numbers like this:

Acceptor <- [11,12,13,14,15];

Quorum <- [11,12,13,14,15,16,17,18,19];

Value <- [0,1];

but I get ArrayIndexOutOfBoundsException error.

Solution

  • There are a few issues with your model:

    1. For specifying a set, you should use curly braces, so Acceptor <- {11,12,13,14,15}.

    2. Quorum should be a set of sets of acceptors, e.g. Quorum <- {{11,12,13},{12,13,14}}.