Added specs to manifest, added README

Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Nov 22, 2023 · e1e8edf · e1e8edf
1 parent 5ac7778
commit e1e8edf
Show file tree

Hide file tree

Showing 10 changed files with 213 additions and 154 deletions.
diff --git a/README.md b/README.md
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 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
@@ -1,4 +1,5 @@
 ------------------------------- MODULE CRDT ---------------------------------
+
 EXTENDS Naturals
 
 CONSTANT Node

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -1,7 +1,8 @@
-SPECIFICATION SimpleSpec
+SPECIFICATION Spec
 CONSTANTS
   Node = {n1, n2, n3}
   Transaction = {tx1, tx2, tx3}
   Divergence = 5
 INVARIANT TypeOK
 PROPERTY Liveness
+