Added Pluscal version of the key-value store with snapshot isolation,…

… instantiated clientcentric checking to model check for snapshot isolation properly, modified manifest Signed-off-by: Murat Demirbas <[email protected]>
tlaplus · Aug 3, 2023 · fbaf36a · fbaf36a
1 parent 245ef9f
commit fbaf36a
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 2 deletions.
diff --git a/manifest.json b/manifest.json
@@ -453,7 +453,8 @@
       "description": "A simple KVS implementing snapshot isolation",
       "source": "",
       "authors": [
-        "Andrew Helwer"
+        "Andrew Helwer",
+        "Murat Demirbas"
       ],
       "tags": [],
       "modules": [
@@ -502,6 +503,32 @@
               "result": "success"
             }
           ]
+        },
+        {
+          "path": "specifications/KeyValueStore/KVsnap.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/KeyValueStore/MCKVsnap.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/KeyValueStore/MCKVsnap.cfg",
+              "runtime": "00:00:50",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "config": [],
+              "features": [
+                "symmetry"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },

diff --git a/specifications/KeyValueStore/README.md b/specifications/KeyValueStore/README.md
@@ -13,4 +13,9 @@ Murat Demirbas wrote a PlusCal version of the key-value store with snapshot isol
 + `MCKVsnap.tla` is the file to use for TLC model checking
 + `MCKVsnap.cfg` is the corresponding config file for model checking (with this config, model checking completes under a minute; it is possible to add another key and model check)
 
-If you uncomment the Serialization invariant in `KVsnap.tla`, and `MCKVsnap.cfg`, you can see a counterexample of how this snapshot-isolation key-value store violates serializability.
+If you uncomment the Serialization invariant in `KVsnap.tla`, and `MCKVsnap.cfg`, you can see a counterexample of how this snapshot-isolation key-value store violates serializability.
+
+## Model checking with VSCode TLA+ plugin
++ Make sure TLA+ plugin is installed in VSCode
++ Open the .cfg file you are interested in checking in VSCode 
++ Get the VSCode panel (Option+X on Mac), and choose "TLA+: Check Model with TLC")