WhichToSplit can reach SPLIT_INNER, but no SplitInner sub-action exists

@lorin While going over the B-tree spec in tlaplus/examples, we noticed the action WhichToSplit can set state' = SPLIT_INNER, but there is no sub-action for SPLIT_INNER, so the algorithm deadlocks when it gets there.

The following config reproduces the deadlock:

SPECIFICATION Spec

CONSTANTS
    READY = ready
    GET_VALUE = get_value
    FIND_LEAF_TO_ADD = find_leaf_to_add
    WHICH_TO_SPLIT = which_to_split

    ADD_TO_LEAF = add_to_leaf
    SPLIT_ROOT_LEAF = split_root_leaf
    SPLIT_ROOT_INNER = split_root_inner
    SPLIT_INNER = split_inner
    SPLIT_LEAF = split_leaf
    UPDATE_LEAF = update_leaf

    NIL = nil
    MISSING = missing

    Vals = {x}

    MaxOccupancy = 2

CONSTANTS
    MaxNode = 12
    MaxKey = 5

CONSTANTS
    Keys <- MCKeys
    Nodes <- MCNodes

INVARIANT
TypeOk
InnersMustHaveLast
LeavesCantHaveLast
KeyOrderPreserved
KeysInLeavesAreUnique

Is SplitInner missing, or deliberately out of scope like deletes?

Inspect the B-tree specification in tlaplus/examples, starting with the WhichToSplit action and the sub-actions named in the issue. Run the supplied model-checker configuration and trace the transition to SPLIT_INNER. Done means either adding the missing behavior with the stated invariants still satisfied or documenting that this state is intentionally out of scope without a deadlock.