Verify some old or new concepts/models/algorithms/ideas of distributed/discrete systems using TLA+.
| Project | Description |
|---|---|
| paxos-eb0 | A basic Paxos with excluded ballot 0 optimization |
| multi-paxos-eb0 | A Multi-Paxos implementation composed by paxos-eb0 instances |
| percolator | The Google's distributed transaction algorithm built on Bigtable |
| sequencer | A distributed sequence generator |
| simplified-fast-paxos | A simplified Fast Paxos implementation |
| isolation-models | Transaction Isolation Models |
What's Next:
- Github CI
- Separate model from specification
- Modeling Transaction Isolation Levels
- Add Liveness Invariants
- Distributed Transaction On Sql Databases
- HLC and Quorum Intersection
In short, Unicode-based has better readability rather than plain ASCII.
In the plain ASCII, many other projects will generate a styled pdf with the TLA+ files for readability, there are some disadvantages:
- pdf files don't work well with git
- (pdf)Latex dependency
- more efforts to sync the TLA+ files and pdf files
Please read: https://github.com/tlaplus/tlaplus-standard/tree/main/unicode