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

Aperta
#234 2 commenti 0 reazioni 0 assegnatari Vedi su GitHub

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
3/5
Tempo stimato
1-2 giorni
Idoneità per principianti
48/100
Tipo di issue
Bug
Chiarezza
Abbastanza chiara
Stato di attività
Attiva
Ambito
devtools

Direzione di ricerca

Esamina la specifica di B-tree in tlaplus/examples, iniziando dall’azione WhichToSplit e dalle sottoazioni nominate nell’issue. Esegui la configurazione del model-checker fornita e traccia la transizione a SPLIT_INNER. Il lavoro è completato se si aggiunge il comportamento mancante mantenendo soddisfatte le invarianti indicate, oppure se si documenta che questo stato è intenzionalmente fuori ambito senza causare un deadlock.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

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?

Lingua principale
TLA
Stelle
1.6k
Fork
224
Merge medio
7g 16h
PR unite (30g)
4

Guida per i contributori

Apri la guida per i contributori

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di tlaplus/Examples

Tutte le issue di tlaplus/Examples

Issue simili

Altre issue su DevTools

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.