mirror of
https://github.com/neondatabase/neon.git
synced 2026-01-04 20:12:54 +00:00
030ab1c0e8
## Problem We want to define the algorithm for safekeeper membership change. ## Summary of changes Add spec for it, several models and logs of checking them. ref https://github.com/neondatabase/neon/issues/8699
35 lines
1.1 KiB
Plaintext
35 lines
1.1 KiB
Plaintext
---- MODULE MCProposerAcceptorStatic ----
|
|
EXTENDS TLC, ProposerAcceptorStatic
|
|
|
|
\* Augments the spec with model checking constraints.
|
|
|
|
\* Note that MCProposerAcceptorReconfig duplicates it and might need to
|
|
\* be updated as well.
|
|
|
|
\* For model checking.
|
|
CONSTANTS
|
|
max_entries, \* model constraint: max log entries acceptor/proposer can hold
|
|
max_term \* model constraint: max allowed term
|
|
|
|
ASSUME max_entries \in Nat /\ max_term \in Nat
|
|
|
|
\* Model space constraint.
|
|
StateConstraint == \A p \in proposers:
|
|
/\ prop_state[p].term <= max_term
|
|
/\ Len(prop_state[p].wal) <= max_entries
|
|
\* Sets of proposers and acceptors are symmetric because we don't take any
|
|
\* actions depending on some concrete proposer/acceptor (like IF p = p1 THEN
|
|
\* ...)
|
|
ProposerAcceptorSymmetry == Permutations(proposers) \union Permutations(acceptors)
|
|
|
|
\* enforce order of the vars in the error trace with ALIAS
|
|
\* Note that ALIAS is supported only since version 1.8.0 which is pre-release
|
|
\* as of writing this.
|
|
Alias == [
|
|
prop_state |-> prop_state,
|
|
acc_state |-> acc_state,
|
|
committed |-> committed
|
|
]
|
|
|
|
====
|