Added B-tree spec to CI validation

Signed-off-by: Andrew Helwer <ahelwer@pm.me>

Author: ahelwer

README.md

@@ -100,6 +100,7 @@ Here is a list of specs included in this repository which are validated by the C
 | [RFC 3506: Voucher Transaction System](specifications/byihive)                                      | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani |          |             |         |     ✔     |          |
 | [Yo-Yo Leader Election](specifications/YoYo)                                                        | Ludovic Yvoz, Stephan Merz                          |          |             |         |      ✔    |          |
 | [TCP as defined in RFC 9293](specifications/tcp)                                                    | Markus Kuppe                                        |          |             |         |      ✔    |          |
+| [B-trees](specifications/btree)                                                                     | Lorin Hochstein                                     |          |             |         |      ✔    |          |
 | [TLA⁺ Level Checking](specifications/LevelChecking)                                                 | Leslie Lamport                                      |          |             |         |           |          |
 | [Condition-Based Consensus](specifications/cbc_max)                                                 | Thanh Hai Tran, Igor Konnov, Josef Widder           |          |             |         |           |          |
 | [Buffered Random Access File](specifications/braf)                                                  | Calvin Loncaric                                     |          |             |         |     ✔     |          |

specifications/btree/README.md

@@ -0,0 +1,2 @@
+TLA⁺ specification of a [B-tree](https://en.wikipedia.org/wiki/B-tree) datastructure by [Lorin Hochstein](https://lorinhochstein.org/), sourced from [this git repo](https://github.com/lorin/btree-tla) and covered at length in [this blog post](https://surfingcomplexity.blog/2024/07/04/modeling-b-trees-in-tla/).
+

specifications/btree/manifest.json

@@ -0,0 +1,51 @@
+{
+  "path": "specifications/btree",
+  "title": "B-trees",
+  "description": "Operations on B-trees. Includes a refinement mapping to a key-value store spec.",
+  "sources": [
+    "https://github.com/lorin/btree-tla",
+    "https://surfingcomplexity.blog/2024/07/04/modeling-b-trees-in-tla/"
+  ],
+  "authors": [
+    "Lorin Hochstein"
+  ],
+  "tags": [],
+  "modules": [
+    {
+      "path": "specifications/btree/btree.tla",
+      "communityDependencies": [],
+      "tlaLanguageVersion": 2,
+      "features": [],
+      "models": [
+        {
+          "path": "specifications/btree/btree.cfg",
+          "runtime": "00:00:15",
+          "size": "small",
+          "mode": "exhaustive search",
+          "result": "success",
+          "distinctStates": 374727,
+          "totalStates": 2820091,
+          "stateDepth": 40
+        }
+      ]
+    },
+    {
+      "path": "specifications/btree/kvstore.tla",
+      "communityDependencies": [],
+      "tlaLanguageVersion": 2,
+      "features": [],
+      "models": [
+        {
+          "path": "specifications/btree/kvstore.cfg",
+          "runtime": "00:00:01",
+          "size": "small",
+          "mode": "exhaustive search",
+          "result": "success",
+          "distinctStates": 2641,
+          "totalStates": 28585,
+          "stateDepth": 11
+        }
+      ]
+    }
+  ]
+}