Publishing three sets of specs:

* Checkpoint Coordination * Least-Circular Substring * Introduction to TLA+ proofs Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Apr 28, 2023 · a398fe3 · a398fe3
1 parent 0a87f52
commit a398fe3
Show file tree

Hide file tree

Showing 20 changed files with 1,616 additions and 1 deletion.
diff --git a/README.md b/README.md
@@ -113,8 +113,11 @@ A central manifest of specs with descriptions and accounts of their various mode
 | 96 | Nano Blockchain Protocol | <a href="specifications/NanoBlockchain">Directory</a> | Andrew Helwer | | &#10004; | Naturals, Bags | | |
 | 97 | Coffee Can White/Black Bean Problem | <a href="specifications/CoffeeCan">Directory</a> | Andrew Helwer | | &#10004; | Naturals | | |
 | 98 | The Slush Protocol | <a href="specifications/SlushProtocol">Directory</a> | Andrew Helwer | | &#10004; | Naturals, FiniteSets, Sequences | &#10004; | |
-| 99 | SDP (Software Defined Perimeter) | <a href="https://github.com/10227694/SDP_Verification">Specifying and Verifying SDP Protocol based Zero Trust Architecture</a> | Luming Dong, Zhi Niu | | &#10004;| FiniteSets, Sequences, Naturals |  |
+| 99 | SDP (Software Defined Perimeter) | <a href="https://github.com/10227694/SDP_Verification">Specifying and Verifying SDP Protocol based Zero Trust Architecture</a> | Luming Dong, Zhi Niu | | &#10004;| FiniteSets, Sequences, Naturals | | |
 | 100 | Simplified Fast Paxos | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/SimplifiedFastPaxos">Simplified version of Fast Paxos (Lamport, 2006)</a> | Lim Ngian Xin Terry, Gaurav Gandhi | |&#10004;| TLC, Naturals, FiniteSets, Integers | | |
+| 101 | Learn TLA⁺ Proofs | <a href="specifications/LearnProofs">Basic PlusCal algorithms and formal proofs of their correctness</a> | Andrew Helwer | &#10004; | &#10004; | Sequences, Naturals, Integers, TLAPS | &#10004; | |
+| 102 | Lexicographically-Least Circular Substring | <a href="specifications/LeastCircularSubstring">Booth's 1980 algorithm to find the lexicographically-least circular substring</a> | Andrew Helwer | | &#10004; | FiniteSets, Integers, Naturals, Sequences | &#10004; | |
+| 103 | Distributed Checkpoint Coordination | <a href="specifications/LeastCircularSubstring">Algorithm for coordinating checkpoint/snapshot leases in a Paxos ring</a> | Andrew Helwer | | &#10004; | FiniteSets, Naturals, Sequences, TLC | | |
 
 ## License
 

diff --git a/manifest.json b/manifest.json
@@ -145,6 +145,57 @@
         }
       ]
     },
+    {
+      "path": "specifications/CheckpointCoordination",
+      "title": "Distributed Checkpoint/Snapshot Coordination",
+      "description": "An algorithm for controlling checkpoint leases in a Paxos ring",
+      "source": "https://github.com/Azure/RingMaster",
+      "authors": [
+        "Andrew Helwer"
+      ],
+      "tags": [],
+      "modules": [
+        {
+          "path": "specifications/CheckpointCoordination/CheckpointCoordination.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/CheckpointCoordination/MCCheckpointCoordination.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/CheckpointCoordination/MCCheckpointCoordination.cfg",
+              "runtime": "00:01:00",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "config": [],
+              "features": [
+                "state constraint",
+                "symmetry"
+              ],
+              "result": "success"
+            },
+            {
+              "path": "specifications/CheckpointCoordination/MCCheckpointCoordinationFailure.cfg",
+              "runtime": "00:00:10",
+              "size": "small",
+              "mode": "exhaustive search",
+              "config": [],
+              "features": [
+                "state constraint",
+                "symmetry"
+              ],
+              "result": "safety failure"
+            }
+          ]
+        }
+      ]
+    },
     {
       "path": "specifications/CigaretteSmokers",
       "title": "The Cigarette Smokers Problem",
@@ -507,6 +558,113 @@
         }
       ]
     },
+    {
+      "path": "specifications/LearnProofs",
+      "title": "Learn TLA⁺ Proofs",
+      "description": "Some specs of very simple algorithms & formal proofs of their correctness",
+      "source": "",
+      "authors": [
+        "Andrew Helwer"
+      ],
+      "tags": [
+        "beginner"
+      ],
+      "modules": [
+        {
+          "path": "specifications/LearnProofs/AddTwo.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [
+            "pluscal",
+            "proof"
+          ],
+          "models": []
+        },
+        {
+          "path": "specifications/LearnProofs/FindHighest.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [
+            "pluscal",
+            "proof"
+          ],
+          "models": []
+        },
+        {
+          "path": "specifications/LearnProofs/MCFindHighest.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/LearnProofs/MCFindHighest.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "config": [],
+              "features": [
+                "state constraint"
+              ],
+              "result": "success"
+            }
+          ]
+        }
+      ]
+    },
+    {
+      "path": "specifications/LeastCircularSubstring",
+      "title": "Lexicographically-Least Circular Substring",
+      "description": "Booth's 1980 algorithm to find the lexicographically-least circular substring",
+      "source": "",
+      "authors": [
+        "Andrew Helwer"
+      ],
+      "tags": [],
+      "modules": [
+        {
+          "path": "specifications/LeastCircularSubstring/LeastCircularSubstring.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [
+            "pluscal"
+          ],
+          "models": []
+        },
+        {
+          "path": "specifications/LeastCircularSubstring/MCLeastCircularSubstring.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/LeastCircularSubstring/MCLeastCircularSubstringMedium.cfg",
+              "runtime": "00:01:00",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "config": [],
+              "features": [],
+              "result": "success"
+            },
+            {
+              "path": "specifications/LeastCircularSubstring/MCLeastCircularSubstringSmall.cfg",
+              "runtime": "00:00:05",
+              "size": "small",
+              "mode": "exhaustive search",
+              "config": [],
+              "features": [],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/LeastCircularSubstring/ZSequences.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        }
+      ]
+    },
     {
       "path": "specifications/LevelChecking",
       "title": "TLA⁺ Level Checking",