From 45a020523c121a67e47d61e325d11305e8be5545 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Fri, 26 Jan 2024 16:04:46 -0500 Subject: [PATCH] Added TLC models for all viable specs (#110) Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/scripts/check_markdown_table.py | 2 + .github/scripts/check_small_models.py | 3 + .github/scripts/format_markdown_table.py | 24 +- .github/scripts/generate_manifest.py | 13 +- .github/scripts/tla_utils.py | 1 + .github/workflows/CI.yml | 6 +- .gitignore | 2 + README.md | 58 +- manifest-schema.json | 2 +- manifest.json | 661 ++++++++++++++++-- .../Bakery-Boulangerie/MCBakery.cfg | 10 + .../Bakery-Boulangerie/MCBakery.tla | 7 + .../Bakery-Boulangerie/MCBoulanger.cfg | 8 + .../Bakery-Boulangerie/MCBoulanger.tla | 8 + specifications/Chameneos/Chameneos.cfg | 9 + .../CigaretteSmokers/CigaretteSmokers.cfg | 6 + .../CigaretteSmokers/CigaretteSmokers.tla | 2 +- specifications/GameOfLife/GameOfLife.cfg | 4 + .../LoopInvariance/MCBinarySearch.cfg | 8 + .../LoopInvariance/MCBinarySearch.tla | 7 + specifications/LoopInvariance/MCQuicksort.cfg | 8 + specifications/LoopInvariance/MCQuicksort.tla | 7 + .../MisraReachability/MCParReach.cfg | 10 + .../MisraReachability/MCParReach.tla | 14 + .../MisraReachability/MCReachabilityTest.tla | 15 + .../MCReachabilityTestAllGraphs.cfg | 6 + .../MCReachabilityTestRandomGraphs.cfg | 6 + .../MisraReachability/MCReachable.cfg | 9 + .../MisraReachability/MCReachable.tla | 14 + specifications/MisraReachability/ParReach.tla | 3 +- .../MisraReachability/Reachable.tla | 3 +- .../PaxosHowToWinATuringAward/MCConsensus.cfg | 17 + .../PaxosHowToWinATuringAward/MCConsensus.tla | 16 + .../PaxosHowToWinATuringAward/MCPaxos.tla | 45 ++ .../MCPaxosSmall.cfg | 35 + .../PaxosHowToWinATuringAward/MCPaxosTiny.cfg | 35 + .../PaxosHowToWinATuringAward/MCVoting.cfg | 33 + .../PaxosHowToWinATuringAward/MCVoting.tla | 39 ++ specifications/SpanningTree/SpanTree.cfg | 10 + .../SpanningTree/SpanTreeRandom.cfg | 10 + .../SpanningTree/SpanTreeTest4Nodes.cfg | 9 + .../SpanningTree/SpanTreeTest5Nodes.cfg | 9 + specifications/Stones/Stones.cfg | 4 + specifications/TeachingConcurrency/Simple.cfg | 4 + .../TeachingConcurrency/SimpleRegular.cfg | 4 + specifications/TwoPhase/MCTwoPhase.cfg | 3 + specifications/TwoPhase/MCTwoPhase.tla | 7 + specifications/aba-asyn-byz/aba_asyn_byz.cfg | 8 + specifications/bcastByz/bcastByz.cfg | 8 + specifications/bcastByz/bcastByzNoBcast.cfg | 8 + .../bcastFolklore/bcastFolklore.cfg | 8 + specifications/bosco/bosco.cfg | 7 + specifications/c1cs/c1cs.cfg | 10 + .../cf1s-folklore/cf1s_folklore.cfg | 8 + .../cf1s-folklore/cf1s_folklore.tla | 4 +- .../chang_roberts/MCChangRoberts.cfg | 6 + .../chang_roberts/MCChangRoberts.tla | 9 + .../detector_chan96/EnvironmentController.cfg | 12 + .../detector_chan96/EnvironmentController.tla | 4 +- specifications/diskpaxos/MC_HDiskSynod.cfg | 12 + specifications/diskpaxos/MC_HDiskSynod.tla | 9 + specifications/glowingRaccoon/clean.cfg | 7 + specifications/glowingRaccoon/product.cfg | 8 + specifications/glowingRaccoon/stages.cfg | 8 + .../lamport_mutex/MCLamportMutex.cfg | 9 + .../lamport_mutex/MCLamportMutex.tla | 7 + specifications/nbacc_ray97/nbacc_ray97.cfg | 4 + specifications/nbacg_guer01/nbacg_guer01.cfg | 5 + specifications/spanning/MC_spanning.cfg | 9 + specifications/spanning/MC_spanning.tla | 4 + specifications/spanning/spanning.tla | 2 +- specifications/sums_even/MC_sums_even.cfg | 4 + specifications/sums_even/MC_sums_even.tla | 8 + .../transaction_commit/PaxosCommit.cfg | 8 + specifications/transaction_commit/TCommit.cfg | 5 + .../transaction_commit/TwoPhase.cfg | 4 + 76 files changed, 1321 insertions(+), 100 deletions(-) create mode 100644 specifications/Bakery-Boulangerie/MCBakery.cfg create mode 100644 specifications/Bakery-Boulangerie/MCBakery.tla create mode 100644 specifications/Bakery-Boulangerie/MCBoulanger.cfg create mode 100644 specifications/Bakery-Boulangerie/MCBoulanger.tla create mode 100644 specifications/Chameneos/Chameneos.cfg create mode 100644 specifications/CigaretteSmokers/CigaretteSmokers.cfg create mode 100644 specifications/GameOfLife/GameOfLife.cfg create mode 100644 specifications/LoopInvariance/MCBinarySearch.cfg create mode 100644 specifications/LoopInvariance/MCBinarySearch.tla create mode 100644 specifications/LoopInvariance/MCQuicksort.cfg create mode 100644 specifications/LoopInvariance/MCQuicksort.tla create mode 100644 specifications/MisraReachability/MCParReach.cfg create mode 100644 specifications/MisraReachability/MCParReach.tla create mode 100644 specifications/MisraReachability/MCReachabilityTest.tla create mode 100644 specifications/MisraReachability/MCReachabilityTestAllGraphs.cfg create mode 100644 specifications/MisraReachability/MCReachabilityTestRandomGraphs.cfg create mode 100644 specifications/MisraReachability/MCReachable.cfg create mode 100644 specifications/MisraReachability/MCReachable.tla create mode 100644 specifications/PaxosHowToWinATuringAward/MCConsensus.cfg create mode 100644 specifications/PaxosHowToWinATuringAward/MCConsensus.tla create mode 100644 specifications/PaxosHowToWinATuringAward/MCPaxos.tla create mode 100644 specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg create mode 100644 specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg create mode 100644 specifications/PaxosHowToWinATuringAward/MCVoting.cfg create mode 100644 specifications/PaxosHowToWinATuringAward/MCVoting.tla create mode 100644 specifications/SpanningTree/SpanTree.cfg create mode 100644 specifications/SpanningTree/SpanTreeRandom.cfg create mode 100644 specifications/SpanningTree/SpanTreeTest4Nodes.cfg create mode 100644 specifications/SpanningTree/SpanTreeTest5Nodes.cfg create mode 100644 specifications/Stones/Stones.cfg create mode 100644 specifications/TeachingConcurrency/Simple.cfg create mode 100644 specifications/TeachingConcurrency/SimpleRegular.cfg create mode 100644 specifications/TwoPhase/MCTwoPhase.cfg create mode 100644 specifications/TwoPhase/MCTwoPhase.tla create mode 100644 specifications/aba-asyn-byz/aba_asyn_byz.cfg create mode 100644 specifications/bcastByz/bcastByz.cfg create mode 100644 specifications/bcastByz/bcastByzNoBcast.cfg create mode 100644 specifications/bcastFolklore/bcastFolklore.cfg create mode 100644 specifications/bosco/bosco.cfg create mode 100644 specifications/c1cs/c1cs.cfg create mode 100644 specifications/cf1s-folklore/cf1s_folklore.cfg create mode 100644 specifications/chang_roberts/MCChangRoberts.cfg create mode 100644 specifications/chang_roberts/MCChangRoberts.tla create mode 100644 specifications/detector_chan96/EnvironmentController.cfg create mode 100644 specifications/diskpaxos/MC_HDiskSynod.cfg create mode 100644 specifications/diskpaxos/MC_HDiskSynod.tla create mode 100644 specifications/glowingRaccoon/clean.cfg create mode 100644 specifications/glowingRaccoon/product.cfg create mode 100644 specifications/glowingRaccoon/stages.cfg create mode 100644 specifications/lamport_mutex/MCLamportMutex.cfg create mode 100644 specifications/lamport_mutex/MCLamportMutex.tla create mode 100644 specifications/nbacc_ray97/nbacc_ray97.cfg create mode 100644 specifications/nbacg_guer01/nbacg_guer01.cfg create mode 100644 specifications/spanning/MC_spanning.cfg create mode 100644 specifications/spanning/MC_spanning.tla create mode 100644 specifications/sums_even/MC_sums_even.cfg create mode 100644 specifications/sums_even/MC_sums_even.tla create mode 100644 specifications/transaction_commit/PaxosCommit.cfg create mode 100644 specifications/transaction_commit/TCommit.cfg create mode 100644 specifications/transaction_commit/TwoPhase.cfg diff --git a/.github/scripts/check_markdown_table.py b/.github/scripts/check_markdown_table.py index 0b6bfd37..f689517e 100644 --- a/.github/scripts/check_markdown_table.py +++ b/.github/scripts/check_markdown_table.py @@ -180,6 +180,7 @@ def from_json(spec): 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) @@ -191,6 +192,7 @@ def from_json(spec): 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') diff --git a/.github/scripts/check_small_models.py b/.github/scripts/check_small_models.py index e1fd4c31..79f87273 100644 --- a/.github/scripts/check_small_models.py +++ b/.github/scripts/check_small_models.py @@ -17,6 +17,7 @@ parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True) parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) parser.add_argument('--skip', nargs='+', help='Space-separated list of models to skip checking', required=False, default=[]) +parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[]) args = parser.parse_args() logging.basicConfig(level=logging.INFO) @@ -27,6 +28,7 @@ manifest_path = normpath(args.manifest_path) examples_root = dirname(manifest_path) skip_models = [normpath(path) for path in args.skip] +only_models = [normpath(path) for path in args.only] def check_model(module_path, model, expected_runtime): module_path = tla_utils.from_cwd(examples_root, module_path) @@ -72,6 +74,7 @@ def check_model(module_path, model, expected_runtime): for model in module['models'] if model['size'] == 'small' and normpath(model['path']) not in skip_models + and (only_models == [] or normpath(model['path']) in only_models) ], key = lambda m: m[2], reverse=True diff --git a/.github/scripts/format_markdown_table.py b/.github/scripts/format_markdown_table.py index 2b1bb41d..c1c7ab88 100644 --- a/.github/scripts/format_markdown_table.py +++ b/.github/scripts/format_markdown_table.py @@ -16,10 +16,6 @@ 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): @@ -64,11 +60,21 @@ def format_table(table): ''' return -table = next((child for child in readme.children if isinstance(child, Table))) -format_table(table) +def format_document(document): + ''' + All document transformations should go here. + ''' + # Gets table of local specs + table = next((child for child in document.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: +# Read, format, write +# Need to both parse & render within same MarkdownRenderer context to preserve other formatting +with MarkdownRenderer() as renderer: + readme = None + with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file: + readme = mistletoe.Document(readme_file) + format_document(readme) + with open(normpath(args.readme_path), 'w', encoding='utf-8') as readme_file: readme_file.write(renderer.render(readme)) diff --git a/.github/scripts/generate_manifest.py b/.github/scripts/generate_manifest.py index 3c55f388..b8c6fe60 100644 --- a/.github/scripts/generate_manifest.py +++ b/.github/scripts/generate_manifest.py @@ -52,15 +52,20 @@ def get_cfg_files(examples_root, tla_path): Assume a .cfg file in the same directory as the .tla file and with the same name is a model of that .tla file; also assume this of any .cfg files where the .tla file name is only a prefix of the .cfg file name, - unless there are other .tla file names in the directory that exactly - match the .cfg file name. + unless there are other .tla file names in the directory that are longer + prefixes of the .cfg file name. """ parent_dir = dirname(tla_path) module_name, _ = splitext(basename(tla_path)) other_module_names = [other for other in get_module_names_in_dir(examples_root, parent_dir) if other != module_name] return [ - path for path in glob.glob(f'{join(parent_dir, module_name)}*.cfg', root_dir=examples_root) - if splitext(basename(path))[0] not in other_module_names + path + for path in glob.glob(f'{join(parent_dir, module_name)}*.cfg', root_dir=examples_root) + if not any([ + splitext(basename(path))[0].startswith(other_module_name) + for other_module_name in other_module_names + if len(other_module_name) > len(module_name) + ]) ] def generate_new_manifest(examples_root, ignored_dirs, parser, queries): diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py index f10b765f..85ea568a 100644 --- a/.github/scripts/tla_utils.py +++ b/.github/scripts/tla_utils.py @@ -108,6 +108,7 @@ def resolve_tlc_exit_code(code): """ tlc_exit_codes = { 0 : 'success', + 10 : 'assumption failure', 11 : 'deadlock failure', 12 : 'safety failure', 13 : 'liveness failure' diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index df6bfab4..c6b491f2 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -28,13 +28,13 @@ jobs: shell: bash steps: - name: Clone repo - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Install python - uses: actions/setup-python@v4 + uses: actions/setup-python@v5 with: python-version: '3.11' - name: Install Java - uses: actions/setup-java@v3 + uses: actions/setup-java@v4 with: distribution: adopt java-version: 17 diff --git a/.gitignore b/.gitignore index 296e2e33..dd480ffd 100644 --- a/.gitignore +++ b/.gitignore @@ -38,9 +38,11 @@ pyvenv.cfg ## Ignore directories used for local CI testing deps/ +tree-sitter-tlaplus/ # Ignore TTrace specs *_TTrace_*.tla ## Blacklist tools/ folder created by .devcontainer.json tools/ + diff --git a/README.md b/README.md index 5daf0b70..359f9dce 100644 --- a/README.md +++ b/README.md @@ -18,10 +18,11 @@ All specs in this repository are subject to CI validation to ensure quality. 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 | | --------------------------------------------------------------------------------------------------- | ------------------------------------------ | :------: | :---------: | :-----: | :-------: | :------: | +| [Teaching Concurrency](specifications/TeachingConcurrency) | Leslie Lamport | ✔ | ✔ | ✔ | ✔ | | +| [Loop Invariance](specifications/LoopInvariance) | Leslie Lamport | ✔ | ✔ | ✔ | ✔ | | | [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 | ✔ | ✔ | | | | +| [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 | ✔ | | | ✔ | | @@ -31,17 +32,16 @@ Here is a list of specs included in this repository, with links to the relevant | [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 | | ✔ | ✔ | | | +| [Stone Scale Puzzle](specifications/Stones) | Leslie Lamport | ✔ | | | ✔ | | +| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | | +| [Misra Reachability Algorithm](specifications/MisraReachability) | 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 | | ✔ | | | | +| [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 | | | ✔ | ✔ | | @@ -49,7 +49,7 @@ Here is a list of specs included in this repository, with links to the relevant | [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 | | | ✔ | | | +| [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 | | | | ✔ | | @@ -65,24 +65,24 @@ Here is a list of specs included in this repository, with links to the relevant | [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 | | | | | | +| [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 | | | | ✔ | | +| [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 | | | | ✔ | | +| [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 | | | | ✔ | | +| [SWMR Shared Memory Disk Paxos](specifications/diskpaxos) | Leslie Lamport, Giuliano Losa | | | | ✔ | | +| [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 | | | | ✔ | | +| [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | | | ✔ | | | [TLA⁺ Level Checking](specifications/LevelChecking) | Leslie Lamport | | | | | | -| [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | | | | | +| [Condition-Based Consensus](specifications/cbc_max) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | ## Examples Elsewhere Here is a list of specs stored in locations outside this repository, including submodules. @@ -137,7 +137,7 @@ Ideally these will be moved into this repo over time. ## 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. +However, your spec can be included in this repo along with your own license if you wish. ## Support or Contact Do you have any questions or comments? diff --git a/manifest-schema.json b/manifest-schema.json index 7570d518..611f72d3 100644 --- a/manifest-schema.json +++ b/manifest-schema.json @@ -78,7 +78,7 @@ "type": "array", "items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint", "ignore deadlock"]} }, - "result": {"enum": ["success", "safety failure", "liveness failure", "deadlock failure", "unknown"]} + "result": {"enum": ["success", "assumption failure", "deadlock failure", "safety failure", "liveness failure", "unknown"]} } } } diff --git a/manifest.json b/manifest.json index fa336cc3..26d75f6c 100644 --- a/manifest.json +++ b/manifest.json @@ -30,6 +30,42 @@ "proof" ], "models": [] + }, + { + "path": "specifications/Bakery-Boulangerie/MCBakery.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/Bakery-Boulangerie/MCBakery.cfg", + "runtime": "00:00:10", + "size": "small", + "mode": "exhaustive search", + "features": [ + "ignore deadlock" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/Bakery-Boulangerie/MCBoulanger.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/Bakery-Boulangerie/MCBoulanger.cfg", + "runtime": "00:01:00", + "size": "medium", + "mode": "exhaustive search", + "features": [ + "state constraint" + ], + "result": "success" + } + ] } ] }, @@ -138,7 +174,18 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/Chameneos/Chameneos.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "ignore deadlock" + ], + "result": "success" + } + ] } ] }, @@ -206,7 +253,16 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/CigaretteSmokers/CigaretteSmokers.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] } ] }, @@ -475,7 +531,16 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/GameOfLife/GameOfLife.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] } ] }, @@ -800,7 +865,9 @@ "authors": [ "Leslie Lamport" ], - "tags": [], + "tags": [ + "beginner" + ], "modules": [ { "path": "specifications/LoopInvariance/BinarySearch.tla", @@ -812,6 +879,42 @@ ], "models": [] }, + { + "path": "specifications/LoopInvariance/MCBinarySearch.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/LoopInvariance/MCBinarySearch.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/LoopInvariance/MCQuicksort.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/LoopInvariance/MCQuicksort.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, { "path": "specifications/LoopInvariance/Quicksort.tla", "communityDependencies": [], @@ -892,6 +995,66 @@ ], "tags": [], "modules": [ + { + "path": "specifications/MisraReachability/MCParReach.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/MisraReachability/MCParReach.cfg", + "runtime": "00:00:30", + "size": "medium", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/MisraReachability/MCReachabilityTest.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/MisraReachability/MCReachabilityTestAllGraphs.cfg", + "runtime": "00:00:20", + "size": "medium", + "mode": "exhaustive search", + "features": [], + "result": "success" + }, + { + "path": "specifications/MisraReachability/MCReachabilityTestRandomGraphs.cfg", + "runtime": "00:00:10", + "size": "small", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/MisraReachability/MCReachable.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/MisraReachability/MCReachable.cfg", + "runtime": "00:01:30", + "size": "medium", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, { "path": "specifications/MisraReachability/ParReach.tla", "communityDependencies": [], @@ -1299,6 +1462,71 @@ ], "models": [] }, + { + "path": "specifications/PaxosHowToWinATuringAward/MCConsensus.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/PaxosHowToWinATuringAward/MCConsensus.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "ignore deadlock" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/PaxosHowToWinATuringAward/MCPaxos.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg", + "runtime": "00:01:00", + "size": "medium", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + }, + { + "path": "specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/PaxosHowToWinATuringAward/MCVoting.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/PaxosHowToWinATuringAward/MCVoting.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "ignore deadlock", + "liveness" + ], + "result": "success" + } + ] + }, { "path": "specifications/PaxosHowToWinATuringAward/Paxos.tla", "communityDependencies": [], @@ -1641,41 +1869,87 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/SpanningTree/SpanTree.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "ignore deadlock", + "liveness" + ], + "result": "success" + } + ] }, { "path": "specifications/SpanningTree/SpanTreeRandom.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/SpanningTree/SpanTreeRandom.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "ignore deadlock" + ], + "result": "success" + } + ] }, { "path": "specifications/SpanningTree/SpanTreeTest.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] - } - ] - }, - { - "path": "specifications/SpecifyingSystems", - "title": "Specs from Specifying Systems", - "description": "All specs seen in the textbook Specifying Systems by Leslie Lamport", - "source": "http://lamport.azurewebsites.net/tla/book.html", - "authors": [ - "Leslie Lamport" - ], - "tags": [ - "beginner" - ], - "modules": [ - { - "path": "specifications/SpecifyingSystems/AdvancedExamples/BNFGrammars.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], + "models": [ + { + "path": "specifications/SpanningTree/SpanTreeTest4Nodes.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "ignore deadlock", + "liveness" + ], + "result": "success" + }, + { + "path": "specifications/SpanningTree/SpanTreeTest5Nodes.cfg", + "runtime": "unknown", + "size": "large", + "mode": "exhaustive search", + "features": [ + "ignore deadlock", + "liveness" + ], + "result": "unknown" + } + ] + } + ] + }, + { + "path": "specifications/SpecifyingSystems", + "title": "Specs from Specifying Systems", + "description": "All specs seen in the textbook Specifying Systems by Leslie Lamport", + "source": "http://lamport.azurewebsites.net/tla/book.html", + "authors": [ + "Leslie Lamport" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/SpecifyingSystems/AdvancedExamples/BNFGrammars.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], "models": [] }, { @@ -2370,7 +2644,16 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/Stones/Stones.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] } ] }, @@ -2433,7 +2716,16 @@ "pluscal", "proof" ], - "models": [] + "models": [ + { + "path": "specifications/TeachingConcurrency/Simple.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] }, { "path": "specifications/TeachingConcurrency/SimpleRegular.tla", @@ -2443,7 +2735,16 @@ "pluscal", "proof" ], - "models": [] + "models": [ + { + "path": "specifications/TeachingConcurrency/SimpleRegular.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] } ] }, @@ -2493,6 +2794,22 @@ "features": [], "models": [] }, + { + "path": "specifications/TwoPhase/MCTwoPhase.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/TwoPhase/MCTwoPhase.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] + }, { "path": "specifications/TwoPhase/TLAPS.tla", "communityDependencies": [], @@ -2530,7 +2847,18 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/aba-asyn-byz/aba_asyn_byz.cfg", + "runtime": "00:10:00", + "size": "large", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] } ] }, @@ -2637,7 +2965,28 @@ "features": [ "proof" ], - "models": [] + "models": [ + { + "path": "specifications/bcastByz/bcastByz.cfg", + "runtime": "00:00:10", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + }, + { + "path": "specifications/bcastByz/bcastByzNoBcast.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] } ] }, @@ -2658,7 +3007,18 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/bcastFolklore/bcastFolklore.cfg", + "runtime": "00:30:00", + "size": "large", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] } ] }, @@ -2679,7 +3039,16 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/bosco/bosco.cfg", + "runtime": "00:03:00", + "size": "medium", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] } ] }, @@ -2700,7 +3069,18 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/c1cs/c1cs.cfg", + "runtime": "unknown", + "size": "large", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "unknown" + } + ] } ] }, @@ -2742,7 +3122,18 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/cf1s-folklore/cf1s_folklore.cfg", + "runtime": "00:01:00", + "size": "medium", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] } ] }, @@ -2764,6 +3155,25 @@ "pluscal" ], "models": [] + }, + { + "path": "specifications/chang_roberts/MCChangRoberts.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/chang_roberts/MCChangRoberts.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "ignore deadlock", + "liveness" + ], + "result": "success" + } + ] } ] }, @@ -2798,7 +3208,18 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/detector_chan96/EnvironmentController.cfg", + "runtime": "02:00:00", + "size": "large", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] } ] }, @@ -2902,6 +3323,22 @@ "features": [], "models": [] }, + { + "path": "specifications/diskpaxos/MC_HDiskSynod.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/diskpaxos/MC_HDiskSynod.cfg", + "runtime": "unknown", + "size": "large", + "mode": "exhaustive search", + "features": [], + "result": "unknown" + } + ] + }, { "path": "specifications/diskpaxos/Synod.tla", "communityDependencies": [], @@ -3480,21 +3917,56 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/glowingRaccoon/clean.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] }, { "path": "specifications/glowingRaccoon/product.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/glowingRaccoon/product.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "ignore deadlock", + "liveness" + ], + "result": "success" + } + ] }, { "path": "specifications/glowingRaccoon/stages.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/glowingRaccoon/stages.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "ignore deadlock", + "liveness" + ], + "result": "success" + } + ] } ] }, @@ -3531,6 +4003,24 @@ ], "models": [] }, + { + "path": "specifications/lamport_mutex/MCLamportMutex.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/lamport_mutex/MCLamportMutex.cfg", + "runtime": "00:00:10", + "size": "small", + "mode": "exhaustive search", + "features": [ + "state constraint" + ], + "result": "success" + } + ] + }, { "path": "specifications/lamport_mutex/NaturalsInduction.tla", "communityDependencies": [], @@ -3580,7 +4070,16 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/nbacc_ray97/nbacc_ray97.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] } ] }, @@ -3601,7 +4100,18 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/nbacg_guer01/nbacg_guer01.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] } ] }, @@ -3617,6 +4127,22 @@ ], "tags": [], "modules": [ + { + "path": "specifications/spanning/MC_spanning.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/spanning/MC_spanning.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [], + "result": "safety failure" + } + ] + }, { "path": "specifications/spanning/spanning.tla", "communityDependencies": [], @@ -3638,6 +4164,22 @@ "beginner" ], "modules": [ + { + "path": "specifications/sums_even/MC_sums_even.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/sums_even/MC_sums_even.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] + }, { "path": "specifications/sums_even/TLAPS.tla", "communityDependencies": [], @@ -3740,21 +4282,50 @@ "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/transaction_commit/PaxosCommit.cfg", + "runtime": "00:00:30", + "size": "medium", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] }, { "path": "specifications/transaction_commit/TCommit.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/transaction_commit/TCommit.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "ignore deadlock" + ], + "result": "success" + } + ] }, { "path": "specifications/transaction_commit/TwoPhase.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], - "models": [] + "models": [ + { + "path": "specifications/transaction_commit/TwoPhase.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [], + "result": "success" + } + ] } ] } diff --git a/specifications/Bakery-Boulangerie/MCBakery.cfg b/specifications/Bakery-Boulangerie/MCBakery.cfg new file mode 100644 index 00000000..b0af6112 --- /dev/null +++ b/specifications/Bakery-Boulangerie/MCBakery.cfg @@ -0,0 +1,10 @@ +CONSTANT + N = 2 + MaxNat = 2 + Nat <- NatOverride +INVARIANTS MutualExclusion TypeOK Inv +\* https://github.com/tlaplus/Examples/issues/109 +\*PROPERTIES DeadlockFree StarvationFree +SPECIFICATION ISpec +CHECK_DEADLOCK FALSE + diff --git a/specifications/Bakery-Boulangerie/MCBakery.tla b/specifications/Bakery-Boulangerie/MCBakery.tla new file mode 100644 index 00000000..d9f40ecf --- /dev/null +++ b/specifications/Bakery-Boulangerie/MCBakery.tla @@ -0,0 +1,7 @@ +---------------------------- MODULE MCBakery -------------------------------- +EXTENDS Bakery +CONSTANT MaxNat +ASSUME MaxNat \in Nat +NatOverride == 0 .. MaxNat +============================================================================= + diff --git a/specifications/Bakery-Boulangerie/MCBoulanger.cfg b/specifications/Bakery-Boulangerie/MCBoulanger.cfg new file mode 100644 index 00000000..5aae39a3 --- /dev/null +++ b/specifications/Bakery-Boulangerie/MCBoulanger.cfg @@ -0,0 +1,8 @@ +CONSTANTS + N = 3 + MaxNat = 3 + Nat <- NatOverride +INVARIANTS MutualExclusion TypeOK Inv +SPECIFICATION Spec +CONSTRAINT StateConstraint + diff --git a/specifications/Bakery-Boulangerie/MCBoulanger.tla b/specifications/Bakery-Boulangerie/MCBoulanger.tla new file mode 100644 index 00000000..a3c6142d --- /dev/null +++ b/specifications/Bakery-Boulangerie/MCBoulanger.tla @@ -0,0 +1,8 @@ +--------------------------- MODULE MCBoulanger ------------------------------ +EXTENDS Boulanger +CONSTANT MaxNat +ASSUME MaxNat \in Nat +NatOverride == 0 .. MaxNat +StateConstraint == \A process \in Procs : num[process] < MaxNat +============================================================================= + diff --git a/specifications/Chameneos/Chameneos.cfg b/specifications/Chameneos/Chameneos.cfg new file mode 100644 index 00000000..82980ea0 --- /dev/null +++ b/specifications/Chameneos/Chameneos.cfg @@ -0,0 +1,9 @@ +CONSTANTS + N = 4 + M = 4 + Faded = Faded + MeetingPlaceEmpty = MeetingPlaceEmpty +INVARIANTS TypeOK SumMet +SPECIFICATION Spec +CHECK_DEADLOCK FALSE + diff --git a/specifications/CigaretteSmokers/CigaretteSmokers.cfg b/specifications/CigaretteSmokers/CigaretteSmokers.cfg new file mode 100644 index 00000000..b568ea64 --- /dev/null +++ b/specifications/CigaretteSmokers/CigaretteSmokers.cfg @@ -0,0 +1,6 @@ +CONSTANTS + Ingredients = {matches, paper, tobacco} + Offers = {{matches, paper}, {matches, tobacco}, {paper, tobacco}} +INVARIANTS TypeOK AtMostOne +SPECIFICATION Spec + diff --git a/specifications/CigaretteSmokers/CigaretteSmokers.tla b/specifications/CigaretteSmokers/CigaretteSmokers.tla index ef52e04d..e4794de8 100644 --- a/specifications/CigaretteSmokers/CigaretteSmokers.tla +++ b/specifications/CigaretteSmokers/CigaretteSmokers.tla @@ -12,7 +12,7 @@ VARIABLE smokers, dealer (***************************************************************************) (* 'Ingredients' is a set of ingredients, originally *) (* {matches, paper, tobacco}. 'Offers' is a subset of subsets of *) -(* ingredients, each missing just one ingriedent *) +(* ingredients, each missing just one ingredient *) (***************************************************************************) ASSUME /\ Offers \subseteq (SUBSET Ingredients) /\ \A n \in Offers : Cardinality(n) = Cardinality(Ingredients) - 1 diff --git a/specifications/GameOfLife/GameOfLife.cfg b/specifications/GameOfLife/GameOfLife.cfg new file mode 100644 index 00000000..521c6e6a --- /dev/null +++ b/specifications/GameOfLife/GameOfLife.cfg @@ -0,0 +1,4 @@ +CONSTANT N = 4 +INVARIANT TypeOK +SPECIFICATION Spec + diff --git a/specifications/LoopInvariance/MCBinarySearch.cfg b/specifications/LoopInvariance/MCBinarySearch.cfg new file mode 100644 index 00000000..5b46fac3 --- /dev/null +++ b/specifications/LoopInvariance/MCBinarySearch.cfg @@ -0,0 +1,8 @@ +CONSTANTS + Values = {1,2,3,4,5} + MaxSeqLen = 8 + Seq <- LimitedSeq +INVARIANTS resultCorrect TypeOK Inv +PROPERTY Termination +SPECIFICATION Spec + diff --git a/specifications/LoopInvariance/MCBinarySearch.tla b/specifications/LoopInvariance/MCBinarySearch.tla new file mode 100644 index 00000000..1a1b63dd --- /dev/null +++ b/specifications/LoopInvariance/MCBinarySearch.tla @@ -0,0 +1,7 @@ +--------------------------- MODULE MCBinarySearch --------------------------- +EXTENDS BinarySearch +CONSTANT MaxSeqLen +ASSUME MaxSeqLen \in Nat +LimitedSeq(S) == UNION {[1 .. n -> S] : n \in 1 .. MaxSeqLen} +============================================================================= + diff --git a/specifications/LoopInvariance/MCQuicksort.cfg b/specifications/LoopInvariance/MCQuicksort.cfg new file mode 100644 index 00000000..bd23c2be --- /dev/null +++ b/specifications/LoopInvariance/MCQuicksort.cfg @@ -0,0 +1,8 @@ +CONSTANTS + Values = {1,2,3} + MaxSeqLen = 4 + Seq <- LimitedSeq +INVARIANTS PCorrect TypeOK Inv +PROPERTY Termination +SPECIFICATION Spec + diff --git a/specifications/LoopInvariance/MCQuicksort.tla b/specifications/LoopInvariance/MCQuicksort.tla new file mode 100644 index 00000000..e3f5d31f --- /dev/null +++ b/specifications/LoopInvariance/MCQuicksort.tla @@ -0,0 +1,7 @@ +---------------------------- MODULE MCQuicksort ----------------------------- +EXTENDS Quicksort +CONSTANT MaxSeqLen +ASSUME MaxSeqLen \in Nat +LimitedSeq(S) == UNION {[1 .. n -> S] : n \in 1 .. MaxSeqLen} +============================================================================= + diff --git a/specifications/MisraReachability/MCParReach.cfg b/specifications/MisraReachability/MCParReach.cfg new file mode 100644 index 00000000..7c58b89e --- /dev/null +++ b/specifications/MisraReachability/MCParReach.cfg @@ -0,0 +1,10 @@ +CONSTANTS + Nodes = {n1, n2, n3, n4} + Root = n1 + Procs = {p1, p2} + Succ <- ConnectedToSomeButNotAll + Seq <- LimitedSeq +INVARIANT Inv +PROPERTY Refines +SPECIFICATION Spec + diff --git a/specifications/MisraReachability/MCParReach.tla b/specifications/MisraReachability/MCParReach.tla new file mode 100644 index 00000000..a519a154 --- /dev/null +++ b/specifications/MisraReachability/MCParReach.tla @@ -0,0 +1,14 @@ +---- MODULE MCParReach ---- +EXTENDS ParReach + +ConnectedToSomeButNotAll == + CHOOSE succ \in [Nodes -> SUBSET Nodes] + : \A n \in Nodes : Cardinality(succ[n]) = 2 + +LimitedSeq(S) == UNION { + [1 .. len -> S] + : len \in 0 .. Cardinality(Nodes) +} + +============================ + diff --git a/specifications/MisraReachability/MCReachabilityTest.tla b/specifications/MisraReachability/MCReachabilityTest.tla new file mode 100644 index 00000000..96ebeb00 --- /dev/null +++ b/specifications/MisraReachability/MCReachabilityTest.tla @@ -0,0 +1,15 @@ +---- MODULE MCReachabilityTest ---- +EXTENDS ReachabilityTest, Sequences + +CONSTANT RandomSuccCount + +RandomSuccSet == SuccSet2(RandomSuccCount) + +ASSUME \A i \in DOMAIN Test : Test[i] + +LimitedSeq(S) == UNION { + [1 .. len -> S] + : len \in 0 .. Cardinality(Nodes) +} +=================================== + diff --git a/specifications/MisraReachability/MCReachabilityTestAllGraphs.cfg b/specifications/MisraReachability/MCReachabilityTestAllGraphs.cfg new file mode 100644 index 00000000..7c117757 --- /dev/null +++ b/specifications/MisraReachability/MCReachabilityTestAllGraphs.cfg @@ -0,0 +1,6 @@ +CONSTANTS + RandomSuccCount = 0 + Nodes = {n1, n2, n3} + SuccSet <- SuccSet1 + Seq <- LimitedSeq + diff --git a/specifications/MisraReachability/MCReachabilityTestRandomGraphs.cfg b/specifications/MisraReachability/MCReachabilityTestRandomGraphs.cfg new file mode 100644 index 00000000..da2eb976 --- /dev/null +++ b/specifications/MisraReachability/MCReachabilityTestRandomGraphs.cfg @@ -0,0 +1,6 @@ +CONSTANTS + RandomSuccCount = 5 + Nodes = {n1, n2, n3, n4} + SuccSet <- RandomSuccSet + Seq <- LimitedSeq + diff --git a/specifications/MisraReachability/MCReachable.cfg b/specifications/MisraReachability/MCReachable.cfg new file mode 100644 index 00000000..efe6ec30 --- /dev/null +++ b/specifications/MisraReachability/MCReachable.cfg @@ -0,0 +1,9 @@ +CONSTANTS + Nodes = {n1, n2, n3, n4} + Root = n1 + Succ <- ConnectedToSomeButNotAll + Seq <- LimitedSeq +INVARIANTS TypeOK Inv1 Inv2 Inv3 PartialCorrectness +PROPERTY Termination +SPECIFICATION Spec + diff --git a/specifications/MisraReachability/MCReachable.tla b/specifications/MisraReachability/MCReachable.tla new file mode 100644 index 00000000..79048427 --- /dev/null +++ b/specifications/MisraReachability/MCReachable.tla @@ -0,0 +1,14 @@ +---- MODULE MCReachable ---- +EXTENDS Reachable + +ConnectedToSomeButNotAll == + CHOOSE succ \in [Nodes -> SUBSET Nodes] + : \A n \in Nodes : Cardinality(succ[n]) = 2 + +LimitedSeq(S) == UNION { + [1 .. len -> S] + : len \in 0 .. Cardinality(Nodes) +} + +============================ + diff --git a/specifications/MisraReachability/ParReach.tla b/specifications/MisraReachability/ParReach.tla index 2a809a35..3d9e8e8c 100644 --- a/specifications/MisraReachability/ParReach.tla +++ b/specifications/MisraReachability/ParReach.tla @@ -216,7 +216,8 @@ R == INSTANCE Reachable WITH vroot <- vrootBar, pc <- pcBar (* it, use models with behavior specification spec that check the temporal *) (* property R!Spec.) *) (***************************************************************************) -THEOREM Spec => R!Spec +Refines == R!Spec +THEOREM Spec => Refines (***************************************************************************) (* By the definition of formula Spec of module Reachable, this theorem *) diff --git a/specifications/MisraReachability/Reachable.tla b/specifications/MisraReachability/Reachable.tla index eeeb697e..1774d908 100644 --- a/specifications/MisraReachability/Reachable.tla +++ b/specifications/MisraReachability/Reachable.tla @@ -190,7 +190,8 @@ Inv3 == Reachable = marked \cup ReachableFrom(vroot) (* then `marked' equals Reachable. The algorithm has terminated when pc *) (* equals "Done", so this theorem asserts partial correctness. *) (***************************************************************************) -THEOREM Spec => []((pc = "Done") => (marked = Reachable)) +PartialCorrectness == (pc = "Done") => (marked = Reachable) +THEOREM Spec => []PartialCorrectness (*************************************************************************) (* TypeOK implies (pc = "Done") => (vroot = {}). Since, *) (* ReachableFrom({}) equals {}, Inv3 implies *) diff --git a/specifications/PaxosHowToWinATuringAward/MCConsensus.cfg b/specifications/PaxosHowToWinATuringAward/MCConsensus.cfg new file mode 100644 index 00000000..cd8b671b --- /dev/null +++ b/specifications/PaxosHowToWinATuringAward/MCConsensus.cfg @@ -0,0 +1,17 @@ +\* MV CONSTANT declarations +CONSTANTS +a = a +b = b +c = c +\* MV CONSTANT definitions +CONSTANT +Value <- const_156017750645611000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* INVARIANT definition +INVARIANT +Inv +\* Generated on Mon Jun 10 07:38:26 PDT 2019 +CHECK_DEADLOCK FALSE + diff --git a/specifications/PaxosHowToWinATuringAward/MCConsensus.tla b/specifications/PaxosHowToWinATuringAward/MCConsensus.tla new file mode 100644 index 00000000..3a343f8a --- /dev/null +++ b/specifications/PaxosHowToWinATuringAward/MCConsensus.tla @@ -0,0 +1,16 @@ +---- MODULE MCConsensus ---- +EXTENDS Consensus, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +a, b, c +---- + +\* MV CONSTANT definitions Value +const_156017750645611000 == +{a, b, c} +---- + +============================================================================= +\* Modification History +\* Created Mon Jun 10 07:38:26 PDT 2019 by lamport diff --git a/specifications/PaxosHowToWinATuringAward/MCPaxos.tla b/specifications/PaxosHowToWinATuringAward/MCPaxos.tla new file mode 100644 index 00000000..09e3d3c9 --- /dev/null +++ b/specifications/PaxosHowToWinATuringAward/MCPaxos.tla @@ -0,0 +1,45 @@ +---- MODULE MCPaxos ---- +EXTENDS Paxos, TLC + +CONSTANT MaxBallot + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +a1, a2, a3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +v1, v2 +---- + +\* MV CONSTANT definitions Acceptor +const_1560336937634605000 == +{a1, a2, a3} +---- + +\* MV CONSTANT definitions Value +const_1560336937634606000 == +{v1, v2} +---- + +\* CONSTANT definitions @modelParameterConstants:1Quorum +const_1560336937634607000 == +{{a1, a2}, {a1, a3}, {a2, a3}} +---- + +\* CONSTANT definition @modelParameterDefinitions:1 +def_ov_1560336937634609000 == +0..MaxBallot +---- +\* CONSTANT definition @modelParameterDefinitions:2 +def_ov_1560336937634610000 == +0..MaxBallot +---- +\* PROPERTY definition @modelCorrectnessProperties:0 +prop_1560336937635612000 == +V!Spec +---- +============================================================================= +\* Modification History +\* Created Wed Jun 12 03:55:37 PDT 2019 by lamport diff --git a/specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg b/specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg new file mode 100644 index 00000000..53a0208c --- /dev/null +++ b/specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg @@ -0,0 +1,35 @@ +\* MV CONSTANT declarations +CONSTANT +MaxBallot = 2 +CONSTANTS +a1 = a1 +a2 = a2 +a3 = a3 +\* MV CONSTANT declarations +CONSTANTS +v1 = v1 +v2 = v2 +\* MV CONSTANT definitions +CONSTANT +Acceptor <- const_1560336937634605000 +\* MV CONSTANT definitions +CONSTANT +Value <- const_1560336937634606000 +\* CONSTANT definitions +CONSTANT +Quorum <- const_1560336937634607000 +\* CONSTANT definition +CONSTANT +None = None +Ballot <- def_ov_1560336937634609000 +Ballot <- [Voting]def_ov_1560336937634610000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* INVARIANT definition +INVARIANT +Inv +\* PROPERTY definition +PROPERTY +prop_1560336937635612000 +\* Generated on Wed Jun 12 03:55:37 PDT 2019 diff --git a/specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg b/specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg new file mode 100644 index 00000000..520e0d69 --- /dev/null +++ b/specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg @@ -0,0 +1,35 @@ +\* MV CONSTANT declarations +CONSTANT +MaxBallot = 1 +CONSTANTS +a1 = a1 +a2 = a2 +a3 = a3 +\* MV CONSTANT declarations +CONSTANTS +v1 = v1 +v2 = v2 +\* MV CONSTANT definitions +CONSTANT +Acceptor <- const_1560336937634605000 +\* MV CONSTANT definitions +CONSTANT +Value <- const_1560336937634606000 +\* CONSTANT definitions +CONSTANT +Quorum <- const_1560336937634607000 +\* CONSTANT definition +CONSTANT +None = None +Ballot <- def_ov_1560336937634609000 +Ballot <- [Voting]def_ov_1560336937634610000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* INVARIANT definition +INVARIANT +Inv +\* PROPERTY definition +PROPERTY +prop_1560336937635612000 +\* Generated on Wed Jun 12 03:55:37 PDT 2019 diff --git a/specifications/PaxosHowToWinATuringAward/MCVoting.cfg b/specifications/PaxosHowToWinATuringAward/MCVoting.cfg new file mode 100644 index 00000000..05eeacc6 --- /dev/null +++ b/specifications/PaxosHowToWinATuringAward/MCVoting.cfg @@ -0,0 +1,33 @@ +\* MV CONSTANT declarations +CONSTANTS +a1 = a1 +a2 = a2 +a3 = a3 +\* MV CONSTANT declarations +CONSTANTS +v1 = v1 +v2 = v2 +\* MV CONSTANT definitions +CONSTANT +Acceptor <- const_156180051387243000 +\* MV CONSTANT definitions +CONSTANT +Value <- const_156180051387244000 +\* CONSTANT definitions +CONSTANT +Quorum <- const_156180051387245000 +\* CONSTANT definition +CONSTANT +Ballot <- def_ov_156180051387246000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* INVARIANT definition +INVARIANT +Inv +\* PROPERTY definition +PROPERTY +prop_156180051387248000 +\* Generated on Sat Jun 29 02:28:33 PDT 2019 +CHECK_DEADLOCK FALSE + diff --git a/specifications/PaxosHowToWinATuringAward/MCVoting.tla b/specifications/PaxosHowToWinATuringAward/MCVoting.tla new file mode 100644 index 00000000..1e61ffe9 --- /dev/null +++ b/specifications/PaxosHowToWinATuringAward/MCVoting.tla @@ -0,0 +1,39 @@ +---- MODULE MCVoting ---- +EXTENDS Voting, TLC + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +a1, a2, a3 +---- + +\* MV CONSTANT declarations@modelParameterConstants +CONSTANTS +v1, v2 +---- + +\* MV CONSTANT definitions Acceptor +const_156180051387243000 == +{a1, a2, a3} +---- + +\* MV CONSTANT definitions Value +const_156180051387244000 == +{v1, v2} +---- + +\* CONSTANT definitions @modelParameterConstants:2Quorum +const_156180051387245000 == +{{a1, a2}, {a1, a3}, {a2, a3}} +---- + +\* CONSTANT definition @modelParameterDefinitions:0 +def_ov_156180051387246000 == +0..2 +---- +\* PROPERTY definition @modelCorrectnessProperties:0 +prop_156180051387248000 == +C!Spec +---- +============================================================================= +\* Modification History +\* Created Sat Jun 29 02:28:33 PDT 2019 by lamport diff --git a/specifications/SpanningTree/SpanTree.cfg b/specifications/SpanningTree/SpanTree.cfg new file mode 100644 index 00000000..36a00d29 --- /dev/null +++ b/specifications/SpanningTree/SpanTree.cfg @@ -0,0 +1,10 @@ +CONSTANTS + Nodes = {n1, n2, n3, n4, n5} + Edges = {{n1, n2}, {n1, n3}, {n2, n3}, {n2, n4}, {n3, n4}, {n3, n5}, {n4, n5}} + MaxCardinality = 6 + Root = n1 +INVARIANT TypeOK +PROPERTIES Liveness Safety +SPECIFICATION Spec +CHECK_DEADLOCK FALSE + diff --git a/specifications/SpanningTree/SpanTreeRandom.cfg b/specifications/SpanningTree/SpanTreeRandom.cfg new file mode 100644 index 00000000..70862f02 --- /dev/null +++ b/specifications/SpanningTree/SpanTreeRandom.cfg @@ -0,0 +1,10 @@ +CONSTANTS + Nodes = {n1, n2, n3, n4, n5, n6} + MaxCardinality = 6 + Root = n1 +INVARIANT TypeOK +\* https://github.com/tlaplus/tlaplus/issues/866 +\*PROPERTY Liveness Safety +SPECIFICATION Spec +CHECK_DEADLOCK FALSE + diff --git a/specifications/SpanningTree/SpanTreeTest4Nodes.cfg b/specifications/SpanningTree/SpanTreeTest4Nodes.cfg new file mode 100644 index 00000000..c1bf5c58 --- /dev/null +++ b/specifications/SpanningTree/SpanTreeTest4Nodes.cfg @@ -0,0 +1,9 @@ +CONSTANTS + Nodes = {n1, n2, n3, n4} + MaxCardinality = 5 + Root = n1 +INVARIANT TypeOK +PROPERTIES Liveness Safety +SPECIFICATION Spec +CHECK_DEADLOCK FALSE + diff --git a/specifications/SpanningTree/SpanTreeTest5Nodes.cfg b/specifications/SpanningTree/SpanTreeTest5Nodes.cfg new file mode 100644 index 00000000..d68ffd09 --- /dev/null +++ b/specifications/SpanningTree/SpanTreeTest5Nodes.cfg @@ -0,0 +1,9 @@ +CONSTANTS + Nodes = {n1, n2, n3, n4, n5} + MaxCardinality = 5 + Root = n1 +INVARIANT TypeOK +PROPERTIES Liveness Safety +SPECIFICATION Spec +CHECK_DEADLOCK FALSE + diff --git a/specifications/Stones/Stones.cfg b/specifications/Stones/Stones.cfg new file mode 100644 index 00000000..51c16a85 --- /dev/null +++ b/specifications/Stones/Stones.cfg @@ -0,0 +1,4 @@ +CONSTANTS + W = 40 + N = 4 + diff --git a/specifications/TeachingConcurrency/Simple.cfg b/specifications/TeachingConcurrency/Simple.cfg new file mode 100644 index 00000000..8372dbb5 --- /dev/null +++ b/specifications/TeachingConcurrency/Simple.cfg @@ -0,0 +1,4 @@ +CONSTANT N = 5 +SPECIFICATION Spec +INVARIANTS PCorrect TypeOK Inv + diff --git a/specifications/TeachingConcurrency/SimpleRegular.cfg b/specifications/TeachingConcurrency/SimpleRegular.cfg new file mode 100644 index 00000000..a3d615fd --- /dev/null +++ b/specifications/TeachingConcurrency/SimpleRegular.cfg @@ -0,0 +1,4 @@ +CONSTANT N = 8 +SPECIFICATION Spec +INVARIANTS PCorrect TypeOK Inv + diff --git a/specifications/TwoPhase/MCTwoPhase.cfg b/specifications/TwoPhase/MCTwoPhase.cfg new file mode 100644 index 00000000..ceec4fe0 --- /dev/null +++ b/specifications/TwoPhase/MCTwoPhase.cfg @@ -0,0 +1,3 @@ +INVARIANT Inv +SPECIFICATION Spec + diff --git a/specifications/TwoPhase/MCTwoPhase.tla b/specifications/TwoPhase/MCTwoPhase.tla new file mode 100644 index 00000000..15bb9827 --- /dev/null +++ b/specifications/TwoPhase/MCTwoPhase.tla @@ -0,0 +1,7 @@ +----------------------------- MODULE MCTwoPhase ----------------------------- +XInit(v) == v = 0 +XAct(i, xInit, xNext) == xNext = xInit +VARIABLES p, c, x +INSTANCE TwoPhase +============================================================================= + diff --git a/specifications/aba-asyn-byz/aba_asyn_byz.cfg b/specifications/aba-asyn-byz/aba_asyn_byz.cfg new file mode 100644 index 00000000..bfc4bce7 --- /dev/null +++ b/specifications/aba-asyn-byz/aba_asyn_byz.cfg @@ -0,0 +1,8 @@ +CONSTANTS + N = 4 + T = 1 + F = 1 +INVARIANTS TypeOK +PROPERTIES Unforg_Ltl Corr_Ltl Agreement_Ltl +SPECIFICATION Spec + diff --git a/specifications/bcastByz/bcastByz.cfg b/specifications/bcastByz/bcastByz.cfg new file mode 100644 index 00000000..581bb993 --- /dev/null +++ b/specifications/bcastByz/bcastByz.cfg @@ -0,0 +1,8 @@ +CONSTANTS + N = 4 + T = 1 + F = 1 +INVARIANTS TypeOK FCConstraints +PROPERTIES CorrLtl RelayLtl UnforgLtl +SPECIFICATION Spec + diff --git a/specifications/bcastByz/bcastByzNoBcast.cfg b/specifications/bcastByz/bcastByzNoBcast.cfg new file mode 100644 index 00000000..f7a5ab49 --- /dev/null +++ b/specifications/bcastByz/bcastByzNoBcast.cfg @@ -0,0 +1,8 @@ +CONSTANTS + N = 10 + T = 3 + F = 2 +INVARIANTS TypeOK FCConstraints Unforg +PROPERTIES CorrLtl RelayLtl +SPECIFICATION SpecNoBcast + diff --git a/specifications/bcastFolklore/bcastFolklore.cfg b/specifications/bcastFolklore/bcastFolklore.cfg new file mode 100644 index 00000000..5371d27c --- /dev/null +++ b/specifications/bcastFolklore/bcastFolklore.cfg @@ -0,0 +1,8 @@ +CONSTANTS + N = 4 + T = 1 + F = 1 +INVARIANTS TypeOK +PROPERTIES UnforgLtl CorrLtl RelayLtl ReliableChan +SPECIFICATION Spec + diff --git a/specifications/bosco/bosco.cfg b/specifications/bosco/bosco.cfg new file mode 100644 index 00000000..30694dce --- /dev/null +++ b/specifications/bosco/bosco.cfg @@ -0,0 +1,7 @@ +CONSTANTS + N = 4 + T = 1 + F = 1 +INVARIANTS TypeOK Lemma3_0 Lemma3_1 Lemma4_0 Lemma4_1 +SPECIFICATION Spec + diff --git a/specifications/c1cs/c1cs.cfg b/specifications/c1cs/c1cs.cfg new file mode 100644 index 00000000..35c98675 --- /dev/null +++ b/specifications/c1cs/c1cs.cfg @@ -0,0 +1,10 @@ +CONSTANTS + N = 4 + T = 1 + F = 1 + Values = {v1, v2} + Bottom = Bottom +INVARIANTS TypeOK Validity Agreement WeakAgreement IndStrengthens +PROPERTIES Termination +SPECIFICATION Spec + diff --git a/specifications/cf1s-folklore/cf1s_folklore.cfg b/specifications/cf1s-folklore/cf1s_folklore.cfg new file mode 100644 index 00000000..b8874992 --- /dev/null +++ b/specifications/cf1s-folklore/cf1s_folklore.cfg @@ -0,0 +1,8 @@ +CONSTANTS + N = 4 + T = 1 + F = 1 +INVARIANTS TypeOK +PROPERTIES OneStep0_Ltl OneStep1_Ltl +SPECIFICATION Spec + diff --git a/specifications/cf1s-folklore/cf1s_folklore.tla b/specifications/cf1s-folklore/cf1s_folklore.tla index 8494dcfa..53c2b7aa 100644 --- a/specifications/cf1s-folklore/cf1s_folklore.tla +++ b/specifications/cf1s-folklore/cf1s_folklore.tla @@ -150,9 +150,7 @@ OneStep0_Ltl == (* If all processes propose 1, then every process crashes or decides 1. *) OneStep1_Ltl == (\A i \in Proc : pc[i] = "V1") => <>(\A i \in Proc : pc[i] # "U0" /\ pc[i] # "U1" /\ pc[i] # "D0") - - - + ============================================================================= \* Modification History \* Last modified Mon Jul 09 13:26:59 CEST 2018 by tthai diff --git a/specifications/chang_roberts/MCChangRoberts.cfg b/specifications/chang_roberts/MCChangRoberts.cfg new file mode 100644 index 00000000..a2f9cfcf --- /dev/null +++ b/specifications/chang_roberts/MCChangRoberts.cfg @@ -0,0 +1,6 @@ +CONSTANT N = 3 +INVARIANTS TypeOK Correctness +PROPERTY Liveness +SPECIFICATION Spec +CHECK_DEADLOCK FALSE + diff --git a/specifications/chang_roberts/MCChangRoberts.tla b/specifications/chang_roberts/MCChangRoberts.tla new file mode 100644 index 00000000..b7796615 --- /dev/null +++ b/specifications/chang_roberts/MCChangRoberts.tla @@ -0,0 +1,9 @@ +--------------------------- MODULE MCChangRoberts --------------------------- +EXTENDS Naturals +CONSTANT N +VARIABLES msgs, pc, initiator, state +ASSUME N \in Nat +Id == [i \in 1 .. N |-> i] +INSTANCE ChangRoberts +============================================================================= + diff --git a/specifications/detector_chan96/EnvironmentController.cfg b/specifications/detector_chan96/EnvironmentController.cfg new file mode 100644 index 00000000..43202d46 --- /dev/null +++ b/specifications/detector_chan96/EnvironmentController.cfg @@ -0,0 +1,12 @@ +CONSTANTS + N = 3 + T = 1 + d0 = 2 + SendPoint = 2 + PredictPoint = 3 + DELTA = 1 + PHI = 1 +INVARIANT TypeOK +PROPERTIES StrongCompleteness EventuallyStrongAccuracy +SPECIFICATION Spec + diff --git a/specifications/detector_chan96/EnvironmentController.tla b/specifications/detector_chan96/EnvironmentController.tla index c3e32f78..0a7fe234 100644 --- a/specifications/detector_chan96/EnvironmentController.tla +++ b/specifications/detector_chan96/EnvironmentController.tla @@ -1,6 +1,6 @@ ----------------------- MODULE EnvironmentController ----------------------- -(* An encoding of a parameterized and partially syncrhonous model of the eventually +(* An encoding of a parameterized and partially synchronous model of the eventually perfect failure detectors with crash faults from: [1] Chandra, Tushar Deepak, and Sam Toueg. "Unreliable failure detectors for @@ -87,7 +87,7 @@ TLC spends more than 2 hours (from 11:17 to 13:26) verifying these properties. o PROBLEMS with TLC: I believe that PHIConstraint and PHIConstraint1 are equivalent. - However, whenever I check this specification with PHIConstraing1, TLC shows an + However, whenever I check this specification with PHIConstraint1, TLC shows an error: "Too many possible next states for the last state in the trace." I guess that the reasons are from optimizations for disjunctions. *) diff --git a/specifications/diskpaxos/MC_HDiskSynod.cfg b/specifications/diskpaxos/MC_HDiskSynod.cfg new file mode 100644 index 00000000..185d4ec5 --- /dev/null +++ b/specifications/diskpaxos/MC_HDiskSynod.cfg @@ -0,0 +1,12 @@ +CONSTANTS + N = 3 + Inputs = {in1, in2} + NotAnInput = NotAnInput + BallotCountPerProcess = 2 + Ballot <- BallotImpl + Disk = {1, 2} + IsMajority <- IsMajorityImpl +INVARIANTS HInv1 HInv2 HInv3 HInv4 HInv6 +INIT HInit +NEXT HNext + diff --git a/specifications/diskpaxos/MC_HDiskSynod.tla b/specifications/diskpaxos/MC_HDiskSynod.tla new file mode 100644 index 00000000..0a6bad4e --- /dev/null +++ b/specifications/diskpaxos/MC_HDiskSynod.tla @@ -0,0 +1,9 @@ +---- MODULE MC_HDiskSynod ---- +EXTENDS HDiskSynod, TLC +CONSTANT BallotCountPerProcess +BallotImpl(p) == + LET start == p * BallotCountPerProcess IN + start .. (start + BallotCountPerProcess - 1) +IsMajorityImpl(s) == Cardinality(s) * 2 > N +============================== + diff --git a/specifications/glowingRaccoon/clean.cfg b/specifications/glowingRaccoon/clean.cfg new file mode 100644 index 00000000..bff77506 --- /dev/null +++ b/specifications/glowingRaccoon/clean.cfg @@ -0,0 +1,7 @@ +CONSTANTS + DNA = 5 + PRIMER = 5 +INVARIANTS TypeOK primerPositive preservationInvariant +PROPERTY preservationProperty +SPECIFICATION Spec + diff --git a/specifications/glowingRaccoon/product.cfg b/specifications/glowingRaccoon/product.cfg new file mode 100644 index 00000000..4da41249 --- /dev/null +++ b/specifications/glowingRaccoon/product.cfg @@ -0,0 +1,8 @@ +CONSTANTS + DNA = 5 + PRIMER = 5 +INVARIANTS TypeOK thirdCycleProduct +PROPERTIES stagesSpec primerDepleted +SPECIFICATION Spec +CHECK_DEADLOCK FALSE + diff --git a/specifications/glowingRaccoon/stages.cfg b/specifications/glowingRaccoon/stages.cfg new file mode 100644 index 00000000..30194aae --- /dev/null +++ b/specifications/glowingRaccoon/stages.cfg @@ -0,0 +1,8 @@ +CONSTANTS + DNA = 5 + PRIMER = 5 +INVARIANT TypeOK +SPECIFICATION Spec +PROPERTIES cleanSpec primerDepleted +CHECK_DEADLOCK FALSE + diff --git a/specifications/lamport_mutex/MCLamportMutex.cfg b/specifications/lamport_mutex/MCLamportMutex.cfg new file mode 100644 index 00000000..2d47c2cf --- /dev/null +++ b/specifications/lamport_mutex/MCLamportMutex.cfg @@ -0,0 +1,9 @@ +CONSTANTS + N = 3 + MaxNat = 7 + maxClock = 6 + Nat <- NatOverride +INVARIANTS TypeOK BoundedNetwork Mutex +SPECIFICATION Spec +CONSTRAINT ClockConstraint + diff --git a/specifications/lamport_mutex/MCLamportMutex.tla b/specifications/lamport_mutex/MCLamportMutex.tla new file mode 100644 index 00000000..e385e0f5 --- /dev/null +++ b/specifications/lamport_mutex/MCLamportMutex.tla @@ -0,0 +1,7 @@ +--------------------------- MODULE MCLamportMutex --------------------------- +EXTENDS LamportMutex +CONSTANT MaxNat +ASSUME MaxNat \in Nat +NatOverride == 0 .. MaxNat +============================================================================= + diff --git a/specifications/nbacc_ray97/nbacc_ray97.cfg b/specifications/nbacc_ray97/nbacc_ray97.cfg new file mode 100644 index 00000000..0b5e4e0f --- /dev/null +++ b/specifications/nbacc_ray97/nbacc_ray97.cfg @@ -0,0 +1,4 @@ +CONSTANT N = 2 +INVARIANT TypeOK +SPECIFICATION Spec + diff --git a/specifications/nbacg_guer01/nbacg_guer01.cfg b/specifications/nbacg_guer01/nbacg_guer01.cfg new file mode 100644 index 00000000..061169d8 --- /dev/null +++ b/specifications/nbacg_guer01/nbacg_guer01.cfg @@ -0,0 +1,5 @@ +CONSTANT N = 3 +INVARIANT TypeOK +PROPERTIES AgrrLtl AbortValidityLtl CommitValidityLtl TerminationLtl +SPECIFICATION Spec + diff --git a/specifications/spanning/MC_spanning.cfg b/specifications/spanning/MC_spanning.cfg new file mode 100644 index 00000000..dbfa8935 --- /dev/null +++ b/specifications/spanning/MC_spanning.cfg @@ -0,0 +1,9 @@ +CONSTANTS + Proc = {1, 2, 3} + NoPrnt = NoPrnt + root = 1 + nbrs <- Neighbors +INVARIANTS TypeOK SntMsg +\*PROPERTIES Termination OneParent +SPECIFICATION Spec + diff --git a/specifications/spanning/MC_spanning.tla b/specifications/spanning/MC_spanning.tla new file mode 100644 index 00000000..c969b1d8 --- /dev/null +++ b/specifications/spanning/MC_spanning.tla @@ -0,0 +1,4 @@ +---- MODULE MC_spanning ---- +EXTENDS spanning +Neighbors == {<<1, 2>>, <<1, 3>>} +============================ diff --git a/specifications/spanning/spanning.tla b/specifications/spanning/spanning.tla index 39fb8b6c..ec92d36a 100644 --- a/specifications/spanning/spanning.tla +++ b/specifications/spanning/spanning.tla @@ -45,4 +45,4 @@ SntMsg == \A i \in Proc: (i # root /\ prnt[i] = NoPrnt => \A j \in Proc: < ============================================================================= \* Modification History -\* Last modified Mon Jul 09 13:30:26 CEST 2018 by tthai \ No newline at end of file +\* Last modified Mon Jul 09 13:30:26 CEST 2018 by tthai diff --git a/specifications/sums_even/MC_sums_even.cfg b/specifications/sums_even/MC_sums_even.cfg new file mode 100644 index 00000000..1969570a --- /dev/null +++ b/specifications/sums_even/MC_sums_even.cfg @@ -0,0 +1,4 @@ +CONSTANT + MaxNat = 1000000 + Nat <- NatOverride + diff --git a/specifications/sums_even/MC_sums_even.tla b/specifications/sums_even/MC_sums_even.tla new file mode 100644 index 00000000..fe79a735 --- /dev/null +++ b/specifications/sums_even/MC_sums_even.tla @@ -0,0 +1,8 @@ +------------------------ MODULE MC_sums_even ----------------------- +EXTENDS sums_even +CONSTANT MaxNat +ASSUME MaxNat \in Nat +NatOverride == 0 .. MaxNat +ASSUME T1 +==================================================================== + diff --git a/specifications/transaction_commit/PaxosCommit.cfg b/specifications/transaction_commit/PaxosCommit.cfg new file mode 100644 index 00000000..aa4ba0a8 --- /dev/null +++ b/specifications/transaction_commit/PaxosCommit.cfg @@ -0,0 +1,8 @@ +CONSTANTS + RM = {r1, r2} + Acceptor = {a1, a2, a3} + Majority = {{a1, a2}, {a1, a3}, {a2, a3}} + Ballot = {0,1} +INVARIANT PCTypeOK +SPECIFICATION PCSpec + diff --git a/specifications/transaction_commit/TCommit.cfg b/specifications/transaction_commit/TCommit.cfg new file mode 100644 index 00000000..62f56f2e --- /dev/null +++ b/specifications/transaction_commit/TCommit.cfg @@ -0,0 +1,5 @@ +CONSTANT RM = {r1, r2, r3} +INVARIANTS TCTypeOK TCConsistent +SPECIFICATION TCSpec +CHECK_DEADLOCK FALSE + diff --git a/specifications/transaction_commit/TwoPhase.cfg b/specifications/transaction_commit/TwoPhase.cfg new file mode 100644 index 00000000..5bda57d9 --- /dev/null +++ b/specifications/transaction_commit/TwoPhase.cfg @@ -0,0 +1,4 @@ +CONSTANT RM = {r1, r2, r3} +INVARIANT TPTypeOK +SPECIFICATION TPSpec +