TLA+ Specification of Flexible Paxos

This repository contains the TLA+ specification and TLC model checking configuration for single shot Flexible Paxos.

Instructions for installing and setting up TLA+ are available elsewhere. These instructions assume that you are running TLA+ from the command line using tla-bin.

You can model check this specification by cloning this directory and running:

$ tlc -config MCFPaxos.cfg MCFPaxosTwoAcc.tla

By editing MCFPaxosTwoAcc.tla, you can modify the configuration to test different models. For example, you might wish to try changing the number of acceptors, how quorums are composed or the number of ballots.

This TLA+ specification is derived from Leslie Lamport's Paxos specification from TLA+ Examples.