diff --git a/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a3_t2_l2_c2.cfg b/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a2_t2_l2_c3.cfg similarity index 70% rename from safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a3_t2_l2_c2.cfg rename to safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a2_t2_l2_c3.cfg index 43d4b970ff..9977601f36 100644 --- a/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a3_t2_l2_c2.cfg +++ b/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a2_t2_l2_c3.cfg @@ -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 - diff --git a/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a2_t2_l2_c5.cfg b/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a2_t2_l2_c5.cfg new file mode 100644 index 0000000000..cc564a2ba0 --- /dev/null +++ b/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a2_t2_l2_c5.cfg @@ -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