Comment modéliser Paxos dans TLA + Toolbox?

Question

J'essaie de modéliser Paxos (Paxos example) dans TLA + Toolbox (toolbox). Quels numéros dois-je mettre dans le modèle pour le faire fonctionner? Ou existe-t-il d'autres façons de confirmer cet algorithme dans cette boîte à outils?

base sur ce 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 

J'essaie de tels chiffres:

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

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

Valeur < - [0,1];

mais j'obtiens l'erreur ArrayIndexOutOfBoundsException.

Answer 1

Il y a quelques problèmes avec votre modèle:

1. Pour spécifier un ensemble, vous devez utiliser des accolades, donc Acceptor < - {} 11,12,13,14,15.

2. Le quorum doit être un ensemble d'ensembles d'accepteurs, par ex. Quorum < - {{11,12,13}, {12,13,14}}.