diff --git a/README.md b/README.md index 1ced8949..069f7fd1 100644 --- a/README.md +++ b/README.md @@ -13,17 +13,17 @@ A central manifest of specs with descriptions and accounts of their various mode ## List of Examples -| # | Name | Description | Authors | TLAPS Proof? | TLC Model? | Module Dependencies | PlusCal? | Apalache? | -|:-:|------|-------------|---------|:------------:|:----------:|---------------------|:--------:|:---------:| -| 1 | 2PCwithBTM | A modified version of P2TCommit (Gray & Lamport, 2006) | Murat Demirbas | | ✔ | FinSet, Int, Seq | ✔ | | -| 2 | 802.16 | IEEE 802.16 WiMAX Protocols | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou | | ✔ | Int, Seq, FinSet | | | -| 3 | aba-asyn-byz | Asynchronous Byzantine agreement (Bracha & Toueg, 1985) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat | | | -| 4 | acp-nb | Non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | | -| 5 | acp-nb-wrong | Wrong version of the non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | | -| 6 | acp-sb | Non-blocking atomic commitment with a simple broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | | -| 7 | allocator | Specification of a resource allocator | Stephan Merz | | ✔ | FinSet | | | -| 8 | async-comm | The diversity of asynchronous communication (Chevrou et al., 2016) | Florent Chevrou, Aurélie Hurault, Philippe Quéinnec | | ✔ | Nat | | | -| 9 | bcastByz | Asynchronous reliable broadcast - Figure 7 (Srikanth & Toeug, 1987) | Thanh Hai Tran, Igor Konnov, Josef Widder | ✔ | ✔ | Nat, FinSet | | | +| # | Name | Description | Authors | TLAPS Proof? | TLC Model? | Module Dependencies | PlusCal? | Apalache? | +|:---:|-----------------------------------|-------------|---------|:------------:|:----------:|---------------------|:--------:|:---------:| +| 1 | 2PCwithBTM | A modified version of P2TCommit (Gray & Lamport, 2006) | Murat Demirbas | | ✔ | FinSet, Int, Seq | ✔ | | +| 2 | 802.16 | IEEE 802.16 WiMAX Protocols | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou | | ✔ | Int, Seq, FinSet | | | +| 3 | aba-asyn-byz | Asynchronous Byzantine agreement (Bracha & Toueg, 1985) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat | | | +| 4 | acp-nb | Non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | | +| 5 | acp-nb-wrong | Wrong version of the non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | | +| 6 | acp-sb | Non-blocking atomic commitment with a simple broadcast (Babaoğlu & Toueg, 1993) | Stephan Merz | | ✔ | default theories | | | +| 7 | allocator | Specification of a resource allocator | Stephan Merz | | ✔ | FinSet | | | +| 8 | async-comm | The diversity of asynchronous communication (Chevrou et al., 2016) | Florent Chevrou, Aurélie Hurault, Philippe Quéinnec | | ✔ | Nat | | | +| 9 | bcastByz | Asynchronous reliable broadcast - Figure 7 (Srikanth & Toeug, 1987) | Thanh Hai Tran, Igor Konnov, Josef Widder | ✔ | ✔ | Nat, FinSet | | | | 10 | bcastFolklore | Folklore reliable broadcast - Figure 4 (Chandra and Toueg, 1996) | Thanh Hai Tran, Igor Konnov, Josef Widder | ✔ | ✔ | Nat | | | | 11 | bosco | One-Step Byzantine asynchronous consensus (Song & Renesse, 2008) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | Nat, FinSet | | | | 12 | Boulangerie | A variant of the bakery algorithm (Yoram & Patkin, 2015) | Leslie Lamport, Stephan Merz | ✔ | ✔ | Int | ✔ | | @@ -101,24 +101,25 @@ A central manifest of specs with descriptions and accounts of their various mode | 84 | EWD687a | Detecting termination in distributed computations by Edsger Dijkstra and Carel Scholten | Stephan Merz (PlusCal spec), Leslie Lamport & Markus Kuppe (TLA+ spec) | | ✔ | Integers, Graphs | ✔ | | | 85 | Huang | Termination detection by using distributed snapshots by Shing-Tsaan Huang | Markus Kuppe | | ✔ | DyadicRationals | | | | 86 | Azure Cosmos DB | Consistency models provided by Azure Cosmos DB | Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe | | ✔ | Integers, Sequences, FiniteSets, Functions, SequencesExt | ✔ | | -| 87 | MET for CRDT-Redis | Model-check the CRDT designs, then generate test cases to test CRDT implementations | Yuqi Zhang | | ✔ | Integers, Sequences, FiniteSets, TLC | ✔ | | -| 88 | Parallel increment | Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry | Chris Jensen | | ✔ | Integers, FiniteSets, TLC | | | -| 89 | The Streamlet consensus algorithm | Specification and model-checking of both safety and liveness properties of Streamlet with TLC | Giuliano Losa | | ✔ | Sequences, Integers, FiniteSets | ✔ | | -| 90 | Petri Nets | Instantiable Petri Nets with liveness properties | Eugene Huang | | ✔ | Integers, Sequences, FiniteSets, TLC | | | -| 91 | Knuth Yao & Markov Chains | Knuth-Yao algorithm for simulating a sixsided die | Ron Pressler, Markus Kuppe | | ✔ | DyadicRationals | | | -| 92 | ewd426 - Token Stabilization | Self-stabilizing systems in spite of distributed control | Murat Demirbas, Markus Kuppe | | ✔ | Naturals, FiniteSets | | | -| 93 | CRDT | Specifying and Verifying CRDT Protocols | Ye Ji, Hengfeng Wei | | ✔| Naturals, FiniteSets | | -| 94 | Multi-Car Elevator System | Directory | Andrew Helwer | | ✔ | Integers | | | -| 95 | Snapshot Key-Value Store | Directory | Andrew Helwer | | ✔ | | | | -| 96 | Nano Blockchain Protocol | Directory | Andrew Helwer | | ✔ | Naturals, Bags | | | -| 97 | Coffee Can White/Black Bean Problem | Directory | Andrew Helwer | | ✔ | Naturals | | | -| 98 | The Slush Protocol | Directory | Andrew Helwer | | ✔ | Naturals, FiniteSets, Sequences | ✔ | | -| 99 | SDP (Software Defined Perimeter) | Specifying and Verifying SDP Protocol based Zero Trust Architecture | Luming Dong, Zhi Niu | | ✔| FiniteSets, Sequences, Naturals | | | -| 100 | Simplified Fast Paxos | Simplified version of Fast Paxos (Lamport, 2006) | Lim Ngian Xin Terry, Gaurav Gandhi | |✔| TLC, Naturals, FiniteSets, Integers | | | -| 101 | Learn TLA⁺ Proofs | Basic PlusCal algorithms and formal proofs of their correctness | Andrew Helwer | ✔ | ✔ | Sequences, Naturals, Integers, TLAPS | ✔ | | -| 102 | Lexicographically-Least Circular Substring | Booth's 1980 algorithm to find the lexicographically-least circular substring | Andrew Helwer | | ✔ | FiniteSets, Integers, Naturals, Sequences | ✔ | | -| 103 | Distributed Checkpoint Coordination | Algorithm for coordinating checkpoint/snapshot leases in a Paxos ring | Andrew Helwer | | ✔ | FiniteSets, Naturals, Sequences, TLC | | | -| 104 | Boyer-Moore Majority Vote | Efficient algorithm for finding a majority value | Stephan Merz | ✔ | ✔ | Integers, Sequences, FiniteSets, TLAPS | | | +| 87 | MET for CRDT-Redis | Model-check the CRDT designs, then generate test cases to test CRDT implementations | Yuqi Zhang | | ✔ | Integers, Sequences, FiniteSets, TLC | ✔ | | +| 88 | Parallel increment | Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry | Chris Jensen | | ✔ | Integers, FiniteSets, TLC | | | +| 89 | The Streamlet consensus algorithm | Specification and model-checking of both safety and liveness properties of Streamlet with TLC | Giuliano Losa | | ✔ | Sequences, Integers, FiniteSets | ✔ | | +| 90 | Petri Nets | Instantiable Petri Nets with liveness properties | Eugene Huang | | ✔ | Integers, Sequences, FiniteSets, TLC | | | +| 91 | Knuth Yao & Markov Chains | Knuth-Yao algorithm for simulating a sixsided die | Ron Pressler, Markus Kuppe | | ✔ | DyadicRationals | | | +| 92 | ewd426 - Token Stabilization | Self-stabilizing systems in spite of distributed control | Murat Demirbas, Markus Kuppe | | ✔ | Naturals, FiniteSets | | | +| 93 | CRDT | Specifying and Verifying CRDT Protocols | Ye Ji, Hengfeng Wei | | ✔| Naturals, FiniteSets | | +| 94 | Multi-Car Elevator System | Directory | Andrew Helwer | | ✔ | Integers | | | +| 95 | Snapshot Key-Value Store | Directory | Andrew Helwer | | ✔ | | | | +| 96 | Nano Blockchain Protocol | Directory | Andrew Helwer | | ✔ | Naturals, Bags | | | +| 97 | The Coffee Can Bean Problem | Directory | Andrew Helwer | | ✔ | Naturals | | | +| 98 | The Slush Protocol | Directory | Andrew Helwer | | ✔ | Naturals, FiniteSets, Sequences | ✔ | | +| 99 | SDP (Software Defined Perimeter) | Specifying and Verifying SDP Protocol based Zero Trust Architecture | Luming Dong, Zhi Niu | | ✔| FiniteSets, Sequences, Naturals | | | +| 100 | Simplified Fast Paxos | Simplified version of Fast Paxos (Lamport, 2006) | Lim Ngian Xin Terry, Gaurav Gandhi | |✔| TLC, Naturals, FiniteSets, Integers | | | +| 101 | Learn TLA⁺ Proofs | Basic PlusCal algorithms and formal proofs of their correctness | Andrew Helwer | ✔ | ✔ | Sequences, Naturals, Integers, TLAPS | ✔ | | +| 102 | Minimal Circular Substring | Booth's 1980 algorithm to find the lexicographically-least circular substring | Andrew Helwer | | ✔ | FiniteSets, Integers, Naturals, Sequences | ✔ | | +| 103 | Checkpoint Coordination | Algorithm for coordinating checkpoint/snapshot leases in a Paxos ring | Andrew Helwer | | ✔ | FiniteSets, Naturals, Sequences, TLC | | | +| 104 | Boyer-Moore Majority Vote | Efficient algorithm for finding a majority value | Stephan Merz | ✔ | ✔ | Integers, Sequences, FiniteSets, TLAPS | | | +| 105 | Finitizing Monotonic Systems | A technique for making infinite-state monotonic systems finite | Andrew Helwer | | ✔ | Naturals, Sequences | | | ## License diff --git a/manifest.json b/manifest.json index fade6579..acecddab 100644 --- a/manifest.json +++ b/manifest.json @@ -389,6 +389,92 @@ } ] }, + { + "path": "specifications/FiniteMonotonic", + "title": "Finite Model-Checking of Monotonic Systems", + "description": "Illustration of a technique for making infinite monotonic systems finite for the purposes of model-checking.", + "source": "https://ahelwer.ca/post/2023-11-01-tla-finite-monotonic/", + "authors": [ + "Andrew Helwer" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/FiniteMonotonic/CRDT.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/FiniteMonotonic/MC_CRDT.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/FiniteMonotonic/MC_CRDT.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/FiniteMonotonic/MC_Constraint_CRDT.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/FiniteMonotonic/MC_Constraint_CRDT.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness", + "state constraint" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/FiniteMonotonic/MC_ReplicatedLog.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/FiniteMonotonic/MC_ReplicatedLog.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [], + "features": [ + "liveness" + ], + "result": "success" + } + ] + }, + { + "path": "specifications/FiniteMonotonic/ReplicatedLog.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } + ] + }, { "path": "specifications/GameOfLife", "title": "Conway's Game of Life", @@ -458,6 +544,22 @@ ], "tags": [], "modules": [ + { + "path": "specifications/KeyValueStore/ClientCentric.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/KeyValueStore/KVsnap.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "pluscal" + ], + "models": [] + }, { "path": "specifications/KeyValueStore/KeyValueStore.tla", "communityDependencies": [], @@ -504,13 +606,6 @@ } ] }, - { - "path": "specifications/KeyValueStore/KVsnap.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": ["pluscal"], - "models": [] - }, { "path": "specifications/KeyValueStore/MCKVsnap.tla", "communityDependencies": [], @@ -539,13 +634,6 @@ "tlaLanguageVersion": 2, "features": [], "models": [] - }, - { - "path": "specifications/KeyValueStore/ClientCentric.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], - "models": [] } ] }, @@ -770,6 +858,55 @@ } ] }, + { + "path": "specifications/Majority", + "title": "Boyer-Moore majority vote algorithm", + "description": "An efficient algorithm for detecting a majority value in a sequence", + "source": "", + "authors": [ + "Stephan Merz" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/Majority/MCMajority.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/Majority/MCMajority.cfg", + "runtime": "00:00:05", + "size": "small", + "mode": "exhaustive search", + "config": [ + "ignore deadlock" + ], + "features": [], + "result": "success" + } + ] + }, + { + "path": "specifications/Majority/Majority.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/Majority/MajorityProof.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [ + "proof" + ], + "models": [] + } + ] + }, { "path": "specifications/MisraReachability", "title": "Misra Reachability Algorithm", @@ -3252,7 +3389,7 @@ "config": [ "ignore deadlock" ], - "features": [ + "features": [ "liveness", "state constraint", "view" @@ -3698,51 +3835,6 @@ "models": [] } ] - }, - { - "path": "specifications/Majority", - "title": "Boyer-Moore majority vote algorithm", - "description": "An efficient algorithm for detecting a majority value in a sequence", - "source": "", - "authors": [ - "Stephan Merz" - ], - "tags": ["beginner"], - "modules": [ - { - "path": "specifications/Majority/Majority.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], - "models": [] - }, - { - "path": "specifications/Majority/MCMajority.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], - "models": [ - { - "path": "specifications/Majority/MCMajority.cfg", - "runtime": "00:00:05", - "size": "small", - "mode": "exhaustive search", - "config": ["ignore deadlock"], - "features": [], - "result": "success" - } - ] - }, - { - "path": "specifications/Majority/MajorityProof.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [ - "proof" - ], - "models": [] - } - ] } ] } diff --git a/specifications/FiniteMonotonic/CRDT.tla b/specifications/FiniteMonotonic/CRDT.tla index 9f617be0..5ddf74e5 100644 --- a/specifications/FiniteMonotonic/CRDT.tla +++ b/specifications/FiniteMonotonic/CRDT.tla @@ -1,4 +1,5 @@ ------------------------------- MODULE CRDT --------------------------------- + EXTENDS Naturals CONSTANT Node diff --git a/specifications/FiniteMonotonic/MC_CRDT.cfg b/specifications/FiniteMonotonic/MC_CRDT.cfg index 381a262b..43e5af04 100644 --- a/specifications/FiniteMonotonic/MC_CRDT.cfg +++ b/specifications/FiniteMonotonic/MC_CRDT.cfg @@ -4,3 +4,4 @@ CONSTANTS Divergence = 3 INVARIANTS TypeOK Safety PROPERTIES Liveness Monotonicity + diff --git a/specifications/FiniteMonotonic/MC_CRDT.tla b/specifications/FiniteMonotonic/MC_CRDT.tla index 02de1edd..6ef77f2e 100644 --- a/specifications/FiniteMonotonic/MC_CRDT.tla +++ b/specifications/FiniteMonotonic/MC_CRDT.tla @@ -1,4 +1,5 @@ ------------------------------- MODULE MC_CRDT ------------------------------ + EXTENDS Naturals CONSTANTS Node, Divergence diff --git a/specifications/FiniteMonotonic/MC_Constraint_CRDT.cfg b/specifications/FiniteMonotonic/MC_Constraint_CRDT.cfg index 866913ee..82ca291e 100644 --- a/specifications/FiniteMonotonic/MC_Constraint_CRDT.cfg +++ b/specifications/FiniteMonotonic/MC_Constraint_CRDT.cfg @@ -3,3 +3,4 @@ CONSTANT Node = {n1, n2, n3} INVARIANTS TypeOK Safety PROPERTIES Monotonicity Liveness CONSTRAINT StateConstraint + diff --git a/specifications/FiniteMonotonic/MC_Constraint_CRDT.tla b/specifications/FiniteMonotonic/MC_Constraint_CRDT.tla index f162a6f0..89b98c9c 100644 --- a/specifications/FiniteMonotonic/MC_Constraint_CRDT.tla +++ b/specifications/FiniteMonotonic/MC_Constraint_CRDT.tla @@ -1,4 +1,5 @@ ------------------------- MODULE MC_Constraint_CRDT ------------------------- + EXTENDS Naturals CONSTANT Node diff --git a/specifications/FiniteMonotonic/MC_ReplicatedLog.cfg b/specifications/FiniteMonotonic/MC_ReplicatedLog.cfg index 10d58a92..027b7109 100644 --- a/specifications/FiniteMonotonic/MC_ReplicatedLog.cfg +++ b/specifications/FiniteMonotonic/MC_ReplicatedLog.cfg @@ -1,7 +1,8 @@ -SPECIFICATION SimpleSpec +SPECIFICATION Spec CONSTANTS Node = {n1, n2, n3} Transaction = {tx1, tx2, tx3} Divergence = 5 INVARIANT TypeOK PROPERTY Liveness + diff --git a/specifications/FiniteMonotonic/MC_ReplicatedLog.tla b/specifications/FiniteMonotonic/MC_ReplicatedLog.tla index 817b4af2..8c39e492 100644 --- a/specifications/FiniteMonotonic/MC_ReplicatedLog.tla +++ b/specifications/FiniteMonotonic/MC_ReplicatedLog.tla @@ -1,4 +1,5 @@ -------------------------- MODULE MC_ReplicatedLog -------------------------- + EXTENDS Naturals, Sequences CONSTANTS Node, Transaction, Divergence @@ -20,46 +21,13 @@ Init == /\ S!Init /\ converge = FALSE -\* Experiment with combining the write & garbage collect steps -GCWriteTx(n, tx) == - LET SetMin(s) == CHOOSE e \in s : \A o \in s : e <= o IN - LET MinExecuted == SetMin({executed[o] : o \in Node}) IN - LET NewTxId == Len(log) - MinExecuted + 1 IN - /\ ~converge - /\ executed[n] = Len(log) - /\ NewTxId <= Divergence - /\ log' = [ - i \in 1 .. NewTxId |-> - IF i < NewTxId THEN log[i + MinExecuted] ELSE tx - ] - /\ executed' = [ - o \in Node |-> - IF o = n THEN NewTxId ELSE executed[o] - MinExecuted - ] - /\ UNCHANGED converge - -\* Experiment with combining the execute & garbage collect steps -GCExecuteTx(n) == - LET SetMin(s) == CHOOSE e \in s : \A o \in s : e <= o IN - LET MinExecuted == SetMin({ - IF o = n THEN executed[o] + 1 ELSE executed[o] : o \in Node - }) IN - /\ log' = [i \in 1 .. Len(log) - MinExecuted |-> log[i + MinExecuted]] - /\ executed' = [ - o \in Node |-> - IF o = n - THEN executed[o] - MinExecuted + 1 - ELSE executed[o] - MinExecuted - ] - /\ UNCHANGED converge - -SimpleWriteTx(n, tx) == +WriteTx(n, tx) == /\ ~converge /\ Len(log) < Divergence /\ S!WriteTx(n, tx) /\ UNCHANGED converge -SimpleExecuteTx(n) == +ExecuteTx(n) == /\ S!ExecuteTx(n) /\ UNCHANGED converge @@ -74,40 +42,18 @@ Converge == /\ converge' = TRUE /\ UNCHANGED <> -GCWriteNext == - \/ \E n \in Node : \E tx \in Transaction : GCWriteTx(n, tx) - \/ \E n \in Node : SimpleExecuteTx(n) - \/ Converge - -SimpleFairness == \A n \in Node : WF_vars(SimpleExecuteTx(n)) - -GCWriteSpec == - /\ Init - /\ [][GCWriteNext]_vars - /\ SimpleFairness - -GCExecuteNext == - \/ \E n \in Node : \E tx \in Transaction : GCWriteTx(n, tx) - \/ \E n \in Node : SimpleExecuteTx(n) - \/ Converge - -GCFairness == \A n \in Node : WF_vars(GCExecuteTx(n)) - -GCExecuteSpec == - /\ Init - /\ [][GCExecuteNext]_vars - /\ GCFairness +Fairness == \A n \in Node : WF_vars(ExecuteTx(n)) -SimpleNext == - \/ \E n \in Node : \E tx \in Transaction : SimpleWriteTx(n, tx) - \/ \E n \in Node : SimpleExecuteTx(n) +Next == + \/ \E n \in Node : \E tx \in Transaction : WriteTx(n, tx) + \/ \E n \in Node : ExecuteTx(n) \/ GarbageCollect \/ Converge -SimpleSpec == +Spec == /\ Init - /\ [][SimpleNext]_vars - /\ SimpleFairness + /\ [][Next]_vars + /\ Fairness ============================================================================= diff --git a/specifications/FiniteMonotonic/README.md b/specifications/FiniteMonotonic/README.md new file mode 100644 index 00000000..b445fe4f --- /dev/null +++ b/specifications/FiniteMonotonic/README.md @@ -0,0 +1,14 @@ +These specifications illustrate a technique for taking ordinarily-infinite monotonic systems and turning them finite for the purposes of model-checking. +Briefly, this is accomplished by limiting the maximum divergence (difference between lowest and highest value) of any monotonic variable across the system, then continually transposing the set of monotonic variables to their lowest value. +The technique is explained at length in [this](https://ahelwer.ca/post/2023-11-01-tla-finite-monotonic/) blog post. + +Specs & models include: +- `CRDT.tla`: the "good copy" spec of a basic grow-only counter CRDT +- `MC_CRDT.tla`: wraps `CRDT.tla` and implements the finitization technique +- `MC_CRDT.cfg`: a model for `MC_CRDT.tla` +- `MC_Constraint_CRDT.tla`: finitizes `CRDT.tla` using state constraints instead; included for comparison +- `MC_Constraint_CRDT.cfg`: a model for `MC_Constraint_CRDT.tla` +- `ReplicatedLog.tla`: the "good copy" spec of a basic append-only replicated log +- `MC_ReplicatedLog.tla`: wraps `ReplicatedLog.tla` and implements the finitization technique +- `MC_ReplicatedLog.cfg`: a model for `MC_ReplicatedLog.tla` +