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