From 0371572bc0b0787feec3efcb1f1adf94c3a3ac0d Mon Sep 17 00:00:00 2001
From: Lorin Hochstein <lorinh@gmail.com>
Date: Thu, 11 Jul 2024 21:49:48 -0700
Subject: [PATCH 1/5] Add b-tree example

Signed-off-by: Lorin Hochstein <lorinh@gmail.com>
---
 README.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/README.md b/README.md
index b51b420f..ce1a03f9 100644
--- a/README.md
+++ b/README.md
@@ -135,6 +135,7 @@ Ideally these will be moved into this repo over time.
 | [Petri Nets](https://github.com/elh/petri-tlaplus)                                                                                | Instantiable Petri Nets with liveness properties                                                                                          | Eugene Huang                                                               |          |             |     ✔     |         |          |
 | [CRDT](https://github.com/JYwellin/CRDT-TLA)                                                                                      | Specifying and Verifying CRDT Protocols                                                                                                   | Ye Ji, Hengfeng Wei                                                        |          |             |     ✔     |         |          |
 | [Azure Cosmos DB](https://github.com/tlaplus/azure-cosmos-tla)                                                                    | Consistency models provided by Azure Cosmos DB                                                                                            | Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe            |          |             |     ✔     |    ✔    |          |
+| [B-trees](https://github.com/lorin/btree-tla)                                                                                     | Operations on B-trees. Includes a refinement mapping to a key-value store spec.                                                           | Lorin Hochstein                                                            |          |             |     ✔     |         |          |
 
 ## License
 The repository is under the MIT license and you are encouraged to publish your spec under a similarly-permissive license.

From 577de0640a328dec629a3393b63266ed474f89e4 Mon Sep 17 00:00:00 2001
From: Lorin Hochstein <lorinh@gmail.com>
Date: Wed, 17 Jul 2024 21:05:59 -0700
Subject: [PATCH 2/5] btree checkpoint

Signed-off-by: Lorin Hochstein <lorinh@gmail.com>
---
 specifications/btree/README.md   |   0
 specifications/btree/btree.cfg   |  35 ++++
 specifications/btree/btree.tla   | 317 +++++++++++++++++++++++++++++++
 specifications/btree/kvstore.cfg |  20 ++
 specifications/btree/kvstore.tla | 140 ++++++++++++++
 5 files changed, 512 insertions(+)
 create mode 100644 specifications/btree/README.md
 create mode 100644 specifications/btree/btree.cfg
 create mode 100644 specifications/btree/btree.tla
 create mode 100644 specifications/btree/kvstore.cfg
 create mode 100644 specifications/btree/kvstore.tla

diff --git a/specifications/btree/README.md b/specifications/btree/README.md
new file mode 100644
index 00000000..e69de29b
diff --git a/specifications/btree/btree.cfg b/specifications/btree/btree.cfg
new file mode 100644
index 00000000..2187114a
--- /dev/null
+++ b/specifications/btree/btree.cfg
@@ -0,0 +1,35 @@
+SPECIFICATION Spec
+
+CONSTANTS
+    READY = ready
+    GET_VALUE = get_value
+    FIND_LEAF_TO_ADD = find_leaf_to_add
+    WHICH_TO_SPLIT = which_to_split
+
+    ADD_TO_LEAF = add_to_leaf
+    SPLIT_ROOT_LEAF = split_root_leaf
+    SPLIT_ROOT_INNER = split_root_inner
+    SPLIT_INNER = split_inner
+    SPLIT_LEAF = split_leaf
+    UPDATE_LEAF = update_leaf
+
+
+    NIL = nil
+    MISSING = missing
+
+    Vals = {x,y,z}
+
+    MaxOccupancy = 2
+    MaxNode = 8
+    MaxKey = 4
+
+PROPERTY
+\* Refinement
+
+INVARIANT
+TypeOk
+InnersMustHaveLast
+LeavesCantHaveLast
+KeyOrderPreserved
+KeysInLeavesAreUnique
+FreeNodesRemain
diff --git a/specifications/btree/btree.tla b/specifications/btree/btree.tla
new file mode 100644
index 00000000..7efe170e
--- /dev/null
+++ b/specifications/btree/btree.tla
@@ -0,0 +1,317 @@
+\* Note: deletes have not been implemented
+---- MODULE btree ----
+EXTENDS TLC,
+        Naturals,
+        FiniteSets,
+        Sequences
+
+CONSTANTS Vals,
+          MaxKey,
+          MaxNode,
+          MaxOccupancy,
+
+          \* states
+          READY,
+          GET_VALUE,
+          FIND_LEAF_TO_ADD,
+          WHICH_TO_SPLIT,
+          ADD_TO_LEAF,
+          SPLIT_LEAF,
+          SPLIT_INNER,
+          SPLIT_ROOT_LEAF,
+          SPLIT_ROOT_INNER,
+          UPDATE_LEAF
+
+Keys == 1..MaxKey
+Nodes == 1..MaxNode
+
+NIL == CHOOSE x : x \notin Nodes
+MISSING == CHOOSE v : v \notin Vals
+
+
+VARIABLES root,
+          isLeaf, keysOf, childOf, lastOf, valOf,
+          focus,
+          toSplit,
+          op, args, ret,
+          state
+
+TypeOk == /\ root \in Nodes
+          /\ isLeaf \in [Nodes -> BOOLEAN]
+          /\ keysOf \in [Nodes -> SUBSET Keys]
+          /\ childOf \in [Nodes \X Keys -> Nodes \union {NIL}]
+          /\ lastOf \in [Nodes -> Nodes \union {NIL}]
+          /\ valOf \in [Nodes \X Keys -> Vals \union {NIL}]
+          /\ focus \in Nodes \union {NIL}
+          /\ toSplit \in Seq(Nodes)
+          /\ op \in {"get", "insert", "update", NIL}
+          /\ ret \in Vals \union {"ok", "error", MISSING, NIL}
+          /\ state \in {READY, GET_VALUE, FIND_LEAF_TO_ADD, WHICH_TO_SPLIT, ADD_TO_LEAF, SPLIT_LEAF, SPLIT_INNER, SPLIT_ROOT_LEAF, SPLIT_ROOT_INNER, UPDATE_LEAF}
+
+\* Max element in a set
+Max(xs) == CHOOSE x \in xs : (\A y \in xs \ {x} : x > y)
+
+\* Find the appropriate child node associated with the key
+ChildNodeFor(node, key) ==
+    LET keys == keysOf[node]
+        maxKey == Max(keys)
+        closestKey ==  CHOOSE k \in keys : /\ k>key
+                                           /\ ~(\E j \in keys \ {k} : j>key /\ j<k)
+    IN IF keys = {} \/ key >= maxKey
+       THEN lastOf[node]
+       \* smallest k that's bigger than key
+       ELSE
+       childOf[node, closestKey]
+
+
+\* Identify the leaf node based on key
+\* Find the leaf node associated with a key
+RECURSIVE FindLeafNode(_, _)
+FindLeafNode(node, key) ==
+    IF isLeaf[node] THEN node ELSE FindLeafNode(ChildNodeFor(node, key), key)
+
+AtMaxOccupancy(node) == Cardinality(keysOf[node]) = MaxOccupancy
+
+
+\* We model a "free" (not yet part of the tree) node as one as a leaf with no keys
+IsFree(node) == isLeaf[node] /\ keysOf[node] = {}
+
+ChooseFreeNode == CHOOSE n \in Nodes : IsFree(n)
+
+
+Init == /\ isLeaf = [n \in Nodes |-> TRUE]
+        /\ keysOf = [n \in Nodes |-> {}]
+        /\ childOf = [n \in Nodes, k \in Keys |-> NIL]
+        /\ lastOf = [n \in Nodes |-> NIL]
+        /\ valOf = [n \in Nodes, k \in Keys |-> NIL]
+        /\ root = ChooseFreeNode
+        /\ focus = NIL
+        /\ toSplit = <<>>
+        /\ op = NIL
+        /\ args = NIL
+        /\ ret = NIL
+        /\ state = READY
+
+GetReq(key) == 
+    /\ state = READY
+    /\ op' = "get"
+    /\ args' = <<key>>
+    /\ ret' = NIL
+    /\ state' = GET_VALUE
+    /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit>>
+
+GetValue ==
+    LET key == args[1] 
+        node == FindLeafNode(root, key) IN
+    /\ state = GET_VALUE
+    /\ state' = READY
+    /\ ret' = IF key \in keysOf[node] THEN valOf[node, key] ELSE MISSING
+    /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit, args, op>>
+    
+
+InsertReq(key, val) ==
+    /\ state = READY
+    /\ op' = "insert"
+    /\ args' = <<key, val>>
+    /\ ret' = NIL
+    /\ state' = FIND_LEAF_TO_ADD
+    /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit>>
+
+UpdateReq(key, val) ==
+    LET leaf == FindLeafNode(root, key)
+    IN /\ state = READY
+       /\ op' = "update"
+       /\ args' = <<key, val>>
+       /\ ret' = NIL
+       /\ focus' = leaf
+       /\ state' = UPDATE_LEAF
+       /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, toSplit>>
+
+UpdateLeaf ==
+    LET key == args[1]
+        val == args[2]
+    IN /\ state = UPDATE_LEAF
+       /\ valOf' = IF key \in keysOf[focus] THEN [valOf EXCEPT ![focus, key]=val] ELSE valOf
+       /\ ret' = IF key \in keysOf[focus] THEN "ok" ELSE "error"
+       /\ state' = READY
+       /\ focus' = NIL
+       /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, toSplit, args, op>>
+
+FindLeafToAdd ==
+    LET key == args[1]
+        leaf == FindLeafNode(root, key)
+    IN /\ state = FIND_LEAF_TO_ADD
+       /\ focus' = leaf
+       /\ toSplit' = IF AtMaxOccupancy(leaf) THEN <<leaf>> ELSE <<>>
+       /\ state' = IF AtMaxOccupancy(leaf) THEN WHICH_TO_SPLIT ELSE ADD_TO_LEAF
+       /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, args, op, ret>>
+
+
+ParentOf(n) == CHOOSE p \in Nodes: \/ \E k \in Keys: n = childOf[p, k]
+                                   \/ lastOf[p]=n
+
+WhichToSplit ==
+    LET  node == Head(toSplit)
+         parent == ParentOf(node)
+         splitParent == AtMaxOccupancy(parent)
+         noMoreSplits == ~splitParent  \* if the parent doesn't need splitting, we don't need to consider more nodes for splitting
+    IN /\ state = WHICH_TO_SPLIT
+       /\ toSplit' =
+           CASE node = root   -> toSplit
+             [] splitParent   -> <<parent>> \o toSplit
+             [] OTHER         -> toSplit
+       /\ state' =
+            CASE node # root /\ noMoreSplits /\ isLeaf[node]  -> SPLIT_LEAF
+              [] node # root /\ noMoreSplits /\ ~isLeaf[node] -> SPLIT_INNER
+              [] node = root /\ isLeaf[node]                  -> SPLIT_ROOT_LEAF
+              [] node = root /\ ~isLeaf[node]                 -> SPLIT_ROOT_INNER
+              [] OTHER                                        -> WHICH_TO_SPLIT
+       /\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, op, args, ret, focus>>
+
+\* Adding the <<key, val>> pair in args to the node indicated by focus
+\* If the key is already present, this is an error
+AddToLeaf ==
+    LET key == args[1]
+        val == args[2] IN
+       /\ state = ADD_TO_LEAF
+       /\ ret' = IF key \notin keysOf[focus] THEN "ok" ELSE "error"
+       /\ keysOf' = IF key \notin keysOf[focus] THEN [keysOf EXCEPT ![focus]=@ \union {key}] ELSE keysOf
+       /\ valOf' = IF key \notin keysOf[focus] THEN [valOf EXCEPT ![focus,key]=val] ELSE valOf
+       /\ state' = READY
+       /\ UNCHANGED <<root, isLeaf, childOf, lastOf, op, args, focus, toSplit>>
+
+\* Return the pivot (midpoint) of a set of keys. If there are an even number of keys, bias towards the smaller one
+PivotOf(keys) == CHOOSE k \in keys :
+    LET smaller == {x \in keys : x < k}
+        larger == {x \in keys: x > k} IN
+     \/ Cardinality(smaller) = Cardinality(larger)
+     \/ Cardinality(smaller) = Cardinality(larger)+1
+
+SplitRootLeaf ==
+    LET n1 == Head(toSplit)
+        n2 == ChooseFreeNode
+        newRoot == CHOOSE n \in Nodes : IsFree(n) /\ (n # n2)
+        keys == keysOf[n1]
+        pivot == PivotOf(keys)
+        n1Keys == {x \in keys: x<pivot}
+        n2Keys == {x \in keys: x>=pivot} 
+        keyToInsert == args[1] IN
+    /\ state = SPLIT_ROOT_LEAF
+    /\ root' = newRoot
+    /\ isLeaf' = [isLeaf EXCEPT ![newRoot]=FALSE, ![n2]=TRUE]
+    /\ keysOf' = [keysOf EXCEPT ![newRoot]={pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
+    /\ childOf' = [childOf EXCEPT ![newRoot, pivot]=n1]
+    /\ lastOf' = [lastOf EXCEPT ![newRoot]=n2]
+    /\ valOf' = [n \in Nodes, k \in Keys |->
+        CASE n=n1 /\ k \in n2Keys -> NIL
+          [] n=n2 /\ k \in n2Keys -> valOf[n1, k]
+          [] OTHER                -> valOf[n, k]]
+    \* No more splits necessary, add the focus to the leaf
+    \* Note that the focus may have changed due to the split
+    /\ state' = ADD_TO_LEAF
+    /\ focus' = IF keyToInsert < pivot THEN n1 ELSE n2
+    /\ UNCHANGED <<op, args, ret, toSplit>>
+
+ParentKeyOf(node) ==
+    LET p == ParentOf(node) IN
+    CHOOSE k \in keysOf[p]: childOf[p, k] = node
+
+IsLastOfParent(node) == lastOf[ParentOf(node)] = node
+
+SplitRootInner ==
+    LET n1 == Head(toSplit)
+        n2 == ChooseFreeNode
+        newRoot == CHOOSE n \in Nodes : IsFree(n) /\ (n # n2)
+        keys == keysOf[n1]
+        pivot == PivotOf(keys)
+        (* when splitting an inner node, pivot does not appear in either node, only in parent *)
+        n1Keys == {x \in keys: x<pivot}
+        n2Keys == {x \in keys: x>pivot} IN
+    /\ state = SPLIT_ROOT_INNER
+    /\ root' = newRoot
+    /\ isLeaf' = [isLeaf EXCEPT ![newRoot]=FALSE, ![n2]=FALSE]
+    /\ keysOf' = [keysOf EXCEPT ![newRoot]={pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
+    /\ childOf' = [n \in Nodes, k \in Keys |->
+        CASE n=newRoot /\ k=pivot -> n1
+          [] n=n1 /\ k \in n2Keys -> NIL
+          [] n=n1 /\ k \in n1Keys -> childOf[n1, k]
+          [] n=n2 /\ k \in n2Keys -> childOf[n1, k]
+          [] OTHER                -> childOf[n, k]]
+    /\ lastOf' = [lastOf EXCEPT ![newRoot]=n2, ![n1]=childOf[n1, pivot], ![n2]=lastOf[n1]]
+    /\ toSplit' = <<>>
+    /\ state' = ADD_TO_LEAF
+    /\ UNCHANGED <<op, args, ret, focus, valOf>>
+
+SplitLeaf ==
+    LET n1 == Head(toSplit)
+        n2 == ChooseFreeNode
+        keys == keysOf[n1]
+        pivot == PivotOf(keys)
+        parent == ParentOf(n1)
+        n1Keys == {x \in keys: x<pivot}
+        n2Keys == {x \in keys: x>=pivot}
+        keyToInsert == args[1]
+    IN
+    /\ state = SPLIT_LEAF
+    /\ isLeaf' = [isLeaf EXCEPT ![n2]=TRUE]
+    /\ keysOf' = [keysOf EXCEPT ![parent]=@ \union {pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
+    \* In the parent, point the pivot key to n1, and point the parent key to n2.
+    \* TODO: handle the edge case where n1 was the last element
+    /\ childOf' = IF IsLastOfParent(n1)
+                  THEN [childOf EXCEPT ![parent, pivot]=n1]
+                  ELSE [childOf EXCEPT ![parent, pivot]=n1, ![parent, ParentKeyOf(n1)]=n2]
+    /\ lastOf' = IF IsLastOfParent(n1) THEN [lastOf EXCEPT ![parent]=n2] ELSE lastOf
+    /\ valOf' = [n \in Nodes, k \in Keys |->
+        CASE n=n1 /\ k \in n2Keys -> NIL
+          [] n=n2 /\ k \in n2Keys -> valOf[n1, k]
+          [] OTHER                -> valOf[n, k]]
+    /\ state' = ADD_TO_LEAF
+    /\ focus' = IF keyToInsert < pivot THEN n1 ELSE n2
+    /\ UNCHANGED <<root, toSplit, op, args, ret>>
+
+
+Next == \/ \E key \in Keys, val \in Vals : 
+            \/ InsertReq(key, val)
+            \/ UpdateReq(key, val)
+        \/ \E key \in Keys: GetReq(key)
+        \/ GetValue
+        \/ FindLeafToAdd
+        \/ WhichToSplit
+        \/ AddToLeaf
+        \/ SplitLeaf
+        \/ SplitRootLeaf
+        \/ SplitRootInner
+        \/ UpdateLeaf
+
+vars == <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit, op, args, ret, state>>
+
+Spec == Init /\ [][Next]_vars /\ WF_op(\E key \in Keys: GetReq(key))
+
+\*
+\* Refinement mapping
+\*
+
+Leaves == {n \in Nodes : isLeaf[n]}
+
+Mapping == INSTANCE kvstore
+    WITH dict <- [key \in Keys |-> IF \E leaf \in Leaves : key \in keysOf[leaf] 
+                                 THEN LET leaf == CHOOSE leaf \in Leaves : key \in keysOf[leaf] 
+                                      IN valOf[leaf, key] ELSE MISSING],
+         state <- IF state = READY THEN "ready" ELSE "working"
+
+
+Refinement == Mapping!Spec
+
+\*
+\* Invariants
+\*
+Inners == {n \in Nodes: ~isLeaf[n]}
+
+InnersMustHaveLast == \A n \in Inners : lastOf[n] # NIL
+KeyOrderPreserved == \A n \in Inners : (\A k \in keysOf[n] : (\A kc \in keysOf[childOf[n, k]]: kc < k))
+LeavesCantHaveLast == \A n \in Leaves : lastOf[n] = NIL
+KeysInLeavesAreUnique ==
+    \A n1, n2 \in Leaves : ((keysOf[n1] \intersect keysOf[n2]) # {}) => n1=n2
+FreeNodesRemain == \E n \in Nodes : IsFree(n)
+
+====
\ No newline at end of file
diff --git a/specifications/btree/kvstore.cfg b/specifications/btree/kvstore.cfg
new file mode 100644
index 00000000..b2a7eaa0
--- /dev/null
+++ b/specifications/btree/kvstore.cfg
@@ -0,0 +1,20 @@
+SPECIFICATION Spec
+\* Uncomment the previous line and provide the specification name if it's declared
+\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.
+
+CONSTANTS
+    Keys = {"A", "B", "C"}
+    Vals = {X, Y, Z}
+    NIL = NIL
+    MISSING = "missing"
+
+\* INIT Init
+\* NEXT Next
+
+\* PROPERTY
+
+\* Uncomment the previous line and add property names
+
+
+INVARIANT
+TypeOK
\ No newline at end of file
diff --git a/specifications/btree/kvstore.tla b/specifications/btree/kvstore.tla
new file mode 100644
index 00000000..8f21cc9e
--- /dev/null
+++ b/specifications/btree/kvstore.tla
@@ -0,0 +1,140 @@
+(*
+
+# Operations
+
+* get
+* insert
+* update
+* delete
+
+## get
+Return NIL if the key is not in the store
+
+## insert
+Return "ok" on success
+Return "error" if the key already exists
+
+## update
+Return "ok" on success
+Return "error" if the key does not exist
+
+## delete
+
+Always returns "ok"
+
+*)
+---- MODULE kvstore ----
+CONSTANTS Keys, Vals, MISSING, NIL
+
+Ops == {"get", "insert", "delete", "update"}
+
+ASSUME MISSING \notin Vals
+ASSUME NIL \notin Vals \union Ops \union {MISSING}
+
+VARIABLES op,
+    args,
+    ret,
+    state,
+    dict \* tracks mapping of keys to values
+
+TypeOK ==
+    /\ args \in {<<k>>: k \in Keys} \union {<<k,v>>: k \in Keys, v \in Vals} \union {NIL}
+    /\ dict \in [Keys -> Vals \union {MISSING}]
+    /\ op \in Ops \union {NIL} \* initial state for Ops is NIL
+    /\ ret \in Vals \union {"ok", "error", MISSING, NIL}
+    /\ state \in {"ready", "working"}
+
+Init ==
+    /\ op = NIL
+    /\ args = NIL
+    /\ ret = NIL
+    /\ dict = [k \in Keys |-> MISSING]
+    /\ state = "ready"
+
+GetReq(key) ==
+    /\ state = "ready"
+    /\ op' = "get"
+    /\ args' = <<key>>
+    /\ ret' = NIL
+    /\ state' = "working"
+    /\ UNCHANGED dict
+
+GetResp == LET key == args[1] IN
+    /\ op = "get"
+    /\ ret' = dict[key]
+    /\ state' = "ready"
+    /\ UNCHANGED <<op, args, dict>>
+
+InsertReq(key, val) ==
+    /\ state = "ready"
+    /\ op' = "insert"
+    /\ args' = <<key, val>>
+    /\ ret' = NIL
+    /\ state' = "working"
+    /\ UNCHANGED <<dict>>
+
+Present(key) == dict[key] \in Vals
+Absent(key) == dict[key] = MISSING
+
+InsertResp == LET key == args[1]
+                  val == args[2] IN
+       /\ op = "insert"
+       /\ state = "working"
+       /\ dict' = IF Absent(key)
+                  THEN [dict EXCEPT ![key] = val]
+                  ELSE dict
+       /\ ret' = IF Absent(key) THEN "ok" ELSE "error"
+       /\ state' = "ready"
+       /\ UNCHANGED <<op, args>>
+
+UpdateReq(key, val) ==
+    /\ state = "ready"
+    /\ op' = "update"
+    /\ args' = <<key, val>>
+    /\ ret' = NIL
+    /\ state' = "working"
+    /\ UNCHANGED dict
+
+UpdateResp ==
+    LET key == args[1]
+        val == args[2]
+    IN /\ op = "update"
+       /\ ret' = IF Present(key) THEN "ok" ELSE "error"
+       /\ dict' = IF Present(key)
+                  THEN [dict EXCEPT ![key]=val]
+                  ELSE dict
+       /\ state' = "ready"
+       /\ UNCHANGED <<op, args>>
+
+DeleteReq(key) ==
+    /\ state = "ready"
+    /\ op' = "delete"
+    /\ args' = <<key>>
+    /\ ret' = NIL
+    /\ state' = "working"
+    /\ UNCHANGED dict
+
+\* we permit deleting keys that aren't there
+DeleteResp ==
+    LET key == args[1]
+    IN /\ op = "delete"
+       /\ ret' = "ok"
+       /\ state' = "ready"
+       /\ dict' = [dict EXCEPT ![key]=MISSING]
+       /\ UNCHANGED <<op, args>>
+
+Next == \/ \E k \in Keys: 
+           \/ GetReq(k)
+           \/ DeleteReq(k)
+           \/ \E v \in Vals: \/ InsertReq(k, v)  
+                             \/ UpdateReq(k, v)
+        \/ GetResp
+        \/ InsertResp
+        \/ UpdateResp
+        \/ DeleteResp
+
+vars == <<op, args, ret, dict, state>>
+
+Spec == Init /\ [][Next]_vars /\ WF_op(\E k \in Keys: DeleteReq(k))
+
+====
\ No newline at end of file

From f93ef5440ec99d91a535e7713b014264e1a3b3be Mon Sep 17 00:00:00 2001
From: Lorin Hochstein <lorinh@gmail.com>
Date: Thu, 17 Oct 2024 18:23:28 -0700
Subject: [PATCH 3/5] Update manifest.json

Signed-off-by: Lorin Hochstein <lorinh@gmail.com>
---
 manifest.json | 451 ++++++++++++++++++++++++++++----------------------
 1 file changed, 255 insertions(+), 196 deletions(-)

diff --git a/manifest.json b/manifest.json
index 6be32189..8e3d1656 100644
--- a/manifest.json
+++ b/manifest.json
@@ -1317,6 +1317,16 @@
           "tlaLanguageVersion": 2,
           "features": [],
           "models": [
+            {
+              "path": "specifications/MultiPaxos-SMR/MultiPaxos_MC.cfg",
+              "runtime": "00:07:53",
+              "size": "large",
+              "mode": "exhaustive search",
+              "features": [
+                "symmetry"
+              ],
+              "result": "success"
+            },
             {
               "path": "specifications/MultiPaxos-SMR/MultiPaxos_MC_small.cfg",
               "runtime": "00:00:10",
@@ -1329,16 +1339,6 @@
               "distinctStates": 343796,
               "totalStates": 736012,
               "stateDepth": 28
-            },
-            {
-              "path": "specifications/MultiPaxos-SMR/MultiPaxos_MC.cfg",
-              "runtime": "00:07:53",
-              "size": "large",
-              "mode": "exhaustive search",
-              "features": [
-                "symmetry"
-              ],
-              "result": "success"
             }
           ]
         }
@@ -2688,14 +2688,14 @@
           "models": []
         },
         {
-          "path": "specifications/SpecifyingSystems/RealTime/RealTime_SS.tla",
+          "path": "specifications/SpecifyingSystems/RealTime/RealTimeHourClock.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
           "models": []
         },
         {
-          "path": "specifications/SpecifyingSystems/RealTime/RealTimeHourClock.tla",
+          "path": "specifications/SpecifyingSystems/RealTime/RealTime_SS.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
@@ -3084,6 +3084,106 @@
         }
       ]
     },
+    {
+      "path": "specifications/YoYo",
+      "title": "Yo-Yo Leader Election",
+      "description": "Algorithm due to Nicola Santoro for leader election in a connected undirected network",
+      "sources": [
+        "https://research.nicola-santoro.com/DADA.html"
+      ],
+      "authors": [
+        "Ludovic Yvoz",
+        "Stephan Merz"
+      ],
+      "tags": [],
+      "modules": [
+        {
+          "path": "specifications/YoYo/MCYoYoNoPruning.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/YoYo/MCYoYoNoPruning.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success",
+              "distinctStates": 60,
+              "totalStates": 110,
+              "stateDepth": 19
+            }
+          ]
+        },
+        {
+          "path": "specifications/YoYo/MCYoYoPruning.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/YoYo/MCYoYoPruning.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success",
+              "distinctStates": 102,
+              "totalStates": 157,
+              "stateDepth": 31
+            }
+          ]
+        },
+        {
+          "path": "specifications/YoYo/YoYoAllGraphs.tla",
+          "communityDependencies": [
+            "UndirectedGraphs"
+          ],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/YoYo/YoYoAllGraphs.cfg",
+              "runtime": "00:00:02",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success",
+              "distinctStates": 26731,
+              "totalStates": 48535,
+              "stateDepth": 39
+            }
+          ]
+        },
+        {
+          "path": "specifications/YoYo/YoYoNoPruning.tla",
+          "communityDependencies": [
+            "UndirectedGraphs"
+          ],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/YoYo/YoYoPruning.tla",
+          "communityDependencies": [
+            "UndirectedGraphs"
+          ],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        }
+      ]
+    },
     {
       "path": "specifications/aba-asyn-byz",
       "title": "Asynchronous Byzantine Consensus",
@@ -3420,8 +3520,12 @@
       "path": "specifications/braf",
       "title": "Buffered Random Access File",
       "description": "Specification of a Java file caching layer",
-      "sources": ["https://github.com/tlaplus/tlaplus/tree/4613109641676389d97b8df209d6cf4d90d31c1c/tlatools/org.lamport.tlatools/src/tlc2/util/BufferedRandomAccessFile.tla"],
-      "authors": ["Calvin Loncaric"],
+      "sources": [
+        "https://github.com/tlaplus/tlaplus/tree/4613109641676389d97b8df209d6cf4d90d31c1c/tlatools/org.lamport.tlatools/src/tlc2/util/BufferedRandomAccessFile.tla"
+      ],
+      "authors": [
+        "Calvin Loncaric"
+      ],
       "tags": [],
       "modules": [
         {
@@ -3437,8 +3541,8 @@
               "mode": "exhaustive search",
               "features": [
                 "alias",
-                "symmetry",
-                "liveness"
+                "liveness",
+                "symmetry"
               ],
               "result": "success",
               "distinctStates": 3316,
@@ -3449,6 +3553,49 @@
         }
       ]
     },
+    {
+      "path": "specifications/btree",
+      "title": "btree",
+      "description": "B-tree",
+      "sources": ["https://surfingcomplexity.blog/2024/07/04/modeling-b-trees-in-tla/"],
+      "authors": ["Lorin Hochstein"],
+      "tags": ["beginner"],
+      "modules": [
+        {
+          "path": "specifications/btree/btree.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/btree/btree.cfg",
+              "runtime": "00:00:39",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [
+              ],
+              "result": "success"
+            }
+          ]
+        },
+        {
+          "path": "specifications/btree/kvstore.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/btree/kvstore.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
+        }
+      ]
+    },
     {
       "path": "specifications/byihive",
       "title": "RFC 3506: Voucher Transaction System",
@@ -4364,28 +4511,6 @@
             }
           ]
         },
-        {
-          "path": "specifications/ewd998/EWD998PCal.tla",
-          "communityDependencies": [
-            "BagsExt"
-          ],
-          "tlaLanguageVersion": 2,
-          "features": ["pluscal"],
-          "models": [
-            {
-              "path": "specifications/ewd998/EWD998PCal.cfg",
-              "runtime": "00:00:21",
-              "size": "medium",
-              "mode": "exhaustive search",
-              "features": [
-                "state constraint",
-                "liveness",
-                "alias"
-              ],
-              "result": "success"
-            }
-          ]
-        },
         {
           "path": "specifications/ewd998/EWD998Chan.tla",
           "communityDependencies": [],
@@ -4469,6 +4594,28 @@
             }
           ]
         },
+        {
+          "path": "specifications/ewd998/EWD998ChanTrace.tla",
+          "communityDependencies": [
+            "IOUtils",
+            "VectorClocks"
+          ],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/ewd998/EWD998ChanTrace.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "alias",
+                "view"
+              ],
+              "result": "success"
+            }
+          ]
+        },
         {
           "path": "specifications/ewd998/EWD998Chan_opts.tla",
           "communityDependencies": [
@@ -4479,6 +4626,30 @@
           "features": [],
           "models": []
         },
+        {
+          "path": "specifications/ewd998/EWD998PCal.tla",
+          "communityDependencies": [
+            "BagsExt"
+          ],
+          "tlaLanguageVersion": 2,
+          "features": [
+            "pluscal"
+          ],
+          "models": [
+            {
+              "path": "specifications/ewd998/EWD998PCal.cfg",
+              "runtime": "00:00:21",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [
+                "alias",
+                "liveness",
+                "state constraint"
+              ],
+              "result": "success"
+            }
+          ]
+        },
         {
           "path": "specifications/ewd998/EWD998_anim.tla",
           "communityDependencies": [
@@ -4582,22 +4753,6 @@
           "tlaLanguageVersion": 2,
           "features": [],
           "models": []
-        },
-        {
-          "path": "specifications/ewd998/EWD998ChanTrace.tla",
-          "communityDependencies": ["VectorClocks", "IOUtils"],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": [
-            {
-              "path": "specifications/ewd998/EWD998ChanTrace.cfg",
-              "runtime": "00:00:01",
-              "size": "small",
-              "mode": "exhaustive search",
-              "features": ["alias", "view"],
-              "result": "success"
-            }
-          ]
         }
       ]
     },
@@ -4920,6 +5075,51 @@
         }
       ]
     },
+    {
+      "path": "specifications/tcp",
+      "title": "TCP as defined in RFC 9293",
+      "description": "Transmission Control Protocol (TCP)",
+      "sources": [
+        "https://datatracker.ietf.org/doc/html/rfc9293"
+      ],
+      "authors": [
+        "Markus Kuppe"
+      ],
+      "tags": [],
+      "modules": [
+        {
+          "path": "specifications/tcp/MCtcp.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/tcp/MCtcp.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness",
+                "state constraint"
+              ],
+              "result": "success",
+              "distinctStates": 1182,
+              "totalStates": 6322,
+              "stateDepth": 14
+            }
+          ]
+        },
+        {
+          "path": "specifications/tcp/tcp.tla",
+          "communityDependencies": [
+            "SequencesExt"
+          ],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        }
+      ]
+    },
     {
       "path": "specifications/tower_of_hanoi",
       "title": "The Tower of Hanoi Puzzle",
@@ -5080,147 +5280,6 @@
           ]
         }
       ]
-    },
-    {
-      "path": "specifications/YoYo",
-      "title": "Yo-Yo Leader Election",
-      "description": "Algorithm due to Nicola Santoro for leader election in a connected undirected network",
-      "sources": ["https://research.nicola-santoro.com/DADA.html"],
-      "authors": [
-        "Ludovic Yvoz",
-        "Stephan Merz"
-      ],
-      "tags": [],
-      "modules": [
-        {
-          "path": "specifications/YoYo/YoYoNoPruning.tla",
-          "communityDependencies": [
-            "UndirectedGraphs"
-          ],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/YoYo/MCYoYoNoPruning.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": [
-            {
-              "path": "specifications/YoYo/MCYoYoNoPruning.cfg",
-              "runtime": "00:00:01",
-              "size": "small",
-              "mode": "exhaustive search",
-              "features": [
-                "liveness"
-              ],
-              "result": "success",
-              "distinctStates": 60,
-              "totalStates": 110,
-              "stateDepth": 19
-            }
-          ]
-        },
-        {
-          "path": "specifications/YoYo/YoYoPruning.tla",
-          "communityDependencies": [
-            "UndirectedGraphs"
-          ],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/YoYo/MCYoYoPruning.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": [
-            {
-              "path": "specifications/YoYo/MCYoYoPruning.cfg",
-              "runtime": "00:00:01",
-              "size": "small",
-              "mode": "exhaustive search",
-              "features": [
-                "ignore deadlock",
-                "liveness"
-              ],
-              "result": "success",
-              "distinctStates": 102,
-              "totalStates": 157,
-              "stateDepth": 31
-            }
-          ]
-        },
-        {
-          "path": "specifications/YoYo/YoYoAllGraphs.tla",
-          "communityDependencies": [
-            "UndirectedGraphs"
-          ],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": [
-            {
-              "path": "specifications/YoYo/YoYoAllGraphs.cfg",
-              "runtime": "00:00:02",
-              "size": "medium",
-              "mode": "exhaustive search",
-              "features": [
-                "ignore deadlock",
-                "liveness"
-              ],
-              "result": "success",
-              "distinctStates": 26731,
-              "totalStates": 48535,
-              "stateDepth": 39
-            }
-          ]
-        }
-      ]
-    },
-    {
-      "path": "specifications/tcp",
-      "title": "TCP as defined in RFC 9293",
-      "description": "Transmission Control Protocol (TCP)",
-      "sources": ["https://datatracker.ietf.org/doc/html/rfc9293"],
-      "authors": [
-        "Markus Kuppe"
-      ],
-      "tags": [],
-      "modules": [
-        {
-          "path": "specifications/tcp/tcp.tla",
-          "communityDependencies": [
-            "SequencesExt"
-          ],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": []
-        },
-        {
-          "path": "specifications/tcp/MCtcp.tla",
-          "communityDependencies": [],
-          "tlaLanguageVersion": 2,
-          "features": [],
-          "models": [
-            {
-              "path": "specifications/tcp/MCtcp.cfg",
-              "runtime": "00:00:01",
-              "size": "small",
-              "mode": "exhaustive search",
-              "features": [
-                "state constraint",
-                "liveness"
-              ],
-              "result": "success",
-              "distinctStates": 1182,
-              "totalStates": 6322,
-              "stateDepth": 14
-            }
-          ]
-        }
-      ]
     }
   ]
-}
+}
\ No newline at end of file

From d898f8ab80a3b94c0b9c5e6303482369cced05e2 Mon Sep 17 00:00:00 2001
From: Lorin Hochstein <lorinh@gmail.com>
Date: Thu, 17 Oct 2024 19:43:19 -0700
Subject: [PATCH 4/5] Comment out PROPERTY so it doesn't expect liveness

Signed-off-by: Lorin Hochstein <lorinh@gmail.com>
---
 specifications/btree/btree.cfg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specifications/btree/btree.cfg b/specifications/btree/btree.cfg
index 2187114a..25036df5 100644
--- a/specifications/btree/btree.cfg
+++ b/specifications/btree/btree.cfg
@@ -23,7 +23,7 @@ CONSTANTS
     MaxNode = 8
     MaxKey = 4
 
-PROPERTY
+\* PROPERTY
 \* Refinement
 
 INVARIANT

From 9d61ab651aa08dc3839731bdac393f1c6add2740 Mon Sep 17 00:00:00 2001
From: Lorin Hochstein <lorinh@gmail.com>
Date: Fri, 18 Oct 2024 22:52:41 -0700
Subject: [PATCH 5/5] Update manifest title so it matches table

Signed-off-by: Lorin Hochstein <lorinh@gmail.com>
---
 manifest.json | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/manifest.json b/manifest.json
index 8e3d1656..308dd3d9 100644
--- a/manifest.json
+++ b/manifest.json
@@ -3555,8 +3555,8 @@
     },
     {
       "path": "specifications/btree",
-      "title": "btree",
-      "description": "B-tree",
+      "title": "B-trees",
+      "description": "Operations on B-trees",
       "sources": ["https://surfingcomplexity.blog/2024/07/04/modeling-b-trees-in-tla/"],
       "authors": ["Lorin Hochstein"],
       "tags": ["beginner"],
