From cc8f57f42bb2fd8691823dc864c3e5b983087179 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 21 Aug 2026 09:42:03 -0700 Subject: [PATCH 1/2] btree: state the assumptions on MaxKey, MaxNode and MaxOccupancy The three constants were declared without any ASSUME, and they are not the same kind of constraint. MaxOccupancy is the branching factor, so the tree itself requires it: below 2, PivotOf leaves one side of every split empty, the emptied leaf is still reachable from its parent, and IsFree reports it as free for ChooseFreeNode to hand out a second time. At MaxOccupancy = 1 that corrupts the tree and KeyOrderPreserved fails in 24 steps. MaxNode must likewise cover the root that Init allocates, or the CHOOSE in ChooseFreeNode has nothing to pick and TLC dies while computing initial states. MaxKey is different. The algorithm bounds neither the key domain nor the node pool; both bounds exist so Keys, Nodes and the domains of childOf and valOf stay finite for TLC, which is also what FreeNodesRemain really checks. An empty key domain leaves the tree well formed but enables no request action, so TLC reports a deadlock on Init rather than a defect. The comments group the assumptions accordingly. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- specifications/btree/btree.tla | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/specifications/btree/btree.tla b/specifications/btree/btree.tla index 7efe170e..8d5a10ee 100644 --- a/specifications/btree/btree.tla +++ b/specifications/btree/btree.tla @@ -22,6 +22,29 @@ CONSTANTS Vals, SPLIT_ROOT_INNER, UPDATE_LEAF +\* +\* Assumptions the algorithm imposes +\* + +\* MaxOccupancy is the branching factor. Below 2, PivotOf leaves one side of +\* every split empty, and IsFree reports the emptied in-tree leaf as free for +\* ChooseFreeNode to hand out a second time. +ASSUME MaxOccupancyPermitsSplitting == MaxOccupancy \in Nat /\ MaxOccupancy >= 2 + +\* Even the empty tree is a root node, which Init takes from the free nodes. +ASSUME NodePoolIsNonEmpty == MaxNode \in Nat \ {0} + +\* +\* Assumptions only model checking imposes +\* +\* The algorithm bounds neither the key domain nor the node pool. MaxKey and +\* MaxNode exist to keep Keys, Nodes and the domains of childOf and valOf +\* finite, which is also why exhausting the pool is reported by FreeNodesRemain, +\* as a model too small rather than a defect in the tree. + +\* With no key, no request action is ever enabled and TLC deadlocks on Init. +ASSUME KeyDomainIsNonEmpty == MaxKey \in Nat \ {0} + Keys == 1..MaxKey Nodes == 1..MaxNode From c89d45b06962ce5aa02f44f210c274db2adadd9c Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 21 Aug 2026 10:42:26 -0700 Subject: [PATCH 2/2] Factor the TLC concerns out of btree into MCbtree Keeping the datastructure and the definitions that exist only to make model checking finite in one module left no way to tell which was which. btree.tla is now the algorithm alone, MCbtree.tla the model. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- .../btree/{btree.cfg => MCbtree.cfg} | 6 ++++ specifications/btree/MCbtree.tla | 27 +++++++++++++++ specifications/btree/btree.tla | 33 +++++++------------ specifications/btree/manifest.json | 9 +++-- 4 files changed, 52 insertions(+), 23 deletions(-) rename specifications/btree/{btree.cfg => MCbtree.cfg} (90%) create mode 100644 specifications/btree/MCbtree.tla diff --git a/specifications/btree/btree.cfg b/specifications/btree/MCbtree.cfg similarity index 90% rename from specifications/btree/btree.cfg rename to specifications/btree/MCbtree.cfg index 25036df5..be7dbb22 100644 --- a/specifications/btree/btree.cfg +++ b/specifications/btree/MCbtree.cfg @@ -20,9 +20,15 @@ CONSTANTS Vals = {x,y,z} MaxOccupancy = 2 + +CONSTANTS MaxNode = 8 MaxKey = 4 +CONSTANTS + Keys <- MCKeys + Nodes <- MCNodes + \* PROPERTY \* Refinement diff --git a/specifications/btree/MCbtree.tla b/specifications/btree/MCbtree.tla new file mode 100644 index 00000000..d9f31ef8 --- /dev/null +++ b/specifications/btree/MCbtree.tla @@ -0,0 +1,27 @@ +---- MODULE MCbtree ---- +\* The B-tree in btree.tla draws keys from an unbounded domain and allocates +\* nodes from an unbounded pool. This module bounds both, so that TLC has a +\* finite state space, and reports when a bound was the binding constraint. +EXTENDS btree + +CONSTANTS MaxKey, + MaxNode + +\* With no key at all, no request action is ever enabled and the tree never +\* leaves its initial state. +ASSUME KeyDomainIsNonEmpty == MaxKey \in Nat \ {0} + +\* Only that the bound is a number: btree's NodePoolIsNonEmpty already rules out +\* an empty pool. +ASSUME NodeBoundIsNat == MaxNode \in Nat + +MCKeys == 1..MaxKey +MCNodes == 1..MaxNode + +\* The tree allocates a node whenever a split needs one, so running out means +\* MaxNode was too small for the keys this model inserts, not that the tree +\* misbehaved. This is a statement about the model, not a property of the +\* B-tree, which is why it lives here and not in btree.tla. +FreeNodesRemain == \E n \in Nodes : IsFree(n) + +==== diff --git a/specifications/btree/btree.tla b/specifications/btree/btree.tla index 8d5a10ee..b27bb3de 100644 --- a/specifications/btree/btree.tla +++ b/specifications/btree/btree.tla @@ -1,13 +1,13 @@ \* Note: deletes have not been implemented ---- MODULE btree ---- -EXTENDS TLC, - Naturals, +EXTENDS Naturals, FiniteSets, - Sequences + Sequences, + Relation CONSTANTS Vals, - MaxKey, - MaxNode, + Keys, + Nodes, MaxOccupancy, \* states @@ -26,27 +26,19 @@ CONSTANTS Vals, \* Assumptions the algorithm imposes \* +\* All the tree does with a key is compare it: ChildNodeFor descends by +\* comparing a key against the ones a node holds, and PivotOf splits a node's +\* keys into a smaller and a larger half. A strict total order is therefore +\* everything the algorithm needs of the key domain, which it does not bound. +ASSUME KeysAreOrdered == IsStrictlyTotallyOrderedUnder(<, Keys) + \* MaxOccupancy is the branching factor. Below 2, PivotOf leaves one side of \* every split empty, and IsFree reports the emptied in-tree leaf as free for \* ChooseFreeNode to hand out a second time. ASSUME MaxOccupancyPermitsSplitting == MaxOccupancy \in Nat /\ MaxOccupancy >= 2 \* Even the empty tree is a root node, which Init takes from the free nodes. -ASSUME NodePoolIsNonEmpty == MaxNode \in Nat \ {0} - -\* -\* Assumptions only model checking imposes -\* -\* The algorithm bounds neither the key domain nor the node pool. MaxKey and -\* MaxNode exist to keep Keys, Nodes and the domains of childOf and valOf -\* finite, which is also why exhausting the pool is reported by FreeNodesRemain, -\* as a model too small rather than a defect in the tree. - -\* With no key, no request action is ever enabled and TLC deadlocks on Init. -ASSUME KeyDomainIsNonEmpty == MaxKey \in Nat \ {0} - -Keys == 1..MaxKey -Nodes == 1..MaxNode +ASSUME NodePoolIsNonEmpty == Nodes # {} NIL == CHOOSE x : x \notin Nodes MISSING == CHOOSE v : v \notin Vals @@ -335,6 +327,5 @@ KeyOrderPreserved == \A n \in Inners : (\A k \in keysOf[n] : (\A kc \in keysOf[c 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/manifest.json b/specifications/btree/manifest.json index 8bf500e6..3a4ce245 100644 --- a/specifications/btree/manifest.json +++ b/specifications/btree/manifest.json @@ -11,15 +11,20 @@ { "path": "specifications/btree/btree.tla", "features": [], + "models": [] + }, + { + "path": "specifications/btree/MCbtree.tla", + "features": [], "models": [ { - "path": "specifications/btree/btree.cfg", + "path": "specifications/btree/MCbtree.cfg", "runtime": "00:00:15", "mode": "exhaustive search", "result": "success", "distinctStates": 374727, "totalStates": 2820091, - "stateDepth": 40 + "stateDepth": 38 } ] },