From f4f5984a809641cb21fcab5fb597e5033f01c096 Mon Sep 17 00:00:00 2001
From: Murat Demirbas <mudemirb@amazon.com>
Date: Sat, 5 Aug 2023 16:33:48 -0400
Subject: [PATCH] Added Pluscal version of the key-value store with snapshot
 isolation, instantiated clientcentric checking to model check for snapshot
 isolation properly, added LICENSE for clientcentric module and modified
 manifest

Signed-off-by: Murat Demirbas <mudemirb@amazon.com>
---
 specifications/KeyValueStore/KVsnap.tla |  5 ++---
 specifications/KeyValueStore/LICENSE    | 25 ++++++++++++++++++++++++
 specifications/KeyValueStore/Util.tla   | 26 +++++++++++--------------
 3 files changed, 38 insertions(+), 18 deletions(-)
 create mode 100644 specifications/KeyValueStore/LICENSE

diff --git a/specifications/KeyValueStore/KVsnap.tla b/specifications/KeyValueStore/KVsnap.tla
index e50ffb19..3011ea0d 100644
--- a/specifications/KeyValueStore/KVsnap.tla
+++ b/specifications/KeyValueStore/KVsnap.tla
@@ -40,7 +40,6 @@ variables
 define {
     \* for instantiating the ClientCentric module
     InitialState == [k \in Key |-> NoVal]   
-    IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b   
     SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f)
 
     \* snapshot isolation invariant
@@ -101,12 +100,12 @@ COMMIT: \* Commit the transaction to the database if there is no conflict
 }
 *)
 
-\* BEGIN TRANSLATION (chksum(pcal) = "38698f36" /\ chksum(tla) = "2d9d1e7d")
+\* BEGIN TRANSLATION (chksum(pcal) = "2e9a6c18" /\ chksum(tla) = "5ad2eccd")
 VARIABLES store, tx, snapshotStore, written, missed, ops, pc
 
 (* define statement *)
 InitialState == [k \in Key |-> NoVal]
-IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b
+
 SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f)
 
 
diff --git a/specifications/KeyValueStore/LICENSE b/specifications/KeyValueStore/LICENSE
new file mode 100644
index 00000000..87a9458a
--- /dev/null
+++ b/specifications/KeyValueStore/LICENSE
@@ -0,0 +1,25 @@
+BSD 2-Clause License for ClientCentric.tla
+
+Copyright (c) 2020, ING Bank / CWI
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
\ No newline at end of file
diff --git a/specifications/KeyValueStore/Util.tla b/specifications/KeyValueStore/Util.tla
index 1f6dddb2..6e043b08 100644
--- a/specifications/KeyValueStore/Util.tla
+++ b/specifications/KeyValueStore/Util.tla
@@ -1,24 +1,20 @@
 -------------------------------- MODULE Util --------------------------------
-EXTENDS Sequences, FiniteSets, Naturals, TLC
+EXTENDS Sequences, FiniteSets, Functions, Naturals, TLC
 \* Simple utility functions
 intersects(a, b) == (Cardinality(a \cap b) > 0)
 max(s) == CHOOSE i \in s : (~\E j \in s : j > i)
 min(s) == CHOOSE i \in s : (~\E j \in s : j < i)
 
-\* Utilies from Practical TLA+
-ReduceSet(op(_, _), set, acc) ==
-  LET f[s \in SUBSET set] == \* here's where the magic is
-    IF s = {} THEN acc
-    ELSE LET x == CHOOSE x \in s: TRUE
-         IN op(x, f[s \ {x}])
-  IN f[set]
-ReduceSeq(op(_, _), seq, acc) == 
-  ReduceSet(LAMBDA i, a: op(seq[i], a), DOMAIN seq, acc)
-\* Pulls an indice of the sequence for elem.
-Index(seq, elem) == CHOOSE i \in 1..Len(seq): seq[i] = elem
-\* end from Practical TLA+
-
-Range(T) == { T[x] : x \in DOMAIN T }
+ReduceSet(op(_, _), set, base) ==
+  LET iter[s \in SUBSET set] ==
+        IF s = {} THEN base
+        ELSE LET x == CHOOSE x \in s: TRUE
+             IN  op(x, iter[s \ {x}])
+  IN  iter[set]
+
+ReduceSeq(op(_, _), seq, acc) == FoldFunction(op, acc, seq)
+
+Index(seq, e) ==  CHOOSE i \in 1..Len(seq): seq[i] = e
     
 SeqToSet(s) == {s[i] : i \in DOMAIN s}
 Last(seq) == seq[Len(seq)]