fpaxos-tlaplus

TLA+ specification of Flexible Paxos

https://github.com/fpaxos/fpaxos-tlaplus

Science Score: 44.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • CITATION.cff file
    Found CITATION.cff file
  • codemeta.json file
    Found codemeta.json file
  • .zenodo.json file
    Found .zenodo.json file
  • DOI references
  • Academic publication links
  • Academic email domains
  • Institutional organization owner
  • JOSS paper metadata
  • Scientific vocabulary similarity
    Low similarity (4.8%) to scientific vocabulary

Keywords

distributed-algorithms paxos tla tla-specification
Last synced: 6 months ago · JSON representation ·

Repository

TLA+ specification of Flexible Paxos

Basic Info
Statistics
  • Stars: 40
  • Watchers: 2
  • Forks: 1
  • Open Issues: 0
  • Releases: 0
Topics
distributed-algorithms paxos tla tla-specification
Created over 9 years ago · Last pushed over 2 years ago
Metadata Files
Readme License Citation

README.md

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.

Owner

  • Name: Flexible Paxos
  • Login: fpaxos
  • Kind: organization

Revisiting quorum intersection for Paxos

Citation (CITATION.cff)

cff-version: 1.2.0
title: TLA+ Specification of Flexible Paxos
message: >-
  If you use this specification, please cite it using the
  metadata from this file.
type: software
authors:
  - given-names: Heidi
    family-names: Howard
repository-code: 'https://github.com/fpaxos/fpaxos-tlaplus'
license: MIT
preferred-citation:
  type: conference-paper
  authors:
  - family-names: Howard
    given-names: Heidi
  - family-names: Malkhi
    given-names: Dahlia
  - family-names: Spiegelman
    given-names: Alexander
  doi: "10.4230/LIPIcs.OPODIS.2016.25"
  conference:
    name: "20th International Conference on Principles of Distributed Systems (OPODIS 2016)"
  month: 9
  title: "Flexible Paxos: Quorum Intersection Revisited"
  volume: 70
  year: 2017

GitHub Events

Total
  • Watch event: 1
Last Year
  • Watch event: 1

Dependencies

.github/workflows/apalache.yml actions
  • actions/checkout v3 composite
  • actions/setup-java v3 composite
.github/workflows/tlatools.yml actions
  • actions/checkout v3 composite
  • actions/upload-artifact v3 composite