mirror of
https://github.com/neondatabase/neon.git
synced 2026-01-06 13:02:55 +00:00
fa909c27fc
The spec was written for the buggy protocol which we had before the one more similar to Raft was implemented. Update the spec with what we currently have. ref https://github.com/neondatabase/neon/issues/8699
20 lines
330 B
INI
20 lines
330 B
INI
\* A very small model just to play.
|
|
CONSTANTS
|
|
NULL = NULL
|
|
proposers = {p1, p2}
|
|
acceptors = {a1, a2, a3}
|
|
max_term = 2
|
|
max_entries = 2
|
|
SPECIFICATION Spec
|
|
CONSTRAINT StateConstraint
|
|
INVARIANT
|
|
TypeOk
|
|
ElectionSafetyFull
|
|
LogIsMonotonic
|
|
LogSafety
|
|
CommittedNotTruncated
|
|
SYMMETRY ProposerAcceptorSymmetry
|
|
CHECK_DEADLOCK FALSE
|
|
ALIAS Alias
|
|
|