From fbaf36a7efa56bbaedb7ca9e56ebf9eb167cc7b1 Mon Sep 17 00:00:00 2001
From: Murat Demirbas <mudemirb@amazon.com>
Date: Thu, 3 Aug 2023 18:21:13 -0400
Subject: [PATCH] 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 <mudemirb@amazon.com>
---
 manifest.json                          | 29 +++++++++++++++++++++++++-
 specifications/KeyValueStore/README.md |  7 ++++++-
 2 files changed, 34 insertions(+), 2 deletions(-)

diff --git a/manifest.json b/manifest.json
index d5528b4b..019a4dcc 100644
--- 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
index f0e225bf..f7e03efa 100644
--- 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.
\ No newline at end of file
+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") 
\ No newline at end of file