diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py index 060bf0e1..07b947aa 100644 --- a/.github/scripts/tla_utils.py +++ b/.github/scripts/tla_utils.py @@ -5,6 +5,7 @@ from os.path import join, normpath, pathsep, dirname from pathlib import PureWindowsPath import subprocess +import sys import re import glob @@ -137,6 +138,23 @@ def get_run_mode(mode): else: raise NotImplementedError(f'Undefined model-check mode {mode}') +_CHECK_DEADLOCK_FALSE_RE = re.compile(r'CHECK_DEADLOCK\s+FALSE') + +def model_disables_deadlock_check(model_path): + """ + Returns True if the given TLC config file contains a `CHECK_DEADLOCK + FALSE` directive. Used to translate the directive to Apalache's + `--no-deadlock` CLI flag, since Apalache silently ignores it in the + config file. If Apalache ever grows native support for `CHECK_DEADLOCK` + in .cfg files (which seems unlikely), this translation can be dropped. + """ + try: + with open(normpath(model_path), 'r', encoding='utf-8') as f: + text = f.read() + except OSError: + return False + return _CHECK_DEADLOCK_FALSE_RE.search(text) is not None + def get_tlc_feature_flags(module_features): """ Selectively enables experimental TLC features according to needs. @@ -163,19 +181,37 @@ def check_model( Model-checks the given model against the given module. """ tools_jar_path = normpath(tools_jar_path) - apalache_path = normpath(join(apalache_path, 'bin', 'apalache-mc')) apalache_jar_path = normpath(join(apalache_path, 'lib', 'apalache.jar')) + # On Windows the launcher is `apalache-mc.bat`, and `subprocess.run` + # cannot exec batch files via CreateProcess directly, so route them + # through `cmd.exe /c`. On Linux/macOS it is the unsuffixed shell script + # `apalache-mc` and we invoke it directly. + if sys.platform == 'win32': + apalache_path = normpath(join(apalache_path, 'bin', 'apalache-mc.bat')) + apalache_launcher = ['cmd.exe', '/c', apalache_path] + else: + apalache_path = normpath(join(apalache_path, 'bin', 'apalache-mc')) + apalache_launcher = [apalache_path] module_path = normpath(module_path) model_path = normpath(model_path) tlapm_lib_path = normpath(tlapm_lib_path) community_jar_path = normpath(community_jar_path) try: if mode == 'symbolic': - apalache = subprocess.run([ - apalache_path, 'check', - f'--config={model_path}', - module_path - ], + # Cap the bounded-model-checking depth at 5 steps for every + # example. Apalache's own default of 10 is itself an arbitrary + # choice; 5 keeps CI runtimes manageable across the suite while + # still exercising each spec non-trivially. + # + # Apalache silently ignores `CHECK_DEADLOCK FALSE` in .cfg files, + # so translate it to the equivalent CLI flag. + apalache_cmd = ( + apalache_launcher + ['check', '--length=5'] + + (['--no-deadlock'] if model_disables_deadlock_check(model_path) else []) + + [f'--config={model_path}', module_path] + ) + apalache = subprocess.run( + apalache_cmd, timeout=hard_timeout_in_seconds, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index cf626601..26df49fb 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -18,7 +18,9 @@ jobs: strategy: matrix: os: [windows-latest, ubuntu-latest, macos-latest] - unicode: [true, false] + # TEMP (Apalache PR): drop unicode variant; Apalache cannot model-check + # unicode-translated specs. + unicode: [false] fail-fast: false env: SCRIPT_DIR: .github/scripts @@ -45,23 +47,27 @@ jobs: if: matrix.os != 'windows-latest' run: $SCRIPT_DIR/linux-setup.sh $SCRIPT_DIR $DEPS_DIR false - name: Check manifest.json format + if: false # TEMP (Apalache PR): only run Apalache model checks. run: | python "$SCRIPT_DIR/check_manifest_schema.py" \ --schema_path manifest-schema.json - name: Check manifest files + if: false # TEMP (Apalache PR): only run Apalache model checks. run: | python "$SCRIPT_DIR/check_manifest_files.py" \ --ci_ignore_path .ciignore - name: Check manifest feature flags + if: false # TEMP (Apalache PR): only run Apalache model checks. run: | python "$SCRIPT_DIR/check_manifest_features.py" \ --examples_root . - name: Check README spec table + if: false # TEMP (Apalache PR): only run Apalache model checks. run: | python "$SCRIPT_DIR/check_markdown_table.py" \ --readme_path README.md - name: Convert specs to unicode - if: matrix.unicode + if: false && matrix.unicode # TEMP (Apalache PR): only run Apalache model checks. run: | python "$SCRIPT_DIR/unicode_conversion.py" \ --tlauc_path "$DEPS_DIR/tlauc/tlauc" \ @@ -75,7 +81,8 @@ jobs: # discard the results. However, discarding the results with git reset # also would discard the Unicode translation. So, only execute this # step if we did not perform Unicode translation. - if: (!matrix.unicode) + # TEMP (Apalache PR): only run Apalache model checks. + if: false && (!matrix.unicode) run: | # https://github.com/tlaplus/tlaplus/issues/906 SKIP=( @@ -89,6 +96,7 @@ jobs: --skip "${SKIP[@]}" git reset --hard HEAD # Restore specs to their original state - name: Parse all modules + if: false # TEMP (Apalache PR): only run Apalache model checks. run: | python $SCRIPT_DIR/parse_modules.py \ --tools_jar_path $DEPS_DIR/tools/tla2tools.jar \ @@ -97,15 +105,17 @@ jobs: --community_modules_jar_path $DEPS_DIR/community/modules.jar \ --examples_root . - name: Check small models + # TEMP (Apalache PR): only run Apalache (`mode: symbolic`) models. The + # `--only` filter restricts check_small_models.py to the AP*.cfg + # configurations introduced by this PR (plus the pre-existing + # EinsteinRiddle Apalache model). run: | - # Need to have a nonempty list to pass as a skip parameter - # SKIP=("does/not/exist") - # strange issue with parsing TLC output - SKIP=("specifications/ewd840/EWD840.cfg") - if [ ${{ matrix.unicode }} ]; then - # Apalache does not yet support Unicode - SKIP+=("specifications/EinsteinRiddle/Einstein.cfg") - fi + ONLY=() + while IFS= read -r f; do ONLY+=("$f"); done < <( + find specifications -type f \( -name 'AP*.cfg' -o -path '*/EinsteinRiddle/Einstein.cfg' \) | sort + ) + echo "Restricting to ${#ONLY[@]} Apalache model(s):" + printf ' %s\n' "${ONLY[@]}" python $SCRIPT_DIR/check_small_models.py \ --verbose \ --tools_jar_path $DEPS_DIR/tools/tla2tools.jar \ @@ -113,8 +123,12 @@ jobs: --tlapm_lib_path $DEPS_DIR/tlapm/library \ --community_modules_jar_path $DEPS_DIR/community/modules.jar \ --examples_root . \ - --skip "${SKIP[@]}" + --only "${ONLY[@]}" - name: Smoke-test large models + # TEMP (Apalache PR): only run Apalache model checks; no AP*.cfg + # entry has a runtime above 30s, so this step would have nothing + # Apalache-related to do. + if: false run: | # SimKnuthYao requires certain number of states to have been generated # before termination or else it fails. This makes it not amenable to @@ -133,7 +147,8 @@ jobs: --examples_root . \ --skip "${SKIP[@]}" - name: Check proofs - if: matrix.os != 'windows-latest' && !matrix.unicode + # TEMP (Apalache PR): only run Apalache model checks. + if: false && matrix.os != 'windows-latest' && !matrix.unicode run: | set -o pipefail find specifications -iname "manifest.json" -print0 \ @@ -147,11 +162,13 @@ jobs: | xargs --verbose --null --no-run-if-empty -I {TLA_FILE} \ "$DEPS_DIR/tlapm/bin/tlapm" "{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5 - name: Smoke-test manifest generation script + if: false # TEMP (Apalache PR): only run Apalache model checks. run: | python $SCRIPT_DIR/generate_manifest.py \ --ci_ignore_path .ciignore git diff -a - name: Smoke-test state space script + if: false # TEMP (Apalache PR): only run Apalache model checks. run: | git reset --hard HEAD python $SCRIPT_DIR/record_model_state_space.py \ diff --git a/README.md b/README.md index 2241260d..cc7ffe12 100644 --- a/README.md +++ b/README.md @@ -33,49 +33,49 @@ Here is a list of specs included in this repository which are validated by the C | [Boyer-Moore Majority Vote](specifications/Majority) | Stephan Merz | ✔ | ✔ | | ✔ | | | [Proof x+x is Even](specifications/sums_even) | Martin Riener | ✔ | ✔ | | ✔ | | | [The N-Queens Puzzle](specifications/N-Queens) | Stephan Merz | ✔ | | ✔ | ✔ | | -| [The Dining Philosophers Problem](specifications/DiningPhilosophers) | Jeff Hemphill | ✔ | | ✔ | ✔ | | +| [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 Die Hard Problem](specifications/DieHard) | Leslie Lamport | ✔ | | | ✔ | ✔ | | [The Prisoners & Switches Puzzle](specifications/Prisoners) | Leslie Lamport | ✔ | | | ✔ | | | [The Prisoners & Switch Puzzle](specifications/Prisoners_Single_Switch) | Florian Schanda | ✔ | | | ✔ | | -| [Specs from Specifying Systems](specifications/SpecifyingSystems) | 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 | ✔ | | | ✔ | | +| [Missionaries and Cannibals](specifications/MissionariesAndCannibals) | Leslie Lamport | ✔ | | | ✔ | ✔ | | [Stone Scale Puzzle](specifications/Stones) | Leslie Lamport | ✔ | | | ✔ | | -| [The Coffee Can Bean Problem](specifications/CoffeeCan) | Andrew Helwer | ✔ | | | ✔ | | +| [The Coffee Can Bean Problem](specifications/CoffeeCan) | Andrew Helwer | ✔ | | | ✔ | ✔ | | [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | ✔ | | (✔) | ✔ | | -| [The Moving Cat Puzzle](specifications/Moving_Cat_Puzzle) | Florian Schanda | ✔ | | | ✔ | | +| [The Moving Cat Puzzle](specifications/Moving_Cat_Puzzle) | Florian Schanda | ✔ | | | ✔ | ✔ | | [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | | -| [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | ✔ | | +| [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | ✔ | ✔ | | [Byzantizing Paxos by Refinement](specifications/byzpaxos) | Leslie Lamport | | ✔ | ✔ | ✔ | | -| [Barrier Synchronization](specifications/barriers) | Jarod Differdange | | ✔ | ✔ | ✔ | | +| [Barrier Synchronization](specifications/barriers) | Jarod Differdange | | ✔ | ✔ | ✔ | ✔ | | [Peterson Lock Refinement With Auxiliary Variables](specifications/locks_auxiliary_vars) | Jarod Differdange | | ✔ | ✔ | ✔ | | -| [EWD840: Termination Detection in a Ring](specifications/ewd840) | Stephan Merz | | ✔ | | ✔ | | +| [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 | | ✔ | | ✔ | | +| [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 | | (✔) | | ✔ | | -| [Finitizing Monotonic Systems](specifications/FiniteMonotonic) | Andrew Helwer, Stephan Merz, Markus Kuppe | | ✔ | | ✔ | | +| [Finitizing Monotonic Systems](specifications/FiniteMonotonic) | Andrew Helwer, Stephan Merz, Markus Kuppe | | ✔ | | ✔ | ✔ | | [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 | | | ✔ | ✔ | | -| [Transaction Commit Models](specifications/transaction_commit) | Leslie Lamport, Jim Gray, Murat Demirbas | | | ✔ | ✔ | | +| [Transaction Commit Models](specifications/transaction_commit) | Leslie Lamport, Jim Gray, Murat Demirbas | | | ✔ | ✔ | ✔ | | [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 | | | ✔ | ✔ | ✔ | | [MultiPaxos in SMR-Style](specifications/MultiPaxos-SMR) | Guanzhou Hu | | | ✔ | ✔ | | | [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain, Giuliano Losa | | | | | ✔ | | [Resource Allocator](specifications/allocator) | Stephan Merz | | | | ✔ | | | [Transitive Closure](specifications/TransitiveClosure) | Stephan Merz | | | | ✔ | | | [Atomic Commitment Protocol](specifications/acp) | Stephan Merz | | | | ✔ | | | [SWMR Shared Memory Disk Paxos](specifications/diskpaxos) | Leslie Lamport, Giuliano Losa | | | | ✔ | | -| [Span Tree Exercise](specifications/SpanningTree) | Leslie Lamport | | | | ✔ | | +| [Span Tree Exercise](specifications/SpanningTree) | Leslie Lamport | | | | ✔ | ✔ | | [The Knuth-Yao Method](specifications/KnuthYao) | Ron Pressler, Markus Kuppe | | | | ✔ | | | [Huang's Algorithm](specifications/Huang) | Markus Kuppe | | | | ✔ | | -| [EWD 426: Token Stabilization](specifications/ewd426) | Murat Demirbas, Markus Kuppe | | | | ✔ | | +| [EWD 426: Token Stabilization](specifications/ewd426) | Murat Demirbas, Markus Kuppe | | | | ✔ | ✔ | | [Sliding Block Puzzle](specifications/SlidingPuzzles) | Mariusz Ryndzionek | | | | ✔ | | | [Single-Lane Bridge Problem](specifications/SingleLaneBridge) | Younes Akhouayri | | | | ✔ | | | [Software-Defined Perimeter](specifications/SDP_Verification) | Luming Dong, Zhi Niu | | | | ✔ | | @@ -83,28 +83,28 @@ Here is a list of specs included in this repository which are validated by the C | [Checkpoint Coordination](specifications/CheckpointCoordination) | Andrew Helwer | | | | ✔ | | | [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | | | ✔ | | | [Nano Blockchain Protocol](specifications/NanoBlockchain) | Andrew Helwer | | | | ✔ | | -| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | | | ✔ | | +| [The Readers-Writers Problem](specifications/ReadersWriters) | 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 | | | | ✔ | | +| [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 | | | | ✔ | | -| [The Cigarette Smokers Problem](specifications/CigaretteSmokers) | Mariusz Ryndzionek | | | | ✔ | | +| [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 | | | | ✔ | ✔ | +| [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 | | | | ✔ | | +| [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | | | ✔ | ✔ | | [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | | | ✔ | | | [Yo-Yo Leader Election](specifications/YoYo) | Ludovic Yvoz, Stephan Merz | | | | ✔ | | -| [TCP as defined in RFC 9293](specifications/tcp) | Markus Kuppe | | | | ✔ | | +| [TCP as defined in RFC 9293](specifications/tcp) | Markus Kuppe | | | | ✔ | ✔ | | [B-trees](specifications/btree) | Lorin Hochstein | | | | ✔ | | | [TLA⁺ Level Checking](specifications/LevelChecking) | Leslie Lamport | | | | | | | [Condition-Based Consensus](specifications/cbc_max) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | | [Buffered Random Access File](specifications/braf) | Calvin Loncaric | | | | ✔ | | -| [Disruptor](specifications/Disruptor) | Nicholas Schultz-Møller | | | | ✔ | | +| [Disruptor](specifications/Disruptor) | Nicholas Schultz-Møller | | | | ✔ | ✔ | | [DAG-based Consensus](specifications/dag-consensus) | Giuliano Losa | | | ✔ | ✔ | | diff --git a/specifications/Chameneos/APChameneos.tla b/specifications/Chameneos/APChameneos.tla new file mode 100644 index 00000000..814c6013 --- /dev/null +++ b/specifications/Chameneos/APChameneos.tla @@ -0,0 +1,32 @@ +----------------------------- MODULE APChameneos ----------------------------- +(* Apalache type annotations for Chameneos.tla, applied via INSTANCE so the + original spec is not modified. + + The polymorphic `Sum(f, S)` cannot be inferred (its argument could equally + be a sequence) and must be typed explicitly. *) + +EXTENDS Integers + +CONSTANT + \* @type: Int; + N, + \* @type: Int; + M + +VARIABLE + \* @type: Int -> <>; + chameneoses, + \* @type: Int; + meetingPlace, + \* @type: Int; + numMeetings + +RECURSIVE Sum(_, _) +\* @type: (Int -> Int, Set(Int)) => Int; +Sum(f, S) == IF S = {} THEN 0 + ELSE LET x == CHOOSE x \in S : TRUE + IN f[x] + Sum(f, S \ {x}) + +INSTANCE Chameneos + +============================================================================== diff --git a/specifications/Chameneos/manifest.json b/specifications/Chameneos/manifest.json index b69a59fe..cf71a42a 100644 --- a/specifications/Chameneos/manifest.json +++ b/specifications/Chameneos/manifest.json @@ -7,6 +7,11 @@ ], "tags": [], "modules": [ + { + "path": "specifications/Chameneos/APChameneos.tla", + "features": [], + "models": [] + }, { "path": "specifications/Chameneos/Chameneos.tla", "features": [], diff --git a/specifications/CigaretteSmokers/APCigaretteSmokers.cfg b/specifications/CigaretteSmokers/APCigaretteSmokers.cfg new file mode 100644 index 00000000..9aae1593 --- /dev/null +++ b/specifications/CigaretteSmokers/APCigaretteSmokers.cfg @@ -0,0 +1,9 @@ +CONSTANTS + Ingredients <- IngredientsVal + Offers <- OffersVal + +INVARIANT + TypeOK + AtMostOne + +SPECIFICATION Spec diff --git a/specifications/CigaretteSmokers/APCigaretteSmokers.tla b/specifications/CigaretteSmokers/APCigaretteSmokers.tla new file mode 100644 index 00000000..7092e5b2 --- /dev/null +++ b/specifications/CigaretteSmokers/APCigaretteSmokers.tla @@ -0,0 +1,26 @@ +-------------------------- MODULE APCigaretteSmokers -------------------------- +(* Apalache type annotations for CigaretteSmokers.tla, applied via INSTANCE so + the original spec is not modified. *) + +EXTENDS Integers, FiniteSets + +CONSTANT + \* @type: Set(INGREDIENT); + Ingredients, + \* @type: Set(Set(INGREDIENT)); + Offers + +VARIABLE + \* @type: INGREDIENT -> { smoking: Bool }; + smokers, + \* @type: Set(INGREDIENT); + dealer + +INSTANCE CigaretteSmokers + +\* Concrete model values for the uninterpreted INGREDIENT type. Used by +\* APCigaretteSmokers.cfg via the `Const <- OpName` syntax. +IngredientsVal == {"matches_OF_INGREDIENT", "paper_OF_INGREDIENT", "tobacco_OF_INGREDIENT"} +OffersVal == { IngredientsVal \ {i} : i \in IngredientsVal } + +============================================================================== diff --git a/specifications/CigaretteSmokers/manifest.json b/specifications/CigaretteSmokers/manifest.json index a28bea3e..e846b88e 100644 --- a/specifications/CigaretteSmokers/manifest.json +++ b/specifications/CigaretteSmokers/manifest.json @@ -7,6 +7,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/CigaretteSmokers/APCigaretteSmokers.tla", + "features": [], + "models": [ + { + "path": "specifications/CigaretteSmokers/APCigaretteSmokers.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/CigaretteSmokers/CigaretteSmokers.tla", "features": [], diff --git a/specifications/CoffeeCan/APCoffeeCan.cfg b/specifications/CoffeeCan/APCoffeeCan.cfg new file mode 100644 index 00000000..a5c6a3bc --- /dev/null +++ b/specifications/CoffeeCan/APCoffeeCan.cfg @@ -0,0 +1,5 @@ +CONSTANT MaxBeanCount = 5 + +INVARIANT TypeInvariant + +SPECIFICATION Spec diff --git a/specifications/CoffeeCan/APCoffeeCan.tla b/specifications/CoffeeCan/APCoffeeCan.tla new file mode 100644 index 00000000..671e32bf --- /dev/null +++ b/specifications/CoffeeCan/APCoffeeCan.tla @@ -0,0 +1,17 @@ +---------------------------- MODULE APCoffeeCan ---------------------------- +(* Apalache type annotations for CoffeeCan.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals + +CONSTANT + \* @type: Int; + MaxBeanCount + +VARIABLES + \* @type: { black: Int, white: Int }; + can + +INSTANCE CoffeeCan + +============================================================================ diff --git a/specifications/CoffeeCan/manifest.json b/specifications/CoffeeCan/manifest.json index 438c6fa2..9f60424c 100644 --- a/specifications/CoffeeCan/manifest.json +++ b/specifications/CoffeeCan/manifest.json @@ -9,6 +9,18 @@ "beginner" ], "modules": [ + { + "path": "specifications/CoffeeCan/APCoffeeCan.tla", + "features": [], + "models": [ + { + "path": "specifications/CoffeeCan/APCoffeeCan.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/CoffeeCan/CoffeeCan.tla", "features": [], diff --git a/specifications/DieHard/APDieHarder.cfg b/specifications/DieHard/APDieHarder.cfg new file mode 100644 index 00000000..afc9d36b --- /dev/null +++ b/specifications/DieHard/APDieHarder.cfg @@ -0,0 +1,8 @@ +CONSTANTS + Jug <- JugVal + Capacity <- CapacityVal + Goal = 4 + +INVARIANT TypeOK + +SPECIFICATION Spec diff --git a/specifications/DieHard/APDieHarder.tla b/specifications/DieHard/APDieHarder.tla new file mode 100644 index 00000000..894d653d --- /dev/null +++ b/specifications/DieHard/APDieHarder.tla @@ -0,0 +1,26 @@ +----------------------------- MODULE APDieHarder ----------------------------- +(* Apalache type annotations for DieHarder.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals + +CONSTANT + \* @type: Set(JUG); + Jug, + \* @type: JUG -> Int; + Capacity, + \* @type: Int; + Goal + +VARIABLE + \* @type: JUG -> Int; + contents + +INSTANCE DieHarder + +\* Concrete values for the constants used by APDieHarder.cfg. +JugVal == { "small_OF_JUG", "big_OF_JUG" } +\* @type: JUG -> Int; +CapacityVal == [ j \in JugVal |-> IF j = "small_OF_JUG" THEN 3 ELSE 5 ] + +============================================================================== diff --git a/specifications/DieHard/manifest.json b/specifications/DieHard/manifest.json index 8e1466f6..4c8947d6 100644 --- a/specifications/DieHard/manifest.json +++ b/specifications/DieHard/manifest.json @@ -7,6 +7,23 @@ "beginner" ], "modules": [ + { + "path": "specifications/DieHard/APADieHardest.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/DieHard/APDieHarder.tla", + "features": [], + "models": [ + { + "path": "specifications/DieHard/APDieHarder.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/DieHard/DieHard.tla", "features": [], @@ -25,7 +42,7 @@ "models": [] }, { - "path": "specifications/DieHard/APADieHardest.tla", + "path": "specifications/DieHard/DieHardest.tla", "features": [], "models": [] }, @@ -41,11 +58,6 @@ } ] }, - { - "path": "specifications/DieHard/DieHardest.tla", - "features": [], - "models": [] - }, { "path": "specifications/DieHard/MCDieHardest.tla", "features": [], diff --git a/specifications/DiningPhilosophers/APDiningPhilosophers.cfg b/specifications/DiningPhilosophers/APDiningPhilosophers.cfg new file mode 100644 index 00000000..523ba28d --- /dev/null +++ b/specifications/DiningPhilosophers/APDiningPhilosophers.cfg @@ -0,0 +1,12 @@ +\* The original Spec includes per-process WF fairness (`\A self \in 1..NP : +\* WF_vars(Philosopher(self))`); Apalache rejects that form, so we drive +\* the safety check from `Init`/`Next` directly. + +CONSTANT NP = 5 + +INIT Init +NEXT Next + +INVARIANT + TypeOK + ExclusiveAccess diff --git a/specifications/DiningPhilosophers/APDiningPhilosophers.tla b/specifications/DiningPhilosophers/APDiningPhilosophers.tla new file mode 100644 index 00000000..ce4045c2 --- /dev/null +++ b/specifications/DiningPhilosophers/APDiningPhilosophers.tla @@ -0,0 +1,21 @@ +---- MODULE APDiningPhilosophers ---- +(* Apalache type annotations for DiningPhilosophers.tla, applied via INSTANCE + so the original spec is not modified. *) + +EXTENDS Integers, TLC + +CONSTANTS + \* @type: Int; + NP + +VARIABLES + \* @type: Int -> { holder: Int, clean: Bool }; + forks, + \* @type: Int -> Str; + pc, + \* @type: Int -> Bool; + hungry + +INSTANCE DiningPhilosophers + +==== diff --git a/specifications/DiningPhilosophers/manifest.json b/specifications/DiningPhilosophers/manifest.json index d847c54b..f71b9010 100644 --- a/specifications/DiningPhilosophers/manifest.json +++ b/specifications/DiningPhilosophers/manifest.json @@ -7,6 +7,18 @@ "beginner" ], "modules": [ + { + "path": "specifications/DiningPhilosophers/APDiningPhilosophers.tla", + "features": [], + "models": [ + { + "path": "specifications/DiningPhilosophers/APDiningPhilosophers.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/DiningPhilosophers/DiningPhilosophers.tla", "features": [ diff --git a/specifications/Disruptor/APDisruptor_MPMC.cfg b/specifications/Disruptor/APDisruptor_MPMC.cfg new file mode 100644 index 00000000..db97c263 --- /dev/null +++ b/specifications/Disruptor/APDisruptor_MPMC.cfg @@ -0,0 +1,16 @@ +\* Use INIT/NEXT directly because the original Spec adds per-reader +\* WF fairness which Apalache does not handle. +\* `TypeOk` references `Seq(Nat)` (an unbounded set) which Apalache cannot +\* enumerate, so we only check `NoDataRaces` here. + +CONSTANTS + MaxPublished = 4 + Writers <- WritersVal + Readers <- ReadersVal + Size = 4 + NULL = -1 + +INIT Init +NEXT Next + +INVARIANT NoDataRaces diff --git a/specifications/Disruptor/APDisruptor_MPMC.tla b/specifications/Disruptor/APDisruptor_MPMC.tla new file mode 100644 index 00000000..a3abbf25 --- /dev/null +++ b/specifications/Disruptor/APDisruptor_MPMC.tla @@ -0,0 +1,48 @@ +--------------------------- MODULE APDisruptor_MPMC --------------------------- +(* Apalache type annotations for Disruptor_MPMC.tla, applied via INSTANCE so + the original spec is not modified. + + The polymorphic helper `Range(f) == { f[x] : x \in DOMAIN(f) }` is shadowed + here with a typed monomorphic version because its only uses in this module + are on `read` and `claimed_sequence`, both of type THREAD -> Int. *) + +EXTENDS Integers, FiniteSets, Sequences + +CONSTANTS + \* @type: Int; + MaxPublished, + \* @type: Set(THREAD); + Writers, + \* @type: Set(THREAD); + Readers, + \* @type: Int; + Size, + \* @type: Int; + NULL + +VARIABLES + \* @type: { slots: Int -> Int, readers: Int -> Set(THREAD), writers: Int -> Set(THREAD) }; + ringbuffer, + \* @type: Int; + next_sequence, + \* @type: THREAD -> Int; + claimed_sequence, + \* @type: Int -> Bool; + published, + \* @type: THREAD -> Int; + read, + \* @type: THREAD -> Str; + pc, + \* @type: THREAD -> Seq(Int); + consumed + +\* @type: (THREAD -> Int) => Set(Int); +Range(f) == { f[x] : x \in DOMAIN(f) } + +INSTANCE Disruptor_MPMC + +\* Concrete values for the constants used by APDisruptor_MPMC.cfg. +WritersVal == { "w1_OF_THREAD", "w2_OF_THREAD" } +ReadersVal == { "r1_OF_THREAD", "r2_OF_THREAD" } + +============================================================================== diff --git a/specifications/Disruptor/APDisruptor_SPMC.cfg b/specifications/Disruptor/APDisruptor_SPMC.cfg new file mode 100644 index 00000000..db97c263 --- /dev/null +++ b/specifications/Disruptor/APDisruptor_SPMC.cfg @@ -0,0 +1,16 @@ +\* Use INIT/NEXT directly because the original Spec adds per-reader +\* WF fairness which Apalache does not handle. +\* `TypeOk` references `Seq(Nat)` (an unbounded set) which Apalache cannot +\* enumerate, so we only check `NoDataRaces` here. + +CONSTANTS + MaxPublished = 4 + Writers <- WritersVal + Readers <- ReadersVal + Size = 4 + NULL = -1 + +INIT Init +NEXT Next + +INVARIANT NoDataRaces diff --git a/specifications/Disruptor/APDisruptor_SPMC.tla b/specifications/Disruptor/APDisruptor_SPMC.tla new file mode 100644 index 00000000..8d4fe32e --- /dev/null +++ b/specifications/Disruptor/APDisruptor_SPMC.tla @@ -0,0 +1,44 @@ +--------------------------- MODULE APDisruptor_SPMC --------------------------- +(* Apalache type annotations for Disruptor_SPMC.tla, applied via INSTANCE so + the original spec is not modified. + + The polymorphic helper `Range(f) == { f[x] : x \in DOMAIN(f) }` is shadowed + here with a typed monomorphic version because its only use in this module + is on `read`, a function from THREAD to Int. *) + +EXTENDS Integers, FiniteSets, Sequences + +CONSTANTS + \* @type: Int; + MaxPublished, + \* @type: Set(THREAD); + Writers, + \* @type: Set(THREAD); + Readers, + \* @type: Int; + Size, + \* @type: Int; + NULL + +VARIABLES + \* @type: { slots: Int -> Int, readers: Int -> Set(THREAD), writers: Int -> Set(THREAD) }; + ringbuffer, + \* @type: Int; + published, + \* @type: THREAD -> Int; + read, + \* @type: THREAD -> Str; + pc, + \* @type: THREAD -> Seq(Int); + consumed + +\* @type: (THREAD -> Int) => Set(Int); +Range(f) == { f[x] : x \in DOMAIN(f) } + +INSTANCE Disruptor_SPMC + +\* Concrete values for the constants used by APDisruptor_SPMC.cfg. +WritersVal == { "w_OF_THREAD" } +ReadersVal == { "r1_OF_THREAD", "r2_OF_THREAD" } + +============================================================================== diff --git a/specifications/Disruptor/manifest.json b/specifications/Disruptor/manifest.json index 8ad8759a..d7af7956 100644 --- a/specifications/Disruptor/manifest.json +++ b/specifications/Disruptor/manifest.json @@ -7,6 +7,30 @@ ], "tags": [], "modules": [ + { + "path": "specifications/Disruptor/APDisruptor_MPMC.tla", + "features": [], + "models": [ + { + "path": "specifications/Disruptor/APDisruptor_MPMC.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/Disruptor/APDisruptor_SPMC.tla", + "features": [], + "models": [ + { + "path": "specifications/Disruptor/APDisruptor_SPMC.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/Disruptor/Disruptor_MPMC.tla", "features": [], diff --git a/specifications/FiniteMonotonic/APCRDT.cfg b/specifications/FiniteMonotonic/APCRDT.cfg new file mode 100644 index 00000000..b96429ca --- /dev/null +++ b/specifications/FiniteMonotonic/APCRDT.cfg @@ -0,0 +1,7 @@ +CONSTANT Node <- NodeVal + +INVARIANT + TypeOK + Safety + +SPECIFICATION Spec diff --git a/specifications/FiniteMonotonic/APCRDT.tla b/specifications/FiniteMonotonic/APCRDT.tla new file mode 100644 index 00000000..5e78f848 --- /dev/null +++ b/specifications/FiniteMonotonic/APCRDT.tla @@ -0,0 +1,20 @@ +------------------------------- MODULE APCRDT ------------------------------- +(* Apalache type annotations for CRDT.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals, FiniteSets + +CONSTANT + \* @type: Set(NODE); + Node + +VARIABLE + \* @type: NODE -> NODE -> Int; + counter + +INSTANCE CRDT + +\* Concrete values for the constants used by APCRDT.cfg. +NodeVal == { "n1_OF_NODE", "n2_OF_NODE", "n3_OF_NODE" } + +============================================================================== diff --git a/specifications/FiniteMonotonic/APDistributedReplicatedLog.tla b/specifications/FiniteMonotonic/APDistributedReplicatedLog.tla new file mode 100644 index 00000000..2adf30bb --- /dev/null +++ b/specifications/FiniteMonotonic/APDistributedReplicatedLog.tla @@ -0,0 +1,28 @@ +--------------------- MODULE APDistributedReplicatedLog --------------------- +(* Apalache type annotations for DistributedReplicatedLog.tla, applied via + INSTANCE so the original spec is not modified. *) + +EXTENDS Sequences, SequencesExt, Integers, FiniteSets, FiniteSetsExt + +CONSTANT + \* @type: Int; + Lag, + \* @type: Set(SERVER); + Servers, + \* @type: Set(VAL); + Values + +VARIABLE + \* @type: SERVER -> Seq(VAL); + cLogs + +\* @type: < Seq(VAL)>>; +vars == <> + +INSTANCE DistributedReplicatedLog + +\* Concrete values for the constants used by APDistributedReplicatedLog.cfg. +ServersVal == { "s1_OF_SERVER", "s2_OF_SERVER" } +ValuesVal == { "v1_OF_VAL", "v2_OF_VAL" } + +============================================================================== diff --git a/specifications/FiniteMonotonic/APReplicatedLog.cfg b/specifications/FiniteMonotonic/APReplicatedLog.cfg new file mode 100644 index 00000000..e9ffec41 --- /dev/null +++ b/specifications/FiniteMonotonic/APReplicatedLog.cfg @@ -0,0 +1,10 @@ +\* `TypeOK` references `Seq(Transaction)` (an unbounded set) which +\* Apalache cannot enumerate; we only check `Safety` here. + +CONSTANTS + Node <- NodeVal + Transaction <- TransactionVal + +INVARIANT Safety + +SPECIFICATION Spec diff --git a/specifications/FiniteMonotonic/APReplicatedLog.tla b/specifications/FiniteMonotonic/APReplicatedLog.tla new file mode 100644 index 00000000..8335b7ea --- /dev/null +++ b/specifications/FiniteMonotonic/APReplicatedLog.tla @@ -0,0 +1,25 @@ +--------------------------- MODULE APReplicatedLog --------------------------- +(* Apalache type annotations for ReplicatedLog.tla, applied via INSTANCE so + the original spec is not modified. *) + +EXTENDS Naturals, Sequences + +CONSTANTS + \* @type: Set(NODE); + Node, + \* @type: Set(TX); + Transaction + +VARIABLES + \* @type: Seq(TX); + log, + \* @type: NODE -> Int; + executed + +INSTANCE ReplicatedLog + +\* Concrete values for the constants used by APReplicatedLog.cfg. +NodeVal == { "n1_OF_NODE", "n2_OF_NODE" } +TransactionVal == { "t1_OF_TX", "t2_OF_TX" } + +============================================================================== diff --git a/specifications/FiniteMonotonic/manifest.json b/specifications/FiniteMonotonic/manifest.json index f4b11fca..c035fa3d 100644 --- a/specifications/FiniteMonotonic/manifest.json +++ b/specifications/FiniteMonotonic/manifest.json @@ -11,6 +11,35 @@ "intermediate" ], "modules": [ + { + "path": "specifications/FiniteMonotonic/APCRDT.tla", + "features": [], + "models": [ + { + "path": "specifications/FiniteMonotonic/APCRDT.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/FiniteMonotonic/APDistributedReplicatedLog.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/FiniteMonotonic/APReplicatedLog.tla", + "features": [], + "models": [ + { + "path": "specifications/FiniteMonotonic/APReplicatedLog.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/FiniteMonotonic/CRDT.tla", "features": [], diff --git a/specifications/KeyValueStore/APKeyValueStore.tla b/specifications/KeyValueStore/APKeyValueStore.tla new file mode 100644 index 00000000..02a757c7 --- /dev/null +++ b/specifications/KeyValueStore/APKeyValueStore.tla @@ -0,0 +1,32 @@ +--------------------------- MODULE APKeyValueStore --------------------------- +(* Apalache type annotations for KeyValueStore.tla, applied via INSTANCE so + the original spec is not modified. *) + +CONSTANTS + \* @type: Set(KEY); + Key, + \* @type: Set(VAL); + Val, + \* @type: Set(TX); + TxId + +VARIABLES + \* @type: KEY -> VAL; + store, + \* @type: Set(TX); + tx, + \* @type: TX -> KEY -> VAL; + snapshotStore, + \* @type: TX -> Set(KEY); + written, + \* @type: TX -> Set(KEY); + missed + +INSTANCE KeyValueStore + +\* Concrete values for the constants used by APKeyValueStore.cfg. +KeyVal == { "k1_OF_KEY", "k2_OF_KEY" } +ValVal == { "v1_OF_VAL", "v2_OF_VAL" } +TxIdVal == { "t1_OF_TX", "t2_OF_TX" } + +============================================================================== diff --git a/specifications/KeyValueStore/manifest.json b/specifications/KeyValueStore/manifest.json index 6c4aa826..0cc8f1bf 100644 --- a/specifications/KeyValueStore/manifest.json +++ b/specifications/KeyValueStore/manifest.json @@ -6,6 +6,11 @@ ], "tags": [], "modules": [ + { + "path": "specifications/KeyValueStore/APKeyValueStore.tla", + "features": [], + "models": [] + }, { "path": "specifications/KeyValueStore/ClientCentric.tla", "features": [], diff --git a/specifications/Majority/APMajority.tla b/specifications/Majority/APMajority.tla new file mode 100644 index 00000000..4f844da3 --- /dev/null +++ b/specifications/Majority/APMajority.tla @@ -0,0 +1,26 @@ +------------------------------ MODULE APMajority ------------------------------ +(* Apalache type annotations for Majority.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Integers, Sequences, FiniteSets + +CONSTANT + \* @type: Set(VAL); + Value + +VARIABLES + \* @type: Seq(VAL); + seq, + \* @type: Int; + i, + \* @type: VAL; + cand, + \* @type: Int; + cnt + +INSTANCE Majority + +\* Concrete values for the constants used by APMajority.cfg. +ValueVal == { "a_OF_VAL", "b_OF_VAL" } + +============================================================================== diff --git a/specifications/Majority/manifest.json b/specifications/Majority/manifest.json index 97e2dfbf..09b9d9fc 100644 --- a/specifications/Majority/manifest.json +++ b/specifications/Majority/manifest.json @@ -7,6 +7,11 @@ "beginner" ], "modules": [ + { + "path": "specifications/Majority/APMajority.tla", + "features": [], + "models": [] + }, { "path": "specifications/Majority/MCMajority.tla", "features": [], diff --git a/specifications/MisraReachability/APParReach.cfg b/specifications/MisraReachability/APParReach.cfg new file mode 100644 index 00000000..ca83400e --- /dev/null +++ b/specifications/MisraReachability/APParReach.cfg @@ -0,0 +1,14 @@ +\* Use INIT/NEXT directly because the original Spec adds per-process +\* WF fairness which Apalache does not handle. + +CONSTANTS + Nodes <- NodesVal + Succ <- SuccVal + Root <- RootVal + Procs <- ProcsVal + +INIT Init +NEXT Next + +INVARIANT + Inv diff --git a/specifications/MisraReachability/APParReach.tla b/specifications/MisraReachability/APParReach.tla new file mode 100644 index 00000000..a57b44a6 --- /dev/null +++ b/specifications/MisraReachability/APParReach.tla @@ -0,0 +1,39 @@ +----------------------------- MODULE APParReach ----------------------------- +(* Apalache type annotations for ParReach.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Integers, FiniteSets + +CONSTANT + \* @type: Set(NODE); + Nodes, + \* @type: NODE -> Set(NODE); + Succ, + \* @type: NODE; + Root, + \* @type: Set(PROC); + Procs + +VARIABLES + \* @type: Set(NODE); + marked, + \* @type: Set(NODE); + vroot, + \* @type: PROC -> Str; + pc, + \* @type: PROC -> NODE; + u, + \* @type: PROC -> Set(NODE); + toVroot + +INSTANCE ParReach + WITH Nodes <- Nodes, Succ <- Succ, Root <- Root, Procs <- Procs + +\* Concrete values for the constants used by APParReach.cfg. +NodesVal == { "n1_OF_NODE", "n2_OF_NODE", "n3_OF_NODE" } +\* @type: NODE -> Set(NODE); +SuccVal == [ n \in NodesVal |-> NodesVal \ {n} ] +RootVal == "n1_OF_NODE" +ProcsVal == { "p1_OF_PROC", "p2_OF_PROC" } + +============================================================================== diff --git a/specifications/MisraReachability/APReachable.tla b/specifications/MisraReachability/APReachable.tla new file mode 100644 index 00000000..53353c7e --- /dev/null +++ b/specifications/MisraReachability/APReachable.tla @@ -0,0 +1,31 @@ +----------------------------- MODULE APReachable ----------------------------- +(* Apalache type annotations for Reachable.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Integers, FiniteSets + +CONSTANT + \* @type: Set(NODE); + Nodes, + \* @type: NODE -> Set(NODE); + Succ, + \* @type: NODE; + Root + +VARIABLES + \* @type: Set(NODE); + marked, + \* @type: Set(NODE); + vroot, + \* @type: Str; + pc + +INSTANCE Reachable WITH Nodes <- Nodes, Succ <- Succ, Root <- Root + +\* Concrete values for the constants used by APReachable.cfg. +NodesVal == { "n1_OF_NODE", "n2_OF_NODE", "n3_OF_NODE" } +\* @type: NODE -> Set(NODE); +SuccVal == [ n \in NodesVal |-> NodesVal \ {n} ] +RootVal == "n1_OF_NODE" + +============================================================================== diff --git a/specifications/MisraReachability/manifest.json b/specifications/MisraReachability/manifest.json index 7034c1a0..413cc249 100644 --- a/specifications/MisraReachability/manifest.json +++ b/specifications/MisraReachability/manifest.json @@ -5,6 +5,23 @@ ], "tags": [], "modules": [ + { + "path": "specifications/MisraReachability/APParReach.tla", + "features": [], + "models": [ + { + "path": "specifications/MisraReachability/APParReach.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/MisraReachability/APReachable.tla", + "features": [], + "models": [] + }, { "path": "specifications/MisraReachability/MCParReach.tla", "features": [], diff --git a/specifications/MissionariesAndCannibals/APMissionariesAndCannibals.cfg b/specifications/MissionariesAndCannibals/APMissionariesAndCannibals.cfg new file mode 100644 index 00000000..738bc4e4 --- /dev/null +++ b/specifications/MissionariesAndCannibals/APMissionariesAndCannibals.cfg @@ -0,0 +1,10 @@ +CONSTANTS + Missionaries <- MissionariesVal + Cannibals <- CannibalsVal + +INIT Init +NEXT Next + +INVARIANT + TypeOK + Solution diff --git a/specifications/MissionariesAndCannibals/APMissionariesAndCannibals.tla b/specifications/MissionariesAndCannibals/APMissionariesAndCannibals.tla new file mode 100644 index 00000000..2cdfd12b --- /dev/null +++ b/specifications/MissionariesAndCannibals/APMissionariesAndCannibals.tla @@ -0,0 +1,25 @@ +--------------- MODULE APMissionariesAndCannibals --------------- +(* Apalache type annotations for MissionariesAndCannibals.tla, applied via + INSTANCE so the original spec is not modified. *) + +EXTENDS Integers, FiniteSets + +CONSTANTS + \* @type: Set(PERSON); + Missionaries, + \* @type: Set(PERSON); + Cannibals + +VARIABLES + \* @type: Str; + bank_of_boat, + \* @type: Str -> Set(PERSON); + who_is_on_bank + +INSTANCE MissionariesAndCannibals + +\* Concrete values for the constants used by APMissionariesAndCannibals.cfg. +MissionariesVal == { "m1_OF_PERSON", "m2_OF_PERSON", "m3_OF_PERSON" } +CannibalsVal == { "c1_OF_PERSON", "c2_OF_PERSON", "c3_OF_PERSON" } + +============================================================================== diff --git a/specifications/MissionariesAndCannibals/manifest.json b/specifications/MissionariesAndCannibals/manifest.json index 587a24bd..707d9c2c 100644 --- a/specifications/MissionariesAndCannibals/manifest.json +++ b/specifications/MissionariesAndCannibals/manifest.json @@ -7,6 +7,18 @@ "beginner" ], "modules": [ + { + "path": "specifications/MissionariesAndCannibals/APMissionariesAndCannibals.tla", + "features": [], + "models": [ + { + "path": "specifications/MissionariesAndCannibals/APMissionariesAndCannibals.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/MissionariesAndCannibals/MissionariesAndCannibals.tla", "features": [], diff --git a/specifications/Moving_Cat_Puzzle/APCat.cfg b/specifications/Moving_Cat_Puzzle/APCat.cfg new file mode 100644 index 00000000..85b433e0 --- /dev/null +++ b/specifications/Moving_Cat_Puzzle/APCat.cfg @@ -0,0 +1,5 @@ +CONSTANT Number_Of_Boxes = 4 + +INVARIANT TypeOK + +SPECIFICATION Spec diff --git a/specifications/Moving_Cat_Puzzle/APCat.tla b/specifications/Moving_Cat_Puzzle/APCat.tla new file mode 100644 index 00000000..4e62dabe --- /dev/null +++ b/specifications/Moving_Cat_Puzzle/APCat.tla @@ -0,0 +1,21 @@ +---- MODULE APCat ---- +(* Apalache type annotations for Cat.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals + +CONSTANTS + \* @type: Int; + Number_Of_Boxes + +VARIABLES + \* @type: Int; + cat_box, + \* @type: Int; + observed_box, + \* @type: Str; + direction + +INSTANCE Cat + +==== diff --git a/specifications/Moving_Cat_Puzzle/manifest.json b/specifications/Moving_Cat_Puzzle/manifest.json index 3a1cc9a3..f6cc66e8 100644 --- a/specifications/Moving_Cat_Puzzle/manifest.json +++ b/specifications/Moving_Cat_Puzzle/manifest.json @@ -7,6 +7,18 @@ "beginner" ], "modules": [ + { + "path": "specifications/Moving_Cat_Puzzle/APCat.tla", + "features": [], + "models": [ + { + "path": "specifications/Moving_Cat_Puzzle/APCat.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/Moving_Cat_Puzzle/Cat.tla", "features": [], diff --git a/specifications/Prisoners/APPrisoners.tla b/specifications/Prisoners/APPrisoners.tla new file mode 100644 index 00000000..53e76b13 --- /dev/null +++ b/specifications/Prisoners/APPrisoners.tla @@ -0,0 +1,29 @@ +----------------------------- MODULE APPrisoners ----------------------------- +(* Apalache type annotations for Prisoners.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals, FiniteSets + +CONSTANTS + \* @type: Set(PRISONER); + Prisoner, + \* @type: PRISONER; + Counter + +VARIABLES + \* @type: Bool; + switchAUp, + \* @type: Bool; + switchBUp, + \* @type: PRISONER -> Int; + timesSwitched, + \* @type: Int; + count + +INSTANCE Prisoners + +\* Concrete values for the constants used by APPrisoners.cfg. +PrisonerVal == { "p1_OF_PRISONER", "p2_OF_PRISONER", "p3_OF_PRISONER" } +CounterVal == "p1_OF_PRISONER" + +============================================================================== diff --git a/specifications/Prisoners/manifest.json b/specifications/Prisoners/manifest.json index 15a6d516..1ba3305d 100644 --- a/specifications/Prisoners/manifest.json +++ b/specifications/Prisoners/manifest.json @@ -7,6 +7,11 @@ "beginner" ], "modules": [ + { + "path": "specifications/Prisoners/APPrisoners.tla", + "features": [], + "models": [] + }, { "path": "specifications/Prisoners/MCPrisoners.tla", "features": [], diff --git a/specifications/Prisoners_Single_Switch/APPrisoner.tla b/specifications/Prisoners_Single_Switch/APPrisoner.tla new file mode 100644 index 00000000..afc41e58 --- /dev/null +++ b/specifications/Prisoners_Single_Switch/APPrisoner.tla @@ -0,0 +1,30 @@ +---- MODULE APPrisoner ---- +(* Apalache type annotations for Prisoner.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS FiniteSets, Naturals + +CONSTANTS + \* @type: Set(PRISONER); + Prisoner, + \* @type: Bool; + Light_Unknown + +VARIABLES + \* @type: Int; + count, + \* @type: Bool; + announced, + \* @type: PRISONER -> Int; + signalled, + \* @type: Str; + light, + \* @type: Set(PRISONER); + has_visited + +INSTANCE Prisoner + +\* Concrete values for the constants used by APPrisoner.cfg. +PrisonerVal == { "Alice_OF_PRISONER", "Bob_OF_PRISONER", "Eve_OF_PRISONER" } + +==== diff --git a/specifications/Prisoners_Single_Switch/manifest.json b/specifications/Prisoners_Single_Switch/manifest.json index b3dad419..cac6e888 100644 --- a/specifications/Prisoners_Single_Switch/manifest.json +++ b/specifications/Prisoners_Single_Switch/manifest.json @@ -7,6 +7,11 @@ "beginner" ], "modules": [ + { + "path": "specifications/Prisoners_Single_Switch/APPrisoner.tla", + "features": [], + "models": [] + }, { "path": "specifications/Prisoners_Single_Switch/Prisoner.tla", "features": [], diff --git a/specifications/ReadersWriters/APReadersWriters.cfg b/specifications/ReadersWriters/APReadersWriters.cfg new file mode 100644 index 00000000..93266ed8 --- /dev/null +++ b/specifications/ReadersWriters/APReadersWriters.cfg @@ -0,0 +1,11 @@ +\* Use INIT/NEXT directly because the original Spec adds per-actor +\* WF fairness which Apalache does not handle. +\* `TypeOK` references `Seq({"read","write"} \X Actors)` (an unbounded +\* set) which Apalache cannot enumerate; we only check `Safety` here. + +CONSTANT NumActors = 3 + +INIT Init +NEXT Next + +INVARIANT Safety diff --git a/specifications/ReadersWriters/APReadersWriters.tla b/specifications/ReadersWriters/APReadersWriters.tla new file mode 100644 index 00000000..232e2981 --- /dev/null +++ b/specifications/ReadersWriters/APReadersWriters.tla @@ -0,0 +1,29 @@ +-------------------------- MODULE APReadersWriters -------------------------- +(* Apalache type annotations for ReadersWriters.tla, applied via INSTANCE so + the original spec is not modified. *) + +EXTENDS FiniteSets, Naturals, Sequences + +CONSTANT + \* @type: Int; + NumActors + +VARIABLES + \* @type: Set(Int); + readers, + \* @type: Set(Int); + writers, + \* @type: Seq(<>); + waiting + +\* @type: Seq(<>) => Set(<>); +ToSet(s) == { s[i] : i \in DOMAIN s } + +\* @type: <> => Bool; +read(s) == s[1] = "read" +\* @type: <> => Bool; +write(s) == s[1] = "write" + +INSTANCE ReadersWriters + +============================================================================== diff --git a/specifications/ReadersWriters/manifest.json b/specifications/ReadersWriters/manifest.json index c0e0f18f..7ccc2a41 100644 --- a/specifications/ReadersWriters/manifest.json +++ b/specifications/ReadersWriters/manifest.json @@ -5,6 +5,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/ReadersWriters/APReadersWriters.tla", + "features": [], + "models": [ + { + "path": "specifications/ReadersWriters/APReadersWriters.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/ReadersWriters/MC.tla", "features": [], diff --git a/specifications/SingleLaneBridge/APSingleLaneBridge.tla b/specifications/SingleLaneBridge/APSingleLaneBridge.tla new file mode 100644 index 00000000..c224b42d --- /dev/null +++ b/specifications/SingleLaneBridge/APSingleLaneBridge.tla @@ -0,0 +1,32 @@ +------------------------- MODULE APSingleLaneBridge ------------------------- +(* Apalache type annotations for SingleLaneBridge.tla, applied via INSTANCE + so the original spec is not modified. *) + +EXTENDS Naturals, FiniteSets, Sequences + +CONSTANTS + \* @type: Set(CAR); + CarsRight, + \* @type: Set(CAR); + CarsLeft, + \* @type: Set(Int); + Bridge, + \* @type: Set(Int); + Positions + +VARIABLES + \* @type: CAR -> Int; + Location, + \* @type: Seq(CAR); + WaitingBeforeBridge + +INSTANCE SingleLaneBridge + +\* Concrete values for the constants used by APSingleLaneBridge.cfg. +CarsRightVal == { "r1_OF_CAR", "r2_OF_CAR" } +CarsLeftVal == { "l1_OF_CAR", "l2_OF_CAR" } +PositionsVal == 1..6 +BridgeVal == 3..4 + + +============================================================================== diff --git a/specifications/SingleLaneBridge/manifest.json b/specifications/SingleLaneBridge/manifest.json index 9c56c27f..da6dfd0f 100644 --- a/specifications/SingleLaneBridge/manifest.json +++ b/specifications/SingleLaneBridge/manifest.json @@ -5,6 +5,11 @@ ], "tags": [], "modules": [ + { + "path": "specifications/SingleLaneBridge/APSingleLaneBridge.tla", + "features": [], + "models": [] + }, { "path": "specifications/SingleLaneBridge/MC.tla", "features": [], diff --git a/specifications/SpanningTree/APSpanTree.cfg b/specifications/SpanningTree/APSpanTree.cfg new file mode 100644 index 00000000..39d64b25 --- /dev/null +++ b/specifications/SpanningTree/APSpanTree.cfg @@ -0,0 +1,11 @@ +CONSTANTS + Nodes <- NodesVal + Edges <- EdgesVal + Root <- RootVal + MaxCardinality = 3 + +INVARIANT TypeOK + +SPECIFICATION Spec + +CHECK_DEADLOCK FALSE diff --git a/specifications/SpanningTree/APSpanTree.tla b/specifications/SpanningTree/APSpanTree.tla new file mode 100644 index 00000000..4f137057 --- /dev/null +++ b/specifications/SpanningTree/APSpanTree.tla @@ -0,0 +1,31 @@ +------------------------------ MODULE APSpanTree ------------------------------ +(* Apalache type annotations for SpanTree.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Integers, FiniteSets + +CONSTANTS + \* @type: Set(NODE); + Nodes, + \* @type: Set(Set(NODE)); + Edges, + \* @type: NODE; + Root, + \* @type: Int; + MaxCardinality + +VARIABLES + \* @type: NODE -> NODE; + mom, + \* @type: NODE -> Int; + dist + +INSTANCE SpanTree + +\* Concrete values for the constants used by APSpanTree.cfg. +NodesVal == { "n1_OF_NODE", "n2_OF_NODE", "n3_OF_NODE" } +\* @type: Set(Set(NODE)); +EdgesVal == { {"n1_OF_NODE", "n2_OF_NODE"}, {"n2_OF_NODE", "n3_OF_NODE"} } +RootVal == "n1_OF_NODE" + +============================================================================== diff --git a/specifications/SpanningTree/manifest.json b/specifications/SpanningTree/manifest.json index 3f8da5c6..9c932054 100644 --- a/specifications/SpanningTree/manifest.json +++ b/specifications/SpanningTree/manifest.json @@ -5,6 +5,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/SpanningTree/APSpanTree.tla", + "features": [], + "models": [ + { + "path": "specifications/SpanningTree/APSpanTree.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/SpanningTree/SpanTree.tla", "features": [], diff --git a/specifications/SpecifyingSystems/AsynchronousInterface/APAsynchInterface.cfg b/specifications/SpecifyingSystems/AsynchronousInterface/APAsynchInterface.cfg new file mode 100644 index 00000000..18704838 --- /dev/null +++ b/specifications/SpecifyingSystems/AsynchronousInterface/APAsynchInterface.cfg @@ -0,0 +1,5 @@ +CONSTANT Data <- DataVal + +INVARIANT TypeInvariant + +SPECIFICATION Spec diff --git a/specifications/SpecifyingSystems/AsynchronousInterface/APAsynchInterface.tla b/specifications/SpecifyingSystems/AsynchronousInterface/APAsynchInterface.tla new file mode 100644 index 00000000..c0920e63 --- /dev/null +++ b/specifications/SpecifyingSystems/AsynchronousInterface/APAsynchInterface.tla @@ -0,0 +1,24 @@ +------------------ MODULE APAsynchInterface --------------------- +(* Apalache type annotations for AsynchInterface.tla, applied via INSTANCE + so the original spec is not modified. *) + +EXTENDS Naturals + +CONSTANT + \* @type: Set(DATUM); + Data + +VARIABLES + \* @type: DATUM; + val, + \* @type: Int; + rdy, + \* @type: Int; + ack + +INSTANCE AsynchInterface + +\* Concrete values for the constants used by APAsynchInterface.cfg. +DataVal == { "d1_OF_DATUM", "d2_OF_DATUM" } + +================================================================ diff --git a/specifications/SpecifyingSystems/AsynchronousInterface/APChannel.cfg b/specifications/SpecifyingSystems/AsynchronousInterface/APChannel.cfg new file mode 100644 index 00000000..18704838 --- /dev/null +++ b/specifications/SpecifyingSystems/AsynchronousInterface/APChannel.cfg @@ -0,0 +1,5 @@ +CONSTANT Data <- DataVal + +INVARIANT TypeInvariant + +SPECIFICATION Spec diff --git a/specifications/SpecifyingSystems/AsynchronousInterface/APChannel.tla b/specifications/SpecifyingSystems/AsynchronousInterface/APChannel.tla new file mode 100644 index 00000000..b022be1e --- /dev/null +++ b/specifications/SpecifyingSystems/AsynchronousInterface/APChannel.tla @@ -0,0 +1,20 @@ +---------------------- MODULE APChannel ---------------------- +(* Apalache type annotations for Channel.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals + +CONSTANT + \* @type: Set(DATUM); + Data + +VARIABLE + \* @type: { val: DATUM, rdy: Int, ack: Int }; + chan + +INSTANCE Channel + +\* Concrete values for the constants used by APChannel.cfg. +DataVal == { "d1_OF_DATUM", "d2_OF_DATUM" } + +================================================================ diff --git a/specifications/SpecifyingSystems/FIFO/APInnerFIFO.cfg b/specifications/SpecifyingSystems/FIFO/APInnerFIFO.cfg new file mode 100644 index 00000000..ef3928b5 --- /dev/null +++ b/specifications/SpecifyingSystems/FIFO/APInnerFIFO.cfg @@ -0,0 +1,12 @@ +\* The original `TypeInvariant` references `Seq(Message)` which Apalache +\* cannot enumerate; we omit it from the cfg but still drive the checker +\* against the channel invariants of the inner Channel modules via +\* `InChan!TypeInvariant` / `OutChan!TypeInvariant`. Those access only +\* the record-typed channels and stay within Apalache's fragment. + +CONSTANT + Message <- MessageVal + +INVARIANT ChannelTypeInvariants + +SPECIFICATION Spec diff --git a/specifications/SpecifyingSystems/FIFO/APInnerFIFO.tla b/specifications/SpecifyingSystems/FIFO/APInnerFIFO.tla new file mode 100644 index 00000000..e74be842 --- /dev/null +++ b/specifications/SpecifyingSystems/FIFO/APInnerFIFO.tla @@ -0,0 +1,30 @@ +---------------------------- MODULE APInnerFIFO ------------------------------- +(* Apalache type annotations for InnerFIFO.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals, Sequences + +CONSTANT + \* @type: Set(MSG); + Message + +VARIABLES + \* @type: { val: MSG, rdy: Int, ack: Int }; + in, + \* @type: { val: MSG, rdy: Int, ack: Int }; + out, + \* @type: Seq(MSG); + q + +INSTANCE InnerFIFO + +\* Concrete values for the constants used by APInnerFIFO.cfg. +MessageVal == { "m1_OF_MSG", "m2_OF_MSG" } + +\* Channel-level invariant that excludes `q \in Seq(Message)` (an unbounded +\* set Apalache cannot enumerate) but keeps the channel record checks. +ChannelTypeInvariants == + /\ InChan!TypeInvariant + /\ OutChan!TypeInvariant + +============================================================================== diff --git a/specifications/SpecifyingSystems/HourClock/APHourClock.cfg b/specifications/SpecifyingSystems/HourClock/APHourClock.cfg new file mode 100644 index 00000000..280d6243 --- /dev/null +++ b/specifications/SpecifyingSystems/HourClock/APHourClock.cfg @@ -0,0 +1,3 @@ +SPECIFICATION HC + +INVARIANT HCini diff --git a/specifications/SpecifyingSystems/HourClock/APHourClock.tla b/specifications/SpecifyingSystems/HourClock/APHourClock.tla new file mode 100644 index 00000000..5942b369 --- /dev/null +++ b/specifications/SpecifyingSystems/HourClock/APHourClock.tla @@ -0,0 +1,13 @@ +---------------------- MODULE APHourClock ---------------------- +(* Apalache type annotations for HourClock.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals + +VARIABLE + \* @type: Int; + hr + +INSTANCE HourClock + +================================================================ diff --git a/specifications/SpecifyingSystems/Liveness/APLiveHourClock.cfg b/specifications/SpecifyingSystems/Liveness/APLiveHourClock.cfg new file mode 100644 index 00000000..bfb6eac3 --- /dev/null +++ b/specifications/SpecifyingSystems/Liveness/APLiveHourClock.cfg @@ -0,0 +1,9 @@ +\* The original LSpec is `HC /\ WF_hr(HCnxt)` where `HC` is itself +\* `HCini /\ [][HCnxt]_hr`. Apalache wants the canonical form +\* `Init /\ [][Next]_vars`, so we set Init/Next directly. + +INIT HCini + +NEXT HCnxt + +INVARIANT HCini diff --git a/specifications/SpecifyingSystems/Liveness/APLiveHourClock.tla b/specifications/SpecifyingSystems/Liveness/APLiveHourClock.tla new file mode 100644 index 00000000..be427c0f --- /dev/null +++ b/specifications/SpecifyingSystems/Liveness/APLiveHourClock.tla @@ -0,0 +1,13 @@ +--------------------------- MODULE APLiveHourClock --------------------------- +(* Apalache type annotations for LiveHourClock.tla, applied via INSTANCE so + the original spec is not modified. *) + +EXTENDS Naturals + +VARIABLE + \* @type: Int; + hr + +INSTANCE LiveHourClock WITH hr <- hr + +============================================================================== diff --git a/specifications/SpecifyingSystems/manifest.json b/specifications/SpecifyingSystems/manifest.json index 1ec2dfc3..b463b856 100644 --- a/specifications/SpecifyingSystems/manifest.json +++ b/specifications/SpecifyingSystems/manifest.json @@ -71,6 +71,30 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/APAsynchInterface.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/APAsynchInterface.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/APChannel.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/APChannel.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface.tla", "features": [], @@ -211,6 +235,18 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/FIFO/APInnerFIFO.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/FIFO/APInnerFIFO.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/SpecifyingSystems/FIFO/Channel.tla", "features": [], @@ -246,6 +282,18 @@ } ] }, + { + "path": "specifications/SpecifyingSystems/HourClock/APHourClock.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/HourClock/APHourClock.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/SpecifyingSystems/HourClock/HourClock.tla", "features": [], @@ -276,6 +324,18 @@ } ] }, + { + "path": "specifications/SpecifyingSystems/Liveness/APLiveHourClock.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/Liveness/APLiveHourClock.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/SpecifyingSystems/Liveness/HourClock.tla", "features": [], diff --git a/specifications/barriers/APBarrier.cfg b/specifications/barriers/APBarrier.cfg new file mode 100644 index 00000000..07670df6 --- /dev/null +++ b/specifications/barriers/APBarrier.cfg @@ -0,0 +1,5 @@ +CONSTANT N = 6 + +INVARIANT TypeOK + +SPECIFICATION Spec diff --git a/specifications/barriers/APBarrier.tla b/specifications/barriers/APBarrier.tla new file mode 100644 index 00000000..af1b3750 --- /dev/null +++ b/specifications/barriers/APBarrier.tla @@ -0,0 +1,21 @@ +------------------------------- MODULE APBarrier ------------------------------- +(* Apalache type annotations for Barrier.tla, applied via INSTANCE so the + original spec is not modified. The locally redefined `vars` provides the + missing annotation that disambiguates the 1-tuple in `Barrier!vars`. *) + +EXTENDS Integers + +CONSTANTS + \* @type: Int; + N + +VARIABLES + \* @type: Int -> Str; + pc + +\* @type: < Str>>; +vars == << pc >> + +INSTANCE Barrier + +================================================================================ diff --git a/specifications/barriers/manifest.json b/specifications/barriers/manifest.json index 8648f354..4968fe1b 100644 --- a/specifications/barriers/manifest.json +++ b/specifications/barriers/manifest.json @@ -7,6 +7,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/barriers/APBarrier.tla", + "features": [], + "models": [ + { + "path": "specifications/barriers/APBarrier.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/barriers/Barrier.tla", "features": [], diff --git a/specifications/bcastFolklore/APbcastFolklore.cfg b/specifications/bcastFolklore/APbcastFolklore.cfg new file mode 100644 index 00000000..3f83f342 --- /dev/null +++ b/specifications/bcastFolklore/APbcastFolklore.cfg @@ -0,0 +1,8 @@ +CONSTANTS + N = 4 + T = 1 + F = 1 + +INVARIANT TypeOK + +SPECIFICATION Spec diff --git a/specifications/bcastFolklore/APbcastFolklore.tla b/specifications/bcastFolklore/APbcastFolklore.tla new file mode 100644 index 00000000..76583b07 --- /dev/null +++ b/specifications/bcastFolklore/APbcastFolklore.tla @@ -0,0 +1,30 @@ +------------------------------ MODULE APbcastFolklore ------------------------------ +(* Apalache type annotations for bcastFolklore.tla. + Instantiates the original spec with typed constants and variables so that + the Apalache type checker can verify it without modifying the original. *) + +EXTENDS Naturals + +CONSTANTS + \* @type: Int; + N, + \* @type: Int; + T, + \* @type: Int; + F + +VARIABLES + \* @type: Set(Int); + Corr, + \* @type: Int; + nCrashed, + \* @type: Int -> Str; + pc, + \* @type: Int -> Set(<>); + rcvd, + \* @type: Set(<>); + sent + +INSTANCE bcastFolklore + +============================================================================= diff --git a/specifications/bcastFolklore/manifest.json b/specifications/bcastFolklore/manifest.json index 5782985f..cd21833d 100644 --- a/specifications/bcastFolklore/manifest.json +++ b/specifications/bcastFolklore/manifest.json @@ -7,6 +7,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/bcastFolklore/APbcastFolklore.tla", + "features": [], + "models": [ + { + "path": "specifications/bcastFolklore/APbcastFolklore.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/bcastFolklore/bcastFolklore.tla", "features": [], diff --git a/specifications/bosco/APbosco.cfg b/specifications/bosco/APbosco.cfg new file mode 100644 index 00000000..863926f3 --- /dev/null +++ b/specifications/bosco/APbosco.cfg @@ -0,0 +1,13 @@ +CONSTANTS + N = 4 + T = 1 + F = 1 + +INVARIANT + TypeOK + Lemma3_0 + Lemma3_1 + Lemma4_0 + Lemma4_1 + +SPECIFICATION Spec diff --git a/specifications/bosco/APbosco.tla b/specifications/bosco/APbosco.tla new file mode 100644 index 00000000..8731687d --- /dev/null +++ b/specifications/bosco/APbosco.tla @@ -0,0 +1,25 @@ +------------------------------- MODULE APbosco ------------------------------- +(* Apalache type annotations for bosco.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals, FiniteSets + +CONSTANTS + \* @type: Int; + N, + \* @type: Int; + T, + \* @type: Int; + F + +VARIABLES + \* @type: Int -> Str; + pc, + \* @type: Int -> Set(<>); + rcvd, + \* @type: Set(<>); + sent + +INSTANCE bosco + +================================================================================ diff --git a/specifications/bosco/manifest.json b/specifications/bosco/manifest.json index fb6c1a80..b1cb3fea 100644 --- a/specifications/bosco/manifest.json +++ b/specifications/bosco/manifest.json @@ -7,6 +7,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/bosco/APbosco.tla", + "features": [], + "models": [ + { + "path": "specifications/bosco/APbosco.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/bosco/bosco.tla", "features": [], diff --git a/specifications/c1cs/APc1cs.cfg b/specifications/c1cs/APc1cs.cfg new file mode 100644 index 00000000..80789985 --- /dev/null +++ b/specifications/c1cs/APc1cs.cfg @@ -0,0 +1,14 @@ +CONSTANTS + N = 4 + T = 1 + F = 1 + Values <- ValuesVal + Bottom <- BottomVal + +INVARIANT + TypeOK + Validity + Agreement + WeakAgreement + +SPECIFICATION Spec diff --git a/specifications/c1cs/APc1cs.tla b/specifications/c1cs/APc1cs.tla new file mode 100644 index 00000000..93635c56 --- /dev/null +++ b/specifications/c1cs/APc1cs.tla @@ -0,0 +1,47 @@ +------------------------------- MODULE APc1cs ------------------------------- +(* Apalache type annotations for c1cs.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Integers, FiniteSets, TLC + +CONSTANT + \* @type: Int; + N, + \* @type: Int; + F, + \* @type: Int; + T, + \* @type: Set(VALUE); + Values, + \* @type: VALUE; + Bottom + +VARIABLES + \* @type: Int -> Str; + pc, + \* @type: Int -> VALUE; + v, + \* @type: Int -> VALUE; + dValue, + \* @type: Set({ type: Str, value: VALUE, sndr: Int }); + bcastMsg, + \* @type: Int -> Set({ type: Str, value: VALUE, sndr: Int }); + rcvdMsg + +\* The original spec uses an inline tuple in +\* `Spec == Init /\ [][Next]_<< pc, v, dValue, bcastMsg, rcvdMsg >> /\ ...` +\* which Snowcat cannot disambiguate. Provide a typed witness that matches the +\* original `vars` operator. +\* @type: < Str, Int -> VALUE, Int -> VALUE, Set({ type: Str, value: VALUE, sndr: Int }), Int -> Set({ type: Str, value: VALUE, sndr: Int })>>; +vars == << pc, v, dValue, bcastMsg, rcvdMsg >> + +INSTANCE c1cs + +\* Concrete values for the uninterpreted-type constants. The .cfg file +\* substitutes them via `Values <- ValuesVal` etc., because TLC-style +\* `Values = {v1, v2}` assignments would tag the model values as `Str` +\* in Apalache (and `VALUE \neq Str`). +ValuesVal == { "v1_OF_VALUE", "v2_OF_VALUE" } +BottomVal == "bottom_OF_VALUE" + +============================================================================= diff --git a/specifications/c1cs/manifest.json b/specifications/c1cs/manifest.json index 569b0188..801b2160 100644 --- a/specifications/c1cs/manifest.json +++ b/specifications/c1cs/manifest.json @@ -7,6 +7,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/c1cs/APc1cs.tla", + "features": [], + "models": [ + { + "path": "specifications/c1cs/APc1cs.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/c1cs/c1cs.tla", "features": [], diff --git a/specifications/cf1s-folklore/APcf1s_folklore.tla b/specifications/cf1s-folklore/APcf1s_folklore.tla new file mode 100644 index 00000000..ae478f0a --- /dev/null +++ b/specifications/cf1s-folklore/APcf1s_folklore.tla @@ -0,0 +1,35 @@ +------------------------- MODULE APcf1s_folklore ------------------------- +(* Apalache type annotations for cf1s_folklore.tla, applied via INSTANCE so + the original spec is not modified. *) + +EXTENDS Naturals, FiniteSets + +CONSTANTS + \* @type: Int; + N, + \* @type: Int; + T, + \* @type: Int; + F + +VARIABLES + \* @type: Int; + nSnt0, + \* @type: Int; + nSnt1, + \* @type: Int; + nSnt0F, + \* @type: Int; + nSnt1F, + \* @type: Int; + nFaulty, + \* @type: Int -> Str; + pc, + \* @type: Int -> Int; + nRcvd0, + \* @type: Int -> Int; + nRcvd1 + +INSTANCE cf1s_folklore + +========================================================================== diff --git a/specifications/cf1s-folklore/manifest.json b/specifications/cf1s-folklore/manifest.json index e127583a..2224949b 100644 --- a/specifications/cf1s-folklore/manifest.json +++ b/specifications/cf1s-folklore/manifest.json @@ -7,6 +7,11 @@ ], "tags": [], "modules": [ + { + "path": "specifications/cf1s-folklore/APcf1s_folklore.tla", + "features": [], + "models": [] + }, { "path": "specifications/cf1s-folklore/cf1s_folklore.tla", "features": [], diff --git a/specifications/chang_roberts/APChangRoberts.cfg b/specifications/chang_roberts/APChangRoberts.cfg new file mode 100644 index 00000000..5f2fe859 --- /dev/null +++ b/specifications/chang_roberts/APChangRoberts.cfg @@ -0,0 +1,15 @@ +\* Drive Init/Next directly because the original Spec adds per-process +\* fairness which Apalache does not check. + +CONSTANTS + N <- NVal + Id <- IdVal + +INIT Init +NEXT Next + +INVARIANT + TypeOK + Correctness + +CHECK_DEADLOCK FALSE diff --git a/specifications/chang_roberts/APChangRoberts.tla b/specifications/chang_roberts/APChangRoberts.tla new file mode 100644 index 00000000..34b3fa2b --- /dev/null +++ b/specifications/chang_roberts/APChangRoberts.tla @@ -0,0 +1,31 @@ +--------------------------- MODULE APChangRoberts --------------------------- +(* Apalache type annotations for ChangRoberts.tla, applied via INSTANCE so + the original spec is not modified. *) + +EXTENDS Naturals, Sequences + +CONSTANTS + \* @type: Int; + N, + \* @type: Seq(Int); + Id + +VARIABLES + \* @type: Int -> Set(Int); + msgs, + \* @type: Int -> Str; + pc, + \* @type: Int -> Bool; + initiator, + \* @type: Int -> Str; + state + +INSTANCE ChangRoberts + +\* Concrete values for the constants. APChangRoberts.cfg substitutes them +\* via `N <- NVal` and `Id <- IdVal`. +NVal == 3 +\* @type: Seq(Int); +IdVal == <<3, 1, 2>> + +============================================================================== diff --git a/specifications/chang_roberts/manifest.json b/specifications/chang_roberts/manifest.json index 195b4104..fd8e0e05 100644 --- a/specifications/chang_roberts/manifest.json +++ b/specifications/chang_roberts/manifest.json @@ -5,6 +5,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/chang_roberts/APChangRoberts.tla", + "features": [], + "models": [ + { + "path": "specifications/chang_roberts/APChangRoberts.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/chang_roberts/ChangRoberts.tla", "features": [ diff --git a/specifications/ewd426/APTokenRing.cfg b/specifications/ewd426/APTokenRing.cfg new file mode 100644 index 00000000..481a5a32 --- /dev/null +++ b/specifications/ewd426/APTokenRing.cfg @@ -0,0 +1,7 @@ +CONSTANTS + N = 6 + M = 6 + +INVARIANT TypeOK + +SPECIFICATION Spec diff --git a/specifications/ewd426/APTokenRing.tla b/specifications/ewd426/APTokenRing.tla new file mode 100644 index 00000000..6d22fee0 --- /dev/null +++ b/specifications/ewd426/APTokenRing.tla @@ -0,0 +1,22 @@ +--------------------------- MODULE APTokenRing --------------------------- +(* Apalache type annotations for TokenRing.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals, FiniteSets + +CONSTANTS + \* @type: Int; + N, + \* @type: Int; + M + +VARIABLES + \* @type: Int -> Int; + c + +\* @type: < Int>>; +vars == << c >> + +INSTANCE TokenRing + +========================================================================== diff --git a/specifications/ewd426/manifest.json b/specifications/ewd426/manifest.json index 8ba79899..9864bf9d 100644 --- a/specifications/ewd426/manifest.json +++ b/specifications/ewd426/manifest.json @@ -8,6 +8,18 @@ "ewd" ], "modules": [ + { + "path": "specifications/ewd426/APTokenRing.tla", + "features": [], + "models": [ + { + "path": "specifications/ewd426/APTokenRing.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/ewd426/SimTokenRing.tla", "features": [], diff --git a/specifications/ewd840/APEWD840.cfg b/specifications/ewd840/APEWD840.cfg new file mode 100644 index 00000000..28a6a45d --- /dev/null +++ b/specifications/ewd840/APEWD840.cfg @@ -0,0 +1,9 @@ +CONSTANT N = 3 + +INVARIANT + TypeOK + TerminationDetection + +SPECIFICATION Spec + +CHECK_DEADLOCK FALSE diff --git a/specifications/ewd840/APEWD840.tla b/specifications/ewd840/APEWD840.tla new file mode 100644 index 00000000..cac7fc3e --- /dev/null +++ b/specifications/ewd840/APEWD840.tla @@ -0,0 +1,23 @@ +------------------------------ MODULE APEWD840 ------------------------------ +(* Apalache type annotations for EWD840.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals + +CONSTANT + \* @type: Int; + N + +VARIABLES + \* @type: Int -> Bool; + active, + \* @type: Int -> Str; + color, + \* @type: Int; + tpos, + \* @type: Str; + tcolor + +INSTANCE EWD840 + +============================================================================== diff --git a/specifications/ewd840/APSyncTerminationDetection.cfg b/specifications/ewd840/APSyncTerminationDetection.cfg new file mode 100644 index 00000000..1cef4991 --- /dev/null +++ b/specifications/ewd840/APSyncTerminationDetection.cfg @@ -0,0 +1,7 @@ +CONSTANT N = 7 + +INVARIANT + TypeOK + TDCorrect + +SPECIFICATION Spec diff --git a/specifications/ewd840/APSyncTerminationDetection.tla b/specifications/ewd840/APSyncTerminationDetection.tla new file mode 100644 index 00000000..f4ea4a7f --- /dev/null +++ b/specifications/ewd840/APSyncTerminationDetection.tla @@ -0,0 +1,19 @@ +--------------------- MODULE APSyncTerminationDetection --------------------- +(* Apalache type annotations for SyncTerminationDetection.tla, applied via + INSTANCE so the original spec is not modified. *) + +EXTENDS Naturals + +CONSTANT + \* @type: Int; + N + +VARIABLES + \* @type: Int -> Bool; + active, + \* @type: Bool; + terminationDetected + +INSTANCE SyncTerminationDetection + +============================================================================== diff --git a/specifications/ewd840/manifest.json b/specifications/ewd840/manifest.json index 43757b3d..a9567350 100644 --- a/specifications/ewd840/manifest.json +++ b/specifications/ewd840/manifest.json @@ -9,6 +9,30 @@ "ewd" ], "modules": [ + { + "path": "specifications/ewd840/APEWD840.tla", + "features": [], + "models": [ + { + "path": "specifications/ewd840/APEWD840.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/ewd840/APSyncTerminationDetection.tla", + "features": [], + "models": [ + { + "path": "specifications/ewd840/APSyncTerminationDetection.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/ewd840/EWD840.tla", "features": [], diff --git a/specifications/glowingRaccoon/APclean.cfg b/specifications/glowingRaccoon/APclean.cfg new file mode 100644 index 00000000..e0fb5048 --- /dev/null +++ b/specifications/glowingRaccoon/APclean.cfg @@ -0,0 +1,10 @@ +CONSTANTS + DNA = 5 + PRIMER = 5 + +INVARIANT + TypeOK + primerPositive + preservationInvariant + +SPECIFICATION Spec diff --git a/specifications/glowingRaccoon/APclean.tla b/specifications/glowingRaccoon/APclean.tla new file mode 100644 index 00000000..aa7eed4e --- /dev/null +++ b/specifications/glowingRaccoon/APclean.tla @@ -0,0 +1,27 @@ +----------------------------- MODULE APclean ----------------------------- +(* Apalache type annotations for clean.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals + +CONSTANTS + \* @type: Int; + DNA, + \* @type: Int; + PRIMER + +VARIABLES + \* @type: Str; + tee, + \* @type: Int; + primer, + \* @type: Int; + dna, + \* @type: Int; + template, + \* @type: Int; + hybrid + +INSTANCE clean + +========================================================================== diff --git a/specifications/glowingRaccoon/APstages.cfg b/specifications/glowingRaccoon/APstages.cfg new file mode 100644 index 00000000..e6832c2c --- /dev/null +++ b/specifications/glowingRaccoon/APstages.cfg @@ -0,0 +1,9 @@ +CONSTANTS + DNA = 5 + PRIMER = 5 + +INVARIANT TypeOK + +SPECIFICATION Spec + +CHECK_DEADLOCK FALSE diff --git a/specifications/glowingRaccoon/APstages.tla b/specifications/glowingRaccoon/APstages.tla new file mode 100644 index 00000000..fad7bf0c --- /dev/null +++ b/specifications/glowingRaccoon/APstages.tla @@ -0,0 +1,31 @@ +----------------------------- MODULE APstages ----------------------------- +(* Apalache type annotations for stages.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Naturals + +CONSTANTS + \* @type: Int; + DNA, + \* @type: Int; + PRIMER + +VARIABLES + \* @type: Str; + tee, + \* @type: Int; + primer, + \* @type: Int; + dna, + \* @type: Int; + template, + \* @type: Int; + hybrid, + \* @type: Str; + stage, + \* @type: Int; + cycle + +INSTANCE stages + +========================================================================== diff --git a/specifications/glowingRaccoon/manifest.json b/specifications/glowingRaccoon/manifest.json index 06d7ea9f..5f17c906 100644 --- a/specifications/glowingRaccoon/manifest.json +++ b/specifications/glowingRaccoon/manifest.json @@ -5,6 +5,30 @@ ], "tags": [], "modules": [ + { + "path": "specifications/glowingRaccoon/APclean.tla", + "features": [], + "models": [ + { + "path": "specifications/glowingRaccoon/APclean.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/glowingRaccoon/APstages.tla", + "features": [], + "models": [ + { + "path": "specifications/glowingRaccoon/APstages.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/glowingRaccoon/clean.tla", "features": [], diff --git a/specifications/lamport_mutex/APLamportMutex.cfg b/specifications/lamport_mutex/APLamportMutex.cfg new file mode 100644 index 00000000..0f094591 --- /dev/null +++ b/specifications/lamport_mutex/APLamportMutex.cfg @@ -0,0 +1,10 @@ +\* `TypeOK` references `Seq(Message)` (an unbounded set) which Apalache +\* cannot enumerate, so we only check `Mutex` here. + +CONSTANTS + N = 3 + maxClock = 10 + +INVARIANT Mutex + +SPECIFICATION Spec diff --git a/specifications/lamport_mutex/APLamportMutex.tla b/specifications/lamport_mutex/APLamportMutex.tla new file mode 100644 index 00000000..82b3763c --- /dev/null +++ b/specifications/lamport_mutex/APLamportMutex.tla @@ -0,0 +1,27 @@ +--------------------------- MODULE APLamportMutex --------------------------- +(* Apalache type annotations for LamportMutex.tla, applied via INSTANCE so + the original spec is not modified. *) + +EXTENDS Naturals, Sequences + +CONSTANT + \* @type: Int; + N, + \* @type: Int; + maxClock + +VARIABLES + \* @type: Int -> Int; + clock, + \* @type: Int -> (Int -> Int); + req, + \* @type: Int -> Set(Int); + ack, + \* @type: Int -> (Int -> Seq({ type: Str, clock: Int })); + network, + \* @type: Set(Int); + crit + +INSTANCE LamportMutex + +============================================================================== diff --git a/specifications/lamport_mutex/manifest.json b/specifications/lamport_mutex/manifest.json index bb2dbaa2..86a5c322 100644 --- a/specifications/lamport_mutex/manifest.json +++ b/specifications/lamport_mutex/manifest.json @@ -5,6 +5,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/lamport_mutex/APLamportMutex.tla", + "features": [], + "models": [ + { + "path": "specifications/lamport_mutex/APLamportMutex.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/lamport_mutex/LamportMutex.tla", "features": [], diff --git a/specifications/nbacg_guer01/APnbacg_guer01.cfg b/specifications/nbacg_guer01/APnbacg_guer01.cfg new file mode 100644 index 00000000..d4140596 --- /dev/null +++ b/specifications/nbacg_guer01/APnbacg_guer01.cfg @@ -0,0 +1,5 @@ +CONSTANT N = 3 + +INVARIANT TypeOK + +SPECIFICATION Spec diff --git a/specifications/nbacg_guer01/APnbacg_guer01.tla b/specifications/nbacg_guer01/APnbacg_guer01.tla new file mode 100644 index 00000000..9c111b74 --- /dev/null +++ b/specifications/nbacg_guer01/APnbacg_guer01.tla @@ -0,0 +1,31 @@ +--------------------------- MODULE APnbacg_guer01 --------------------------- +(* Apalache type annotations for nbacg_guer01.tla, applied via INSTANCE so + the original spec is not modified. *) + +EXTENDS Naturals, FiniteSets + +CONSTANTS + \* @type: Int; + N + +VARIABLES + \* @type: Int; + nSntNo, + \* @type: Int; + nSntYes, + \* @type: Int; + nSntNoF, + \* @type: Int; + nSntYesF, + \* @type: Int -> Int; + nRcvdYes, + \* @type: Int -> Int; + nRcvdNo, + \* @type: Int -> Bool; + someFail, + \* @type: Int -> Str; + pc + +INSTANCE nbacg_guer01 + +========================================================================== diff --git a/specifications/nbacg_guer01/manifest.json b/specifications/nbacg_guer01/manifest.json index 1ca3cc65..72509678 100644 --- a/specifications/nbacg_guer01/manifest.json +++ b/specifications/nbacg_guer01/manifest.json @@ -7,6 +7,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/nbacg_guer01/APnbacg_guer01.tla", + "features": [], + "models": [ + { + "path": "specifications/nbacg_guer01/APnbacg_guer01.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/nbacg_guer01/nbacg_guer01.tla", "features": [], diff --git a/specifications/spanning/APspanning.cfg b/specifications/spanning/APspanning.cfg new file mode 100644 index 00000000..f4d4177f --- /dev/null +++ b/specifications/spanning/APspanning.cfg @@ -0,0 +1,13 @@ +\* Use INIT/NEXT directly because the original Spec adds WF fairness +\* which Apalache does not handle. + +CONSTANTS + Proc <- ProcVal + NoPrnt <- NoPrntVal + root <- rootVal + nbrs <- nbrsVal + +INIT Init +NEXT Next + +INVARIANT TypeOK diff --git a/specifications/spanning/APspanning.tla b/specifications/spanning/APspanning.tla new file mode 100644 index 00000000..2352a1fb --- /dev/null +++ b/specifications/spanning/APspanning.tla @@ -0,0 +1,35 @@ +------------------------------ MODULE APspanning ------------------------------ +(* Apalache type annotations for spanning.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Integers + +CONSTANTS + \* @type: Set(PROC); + Proc, + \* @type: PROC; + NoPrnt, + \* @type: PROC; + root, + \* @type: Set(<>); + nbrs + +VARIABLES + \* @type: PROC -> PROC; + prnt, + \* @type: PROC -> Bool; + rpt, + \* @type: Set(<>); + msg + +INSTANCE spanning + +\* Concrete values for the constants used by APspanning.cfg. +ProcVal == { "p1_OF_PROC", "p2_OF_PROC", "p3_OF_PROC" } +NoPrntVal == "noprnt_OF_PROC" +rootVal == "p1_OF_PROC" +\* @type: Set(<>); +nbrsVal == { <<"p1_OF_PROC", "p2_OF_PROC">>, <<"p2_OF_PROC", "p1_OF_PROC">>, + <<"p2_OF_PROC", "p3_OF_PROC">>, <<"p3_OF_PROC", "p2_OF_PROC">> } + +============================================================================== diff --git a/specifications/spanning/manifest.json b/specifications/spanning/manifest.json index 12ea334c..522c5c7f 100644 --- a/specifications/spanning/manifest.json +++ b/specifications/spanning/manifest.json @@ -7,6 +7,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/spanning/APspanning.tla", + "features": [], + "models": [ + { + "path": "specifications/spanning/APspanning.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/spanning/MC_spanning.tla", "features": [], diff --git a/specifications/tcp/APtcp.cfg b/specifications/tcp/APtcp.cfg new file mode 100644 index 00000000..8d6a52ef --- /dev/null +++ b/specifications/tcp/APtcp.cfg @@ -0,0 +1,10 @@ +\* Use INIT/NEXT directly because the original Spec adds WF fairness +\* which Apalache does not handle. +\* `TypeOK` references an unbounded `Seq(...)`; we only check `Inv`. + +CONSTANT Peers <- PeersVal + +INIT Init +NEXT Next + +INVARIANT Inv diff --git a/specifications/tcp/APtcp.tla b/specifications/tcp/APtcp.tla new file mode 100644 index 00000000..fd2609cf --- /dev/null +++ b/specifications/tcp/APtcp.tla @@ -0,0 +1,24 @@ +------------------------------- MODULE APtcp ---------------------------------- +(* Apalache type annotations for tcp.tla, applied via INSTANCE so the + original spec is not modified. *) + +EXTENDS Integers, Sequences, SequencesExt, FiniteSets + +CONSTANT + \* @type: Set(PEER); + Peers + +VARIABLE + \* @type: PEER -> Bool; + tcb, + \* @type: PEER -> Str; + connstate, + \* @type: PEER -> Seq(Str); + network + +INSTANCE tcp + +\* Concrete values for the constants used by APtcp.cfg. +PeersVal == { "p1_OF_PEER", "p2_OF_PEER" } + +============================================================================== diff --git a/specifications/tcp/manifest.json b/specifications/tcp/manifest.json index 303204f2..db696734 100644 --- a/specifications/tcp/manifest.json +++ b/specifications/tcp/manifest.json @@ -7,6 +7,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/tcp/APtcp.tla", + "features": [], + "models": [ + { + "path": "specifications/tcp/APtcp.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/tcp/MCtcp.tla", "features": [], diff --git a/specifications/transaction_commit/APTCommit.cfg b/specifications/transaction_commit/APTCommit.cfg new file mode 100644 index 00000000..0d42e82d --- /dev/null +++ b/specifications/transaction_commit/APTCommit.cfg @@ -0,0 +1,9 @@ +CONSTANT RM <- RMVal + +INVARIANT + TCTypeOK + TCConsistent + +SPECIFICATION TCSpec + +CHECK_DEADLOCK FALSE diff --git a/specifications/transaction_commit/APTCommit.tla b/specifications/transaction_commit/APTCommit.tla new file mode 100644 index 00000000..b1bedb58 --- /dev/null +++ b/specifications/transaction_commit/APTCommit.tla @@ -0,0 +1,18 @@ +------------------------------ MODULE APTCommit ------------------------------ +(* Apalache type annotations for TCommit.tla, applied via INSTANCE so the + original spec is not modified. *) + +CONSTANT + \* @type: Set(RM); + RM + +VARIABLE + \* @type: RM -> Str; + rmState + +INSTANCE TCommit + +\* Concrete values for the constants used by APTCommit.cfg. +RMVal == { "r1_OF_RM", "r2_OF_RM", "r3_OF_RM" } + +============================================================================== diff --git a/specifications/transaction_commit/manifest.json b/specifications/transaction_commit/manifest.json index 8594bac7..5b79e51f 100644 --- a/specifications/transaction_commit/manifest.json +++ b/specifications/transaction_commit/manifest.json @@ -28,6 +28,18 @@ } ] }, + { + "path": "specifications/transaction_commit/APTCommit.tla", + "features": [], + "models": [ + { + "path": "specifications/transaction_commit/APTCommit.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/transaction_commit/PaxosCommit.tla", "features": [],