From 3264cabcf065f75edea0336b2cc737eef3167539 Mon Sep 17 00:00:00 2001 From: Qian-Cheng-nju Date: Tue, 20 Oct 2026 17:09:23 +0000 Subject: [PATCH] Avoid splitting a nonexistent B-tree root parent Signed-off-by: Qian-Cheng-nju --- specifications/btree/btree.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specifications/btree/btree.tla b/specifications/btree/btree.tla index 64c9a761..e862c3f0 100644 --- a/specifications/btree/btree.tla +++ b/specifications/btree/btree.tla @@ -173,7 +173,7 @@ ParentOf(n) == CHOOSE p \in Nodes: \/ \E k \in Keys: n = childOf[p, k] WhichToSplit == LET node == Head(toSplit) parent == ParentOf(node) - splitParent == AtMaxOccupancy(parent) + splitParent == IF node = root THEN FALSE ELSE 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' =