State the assumptions and split the model into MCbtree

specifications/btree/btree.cfg → 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
@@ -22,8 +22,23 @@ CONSTANTS Vals,
           SPLIT_ROOT_INNER,
           UPDATE_LEAF
 
-Keys == 1..MaxKey
-Nodes == 1..MaxNode
+\*
+\* 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 == Nodes # {}
 
 NIL == CHOOSE x : x \notin Nodes
 MISSING == CHOOSE v : v \notin Vals
@@ -312,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
         }
       ]
     },