From f5e59cf51b0fa83819cf171185d57cedae90420f Mon Sep 17 00:00:00 2001
From: Arseny Sher <sher-ars@yandex.ru>
Date: Mon, 2 Dec 2024 12:32:51 +0100
Subject: [PATCH] add a4 recondig model

---
 ...ProposerAcceptorReconfig_p2_a4_t2_l2_c3.cfg | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a4_t2_l2_c3.cfg

diff --git a/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a4_t2_l2_c3.cfg b/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a4_t2_l2_c3.cfg
new file mode 100644
index 0000000000..f287014ad5
--- /dev/null
+++ b/safekeeper/spec/models/MCProposerAcceptorReconfig_p2_a4_t2_l2_c3.cfg
@@ -0,0 +1,18 @@
+CONSTANTS
+NULL = NULL
+proposers = {p1, p2}
+acceptors = {a1, a2, a3, a4}
+max_term = 2
+max_entries = 2
+max_generation = 3
+SPECIFICATION Spec
+CONSTRAINT StateConstraint
+INVARIANT
+TypeOk
+ElectionSafetyFull
+LogIsMonotonic
+LogSafety
+SYMMETRY ProposerAcceptorSymmetry
+CHECK_DEADLOCK FALSE
+ALIAS Alias
+