All Projects → fpaxos → fpaxos-tlaplus

fpaxos / fpaxos-tlaplus

Licence: other
TLA+ specification of Flexible Paxos

Programming Languages

TLA
29 projects

Projects that are alternatives of or similar to fpaxos-tlaplus

Distributed-Algorithms
利用 Go 语言实现多种分布式算法
Stars: ✭ 53 (+65.63%)
Mutual labels:  paxos, distributed-algorithms
tezedge-specification
TLA+ specs and models for the TezEdge node's p2p overlay network, shell, and consensus
Stars: ✭ 19 (-40.62%)
Mutual labels:  tla-specification
oceanbase
OceanBase is an enterprise distributed relational database with high availability, high performance, horizontal scalability, and compatibility with SQL standards.
Stars: ✭ 4,466 (+13856.25%)
Mutual labels:  paxos
kshaka
Kshaka is a Go implementation of the CASPaxos consensus protocol.
Stars: ✭ 23 (-28.12%)
Mutual labels:  paxos
paper
Computer Foundations Practices
Stars: ✭ 17 (-46.87%)
Mutual labels:  paxos
Raft-Paxos-Sample
MIT6.824实现分布式一致性算法——Raft&Paxos
Stars: ✭ 37 (+15.63%)
Mutual labels:  paxos
paxakos
Rust implementation of Paxos consensus algorithm
Stars: ✭ 79 (+146.88%)
Mutual labels:  paxos
paxoid
Paxos based masterless ID/Sequence generator.
Stars: ✭ 20 (-37.5%)
Mutual labels:  paxos
paxos-rs
Paxos implementation in Rust
Stars: ✭ 66 (+106.25%)
Mutual labels:  paxos
Awesome Consensus
Awesome list for Paxos and friends
Stars: ✭ 1,619 (+4959.38%)
Mutual labels:  paxos
Awesome Distributed Systems
A curated list to learn about distributed systems
Stars: ✭ 7,263 (+22596.88%)
Mutual labels:  paxos
Translations
🐼 Chinese translations for classic IT resources
Stars: ✭ 6,074 (+18881.25%)
Mutual labels:  paxos
Dragonboat
Dragonboat is a high performance multi-group Raft consensus library in pure Go.
Stars: ✭ 3,983 (+12346.88%)
Mutual labels:  paxos
epaxos
A pluggable implementation of the Egalitarian Paxos Consensus Protocol
Stars: ✭ 39 (+21.88%)
Mutual labels:  paxos
Distributed-Data-Structures
[GSoC] Distributed Data Structures - Collections Framework for Chapel language
Stars: ✭ 13 (-59.37%)
Mutual labels:  distributed-algorithms
CommunityModules
TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
Stars: ✭ 167 (+421.88%)
Mutual labels:  tla-specification

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 MCFPaxos.tla

By editing MCFPaxos.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.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].