Finitizing monotonic systems (#97)

* Added basic monotonic specs * Specs from blog post * Constrained model * Added divergence based model * CRDT spec finished * Wrote simple replicated log model * Experiment with different GC methods * Added specs to manifest, added README * Minor change to re-run CI * Added blog post * Renamed MC specs * Changed tag to intermediate Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Dec 1, 2023 · 2369052 · 2369052
1 parent 68aec27
commit 2369052
Show file tree

Hide file tree

Showing 13 changed files with 903 additions and 90 deletions.
diff --git a/README.md b/README.md
diff --git a/manifest-schema.json b/manifest-schema.json
@@ -20,7 +20,7 @@
           },
           "tags": {
             "type": "array",
-            "items": {"enum": ["beginner"]}
+            "items": {"enum": ["beginner", "intermediate"]}
           },
           "modules": {
             "type": "array",

diff --git a/manifest.json b/manifest.json
@@ -389,6 +389,92 @@
         }
       ]
     },
+    {
+      "path": "specifications/FiniteMonotonic",
+      "title": "Finite Model-Checking of Monotonic Systems",
+      "description": "Illustration of technique for making ordinarily-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": [
+        "intermediate"
+      ],
+      "modules": [
+        {
+          "path": "specifications/FiniteMonotonic/CRDT.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/FiniteMonotonic/Finitize_CRDT.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/FiniteMonotonic/Finitize_CRDT.cfg",
+              "runtime": "00:00:05",
+              "size": "small",
+              "mode": "exhaustive search",
+              "config": [],
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/FiniteMonotonic/Constrain_CRDT.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/FiniteMonotonic/Constrain_CRDT.cfg",
+              "runtime": "00:00:05",
+              "size": "small",
+              "mode": "exhaustive search",
+              "config": [],
+              "features": [
+                "liveness",
+                "state constraint"
+              ],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/FiniteMonotonic/Finitize_ReplicatedLog.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/FiniteMonotonic/Finitize_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": []
-        }
-      ]
     }
   ]
 }