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 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

specifications/btree/btree.cfg specifications/btree/MCbtree.cfgspecifications/btree/btree.cfg renamed to 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
 

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)
+
+====

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)
 
 ====

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
         }
       ]
     },