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

Open
#234 2 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
3/5
Estimated time
1-2 days
Newbie friendliness
48/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Active
Domain
devtools

Research direction

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.

Written by the indexing model from the issue text.

Description

question

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

Dominant language
TLA
Stars
1.6k
Forks
224
Avg merge
7d 16h
Merged PRs (30d)
4

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from tlaplus/Examples

All issues in tlaplus/Examples

Similar issues

More DevTools issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.