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

[lemmy]

@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?

[lemmy]

Related, the current specs should probably state core btree invariants such as MinOccupancy and MaxOccupancy (perhaps by reusing defs from https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla).