From 323433514f59494cc75e681b78a01641614202a9 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 22 Apr 2026 10:31:34 -0700 Subject: [PATCH 1/4] CI: invoke Apalache via apalache-mc.bat (and cmd.exe) on Windows `tla_utils.check_model` hard-coded `bin/apalache-mc`, but on Windows the launcher is `bin/apalache-mc.bat` and `subprocess.run` cannot spawn `.bat` files via CreateProcess directly. Pick the launcher per platform and route the Windows batch file through `cmd.exe /c`. This was latent because the only symbolic-mode model in CI (EinsteinRiddle) was always being skipped: `[ ${{ matrix.unicode }} ]` in CI.yml is truthy for both "true" and "false", so the SKIP entry was added unconditionally rather than only on the Unicode variant. Signed-off-by: Markus Alexander Kuppe --- .github/scripts/tla_utils.py | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py index 060bf0e1..e1f27c2d 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 @@ -163,16 +164,24 @@ 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. + apalache_launcher = ( + ['cmd.exe', '/c', normpath(join(apalache_path, 'bin', 'apalache-mc.bat'))] + if sys.platform == 'win32' else + [normpath(join(apalache_path, 'bin', 'apalache-mc'))]) 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', + apalache = subprocess.run( + apalache_launcher + [ + 'check', f'--config={model_path}', module_path ], From 27f0afe2c55da7cf76e3002682cfd7b8aa70557a Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 22 Apr 2026 15:11:21 -0700 Subject: [PATCH 2/4] CI: Default Apalache --length=5 for all examples Always pass `--length=5` to `apalache-mc check` from the CI driver, instead of opting individual model .cfg files in via a per-model marker comment. Apalache's own default of 10 is just as arbitrary; 5 keeps the suite within CI timeouts while still exercising each spec. Signed-off-by: Markus Alexander Kuppe --- .github/scripts/tla_utils.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py index e1f27c2d..1c755211 100644 --- a/.github/scripts/tla_utils.py +++ b/.github/scripts/tla_utils.py @@ -179,9 +179,14 @@ def check_model( community_jar_path = normpath(community_jar_path) try: if mode == 'symbolic': + # 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 = subprocess.run( apalache_launcher + [ 'check', + '--length=5', f'--config={model_path}', module_path ], From a46dcaeb4f42c9b34cb79e33d7d80f4ba4fe463b Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sat, 25 Apr 2026 08:25:42 -0700 Subject: [PATCH 3/4] CI: skip Apalache checks on Unicode specs Apalache does not yet support Unicode TLA+ syntax (apalache-mc/apalache#2995), so running symbolic-mode models against the Unicode-converted specs in CI fails for reasons unrelated to the specs themselves. Signed-off-by: Markus Alexander Kuppe --- .github/scripts/check_small_models.py | 3 +++ .github/workflows/CI.yml | 9 ++++++--- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/.github/scripts/check_small_models.py b/.github/scripts/check_small_models.py index 993d5b90..001e9f77 100644 --- a/.github/scripts/check_small_models.py +++ b/.github/scripts/check_small_models.py @@ -22,6 +22,7 @@ parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[]) parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true') parser.add_argument('--enable_assertions', help='Enable Java assertions (pass -enableassertions to JVM)', action='store_true') +parser.add_argument('--skip_apalache', help='Skip all symbolic (Apalache) models; useful when running against Unicode specs since Apalache does not yet support Unicode (https://github.com/apalache-mc/apalache/issues/2995)', action='store_true') args = parser.parse_args() logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO) @@ -34,6 +35,7 @@ skip_models = args.skip only_models = args.only enable_assertions = args.enable_assertions +skip_apalache = args.skip_apalache def check_model(module, model, expected_runtime): module_path = tla_utils.from_cwd(examples_root, module['path']) @@ -100,6 +102,7 @@ def check_model(module, model, expected_runtime): for model in module['models'] if (runtime := tla_utils.parse_timespan(model['runtime'])) <= timedelta(seconds=30) and model['path'] not in skip_models + and not (skip_apalache and model['mode'] == 'symbolic') and (only_models == [] or model['path'] in only_models) ], key = lambda m: m[2], diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index cf626601..ddaf2a2d 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -102,9 +102,11 @@ jobs: # SKIP=("does/not/exist") # strange issue with parsing TLC output SKIP=("specifications/ewd840/EWD840.cfg") + # Apalache does not yet support Unicode specs: + # https://github.com/apalache-mc/apalache/issues/2995 + APALACHE_FLAG=() if [ ${{ matrix.unicode }} ]; then - # Apalache does not yet support Unicode - SKIP+=("specifications/EinsteinRiddle/Einstein.cfg") + APALACHE_FLAG+=("--skip_apalache") fi python $SCRIPT_DIR/check_small_models.py \ --verbose \ @@ -113,7 +115,8 @@ jobs: --tlapm_lib_path $DEPS_DIR/tlapm/library \ --community_modules_jar_path $DEPS_DIR/community/modules.jar \ --examples_root . \ - --skip "${SKIP[@]}" + --skip "${SKIP[@]}" \ + "${APALACHE_FLAG[@]}" - name: Smoke-test large models run: | # SimKnuthYao requires certain number of states to have been generated From eaa5c65480388005b6ec9cb148c8b5a3bb84afc3 Mon Sep 17 00:00:00 2001 From: Markus Kuppe Date: Wed, 22 Apr 2026 09:38:05 -0700 Subject: [PATCH 4/4] Add Apalache wrappers and configurations for example specifications For each spec where it was feasible, add: * AP.tla -- a non-invasive wrapper module that INSTANCEs the untyped original specification with typed CONSTANTS and VARIABLES, so that `apalache-mc typecheck` accepts the spec without modifying the source. A few wrappers also shadow polymorphic helpers (`Sum`, `Range`, `ToSet`, ...) with monomorphic versions, or define `Val` operators used by the .cfg below to fill in uninterpreted-type constants. * AP.cfg -- a TLC-style model configuration adapted for Apalache. Each .cfg drives `apalache-mc check` for the spec's safety properties (TLC `PROPERTIES` are intentionally dropped). Constants are either inlined (Int/Bool/Str) or substituted via `Const <- ConstVal` to attach the right uninterpreted type. manifest.json files are updated with the new wrappers; check_manifest_files.py and check_manifest_schema.py both pass. Requires Apalache 0.57 due to https://github.com/apalache-mc/apalache/issues/3311 Co-authored-by: Claude Code 4.7 Signed-off-by: Markus Alexander Kuppe --- .project | 11 ++ README.md | 52 +++---- specifications/Chameneos/APChameneos.tla | 37 +++++ specifications/Chameneos/manifest.json | 5 + .../CigaretteSmokers/APCigaretteSmokers.cfg | 9 ++ .../CigaretteSmokers/APCigaretteSmokers.tla | 26 ++++ specifications/CigaretteSmokers/manifest.json | 12 ++ specifications/CoffeeCan/APCoffeeCan.cfg | 5 + specifications/CoffeeCan/APCoffeeCan.tla | 17 +++ specifications/CoffeeCan/manifest.json | 12 ++ specifications/DieHard/APDieHarder.cfg | 8 + specifications/DieHard/APDieHarder.tla | 26 ++++ specifications/DieHard/manifest.json | 24 ++- .../APDiningPhilosophers.cfg | 12 ++ .../APDiningPhilosophers.tla | 22 +++ .../DiningPhilosophers/manifest.json | 12 ++ specifications/Disruptor/APDisruptor_MPMC.cfg | 16 ++ specifications/Disruptor/APDisruptor_MPMC.tla | 52 +++++++ specifications/Disruptor/APDisruptor_SPMC.cfg | 16 ++ specifications/Disruptor/APDisruptor_SPMC.tla | 48 ++++++ specifications/Disruptor/APRingBuffer.tla | 34 +++++ specifications/Disruptor/manifest.json | 29 ++++ specifications/FiniteMonotonic/APCRDT.cfg | 7 + specifications/FiniteMonotonic/APCRDT.tla | 20 +++ .../APDistributedReplicatedLog.tla | 29 ++++ .../FiniteMonotonic/APReplicatedLog.cfg | 10 ++ .../FiniteMonotonic/APReplicatedLog.tla | 25 +++ specifications/FiniteMonotonic/manifest.json | 29 ++++ .../KeyValueStore/APKeyValueStore.tla | 32 ++++ specifications/KeyValueStore/manifest.json | 5 + specifications/Majority/APMajority.tla | 26 ++++ specifications/Majority/manifest.json | 5 + .../MisraReachability/APParReach.cfg | 14 ++ .../MisraReachability/APParReach.tla | 39 +++++ .../MisraReachability/APReachable.tla | 31 ++++ .../MisraReachability/manifest.json | 17 +++ .../APMissionariesAndCannibals.cfg | 10 ++ .../APMissionariesAndCannibals.tla | 26 ++++ .../MissionariesAndCannibals/manifest.json | 12 ++ specifications/Moving_Cat_Puzzle/APCat.cfg | 5 + specifications/Moving_Cat_Puzzle/APCat.tla | 21 +++ .../Moving_Cat_Puzzle/manifest.json | 12 ++ specifications/Prisoners/APPrisoners.tla | 29 ++++ specifications/Prisoners/manifest.json | 5 + .../Prisoners_Single_Switch/APPrisoner.tla | 30 ++++ .../Prisoners_Single_Switch/manifest.json | 5 + .../ReadersWriters/APReadersWriters.cfg | 11 ++ .../ReadersWriters/APReadersWriters.tla | 39 +++++ specifications/ReadersWriters/manifest.json | 12 ++ .../SingleLaneBridge/APSingleLaneBridge.tla | 32 ++++ specifications/SingleLaneBridge/manifest.json | 5 + specifications/SpanningTree/APSpanTree.cfg | 11 ++ specifications/SpanningTree/APSpanTree.tla | 31 ++++ specifications/SpanningTree/manifest.json | 12 ++ .../APAsynchInterface.cfg | 5 + .../APAsynchInterface.tla | 24 +++ .../AsynchronousInterface/APChannel.cfg | 5 + .../AsynchronousInterface/APChannel.tla | 20 +++ .../SpecifyingSystems/Composing/APChannel.cfg | 5 + .../SpecifyingSystems/Composing/APChannel.tla | 23 +++ .../Composing/APHourClock.cfg | 3 + .../Composing/APHourClock.tla | 17 +++ .../SpecifyingSystems/FIFO/APChannel.cfg | 5 + .../SpecifyingSystems/FIFO/APChannel.tla | 23 +++ .../SpecifyingSystems/FIFO/APInnerFIFO.cfg | 12 ++ .../SpecifyingSystems/FIFO/APInnerFIFO.tla | 30 ++++ .../FIFO/APInnerFIFOInstanced.cfg | 6 + .../FIFO/APInnerFIFOInstanced.tla | 33 ++++ .../SpecifyingSystems/FIFO/APMCInnerFIFO.cfg | 7 + .../SpecifyingSystems/FIFO/APMCInnerFIFO.tla | 36 +++++ .../HourClock/APHourClock.cfg | 3 + .../HourClock/APHourClock.tla | 13 ++ .../HourClock/APHourClock2.cfg | 3 + .../HourClock/APHourClock2.tla | 16 ++ .../Liveness/APHourClock.cfg | 3 + .../Liveness/APHourClock.tla | 17 +++ .../Liveness/APLiveHourClock.cfg | 9 ++ .../Liveness/APLiveHourClock.tla | 13 ++ .../SpecifyingSystems/manifest.json | 144 ++++++++++++++++++ specifications/acp/APACP_SB.cfg | 17 +++ specifications/acp/APACP_SB.tla | 38 +++++ specifications/acp/manifest.json | 12 ++ specifications/barriers/APBarrier.cfg | 5 + specifications/barriers/APBarrier.tla | 22 +++ specifications/barriers/manifest.json | 12 ++ .../bcastFolklore/APbcastFolklore.cfg | 8 + .../bcastFolklore/APbcastFolklore.tla | 29 ++++ specifications/bcastFolklore/manifest.json | 12 ++ specifications/bosco/APbosco.cfg | 13 ++ specifications/bosco/APbosco.tla | 25 +++ specifications/bosco/manifest.json | 12 ++ specifications/c1cs/APc1cs.cfg | 14 ++ specifications/c1cs/APc1cs.tla | 47 ++++++ specifications/c1cs/manifest.json | 12 ++ .../cf1s-folklore/APcf1s_folklore.tla | 35 +++++ specifications/cf1s-folklore/manifest.json | 5 + .../chang_roberts/APChangRoberts.cfg | 15 ++ .../chang_roberts/APChangRoberts.tla | 31 ++++ specifications/chang_roberts/manifest.json | 12 ++ specifications/ewd426/APTokenRing.cfg | 7 + specifications/ewd426/APTokenRing.tla | 22 +++ specifications/ewd426/manifest.json | 12 ++ specifications/ewd840/APEWD840.cfg | 9 ++ specifications/ewd840/APEWD840.tla | 23 +++ .../ewd840/APSyncTerminationDetection.cfg | 7 + .../ewd840/APSyncTerminationDetection.tla | 20 +++ specifications/ewd840/manifest.json | 24 +++ specifications/glowingRaccoon/APclean.cfg | 10 ++ specifications/glowingRaccoon/APclean.tla | 27 ++++ specifications/glowingRaccoon/APstages.cfg | 9 ++ specifications/glowingRaccoon/APstages.tla | 31 ++++ specifications/glowingRaccoon/manifest.json | 24 +++ .../lamport_mutex/APLamportMutex.cfg | 10 ++ .../lamport_mutex/APLamportMutex.tla | 27 ++++ specifications/lamport_mutex/manifest.json | 12 ++ .../nbacg_guer01/APnbacg_guer01.cfg | 5 + .../nbacg_guer01/APnbacg_guer01.tla | 31 ++++ specifications/nbacg_guer01/manifest.json | 12 ++ specifications/spanning/APspanning.cfg | 13 ++ specifications/spanning/APspanning.tla | 35 +++++ specifications/spanning/manifest.json | 12 ++ specifications/tcp/APtcp.cfg | 10 ++ specifications/tcp/APtcp.tla | 24 +++ specifications/tcp/manifest.json | 12 ++ .../transaction_commit/APTCommit.cfg | 9 ++ .../transaction_commit/APTCommit.tla | 18 +++ .../transaction_commit/manifest.json | 12 ++ 127 files changed, 2368 insertions(+), 32 deletions(-) create mode 100644 .project create mode 100644 specifications/Chameneos/APChameneos.tla create mode 100644 specifications/CigaretteSmokers/APCigaretteSmokers.cfg create mode 100644 specifications/CigaretteSmokers/APCigaretteSmokers.tla create mode 100644 specifications/CoffeeCan/APCoffeeCan.cfg create mode 100644 specifications/CoffeeCan/APCoffeeCan.tla create mode 100644 specifications/DieHard/APDieHarder.cfg create mode 100644 specifications/DieHard/APDieHarder.tla create mode 100644 specifications/DiningPhilosophers/APDiningPhilosophers.cfg create mode 100644 specifications/DiningPhilosophers/APDiningPhilosophers.tla create mode 100644 specifications/Disruptor/APDisruptor_MPMC.cfg create mode 100644 specifications/Disruptor/APDisruptor_MPMC.tla create mode 100644 specifications/Disruptor/APDisruptor_SPMC.cfg create mode 100644 specifications/Disruptor/APDisruptor_SPMC.tla create mode 100644 specifications/Disruptor/APRingBuffer.tla create mode 100644 specifications/FiniteMonotonic/APCRDT.cfg create mode 100644 specifications/FiniteMonotonic/APCRDT.tla create mode 100644 specifications/FiniteMonotonic/APDistributedReplicatedLog.tla create mode 100644 specifications/FiniteMonotonic/APReplicatedLog.cfg create mode 100644 specifications/FiniteMonotonic/APReplicatedLog.tla create mode 100644 specifications/KeyValueStore/APKeyValueStore.tla create mode 100644 specifications/Majority/APMajority.tla create mode 100644 specifications/MisraReachability/APParReach.cfg create mode 100644 specifications/MisraReachability/APParReach.tla create mode 100644 specifications/MisraReachability/APReachable.tla create mode 100644 specifications/MissionariesAndCannibals/APMissionariesAndCannibals.cfg create mode 100644 specifications/MissionariesAndCannibals/APMissionariesAndCannibals.tla create mode 100644 specifications/Moving_Cat_Puzzle/APCat.cfg create mode 100644 specifications/Moving_Cat_Puzzle/APCat.tla create mode 100644 specifications/Prisoners/APPrisoners.tla create mode 100644 specifications/Prisoners_Single_Switch/APPrisoner.tla create mode 100644 specifications/ReadersWriters/APReadersWriters.cfg create mode 100644 specifications/ReadersWriters/APReadersWriters.tla create mode 100644 specifications/SingleLaneBridge/APSingleLaneBridge.tla create mode 100644 specifications/SpanningTree/APSpanTree.cfg create mode 100644 specifications/SpanningTree/APSpanTree.tla create mode 100644 specifications/SpecifyingSystems/AsynchronousInterface/APAsynchInterface.cfg create mode 100644 specifications/SpecifyingSystems/AsynchronousInterface/APAsynchInterface.tla create mode 100644 specifications/SpecifyingSystems/AsynchronousInterface/APChannel.cfg create mode 100644 specifications/SpecifyingSystems/AsynchronousInterface/APChannel.tla create mode 100644 specifications/SpecifyingSystems/Composing/APChannel.cfg create mode 100644 specifications/SpecifyingSystems/Composing/APChannel.tla create mode 100644 specifications/SpecifyingSystems/Composing/APHourClock.cfg create mode 100644 specifications/SpecifyingSystems/Composing/APHourClock.tla create mode 100644 specifications/SpecifyingSystems/FIFO/APChannel.cfg create mode 100644 specifications/SpecifyingSystems/FIFO/APChannel.tla create mode 100644 specifications/SpecifyingSystems/FIFO/APInnerFIFO.cfg create mode 100644 specifications/SpecifyingSystems/FIFO/APInnerFIFO.tla create mode 100644 specifications/SpecifyingSystems/FIFO/APInnerFIFOInstanced.cfg create mode 100644 specifications/SpecifyingSystems/FIFO/APInnerFIFOInstanced.tla create mode 100644 specifications/SpecifyingSystems/FIFO/APMCInnerFIFO.cfg create mode 100644 specifications/SpecifyingSystems/FIFO/APMCInnerFIFO.tla create mode 100644 specifications/SpecifyingSystems/HourClock/APHourClock.cfg create mode 100644 specifications/SpecifyingSystems/HourClock/APHourClock.tla create mode 100644 specifications/SpecifyingSystems/HourClock/APHourClock2.cfg create mode 100644 specifications/SpecifyingSystems/HourClock/APHourClock2.tla create mode 100644 specifications/SpecifyingSystems/Liveness/APHourClock.cfg create mode 100644 specifications/SpecifyingSystems/Liveness/APHourClock.tla create mode 100644 specifications/SpecifyingSystems/Liveness/APLiveHourClock.cfg create mode 100644 specifications/SpecifyingSystems/Liveness/APLiveHourClock.tla create mode 100644 specifications/acp/APACP_SB.cfg create mode 100644 specifications/acp/APACP_SB.tla create mode 100644 specifications/barriers/APBarrier.cfg create mode 100644 specifications/barriers/APBarrier.tla create mode 100644 specifications/bcastFolklore/APbcastFolklore.cfg create mode 100644 specifications/bcastFolklore/APbcastFolklore.tla create mode 100644 specifications/bosco/APbosco.cfg create mode 100644 specifications/bosco/APbosco.tla create mode 100644 specifications/c1cs/APc1cs.cfg create mode 100644 specifications/c1cs/APc1cs.tla create mode 100644 specifications/cf1s-folklore/APcf1s_folklore.tla create mode 100644 specifications/chang_roberts/APChangRoberts.cfg create mode 100644 specifications/chang_roberts/APChangRoberts.tla create mode 100644 specifications/ewd426/APTokenRing.cfg create mode 100644 specifications/ewd426/APTokenRing.tla create mode 100644 specifications/ewd840/APEWD840.cfg create mode 100644 specifications/ewd840/APEWD840.tla create mode 100644 specifications/ewd840/APSyncTerminationDetection.cfg create mode 100644 specifications/ewd840/APSyncTerminationDetection.tla create mode 100644 specifications/glowingRaccoon/APclean.cfg create mode 100644 specifications/glowingRaccoon/APclean.tla create mode 100644 specifications/glowingRaccoon/APstages.cfg create mode 100644 specifications/glowingRaccoon/APstages.tla create mode 100644 specifications/lamport_mutex/APLamportMutex.cfg create mode 100644 specifications/lamport_mutex/APLamportMutex.tla create mode 100644 specifications/nbacg_guer01/APnbacg_guer01.cfg create mode 100644 specifications/nbacg_guer01/APnbacg_guer01.tla create mode 100644 specifications/spanning/APspanning.cfg create mode 100644 specifications/spanning/APspanning.tla create mode 100644 specifications/tcp/APtcp.cfg create mode 100644 specifications/tcp/APtcp.tla create mode 100644 specifications/transaction_commit/APTCommit.cfg create mode 100644 specifications/transaction_commit/APTCommit.tla diff --git a/.project b/.project new file mode 100644 index 00000000..0abae369 --- /dev/null +++ b/.project @@ -0,0 +1,11 @@ + + + examples + + + + + + + + diff --git a/README.md b/README.md index 2241260d..8b7e1588 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 | | | | ✔ | | +| [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..613d2c88 --- /dev/null +++ b/specifications/Chameneos/APChameneos.tla @@ -0,0 +1,37 @@ +----------------------------- MODULE APChameneos ----------------------------- +(* Apalache type annotations for Chameneos.tla, applied via INSTANCE so the + original spec remains free of tool-specific idiosyncrasies. *) + +EXTENDS Integers + +CONSTANT + \* @type: Int; + N, + \* @type: Int; + M + +VARIABLE + \* @type: Int -> <>; + chameneoses, + \* @type: Int; + meetingPlace, + \* @type: Int; + numMeetings + +\* `Sum` is redefined here solely to attach a type annotation that constrains +\* the operator to `Int`. In TLA+ the original definition works for any value +\* whose `+` is defined (e.g. reals, sequences via concatenation in analogous +\* folds), but Apalache requires a concrete, monomorphic type. +\* +\* Brittle: this trick relies on SANY tolerating a duplicate definition only +\* when the body is identical to the one in `Chameneos`. Any change to the +\* body below turns the warning into a hard "Multiple declarations" error. +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..6253a19c --- /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 remains free of tool-specific idiosyncrasies. *) + +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..5c719f09 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..690b04d7 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..0f8ac5a7 --- /dev/null +++ b/specifications/DiningPhilosophers/APDiningPhilosophers.tla @@ -0,0 +1,22 @@ +---- MODULE APDiningPhilosophers ---- +(* Apalache type annotations for DiningPhilosophers.tla, applied via + INSTANCE so the original spec remains free of tool-specific + idiosyncrasies. *) + +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..6f527a9f --- /dev/null +++ b/specifications/Disruptor/APDisruptor_MPMC.tla @@ -0,0 +1,52 @@ +--------------------------- MODULE APDisruptor_MPMC --------------------------- +(* Apalache type annotations for Disruptor_MPMC.tla, applied via INSTANCE so + the original spec remains free of tool-specific idiosyncrasies. *) + +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 + +\* 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. +\* +\* Brittle: this trick relies on SANY tolerating a duplicate definition only +\* when the body is identical to the one in `Disruptor_MPMC`. Any change to +\* the body below turns the warning into a hard "Multiple declarations" +\* error. +\* @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..d2a2b6ec --- /dev/null +++ b/specifications/Disruptor/APDisruptor_SPMC.tla @@ -0,0 +1,48 @@ +--------------------------- MODULE APDisruptor_SPMC --------------------------- +(* Apalache type annotations for Disruptor_SPMC.tla, applied via INSTANCE so + the original spec remains free of tool-specific idiosyncrasies. *) + +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 + +\* 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. +\* +\* Brittle: this trick relies on SANY tolerating a duplicate definition only +\* when the body is identical to the one in `Disruptor_SPMC`. Any change to +\* the body below turns the warning into a hard "Multiple declarations" +\* error. +\* @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/APRingBuffer.tla b/specifications/Disruptor/APRingBuffer.tla new file mode 100644 index 00000000..f266c22a --- /dev/null +++ b/specifications/Disruptor/APRingBuffer.tla @@ -0,0 +1,34 @@ +----------------------------- MODULE APRingBuffer ---------------------------- +(* Apalache type annotations for RingBuffer.tla, applied via INSTANCE so the + original spec remains free of tool-specific idiosyncrasies. RingBuffer is + also exercised indirectly via APDisruptor_SPMC and APDisruptor_MPMC; this + wrapper checks the helper module on its own. *) + +EXTENDS Integers, FiniteSets + +CONSTANTS + \* @type: Int; + Size, + \* @type: Set(THREAD); + Readers, + \* @type: Set(THREAD); + Writers, + \* @type: Set(Int); + Values, + \* @type: Int; + NULL + +VARIABLE + \* @type: { slots: Int -> Int, readers: Int -> Set(THREAD), writers: Int -> Set(THREAD) }; + ringbuffer + +INSTANCE RingBuffer + +\* The original `RingBuffer` is a helper module that only defines `Init` +\* plus the parameterised actions `Write`, `EndWrite`, `BeginRead`, +\* `EndRead`; it intentionally does not define a `Next`. The concrete +\* protocol (e.g. `Disruptor_SPMC`) is responsible for ensuring that +\* `NoDataRaces` is preserved. There is therefore no `.cfg` for this +\* wrapper -- run `apalache-mc typecheck APRingBuffer.tla` only. + +============================================================================== diff --git a/specifications/Disruptor/manifest.json b/specifications/Disruptor/manifest.json index 8ad8759a..972d934f 100644 --- a/specifications/Disruptor/manifest.json +++ b/specifications/Disruptor/manifest.json @@ -7,6 +7,35 @@ ], "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/APRingBuffer.tla", + "features": [], + "models": [] + }, + { + "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..2531ac1f --- /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 remains free of tool-specific idiosyncrasies. *) + +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..27041be1 --- /dev/null +++ b/specifications/FiniteMonotonic/APDistributedReplicatedLog.tla @@ -0,0 +1,29 @@ +--------------------- MODULE APDistributedReplicatedLog --------------------- +(* Apalache type annotations for DistributedReplicatedLog.tla, applied via + INSTANCE so the original spec remains free of tool-specific + idiosyncrasies. *) + +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..37d4063b --- /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 remains free of tool-specific idiosyncrasies. *) + +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..fa1897eb --- /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 remains free of tool-specific idiosyncrasies. *) + +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..18357b41 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..f65a422c --- /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 remains free of tool-specific idiosyncrasies. *) + +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..1a45bc61 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..81b3add1 --- /dev/null +++ b/specifications/MissionariesAndCannibals/APMissionariesAndCannibals.tla @@ -0,0 +1,26 @@ +--------------- MODULE APMissionariesAndCannibals --------------- +(* Apalache type annotations for MissionariesAndCannibals.tla, applied via + INSTANCE so the original spec remains free of tool-specific + idiosyncrasies. *) + +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..4e1b9804 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..10273703 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..d62519de --- /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 remains free of tool-specific idiosyncrasies. *) + +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..860fc2f3 --- /dev/null +++ b/specifications/ReadersWriters/APReadersWriters.tla @@ -0,0 +1,39 @@ +-------------------------- MODULE APReadersWriters -------------------------- +(* Apalache type annotations for ReadersWriters.tla, applied via INSTANCE so + the original spec remains free of tool-specific idiosyncrasies. *) + +EXTENDS FiniteSets, Naturals, Sequences + +CONSTANT + \* @type: Int; + NumActors + +VARIABLES + \* @type: Set(Int); + readers, + \* @type: Set(Int); + writers, + \* @type: Seq(<>); + waiting + +\* The helpers `ToSet`, `read` and `write` are redefined here solely to attach +\* type annotations that constrain them to the concrete shape used by this +\* spec (sequences of `<>`). In plain TLA+ the original definitions +\* are polymorphic and work for any sequence / tuple where the indexing makes +\* sense, but Apalache requires a concrete, monomorphic type. +\* +\* Brittle: this trick relies on SANY tolerating a duplicate definition only +\* when the body is identical to the one in `ReadersWriters`. Any change to +\* the bodies below turns the warning into a hard "Multiple declarations" +\* error. +\* @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..12300ba0 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..c9b5ab6e --- /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 remains free of tool-specific idiosyncrasies. *) + +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..d391c977 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..78314aff --- /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 remains free of tool-specific idiosyncrasies. *) + +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/Composing/APChannel.cfg b/specifications/SpecifyingSystems/Composing/APChannel.cfg new file mode 100644 index 00000000..18704838 --- /dev/null +++ b/specifications/SpecifyingSystems/Composing/APChannel.cfg @@ -0,0 +1,5 @@ +CONSTANT Data <- DataVal + +INVARIANT TypeInvariant + +SPECIFICATION Spec diff --git a/specifications/SpecifyingSystems/Composing/APChannel.tla b/specifications/SpecifyingSystems/Composing/APChannel.tla new file mode 100644 index 00000000..c2b42528 --- /dev/null +++ b/specifications/SpecifyingSystems/Composing/APChannel.tla @@ -0,0 +1,23 @@ +---------------------- MODULE APChannel ---------------------- +(* Apalache type annotations for Composing/Channel.tla, applied via INSTANCE + so the original spec remains free of tool-specific idiosyncrasies. The + Channel module is duplicated verbatim across the AsynchronousInterface, + Composing, and FIFO chapter directories of the Specifying Systems + repository; each chapter's wrapper instantiates the local copy. *) + +EXTENDS Naturals + +CONSTANT + \* @type: Set(DATUM); + Data + +VARIABLE + \* @type: { val: DATUM, rdy: Int, ack: Int }; + chan + +INSTANCE Channel + +\* Concrete value for the constant used by APChannel.cfg. +DataVal == { "d1_OF_DATUM", "d2_OF_DATUM" } + +================================================================ diff --git a/specifications/SpecifyingSystems/Composing/APHourClock.cfg b/specifications/SpecifyingSystems/Composing/APHourClock.cfg new file mode 100644 index 00000000..280d6243 --- /dev/null +++ b/specifications/SpecifyingSystems/Composing/APHourClock.cfg @@ -0,0 +1,3 @@ +SPECIFICATION HC + +INVARIANT HCini diff --git a/specifications/SpecifyingSystems/Composing/APHourClock.tla b/specifications/SpecifyingSystems/Composing/APHourClock.tla new file mode 100644 index 00000000..6ac4892c --- /dev/null +++ b/specifications/SpecifyingSystems/Composing/APHourClock.tla @@ -0,0 +1,17 @@ +---------------------- MODULE APHourClock ---------------------- +(* Apalache type annotations for Composing/HourClock.tla, applied via + INSTANCE so the original spec remains free of tool-specific + idiosyncrasies. This module is an exact duplicate of + SpecifyingSystems/HourClock/HourClock.tla, kept here so + Specifying-Systems chapter Composing examples can `EXTENDS HourClock` + from a sibling module. *) + +EXTENDS Naturals + +VARIABLE + \* @type: Int; + hr + +INSTANCE HourClock + +================================================================ diff --git a/specifications/SpecifyingSystems/FIFO/APChannel.cfg b/specifications/SpecifyingSystems/FIFO/APChannel.cfg new file mode 100644 index 00000000..18704838 --- /dev/null +++ b/specifications/SpecifyingSystems/FIFO/APChannel.cfg @@ -0,0 +1,5 @@ +CONSTANT Data <- DataVal + +INVARIANT TypeInvariant + +SPECIFICATION Spec diff --git a/specifications/SpecifyingSystems/FIFO/APChannel.tla b/specifications/SpecifyingSystems/FIFO/APChannel.tla new file mode 100644 index 00000000..95b14b3c --- /dev/null +++ b/specifications/SpecifyingSystems/FIFO/APChannel.tla @@ -0,0 +1,23 @@ +---------------------- MODULE APChannel ---------------------- +(* Apalache type annotations for FIFO/Channel.tla, applied via INSTANCE so + the original spec remains free of tool-specific idiosyncrasies. The + Channel module is duplicated verbatim across the AsynchronousInterface, + Composing, and FIFO chapter directories of the Specifying Systems + repository; each chapter's wrapper instantiates the local copy. *) + +EXTENDS Naturals + +CONSTANT + \* @type: Set(DATUM); + Data + +VARIABLE + \* @type: { val: DATUM, rdy: Int, ack: Int }; + chan + +INSTANCE Channel + +\* Concrete value for the constant 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..f7f6b1d5 --- /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 remains free of tool-specific idiosyncrasies. *) + +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/FIFO/APInnerFIFOInstanced.cfg b/specifications/SpecifyingSystems/FIFO/APInnerFIFOInstanced.cfg new file mode 100644 index 00000000..fb804282 --- /dev/null +++ b/specifications/SpecifyingSystems/FIFO/APInnerFIFOInstanced.cfg @@ -0,0 +1,6 @@ +CONSTANT + Message <- MessageVal + +INVARIANT ChannelTypeInvariants + +SPECIFICATION Spec diff --git a/specifications/SpecifyingSystems/FIFO/APInnerFIFOInstanced.tla b/specifications/SpecifyingSystems/FIFO/APInnerFIFOInstanced.tla new file mode 100644 index 00000000..b30c31d9 --- /dev/null +++ b/specifications/SpecifyingSystems/FIFO/APInnerFIFOInstanced.tla @@ -0,0 +1,33 @@ +------------------------ MODULE APInnerFIFOInstanced -------------------------- +(* Apalache type annotations for InnerFIFOInstanced.tla, applied via + INSTANCE so the original spec remains free of tool-specific + idiosyncrasies. InnerFIFOInstanced is a hand-expanded variant of + InnerFIFO that does not use the INSTANCE statement (because older + versions of TLC did not support it). *) + +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 InnerFIFOInstanced + +\* Concrete value for the constant used by APInnerFIFOInstanced.cfg. +MessageVal == { "m1_OF_MSG", "m2_OF_MSG" } + +\* The original `TypeInvariant` includes `q \in Seq(Message)` (an unbounded +\* set Apalache cannot enumerate); replace it with the channel-only checks. +ChannelTypeInvariants == + /\ InChan_TypeInvariant + /\ OutChan_TypeInvariant + +============================================================================== diff --git a/specifications/SpecifyingSystems/FIFO/APMCInnerFIFO.cfg b/specifications/SpecifyingSystems/FIFO/APMCInnerFIFO.cfg new file mode 100644 index 00000000..e8724391 --- /dev/null +++ b/specifications/SpecifyingSystems/FIFO/APMCInnerFIFO.cfg @@ -0,0 +1,7 @@ +CONSTANTS + Message <- MessageVal + qLen = 3 + +INVARIANT ChannelTypeInvariants + +SPECIFICATION Spec diff --git a/specifications/SpecifyingSystems/FIFO/APMCInnerFIFO.tla b/specifications/SpecifyingSystems/FIFO/APMCInnerFIFO.tla new file mode 100644 index 00000000..98623e4c --- /dev/null +++ b/specifications/SpecifyingSystems/FIFO/APMCInnerFIFO.tla @@ -0,0 +1,36 @@ +--------------------------- MODULE APMCInnerFIFO ---------------------------- +(* Apalache type annotations for MCInnerFIFO.tla, applied via INSTANCE so + the original spec remains free of tool-specific idiosyncrasies. + MCInnerFIFO is a TLC-style model wrapper around InnerFIFOInstanced that + adds the bounded-queue constraint `qConstraint == Len(q) <= qLen`. *) + +EXTENDS Naturals, Sequences + +CONSTANTS + \* @type: Set(MSG); + Message, + \* @type: Int; + qLen + +VARIABLES + \* @type: { val: MSG, rdy: Int, ack: Int }; + in, + \* @type: { val: MSG, rdy: Int, ack: Int }; + out, + \* @type: Seq(MSG); + q + +INSTANCE MCInnerFIFO + +\* Concrete value for the constant used by APMCInnerFIFO.cfg. +MessageVal == { "m1_OF_MSG", "m2_OF_MSG", "m3_OF_MSG" } + +\* The original `TypeInvariant` references `Seq(Message)` which Apalache +\* cannot enumerate; replace it with the channel-only checks plus a +\* bounded-length check that mirrors `qConstraint`. +ChannelTypeInvariants == + /\ InChan_TypeInvariant + /\ OutChan_TypeInvariant + /\ Len(q) <= qLen + +============================================================================== 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..6dd463da --- /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 remains free of tool-specific idiosyncrasies. *) + +EXTENDS Naturals + +VARIABLE + \* @type: Int; + hr + +INSTANCE HourClock + +================================================================ diff --git a/specifications/SpecifyingSystems/HourClock/APHourClock2.cfg b/specifications/SpecifyingSystems/HourClock/APHourClock2.cfg new file mode 100644 index 00000000..01eaf286 --- /dev/null +++ b/specifications/SpecifyingSystems/HourClock/APHourClock2.cfg @@ -0,0 +1,3 @@ +SPECIFICATION HC2 + +INVARIANT HCini diff --git a/specifications/SpecifyingSystems/HourClock/APHourClock2.tla b/specifications/SpecifyingSystems/HourClock/APHourClock2.tla new file mode 100644 index 00000000..8c00257a --- /dev/null +++ b/specifications/SpecifyingSystems/HourClock/APHourClock2.tla @@ -0,0 +1,16 @@ +---------------------- MODULE APHourClock2 ---------------------- +(* Apalache type annotations for HourClock2.tla, applied via INSTANCE so the + original spec remains free of tool-specific idiosyncrasies. HourClock2 is + an alternative formulation of HourClock (using `(hr % 12) + 1` instead of + an `IF`-`THEN`-`ELSE`); the two spec formulations are claimed equivalent + (THEOREM HC <=> HC2). *) + +EXTENDS Naturals + +VARIABLE + \* @type: Int; + hr + +INSTANCE HourClock2 + +================================================================ diff --git a/specifications/SpecifyingSystems/Liveness/APHourClock.cfg b/specifications/SpecifyingSystems/Liveness/APHourClock.cfg new file mode 100644 index 00000000..280d6243 --- /dev/null +++ b/specifications/SpecifyingSystems/Liveness/APHourClock.cfg @@ -0,0 +1,3 @@ +SPECIFICATION HC + +INVARIANT HCini diff --git a/specifications/SpecifyingSystems/Liveness/APHourClock.tla b/specifications/SpecifyingSystems/Liveness/APHourClock.tla new file mode 100644 index 00000000..6a507f6f --- /dev/null +++ b/specifications/SpecifyingSystems/Liveness/APHourClock.tla @@ -0,0 +1,17 @@ +---------------------- MODULE APHourClock ---------------------- +(* Apalache type annotations for Liveness/HourClock.tla, applied via + INSTANCE so the original spec remains free of tool-specific + idiosyncrasies. This module is an exact duplicate of + SpecifyingSystems/HourClock/HourClock.tla, kept here so + Specifying-Systems chapter Liveness examples can `EXTENDS HourClock` from + a sibling module. *) + +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..33e1a5ac --- /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 remains free of tool-specific idiosyncrasies. *) + +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..d39248dc 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": [], @@ -171,6 +195,30 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/Composing/APChannel.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/Composing/APChannel.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/Composing/APHourClock.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/Composing/APHourClock.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/SpecifyingSystems/Composing/BinaryHourClock.tla", "features": [], @@ -211,6 +259,54 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/FIFO/APChannel.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/FIFO/APChannel.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "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/APInnerFIFOInstanced.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/FIFO/APInnerFIFOInstanced.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/SpecifyingSystems/FIFO/APMCInnerFIFO.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/FIFO/APMCInnerFIFO.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/SpecifyingSystems/FIFO/Channel.tla", "features": [], @@ -246,6 +342,30 @@ } ] }, + { + "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/APHourClock2.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/HourClock/APHourClock2.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/SpecifyingSystems/HourClock/HourClock.tla", "features": [], @@ -276,6 +396,30 @@ } ] }, + { + "path": "specifications/SpecifyingSystems/Liveness/APHourClock.tla", + "features": [], + "models": [ + { + "path": "specifications/SpecifyingSystems/Liveness/APHourClock.cfg", + "runtime": "00:00:01", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "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/acp/APACP_SB.cfg b/specifications/acp/APACP_SB.cfg new file mode 100644 index 00000000..09966314 --- /dev/null +++ b/specifications/acp/APACP_SB.cfg @@ -0,0 +1,17 @@ +CONSTANTS + participants <- participantsVal + yes = "yes" + no = "no" + undecided = "undecided" + commit = "commit" + abort = "abort" + waiting = "waiting" + notsent = "notsent" + +INVARIANTS + TypeInv + +INIT Init +NEXT progN + +CHECK_DEADLOCK FALSE diff --git a/specifications/acp/APACP_SB.tla b/specifications/acp/APACP_SB.tla new file mode 100644 index 00000000..5a66cb81 --- /dev/null +++ b/specifications/acp/APACP_SB.tla @@ -0,0 +1,38 @@ +------------------------------- MODULE APACP_SB ------------------------------- +(* Apalache type annotations for ACP_SB.tla, applied via INSTANCE so the + original spec remains free of tool-specific idiosyncrasies. The seven + uninterpreted "tag" constants (yes, no, undecided, commit, abort, + waiting, notsent) are typed as Str, and the configuration substitutes + them with concrete strings. The set of participant identifiers is typed + with the uninterpreted type PARTICIPANT. *) + +CONSTANTS + \* @type: Set(PARTICIPANT); + participants, + \* @type: Str; + yes, + \* @type: Str; + no, + \* @type: Str; + undecided, + \* @type: Str; + commit, + \* @type: Str; + abort, + \* @type: Str; + waiting, + \* @type: Str; + notsent + +VARIABLES + \* @type: PARTICIPANT -> { vote: Str, alive: Bool, decision: Str, faulty: Bool, voteSent: Bool }; + participant, + \* @type: { request: PARTICIPANT -> Bool, vote: PARTICIPANT -> Str, broadcast: PARTICIPANT -> Str, decision: Str, alive: Bool, faulty: Bool }; + coordinator + +INSTANCE ACP_SB + +\* Concrete value for the participants constant used by APACP_SB.cfg. +participantsVal == { "p1_OF_PARTICIPANT", "p2_OF_PARTICIPANT", "p3_OF_PARTICIPANT" } + +================================================================================ diff --git a/specifications/acp/manifest.json b/specifications/acp/manifest.json index 1ea1cc42..2fee9f4f 100644 --- a/specifications/acp/manifest.json +++ b/specifications/acp/manifest.json @@ -8,6 +8,18 @@ ], "tags": [], "modules": [ + { + "path": "specifications/acp/APACP_SB.tla", + "features": [], + "models": [ + { + "path": "specifications/acp/APACP_SB.cfg", + "runtime": "00:00:10", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/acp/ACP_NB.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..becead8e --- /dev/null +++ b/specifications/barriers/APBarrier.tla @@ -0,0 +1,22 @@ +------------------------------- MODULE APBarrier ------------------------------- +(* Apalache type annotations for Barrier.tla, applied via INSTANCE so the + original spec remains free of tool-specific idiosyncrasies. 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..c45519c4 --- /dev/null +++ b/specifications/bcastFolklore/APbcastFolklore.tla @@ -0,0 +1,29 @@ +------------------------------ MODULE APbcastFolklore ------------------------------ +(* Apalache type annotations for bcastFolklore.tla, applied via INSTANCE + so the original spec remains free of tool-specific idiosyncrasies. *) + +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..4588b2b2 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..a8df0750 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..73737abb --- /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 remains free of tool-specific idiosyncrasies. *) + +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..486b5183 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..168e0fef --- /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 remains free of tool-specific idiosyncrasies. *) + +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..fc760cef --- /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 remains free of tool-specific idiosyncrasies. *) + +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..512cd862 --- /dev/null +++ b/specifications/ewd840/APSyncTerminationDetection.tla @@ -0,0 +1,20 @@ +--------------------- MODULE APSyncTerminationDetection --------------------- +(* Apalache type annotations for SyncTerminationDetection.tla, applied via + INSTANCE so the original spec remains free of tool-specific + idiosyncrasies. *) + +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..a26cb0e0 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..26b2d80e --- /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 remains free of tool-specific idiosyncrasies. *) + +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..ac6d9e25 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..c1e2342d --- /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 remains free of tool-specific idiosyncrasies. *) + +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..fc0b0f9d --- /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 remains free of tool-specific idiosyncrasies. *) + +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..7bed4c54 --- /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 remains free of tool-specific idiosyncrasies. *) + +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..14b1f5b5 --- /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 remains free of tool-specific idiosyncrasies. *) + +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": [],