From 58906abfea1370c780c629b926e68370d87777c1 Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Sun, 14 Jan 2024 17:32:39 -0500 Subject: [PATCH] Subjected README.md spec table to CI validation Simplified & expanded spec table Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/scripts/check_markdown_table.py | 201 ++++++++++++++++ .github/scripts/format_markdown_table.py | 74 ++++++ .github/scripts/requirements.txt | 5 +- .github/workflows/CI.yml | 5 + README.md | 291 ++++++++++++----------- manifest-schema.json | 2 +- manifest.json | 84 ++++--- 7 files changed, 484 insertions(+), 178 deletions(-) create mode 100644 .github/scripts/check_markdown_table.py create mode 100644 .github/scripts/format_markdown_table.py diff --git a/.github/scripts/check_markdown_table.py b/.github/scripts/check_markdown_table.py new file mode 100644 index 00000000..0b6bfd37 --- /dev/null +++ b/.github/scripts/check_markdown_table.py @@ -0,0 +1,201 @@ +""" +Validates the spec table in README.md, ensuring it matches manifest.json. +""" + +from argparse import ArgumentParser +from dataclasses import dataclass +from os.path import normpath +from typing import Any, Set +import tla_utils +import mistletoe +from mistletoe.block_token import Table + +@dataclass +class TableRow: + name : str + path : str + authors : Set[str] + beginner : bool + proof : bool + pcal : bool + tlc : bool + apalache : bool + underlying : Any + +columns = ['name', 'authors', 'beginner', 'proof', 'pcal', 'tlc', 'apalache'] + +def get_column(row, index): + ''' + Gets the cell of the given column in the given row. + ''' + return row.children[columns.index(index)].children[0] + +def is_column_empty(row, index): + ''' + Whether the given column cell is empty. + ''' + return not any(row.children[columns.index(index)].children) + +def get_link_text(link): + ''' + Gets the text in a markdown link. + ''' + return link.children[0].content + +def from_markdown(record): + ''' + Transforms a parsed markdown table row into a normalized form. + ''' + return TableRow( + get_link_text(get_column(record, 'name')), + get_column(record, 'name').target, + set(name.strip() for name in get_column(record, 'authors').content.split(',')), + not is_column_empty(record, 'beginner'), + not is_column_empty(record, 'proof'), + not is_column_empty(record, 'pcal'), + not is_column_empty(record, 'tlc'), + not is_column_empty(record, 'apalache'), + record + ) + +def from_json(spec): + ''' + Transforms JSON from the manifest into a normalized form. + ''' + return TableRow( + spec['title'], + spec['path'], + set(spec['authors']), + 'beginner' in spec['tags'], + any([module for module in spec['modules'] if 'proof' in module['features']]), + any([module for module in spec['modules'] if 'pluscal' in module['features']]), + any([model for module in spec['modules'] for model in module['models'] if model['mode'] != 'symbolic']), + any([model for module in spec['modules'] for model in module['models'] if model['mode'] == 'symbolic']), + spec + ) + +parser = ArgumentParser(description='Validates the spec table in README.md against the manifest.json.') +parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) +parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True) +args = parser.parse_args() + +manifest = tla_utils.load_json(normpath(args.manifest_path)) + +readme = None +with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file: + readme = mistletoe.Document(readme_file) + +spec_table = next((child for child in readme.children if isinstance(child, Table))) + +table_specs = dict([(record.path, record) for record in [from_markdown(node) for node in spec_table.children]]) +manifest_specs = dict([(record.path, record) for record in [from_json(spec) for spec in manifest['specifications']]]) + +# Checks that set of specs in manifest and table are equivalent +success = True +specs_not_in_table = manifest_specs.keys() - table_specs.keys() +if any(specs_not_in_table): + success = False + print('ERROR: specs in manifest.json missing from README.md table:\n' + '\n'.join(specs_not_in_table)) +specs_not_in_manifest = table_specs.keys() - manifest_specs.keys() +if any(specs_not_in_manifest): + success = False + print('ERROR: specs in README.md table missing from manifest.json:\n' + '\n'.join(specs_not_in_manifest)) + +# Join the spec records together for comparison +specs = [ + (manifest_spec, table_specs[path]) + for (path, manifest_spec) in manifest_specs.items() + if path in table_specs +] + +# Ensure spec names are identical +different_names = [ + (manifest_spec.path, manifest_spec.name, table_spec.name) + for (manifest_spec, table_spec) in specs + if manifest_spec.name != table_spec.name +] +if any(different_names): + success = False + print('ERROR: spec names in README.md table differ from manifest.json:') + for path, json, md in different_names: + print(f'Spec {path} has name {json} in manifest and {md} in README') + +# Ensure spec authors are identical +different_authors = [ + (manifest_spec.path, manifest_spec.authors, table_spec.authors) + for (manifest_spec, table_spec) in specs + if manifest_spec.authors != table_spec.authors +] +if any(different_authors): + success = False + print('ERROR: spec author(s) in README.md table differ from manifest.json:') + for path, json, md in different_authors: + print(f'Spec {path} has author(s) {json} in manifest.json and {md} in README.md') + +# Ensure Beginner flag is correct +different_beginner_flag = [ + (manifest_spec.path, manifest_spec.beginner, table_spec.beginner) + for (manifest_spec, table_spec) in specs + if manifest_spec.beginner != table_spec.beginner +] +if any(different_beginner_flag): + success = False + print('ERROR: Beginner flags in README.md table differ from tags in manifest.json:') + for path, json, md in different_beginner_flag: + print(f'Spec {path} is missing a Beginner ' + ('tag in manifest.json' if md else 'flag in README.md')) + +# Ensure TLAPS proof flag is correct +different_tlaps_flag = [ + (manifest_spec.path, manifest_spec.proof, table_spec.proof) + for (manifest_spec, table_spec) in specs + if manifest_spec.proof != table_spec.proof +] +if any(different_tlaps_flag): + success = False + print('ERROR: Proof flags in README.md table differ from features in manifest.json:') + for path, json, md in different_tlaps_flag: + print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a proof flag in README.md table') + +# Ensure PlusCal flag is correct +different_pcal_flag = [ + (manifest_spec.path, manifest_spec.pcal, table_spec.pcal) + for (manifest_spec, table_spec) in specs + if manifest_spec.pcal != table_spec.pcal +] +if any(different_pcal_flag): + success = False + print('ERROR: PlusCal flags in README.md table differ from features in manifest.json:') + for path, json, md in different_pcal_flag: + print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a PlusCal flag in README.md table') + +# Ensure TLC flag is correct +different_tlc_flag = [ + (manifest_spec.path, manifest_spec.tlc, table_spec.tlc) + for (manifest_spec, table_spec) in specs + if manifest_spec.tlc != table_spec.tlc +] +if any(different_tlc_flag): + success = False + print('ERROR: TLC Model flags in README.md table differ from model records in manifest.json:') + for path, json, md in different_tlc_flag: + print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a TLC Model flag in README.md table') + +# Ensure Apalache flag is correct +different_apalache_flag = [ + (manifest_spec.path, manifest_spec.apalache, table_spec.apalache) + for (manifest_spec, table_spec) in specs + if manifest_spec.apalache != table_spec.apalache +] +if any(different_apalache_flag): + success = False + print('ERROR: Apalache Model flags in README.md table differ from model records in manifest.json:') + for path, json, md in different_tlc_flag: + print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' an Apalache Model flag in README.md table') + +if success: + print('SUCCESS: manifest.json concords with README.md table') + exit(0) +else: + print('ERROR: differences exist between manifest.json and README.md table; see above error messages') + exit(1) + diff --git a/.github/scripts/format_markdown_table.py b/.github/scripts/format_markdown_table.py new file mode 100644 index 00000000..2b1bb41d --- /dev/null +++ b/.github/scripts/format_markdown_table.py @@ -0,0 +1,74 @@ +""" +Format or modify the spec table in README.md. This is a utility script kept +around for occasional modifications to the README.md table(s), such as +swapping/deleting columns or transforming each row element. By doing a simple +round-trip without any transformation the tables will also be formatted +nicely. +""" + +from argparse import ArgumentParser +from os.path import normpath +import mistletoe +from mistletoe.block_token import Table +from mistletoe.markdown_renderer import MarkdownRenderer + +parser = ArgumentParser(description='Formats or modifies the spec table in README.md.') +parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True) +args = parser.parse_args() + +readme = None +with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file: + readme = mistletoe.Document(readme_file) + +columns = ['name', 'authors', 'beginner', 'proof', 'tlc', 'pcal', 'apalache'] + +def get_column(row, index): + ''' + Gets the cell of the given column in the given row. + ''' + return row.children[columns.index(index)].children[0] + +def remove_column(table, col_index): + ''' + Removes the column of the given index from the table. + ''' + index = columns.index(col_index) + table.header.children.pop(index) + table.column_align.pop(index) + for row in table.children: + row.children.pop(index) + +def blank_column(table, col_index): + ''' + Removes all data in the given column. + ''' + index = columns.index(col_index) + for row in table.children: + row.children[index].children = [] + +def swap_columns(table, first_col_index, second_col_index): + ''' + Swaps two columns in a table. + ''' + first = columns.index(first_col_index) + second = columns.index(second_col_index) + table.header.children[second], table.header.children[first] = table.header.children[first], table.header.children[second] + table.column_align[second], table.column_align[first] = table.column_align[first], table.column_align[second] + for row in table.children: + row.children[second], row.children[first] = row.children[first], row.children[second] + + +def format_table(table): + ''' + All table transformations should go here. + ''' + return + +table = next((child for child in readme.children if isinstance(child, Table))) +format_table(table) + +# Write formatted markdown to README.md +with open(normpath(args.readme_path), 'w', encoding='utf-8') as readme_file: + with MarkdownRenderer() as renderer: + readme_file.write(renderer.render(readme)) + diff --git a/.github/scripts/requirements.txt b/.github/scripts/requirements.txt index 7dbb4656..aa60daba 100644 --- a/.github/scripts/requirements.txt +++ b/.github/scripts/requirements.txt @@ -1,3 +1,4 @@ -jsonschema == 4.17.3 -tree-sitter==0.20.1 +jsonschema == 4.20.0 +tree-sitter==0.20.4 +mistletoe==1.2.1 diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 8a2eb8bf..df6bfab4 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -134,6 +134,11 @@ jobs: python $SCRIPT_DIR/check_manifest_features.py \ --manifest_path manifest.json \ --ts_path deps/tree-sitter-tlaplus + - name: Check README spec table + run: | + python $SCRIPT_DIR/check_markdown_table.py \ + --manifest_path manifest.json \ + --readme_path README.md - name: Parse all modules run: | python $SCRIPT_DIR/parse_modules.py \ diff --git a/README.md b/README.md index 3683ec65..b9beacc7 100644 --- a/README.md +++ b/README.md @@ -8,177 +8,184 @@ It serves as: - a diverse corpus facilitating development & testing of TLA+ language tools - a collection of case studies in the application of formal specification in TLA+ -All TLA+ specs can be found in the `specifications` directory. -A central manifest of specs with descriptions and accounts of their various models and features can be found in the [`manifest.json`](manifest.json) file. -Beginner-friendly specs can be found by searching for the "beginner" tag in that file. -Similarly, PlusCal specs can be found by searching for the "pluscal" feature, or "proof" for specs with proofs. +All TLA+ specs can be found in the [`specifications`](specifications) directory. +The table below lists all specs and their features, such as whether they are suitable for beginners or use PlusCal. +The [`manifest.json`](manifest.json) file is the source of truth for this table, and is a detailed human- & machine-readable description of the specs & their models. +Its schema is [`manifest-schema.json`](manifest-schema.json). +All specs in this repository are subject to CI validation to ensure quality. -## List of Examples +## Examples Included Here +Here is a list of specs included in this repository, with links to the relevant directory and flags for various features: +| Name | Author(s) | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache | +| --------------------------------------------------------------------------------------------------- | ------------------------------------------ | :------: | :---------: | :-----: | :-------: | :------: | +| [Learn TLA⁺ Proofs](specifications/LearnProofs) | Andrew Helwer | ✔ | ✔ | ✔ | ✔ | | +| [Teaching Concurrency](specifications/TeachingConcurrency) | Leslie Lamport | ✔ | ✔ | ✔ | | | +| [Boyer-Moore Majority Vote](specifications/Majority) | Stephan Merz | ✔ | ✔ | | ✔ | | +| [Proof x+x is Even](specifications/sums_even) | Stephan Merz | ✔ | ✔ | | | | +| [The N-Queens Puzzle](specifications/N-Queens) | Stephan Merz | ✔ | | ✔ | ✔ | | +| [The Dining Philosophers Problem](specifications/DiningPhilosophers) | Jeff Hemphill | ✔ | | ✔ | ✔ | | +| [The Car Talk Puzzle](specifications/CarTalkPuzzle) | Leslie Lamport | ✔ | | | ✔ | | +| [The Die Hard Problem](specifications/DieHard) | Leslie Lamport | ✔ | | | ✔ | | +| [The Prisoners & Switches Puzzle](specifications/Prisoners) | Leslie Lamport | ✔ | | | ✔ | | +| [Specs from Specifying Systems](specifications/SpecifyingSystems) | Leslie Lamport | ✔ | | | ✔ | | +| [The Tower of Hanoi Puzzle](specifications/tower_of_hanoi) | Markus Kuppe, Alexander Niederbühl | ✔ | | | ✔ | | +| [Missionaries and Cannibals](specifications/MissionariesAndCannibals) | Leslie Lamport | ✔ | | | ✔ | | +| [The Coffee Can Bean Problem](specifications/CoffeeCan) | Andrew Helwer | ✔ | | | ✔ | | +| [Stone Scale Puzzle](specifications/Stones) | Leslie Lamport | ✔ | | | | | +| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | | | +| [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | | | +| [Loop Invariance](specifications/LoopInvariance) | Leslie Lamport | | ✔ | ✔ | | | +| [EWD840: Termination Detection in a Ring](specifications/ewd840) | Stephan Merz | | ✔ | | ✔ | | +| [EWD998: Termination Detection in a Ring with Asynchronous Message Delivery](specifications/ewd998) | Stephan Merz, Markus Kuppe | | ✔ | | ✔ | | +| [The Paxos Protocol](specifications/Paxos) | Leslie Lamport | | ✔ | | ✔ | | +| [Asynchronous Reliable Broadcast](specifications/bcastByz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | | | | +| [Distributed Mutual Exclusion](specifications/lamport_mutex) | Stephan Merz | | ✔ | | | | +| [Two-Phase Handshaking](specifications/TwoPhase) | Leslie Lamport, Stephan Merz | | ✔ | | | | +| [Paxos (How to Win a Turing Award)](specifications/PaxosHowToWinATuringAward) | Leslie Lamport | | ✔ | | | | +| [Dijkstra's Mutual Exclusion Algorithm](specifications/dijkstra-mutex) | Leslie Lamport | | | ✔ | ✔ | | +| [The Echo Algorithm](specifications/echo) | Stephan Merz | | | ✔ | ✔ | | +| [The TLC Safety Checking Algorithm](specifications/TLC) | Markus Kuppe | | | ✔ | ✔ | | +| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | | | ✔ | ✔ | | +| [The Slush Protocol](specifications/SlushProtocol) | Andrew Helwer | | | ✔ | ✔ | | +| [Minimal Circular Substring](specifications/LeastCircularSubstring) | Andrew Helwer | | | ✔ | ✔ | | +| [Snapshot Key-Value Store](specifications/KeyValueStore) | Andrew Helwer, Murat Demirbas | | | ✔ | ✔ | | +| [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts) | Stephan Merz | | | ✔ | | | +| [Resource Allocator](specifications/allocator) | Stephan Merz | | | | ✔ | | +| [Transitive Closure](specifications/TransitiveClosure) | Stephan Merz | | | | ✔ | | +| [Sliding Block Puzzle](specifications/SlidingPuzzles) | Mariusz Ryndzionek | | | | ✔ | | +| [Single-Lane Bridge Problem](specifications/SingleLaneBridge) | Younes Akhouayri | | | | ✔ | | +| [Huang's Algorithm](specifications/Huang) | Markus Kuppe | | | | ✔ | | +| [The Knuth-Yao Method](specifications/KnuthYao) | Ron Pressler, Markus Kuppe | | | | ✔ | | +| [EWD 426: Token Stabilization](specifications/ewd426) | Murat Demirbas, Markus Kuppe | | | | ✔ | | +| [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | | | ✔ | | +| [Nano Blockchain Protocol](specifications/NanoBlockchain) | Andrew Helwer | | | | ✔ | | +| [Software-Defined Perimeter](specifications/SDP_Verification) | Luming Dong, Zhi Niu | | | | ✔ | | +| [Simplified Fast Paxos](specifications/SimplifiedFastPaxos) | Lim Ngian Xin Terry, Gaurav Gandhi | | | | ✔ | | +| [Checkpoint Coordination](specifications/CheckpointCoordination) | Andrew Helwer | | | | ✔ | | +| [Finitizing Monotonic Systems](specifications/FiniteMonotonic) | Andrew Helwer | | | | ✔ | | +| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | | | ✔ | | +| [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain | | | | ✔ | | +| [Asynchronous Byzantine Consensus](specifications/aba-asyn-byz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | +| [Folklore Reliable Broadcast](specifications/bcastFolklore) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | +| [The Bosco Byzantine Consensus Algorithm](specifications/bosco) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | +| [Consensus in One Communication Step](specifications/c1cs) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | +| [Condition-Based Consensus](specifications/cbc_max) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | +| [One-Step Consensus with Zero-Degradation](specifications/cf1s-folklore) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | +| [Failure Detector](specifications/detector_chan96) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | +| [SWMR Shared Memory Disk Paxos](specifications/diskpaxos) | Leslie Lamport, Giuliano Losa | | | | | | +| [Asynchronous Non-Blocking Atomic Commit](specifications/nbacc_ray97) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | +| [Asynchronous Non-Blocking Atomic Commitment with Failure Detectors](specifications/nbacg_guer01) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | +| [Spanning Tree Broadcast Algorithm](specifications/spanning) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | +| [Transaction Commit Models](specifications/transaction_commit) | Leslie Lamport, Jim Gray | | | | | | +| [Span Tree Exercise](specifications/SpanningTree) | Leslie Lamport | | | | | | +| [The Cigarette Smokers Problem](specifications/CigaretteSmokers) | Mariusz Ryndzionek | | | | | | +| [Conway's Game of Life](specifications/GameOfLife) | Mariusz Ryndzionek | | | | | | +| [Chameneos, a Concurrency Game](specifications/Chameneos) | Mariusz Ryndzionek | | | | | | +| [TLA⁺ Level Checking](specifications/LevelChecking) | Leslie Lamport | | | | | | +| [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | | | | | -| # | Name | Description | Authors | TLAPS Proof? | TLC Model? | Module Dependencies | PlusCal? | Apalache? | -|:---:|-----------------------------------|-------------|---------|:------------:|:----------:|---------------------|:--------:|:---------:| -| 1 | 2PCwithBTM | A modified version of P2TCommit (Gray & Lamport, 2006) | Murat Demirbas | | ✔ | FinSet, Int, Seq | ✔ | | -| 2 | 802.16 | IEEE 802.16 WiMAX Protocols | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou | | ✔ | Int, Seq, FinSet | | | -| 3 | aba-asyn-byz | Asynchronous Byzantine agreement (Bracha & Toueg, 1985) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat | | | -| 4 | acp-nb | Non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | | -| 5 | acp-nb-wrong | Wrong version of the non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | | -| 6 | acp-sb | Non-blocking atomic commitment with a simple broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | | -| 7 | allocator | Specification of a resource allocator | Stephan Merz | | ✔ | FinSet | | | -| 8 | async-comm | The diversity of asynchronous communication (Chevrou et al., 2016) | Florent Chevrou, Aurélie Hurault, Philippe Quéinnec | | ✔ | Nat | | | -| 9 | bcastByz | Asynchronous reliable broadcast - Figure 7 (Srikanth & Toeug, 1987) | Thanh Hai Tran, Igor Konnov, Josef Widder | ✔ | ✔ | Nat, FinSet | | | -| 10 | bcastFolklore | Folklore reliable broadcast - Figure 4 (Chandra and Toueg, 1996) | Thanh Hai Tran, Igor Konnov, Josef Widder | ✔ | ✔ | Nat | | | -| 11 | bosco | One-Step Byzantine asynchronous consensus (Song & Renesse, 2008) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat, FinSet | | | -| 12 | Boulangerie | A variant of the bakery algorithm (Yoram & Patkin, 2015) | Leslie Lamport, Stephan Merz | ✔ | ✔ | Int | ✔ | | -| 13 | byihive | Based on RFC3506 - Requirements and Design for Voucher Trading System (Fujimura & Eastlake) | Santhosh Raju | | ✔ | default theories | | | -| 14 | byzpaxos | Byzantizing Paxos by Refinement (Lamport, 2011) | Leslie Lamport | | ✔ | Int, FinSet | | | -| 15 | c1cs | Consensus in one communication step (Brasileiro et al., 2001) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Int, FinSet | | | -| 16 | Caesar | Multi-leader generalized consensus protocol (Arun et al., 2017) | Giuliano Losa | | ✔ | FinSet, Seq, Int | ✔ | | -| 17 | CarTalkPuzzle | A TLA+ specification of the solution to a nice puzzle. | | | ✔ | Int | | | -| 18 | CASPaxos | An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov) | Tobias Schottdorf | | ✔ | Int, FinSet | | | -| 19 | cbc_max | Condition-based consensus (Mostefaoui et al., 2003) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Int, FinSet | | | -| 20 | cf1s-folklore | One-step consensus with zero-degradation (Dobre & Suri, 2006) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat | | | -| 21 | ChangRoberts | Leader election in a ring (Chang & Roberts, 1979) | Stephan Merz | | ✔ | Nat, Seq | ✔ | | -| 22 | DataPort | Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016) | Geoffrey Biggs, Noriaki Ando | | | Int, Seq | | | -| 23 | detector_chan96 | Chandra and Toueg’s eventually perfect failure detector | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Int, FinSet | | | -| 24 | DieHard | A very elementary example based on a puzzle from a movie | | | ✔ | Nat | | | -| 25 | dijkstra-mutex | Mutual exclusion algorithm (Dijkstra, 1965) | | | ✔ | Int | ✔ | | -| 26 | diskpaxos | Disk Paxos (Gafni & Lamport, 2003) | Leslie Lamport, Giuliano Losa | | ✔ | Int | | | -| 27 | egalitarian-paxos | Leaderless replication protocol based on Paxos (Moraru et al., 2013) | Iulian Moraru | | ✔ | Nat, FinSet | | | -| 28 | ewd840 | Termination detection in a ring (Dijkstra et al., 1986) | Stephan Merz | ✔ | ✔ | Nat | | | -| 70 | ewd998 | Shmuel safra's version of termination detection | Stephan Merz, Markus Kuppe | | ✔ | Int, FinSet | | | -| 29 | fastpaxos | An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006) | Leslie Lamport | | | Nat, FinSet | | | -| 30 | fpaxos | A variant of Paxos with flexible quorums (Howard et al., 2017) | Heidi Howard | | ✔ | Int | | | -| 31 | HLC | Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014) | Murat Demirbas | | ✔ | Int | ✔ | | -| 32 | L1 | Data center network L1 switch protocol, only PDF files (Thacker) | Tom Rodeheffer | | | FinSet, Nat, Seq | | | -| 33 | lamport_mutex | Mutual exclusion (Lamport, 1978) | Stephan Merz | ✔ | ✔ | Nat, Seq | | | -| 34 | leaderless | Leaderless generalized-consensus algorithms (Losa, 2016) | Giuliano Losa | | ✔ | FinSet, Int, Seq | ✔ | | -| 35 | losa_ap | The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018) | Giuliano Losa | | ✔ | FinSet, Nat, Seq | ✔ | | -| 36 | losa_rda | Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014) | Giuliano Losa | | | FinSet, Nat, Seq | | | -| 37 | m2paxos | Multi-leader consensus protocols (Peluso et al., 2016) | Giuliano Losa | | ✔ | Int, Seq, FinSet | | | -| 38 | mongo-repl-tla | A simplified part of Raft in MongoDB (Ongaro, 2014) | Siyuan Zhou | | ✔ | FinSet, Nat, Seq | | | -| 39 | MultiPaxos | The abstract specification of Generalized Paxos (Lamport, 2004) | Giuliano Losa | | ✔ | Int, FinSet | | | -| 40 | N-Queens | The N queens problem | Stephan Merz | | ✔ | Nat, Seq | ✔ | | -| 41 | naiad | Naiad clock protocol, only PDF files (Murray et al., 2013) | Tom Rodeheffer | | ✔ | Int, Seq, FinSet | | | -| 42 | nbacc_ray97 | Asynchronous non-blocking atomic commit (Raynal, 1997) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat, FinSet | | | -| 43 | nbacg_guer01 | On the hardness of failure-sensitive agreement problems (Guerraoui, 2001) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat, FinSet | | | -| 44 | nfc04 | Non-functional properties of component-based software systems (Zschaler, 2010) | Steffen Zschaler | | ✔ | Real, Nat | | | -| 45 | Paxos | Paxos consensus algorithm (Lamport, 1998) | Leslie Lamport | | ✔ | Int, FinSet | | | -| 46 | Prisoners | A puzzle that was presented on an American radio program. | | | ✔ | Nat, FinSet | | | -| 47 | raft | Raft consensus algorithm (Ongaro, 2014) | Diego Ongaro | | ✔ | FinSet, Nat, Seq | | | -| 48 | SnapshotIsolation | Serializable snapshot isolation (Cahill et al., 2010) | Michael J. Cahill, Uwe Röhm, Alan D. Fekete | | ✔ | FinSet, Int, Seq | | | -| 49 | spanning | Spanning tree broadcast algorithm in Attiya and Welch’s book | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Int | | | -| 50 | SpecifyingSystems | Examples to accompany the book Specifying Systems (Lamport, 2002) | | | ✔ | all modules | | | -| 51 | Stones | The same problem as CarTalkPuzzle | | | ✔ | FinSet, Int, Seq | | | -| 52 | sums_even | Two proofs for showing that x+x is even, for any natural number x. | | ✔ | ✔ | Int | | | -| 53 | SyncConsensus | Synchronized round consensus algorithm (Demirbas) | Murat Demirbas | | ✔ | FinSet, Int, Seq | ✔ | | -| 54 | Termination | Channel-counting algorithm (Kumar, 1985) | Giuliano Losa | | ✔ | Integers, FiniteSets, Apalache, Sequences | ✔ | ✔ | -| 55 | Tla-tortoise-hare | Robert Floyd's cycle detection algorithm | Lorin Hochstein | | ✔ | Nat | ✔ | | -| 56 | tower_of_hanoi | The well-known Towers of Hanoi puzzle. | Markus Kuppe, Alexander Niederbühl | | ✔ | Bit, FinSet, Int, Nat, Seq | | | -| 57 | transaction_commit | Consensus on transaction commit (Gray & Lamport, 2006) | Leslie Lamport | | ✔ | Int | | | -| 58 | TransitiveClosure | The transitive closure of a relation | | | ✔ | FinSet, Int, Seq | | | -| 59 | TwoPhase | Two-phase handshaking | Leslie Lamport, Stephan Merz | | ✔ | Nat | | | -| 60 | VoldemortKV | Voldemort distributed key value store | Murat Demirbas | | ✔ | FinSet, Int, Seq | ✔ | | -| 61 | Missionaries and Cannibals | Missionaries and Cannibals | Leslie Lamport | | ✔ | FinSet, Int | | | -| 62 | Misra Reachability Algorithm | Misra Reachability Algorithm | Leslie Lamport | ✔ | ✔ | Int, Seq, FiniteSets, TLC, TLAPS, NaturalsInduction | ✔ | | -| 63 | Loop Invariance | Loop Invariance | Leslie Lamport | ✔ | ✔ | Int, Seq, FiniteSets, TLC, TLAPS, SequenceTheorems, NaturalsInduction | ✔ | | -| 64 | Teaching Concurrency | Teaching Concurrency | Leslie Lamport | ✔ | ✔ | Int, TLAPS | ✔ | | -| 65 | Spanning Tree | Spanning Tree | Leslie Lamport | | ✔ | Int, FiniteSets, TLC, Randomization | | | -| 66 | Paxos (How to win a Turing Award) | Paxos | Leslie Lamport | | ✔ | Nat, Int, FiniteSets | | | -| 67 | Tencent-Paxos | PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017) | Xingchen Yi, Hengfeng Wei | ✔ | ✔ | Int, FiniteSets | | | -| 68 | Blocking Queue | BlockingQueue | Markus Kuppe | ✔ | ✔ [(LiveEnv)](https://gitpod.io/#https://github.com/lemmy/BlockingQueue/blob/master/BlockingQueue.tla) | Naturals, Sequences, FiniteSets | | | -| 69 | Paxos | Paxos | | | ✔ | Int, FiniteSets | | | -| 71 | Echo Algorithm | Echo Algorithm | Stephan Merz | | ✔ | Naturals, FiniteSets, Relation, TLC | ✔ | | -| 72 | Cigarette Smokers problem | Cigarette Smokers problem | Mariusz Ryndzionek | | ✔ | Integers, FiniteSets | | | -| 73 | Conway's Game of Life | Conway's Game of Life | Mariusz Ryndzionek | | ✔ | Integers | | | -| 74 | Sliding puzzles | Sliding puzzles | Mariusz Ryndzionek | | ✔ | Integers | | | -| 75 | Lock-Free Set | PlusCal spec of a lock-Free set used by TLC | Markus Kuppe | | ✔ | Sequences, FiniteSets, Integers, TLC | ✔ | | -| 76 | Chameneos | Chameneos, a Concurrency Game | Mariusz Ryndzionek | | ✔ | Integers | | | -| 77 | ParallelRaft | A variant of Raft | Xiaosong Gu, Hengfeng Wei, Yu Huang | | ✔ | Integers, FiniteSets, Sequences, Naturals | | | -| 78 | TLC MC | PlusCal spec of safety checking as implemented in TLC | Markus Kuppe | | ✔ | Integers, FiniteSets, Sequences, TLC | ✔ | | -| 79 | TLA+ Level Checking | Level-checking of TLA+ formulas as described in Specifying Systems | Leslie Lamport | | | Integers, Sequences | | | -| 80 | CRDT-Bug | CRDT algorithm with defect and fixed version | Alexander Niederbühl | | ✔ | FiniteSets, Naturals, Sequences | | | -| 81 | asyncio-lock | Bugs from old versions of Python's asyncio lock | Alexander Niederbühl | | ✔ | Sequences | | | -| 82 | Single Lane Bridge problem | Single Lane Bridge | Younes Akhouayri | | ✔ | Naturals, FiniteSets, Sequences | | | -| 83 | Raft (with cluster changes) | Raft with cluster changes, and a version with Apalache type annotations but no cluster changes | George Pîrlea, Darius Foom, Brandon Amos, Huanchen Zhang, Daniel Ricketts | | ✔ | Functions, SequencesExt, FiniteSetsExt, TypedBags | | ✔ | -| 84 | EWD687a | Detecting termination in distributed computations by Edsger Dijkstra and Carel Scholten | Stephan Merz (PlusCal spec), Leslie Lamport & Markus Kuppe (TLA+ spec) | | ✔ | Integers, Graphs | ✔ | | -| 85 | Huang | Termination detection by using distributed snapshots by Shing-Tsaan Huang | Markus Kuppe | | ✔ | DyadicRationals | | | -| 86 | Azure Cosmos DB | Consistency models provided by Azure Cosmos DB | Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe | | ✔ | Integers, Sequences, FiniteSets, Functions, SequencesExt | ✔ | | -| 87 | MET for CRDT-Redis | Model-check the CRDT designs, then generate test cases to test CRDT implementations | Yuqi Zhang | | ✔ | Integers, Sequences, FiniteSets, TLC | ✔ | | -| 88 | Parallel increment | Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry | Chris Jensen | | ✔ | Integers, FiniteSets, TLC | | | -| 89 | The Streamlet consensus algorithm | Specification and model-checking of both safety and liveness properties of Streamlet with TLC | Giuliano Losa | | ✔ | Sequences, Integers, FiniteSets | ✔ | | -| 90 | Petri Nets | Instantiable Petri Nets with liveness properties | Eugene Huang | | ✔ | Integers, Sequences, FiniteSets, TLC | | | -| 91 | Knuth Yao & Markov Chains | Knuth-Yao algorithm for simulating a sixsided die | Ron Pressler, Markus Kuppe | | ✔ | DyadicRationals | | | -| 92 | ewd426 - Token Stabilization | Self-stabilizing systems in spite of distributed control | Murat Demirbas, Markus Kuppe | | ✔ | Naturals, FiniteSets | | | -| 93 | CRDT | Specifying and Verifying CRDT Protocols | Ye Ji, Hengfeng Wei | | ✔| Naturals, FiniteSets | | -| 94 | Multi-Car Elevator System | Directory | Andrew Helwer | | ✔ | Integers | | | -| 95 | Snapshot Key-Value Store | Directory | Andrew Helwer | | ✔ | | | | -| 96 | Nano Blockchain Protocol | Directory | Andrew Helwer | | ✔ | Naturals, Bags | | | -| 97 | The Coffee Can Bean Problem | Directory | Andrew Helwer | | ✔ | Naturals | | | -| 98 | The Slush Protocol | Directory | Andrew Helwer | | ✔ | Naturals, FiniteSets, Sequences | ✔ | | -| 99 | SDP (Software Defined Perimeter) | Specifying and Verifying SDP Protocol based Zero Trust Architecture | Luming Dong, Zhi Niu | | ✔| FiniteSets, Sequences, Naturals | | | -| 100 | Simplified Fast Paxos | Simplified version of Fast Paxos (Lamport, 2006) | Lim Ngian Xin Terry, Gaurav Gandhi | |✔| TLC, Naturals, FiniteSets, Integers | | | -| 101 | Learn TLA⁺ Proofs | Basic PlusCal algorithms and formal proofs of their correctness | Andrew Helwer | ✔ | ✔ | Sequences, Naturals, Integers, TLAPS | ✔ | | -| 102 | Minimal Circular Substring | Booth's 1980 algorithm to find the lexicographically-least circular substring | Andrew Helwer | | ✔ | FiniteSets, Integers, Naturals, Sequences | ✔ | | -| 103 | Checkpoint Coordination | Algorithm for coordinating checkpoint/snapshot leases in a Paxos ring | Andrew Helwer | | ✔ | FiniteSets, Naturals, Sequences, TLC | | | -| 104 | Boyer-Moore Majority Vote | Efficient algorithm for finding a majority value | Stephan Merz | ✔ | ✔ | Integers, Sequences, FiniteSets, TLAPS | | | -| 105 | Finitizing Monotonic Systems | A technique for making infinite-state monotonic systems finite | Andrew Helwer | | ✔ | Naturals, Sequences | | | +## Examples Elsewhere +Here is a list of specs stored in locations outside this repository, including submodules. +They are not covered by CI testing so it is possible they contain errors, the reported details are incorrect, or they are no longer available. +Ideally these will be moved into this repo over time. +| Name | Description | Author(s) | TLAPS Proof? | TLC Model? | PlusCal? | Apalache? | +| --------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------ | :----------: | :--------: | :------: | :-------: | +| [2PCwithBTM](specifications/2PCwithBTM) | A modified version of P2TCommit (Gray & Lamport, 2006) | Murat Demirbas | | ✔ | ✔ | | +| [802.16](specifications/802.16) | IEEE 802.16 WiMAX Protocols | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou | | ✔ | | | +| [acp-nb](specifications/acp-nb) | Non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | | | +| [acp-nb-wrong](specifications/acp-nb-wrong) | Wrong version of the non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | | | +| [acp-sb](specifications/acp-sb) | Non-blocking atomic commitment with a simple broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | | | +| [async-comm](specifications/async-comm) | The diversity of asynchronous communication (Chevrou et al., 2016) | Florent Chevrou, Aurélie Hurault, Philippe Quéinnec | | ✔ | | | +| [byihive](specifications/byihive) | Based on RFC3506 - Requirements and Design for Voucher Trading System (Fujimura & Eastlake) | Santhosh Raju | | ✔ | | | +| [byzpaxos](specifications/byzpaxos) | Byzantizing Paxos by Refinement (Lamport, 2011) | Leslie Lamport | | ✔ | | | +| [Caesar](specifications/Caesar) | Multi-leader generalized consensus protocol (Arun et al., 2017) | Giuliano Losa | | ✔ | ✔ | | +| [CASPaxos](specifications/CASPaxos) | An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov) | Tobias Schottdorf | | ✔ | | | +| [DataPort](specifications/DataPort) | Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016) | Geoffrey Biggs, Noriaki Ando | | | | | +| [egalitarian-paxos](specifications/egalitarian-paxos) | Leaderless replication protocol based on Paxos (Moraru et al., 2013) | Iulian Moraru | | ✔ | | | +| [fastpaxos](specifications/fastpaxos) | An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006) | Leslie Lamport | | | | | +| [fpaxos](specifications/fpaxos) | A variant of Paxos with flexible quorums (Howard et al., 2017) | Heidi Howard | | ✔ | | | +| [HLC](specifications/HLC) | Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014) | Murat Demirbas | | ✔ | ✔ | | +| [L1](specifications/L1) | Data center network L1 switch protocol, only PDF files (Thacker) | Tom Rodeheffer | | | | | +| [leaderless](specifications/leaderless) | Leaderless generalized-consensus algorithms (Losa, 2016) | Giuliano Losa | | ✔ | ✔ | | +| [losa_ap](specifications/losa_ap) | The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018) | Giuliano Losa | | ✔ | ✔ | | +| [losa_rda](specifications/losa_rda) | Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014) | Giuliano Losa | | | | | +| [m2paxos](specifications/m2paxos) | Multi-leader consensus protocols (Peluso et al., 2016) | Giuliano Losa | | ✔ | | | +| [mongo-repl-tla](specifications/mongo-repl-tla) | A simplified part of Raft in MongoDB (Ongaro, 2014) | Siyuan Zhou | | ✔ | | | +| [MultiPaxos](specifications/MultiPaxos) | The abstract specification of Generalized Paxos (Lamport, 2004) | Giuliano Losa | | ✔ | | | +| [naiad](specifications/naiad) | Naiad clock protocol, only PDF files (Murray et al., 2013) | Tom Rodeheffer | | ✔ | | | +| [nfc04](specifications/nfc04) | Non-functional properties of component-based software systems (Zschaler, 2010) | Steffen Zschaler | | ✔ | | | +| [raft](specifications/raft) | Raft consensus algorithm (Ongaro, 2014) | Diego Ongaro | | ✔ | | | +| [SnapshotIsolation](specifications/SnapshotIsolation) | Serializable snapshot isolation (Cahill et al., 2010) | Michael J. Cahill, Uwe Röhm, Alan D. Fekete | | ✔ | | | +| [SyncConsensus](specifications/SyncConsensus) | Synchronized round consensus algorithm (Demirbas) | Murat Demirbas | | ✔ | ✔ | | +| [Termination](specifications/Termination) | Channel-counting algorithm (Kumar, 1985) | Giuliano Losa | | ✔ | ✔ | ✔ | +| [Tla-tortoise-hare](specifications/Tla-tortoise-hare) | Robert Floyd's cycle detection algorithm | Lorin Hochstein | | ✔ | ✔ | | +| [VoldemortKV](specifications/VoldemortKV) | Voldemort distributed key value store | Murat Demirbas | | ✔ | ✔ | | +| [Tencent-Paxos](specifications/TencentPaxos) | PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017) | Xingchen Yi, Hengfeng Wei | ✔ | ✔ | | | +| [Paxos](https://github.com/neoschizomer/Paxos) | Paxos | | | ✔ | | | +| [Lock-Free Set](https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OpenAddressing.tla) | PlusCal spec of a lock-Free set used by TLC | Markus Kuppe | | ✔ | ✔ | | +| [ParallelRaft](specifications/ParalleRaft) | A variant of Raft | Xiaosong Gu, Hengfeng Wei, Yu Huang | | ✔ | | | +| [CRDT-Bug](https://github.com/Alexander-N/tla-specs/tree/main/crdt-bug) | CRDT algorithm with defect and fixed version | Alexander Niederbühl | | ✔ | | | +| [asyncio-lock](https://github.com/Alexander-N/tla-specs/tree/main/asyncio-lock) | Bugs from old versions of Python's asyncio lock | Alexander Niederbühl | | ✔ | | | +| [Raft (with cluster changes)](https://github.com/dranov/raft-tla) | Raft with cluster changes, and a version with Apalache type annotations but no cluster changes | George Pîrlea, Darius Foom, Brandon Amos, Huanchen Zhang, Daniel Ricketts | | ✔ | | ✔ | +| [MET for CRDT-Redis](https://github.com/elem-azar-unis/CRDT-Redis/tree/master/MET/TLA) | Model-check the CRDT designs, then generate test cases to test CRDT implementations | Yuqi Zhang | | ✔ | ✔ | | +| [Parallel increment](https://github.com/Cjen1/tla_increment) | Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry | Chris Jensen | | ✔ | | | +| [The Streamlet consensus algorithm](https://github.com/nano-o/streamlet) | Specification and model-checking of both safety and liveness properties of Streamlet with TLC | Giuliano Losa | | ✔ | ✔ | | +| [Petri Nets](https://github.com/elh/petri-tlaplus) | Instantiable Petri Nets with liveness properties | Eugene Huang | | ✔ | | | +| [CRDT](https://github.com/JYwellin/CRDT-TLA) | Specifying and Verifying CRDT Protocols | Ye Ji, Hengfeng Wei | | ✔ | | | +| [Azure Cosmos DB](https://github.com/tlaplus/azure-cosmos-tla) | Consistency models provided by Azure Cosmos DB | Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe | | ✔ | ✔ | | +| [Blocking Queue](https://github.com/lemmy/BlockingQueue) | BlockingQueue | Markus Kuppe | ✔ | ✔ | | | ## License - -The repository is under the MIT license. However, we can upload your benchmarks under your license. +The repository is under the MIT license and you are encouraged to publish your spec under a similarly-permissive license. +However, your spec can be included in this repo along with you own license if you wish. ## Support or Contact - Do you have any questions or comments? Please open an issue or send an email to the [TLA+ group](https://groups.google.com/g/tlaplus). ## Contributing - Do you have your own case study or TLA+ specification you'd like to share with the community? Follow these instructions: -1. Ensure your spec is released under MIT or a similarly-permissive license 1. Fork this repository and create a new directory under `specifications` with the name of your spec 1. Place all TLA+ files in the directory, along with their `.cfg` model files; you are encouraged to include at least one model that completes execution in less than 10 seconds 1. Ensure name of each `.cfg` file matches the `.tla` file it models, or has its name as a prefix; for example `SpecName.tla` can have the models `SpecName.cfg` and `SpecNameLiveness.cfg`, etc. 1. Consider including a `README.md` in the spec directory explaining the significance of the spec with links to any relevant websites or publications, or integrate this info as comments in the spec itself -1. Add an entry to the below table in this top-level `README.md` summarizing your spec and its attributes +1. Add an entry to the table of specs included in this repo, summarizing your spec and its attributes ## Adding Spec to Continuous Integration - To combat bitrot, it is important to add your spec and model to the continuous integration system. To do this, you'll have to update the [`manifest.json`](manifest.json) file with machine-readable records of your spec files. If this process doesn't work for you, you can alternatively modify the [`.ciignore`](.ciignore) file to exclude your spec from validation. Otherwise, follow these directions: - 1. Ensure you have Python 3.11+ installed 1. Download & extract tree-sitter-tlaplus ([zip](https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/refs/heads/main.zip), [tar.gz](https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/refs/heads/main.tar.gz)) to the root of the repository; ensure the extracted folder is named `tree-sitter-tlaplus` 1. Open a shell and navigate to the repo root; ensure a C++ compiler is installed and on your path - - On Windows, this might entail running the below script from the visual studio developer command prompt + - On Windows, this might entail running the below script from the visual studio developer command prompt 1. It is considered best practice to create & initialize a Python virtual environment to preserve your system package store; run `python -m venv .` then `source ./bin/activate` on Linux & macOS or `.\Scripts\activate.bat` on Windows (run `deactivate` to exit) 1. Run `pip install -r .github/scripts/requirements.txt` 1. Run `python .github/scripts/generate_manifest.py` 1. Locate your spec's entry in the [`manifest.json`](manifest.json) file and ensure the following fields are filled out: - - Spec title: an appropriate title for your specification - - Spec description: a short description of your specification - - Spec source: if this spec was first published elsewhere, provide a link to this location - - Spec authors: a list of people who authored the spec - - Spec tags: - - `"beginner"` if your spec is appropriate for TLA+ newcomers - - Model runtime: approximate model runtime on an ordinary workstation, in `"HH:MM:SS"` format - - Model size: - - `"small"` if the model can be executed in less than 10 seconds - - `"medium"` if the model can be executed in less than five minutes - - `"large"` if the model takes more than five minutes to execute - - Model mode: - - `"exhaustive search"` by default - - `{"simulate": {"traceCount": N}}` for a simulation model - - `"generate"` for model trace generation - - Model result: - - `"success"` if the model completes successfully - - `"safety failure"` if the model violates an invariant - - `"liveness failure"` if the model fails to satisfy a liveness property - - `"deadlock failure"` if the model encounters deadlock - - Other fields are auto-generated by the script; if you are adding an entry manually, ensure their values are present and correct (see other entries or the [`manifest-schema.json`](manifest-schema.json) file) + - Spec title: an appropriate title for your specification + - Spec description: a short description of your specification + - Spec source: if this spec was first published elsewhere, provide a link to this location + - Spec authors: a list of people who authored the spec + - Spec tags: + - `"beginner"` if your spec is appropriate for TLA+ newcomers + - Model runtime: approximate model runtime on an ordinary workstation, in `"HH:MM:SS"` format + - Model size: + - `"small"` if the model can be executed in less than 10 seconds + - `"medium"` if the model can be executed in less than five minutes + - `"large"` if the model takes more than five minutes to execute + - Model mode: + - `"exhaustive search"` by default + - `{"simulate": {"traceCount": N}}` for a simulation model + - `"generate"` for model trace generation + - Model result: + - `"success"` if the model completes successfully + - `"safety failure"` if the model violates an invariant + - `"liveness failure"` if the model fails to satisfy a liveness property + - `"deadlock failure"` if the model encounters deadlock + - Other fields are auto-generated by the script; if you are adding an entry manually, ensure their values are present and correct (see other entries or the [`manifest-schema.json`](manifest-schema.json) file) Before submitted your changes to run in the CI, you can quickly check your [`manifest.json`](manifest.json) for errors and also check it against [`manifest-schema.json`](manifest-schema.json) at https://www.jsonschemavalidator.net/. diff --git a/manifest-schema.json b/manifest-schema.json index 776efa5d..7570d518 100644 --- a/manifest-schema.json +++ b/manifest-schema.json @@ -20,7 +20,7 @@ }, "tags": { "type": "array", - "items": {"enum": ["beginner", "intermediate"]} + "items": {"enum": ["beginner", "intermediate", "ewd"]} }, "modules": { "type": "array", diff --git a/manifest.json b/manifest.json index ccad3aff..fa336cc3 100644 --- a/manifest.json +++ b/manifest.json @@ -144,7 +144,7 @@ }, { "path": "specifications/CheckpointCoordination", - "title": "Distributed Checkpoint/Snapshot Coordination", + "title": "Checkpoint Coordination", "description": "An algorithm for controlling checkpoint leases in a Paxos ring", "source": "https://github.com/Azure/RingMaster", "authors": [ @@ -212,7 +212,7 @@ }, { "path": "specifications/CoffeeCan", - "title": "The Coffee Can Black/White Bean Problem", + "title": "The Coffee Can Bean Problem", "description": "Math problem published by Dijkstra attributed to Carel Scholten", "source": "https://stackoverflow.com/a/66304920/2852699", "authors": [ @@ -379,7 +379,7 @@ }, { "path": "specifications/FiniteMonotonic", - "title": "Finite Model-Checking of Monotonic Systems", + "title": "Finitizing Monotonic Systems", "description": "Illustration of technique for making ordinarily-infinite monotonic systems finite for the purposes of model-checking.", "source": "https://ahelwer.ca/post/2023-11-01-tla-finite-monotonic/", "authors": [ @@ -518,7 +518,7 @@ }, { "path": "specifications/KeyValueStore", - "title": "Key-Value Store with Snapshot Isolation", + "title": "Snapshot Key-Value Store", "description": "A simple KVS implementing snapshot isolation", "source": "", "authors": [ @@ -723,7 +723,7 @@ }, { "path": "specifications/LeastCircularSubstring", - "title": "Lexicographically-Least Circular Substring", + "title": "Minimal Circular Substring", "description": "Booth's 1980 algorithm to find the lexicographically-least circular substring", "source": "", "authors": [ @@ -836,7 +836,7 @@ }, { "path": "specifications/Majority", - "title": "Boyer-Moore majority vote algorithm", + "title": "Boyer-Moore Majority Vote", "description": "An efficient algorithm for detecting a majority value in a sequence", "source": "", "authors": [ @@ -1131,7 +1131,7 @@ }, { "path": "specifications/NanoBlockchain", - "title": "The Nano Blockchain Protocol", + "title": "Nano Blockchain Protocol", "description": "A specification of the protocol originally used by the Nano blockchain", "source": "", "authors": [ @@ -1282,7 +1282,7 @@ }, { "path": "specifications/PaxosHowToWinATuringAward", - "title": "How to Win a Turing Award", + "title": "Paxos (How to Win a Turing Award)", "description": "Exercises from the lecture The Paxos Algorithm - or How to Win a Turing Award", "source": "https://www.youtube.com/watch?v=tw3gsBms-f8", "authors": [ @@ -1521,7 +1521,7 @@ "description": "Controlling cars moving over a single-lange bridge in opposite directions", "source": "", "authors": [ - "Younes Aka" + "Younes Akhouayri" ], "tags": [], "modules": [ @@ -1582,7 +1582,7 @@ }, { "path": "specifications/SlushProtocol", - "title": "The Slush Probabilistic Consensus Protocol", + "title": "The Slush Protocol", "description": "An attempt to use TLA⁺ to analyze a probabilistic protocol in the Avalanche family", "source": "https://github.com/ahelwer/avalanche-analysis", "authors": [ @@ -1667,7 +1667,9 @@ "authors": [ "Leslie Lamport" ], - "tags": [], + "tags": [ + "beginner" + ], "modules": [ { "path": "specifications/SpecifyingSystems/AdvancedExamples/BNFGrammars.tla", @@ -2359,7 +2361,9 @@ "authors": [ "Leslie Lamport" ], - "tags": [], + "tags": [ + "beginner" + ], "modules": [ { "path": "specifications/Stones/Stones.tla", @@ -2417,7 +2421,9 @@ "authors": [ "Leslie Lamport" ], - "tags": [], + "tags": [ + "beginner" + ], "modules": [ { "path": "specifications/TeachingConcurrency/Simple.tla", @@ -2642,7 +2648,7 @@ "source": "", "authors": [ "Igor Konnov", - "Josev Widder", + "Josef Widder", "Thanh Hai Tran" ], "tags": [], @@ -2663,7 +2669,7 @@ "source": "", "authors": [ "Igor Konnov", - "Josev Widder", + "Josef Widder", "Thanh Hai Tran" ], "tags": [], @@ -2684,7 +2690,7 @@ "source": "", "authors": [ "Igor Konnov", - "Josev Widder", + "Josef Widder", "Thanh Hai Tran" ], "tags": [], @@ -2705,7 +2711,7 @@ "source": "", "authors": [ "Igor Konnov", - "Josev Widder", + "Josef Widder", "Thanh Hai Tran" ], "tags": [], @@ -2726,7 +2732,7 @@ "source": "", "authors": [ "Igor Konnov", - "Josev Widder", + "Josef Widder", "Thanh Hai Tran" ], "tags": [], @@ -2768,7 +2774,7 @@ "source": "", "authors": [ "Igor Konnov", - "Josev Widder", + "Josef Widder", "Thanh Hai Tran" ], "tags": [], @@ -2804,7 +2810,9 @@ "authors": [ "Leslie Lamport" ], - "tags": [], + "tags": [ + "ewd" + ], "modules": [ { "path": "specifications/dijkstra-mutex/DijkstraMutex.tla", @@ -2871,7 +2879,7 @@ }, { "path": "specifications/diskpaxos", - "title": "diskpaxos", + "title": "SWMR Shared Memory Disk Paxos", "description": "A formalization of the SWMR-Shared-Memory Disk Paxos", "source": "https://github.com/nano-o/MultiPaxos/blob/master/DiskPaxos.tla", "authors": [ @@ -2949,14 +2957,16 @@ }, { "path": "specifications/ewd426", - "title": "Token Stabilization", - "description": "Dijkstra's classical stabilizing token ring algorithm: EWD426", + "title": "EWD 426: Token Stabilization", + "description": "Dijkstra's classical stabilizing token ring algorithm, EWD426", "source": "", "authors": [ "Markus Kuppe", "Murat Demirbas" ], - "tags": [], + "tags": [ + "ewd" + ], "modules": [ { "path": "specifications/ewd426/SimTokenRing.tla", @@ -3004,7 +3014,7 @@ }, { "path": "specifications/ewd687a", - "title": "Detecting Termination in Distributed Computations", + "title": "EWD687a: Detecting Termination in Distributed Computations", "description": "Dijkstra's Termination Detection Algorithm", "source": "", "authors": [ @@ -3012,7 +3022,9 @@ "Markus Kuppe", "Stephan Merz" ], - "tags": [], + "tags": [ + "ewd" + ], "modules": [ { "path": "specifications/ewd687a/EWD687a.tla", @@ -3083,13 +3095,15 @@ }, { "path": "specifications/ewd840", - "title": "ewd840", - "description": "Termination Detection in a Ring", + "title": "EWD840: Termination Detection in a Ring", + "description": "EWD840: Termination Detection in a Ring", "source": "Dijkstra's termination detection algorithm for ring topologies", "authors": [ "Stephan Merz" ], - "tags": [], + "tags": [ + "ewd" + ], "modules": [ { "path": "specifications/ewd840/EWD840.tla", @@ -3192,14 +3206,16 @@ }, { "path": "specifications/ewd998", - "title": "Termination Detection in a Ring with Asynchronous Message Delivery", + "title": "EWD998: Termination Detection in a Ring with Asynchronous Message Delivery", "description": "Variant of EWD 840 given by Shmuel Safra", "source": "", "authors": [ "Markus Kuppe", "Stephan Merz" ], - "tags": [], + "tags": [ + "ewd" + ], "modules": [ { "path": "specifications/ewd998/AsyncTerminationDetection.tla", @@ -3618,7 +3634,9 @@ "authors": [ "Stephan Merz" ], - "tags": [], + "tags": [ + "beginner" + ], "modules": [ { "path": "specifications/sums_even/TLAPS.tla", @@ -3741,4 +3759,4 @@ ] } ] -} \ No newline at end of file +}