rust/neon
1
0
Fork 0
mirror of https://github.com/neondatabase/neon.git synced 2026-05-24 16:40:38 +00:00
Code Issues Packages Projects Releases Wiki Activity

add small models

Browse Source
This commit is contained in:
Arseny Sher
2024-12-02 12:26:06 +01:00
parent db343caf5d
commit 691c290280
2 changed files with 21 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a3_t2_l2_c2.cfg → safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a2_t2_l2_c3.cfg
View File

@@ -1,11 +1,10 @@
\* A minimal reconfiguration model.
CONSTANTS
NULL = NULL
proposers = {p1, p2}
acceptors = {a1, a2, a3}
acceptors = {a1, a2}
max_term = 2
max_entries = 2
max_generation = 2
max_generation = 3
SPECIFICATION Spec
CONSTRAINT StateConstraint
INVARIANT
@@ -13,8 +12,7 @@ TypeOk
ElectionSafetyFull
LogIsMonotonic
LogSafety
CommittedNotTruncated
\* CommittedNotTruncated
SYMMETRY ProposerAcceptorSymmetry
CHECK_DEADLOCK FALSE
ALIAS Alias

18
safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a2_t2_l2_c5.cfg Normal file
View File

@@ -0,0 +1,18 @@
CONSTANTS
NULL = NULL
proposers = {p1, p2}
acceptors = {a1, a2}
max_term = 2
max_entries = 2
max_generation = 5
SPECIFICATION Spec
CONSTRAINT StateConstraint
INVARIANT
TypeOk
ElectionSafetyFull
LogIsMonotonic
LogSafety
\* CommittedNotTruncated
SYMMETRY ProposerAcceptorSymmetry
CHECK_DEADLOCK FALSE
ALIAS Alias