From ec7c8814f49b10780e8f46a78380913ff566db73 Mon Sep 17 00:00:00 2001
From: Arseny Sher <sher-ars@yandex.ru>
Date: Wed, 6 Nov 2024 16:47:32 +0300
Subject: [PATCH] add p2a3t4l4 model

---
 .../MCProposerAcceptorStatic_p2_a3_t4_l4.cfg    | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 safekeeper/spec/models/MCProposerAcceptorStatic_p2_a3_t4_l4.cfg

diff --git a/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a3_t4_l4.cfg b/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a3_t4_l4.cfg
new file mode 100644
index 0000000000..4763a34ec4
--- /dev/null
+++ b/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a3_t4_l4.cfg
@@ -0,0 +1,17 @@
+CONSTANTS
+NULL = NULL
+proposers = {p1, p2}
+acceptors = {a1, a2, a3}
+max_term = 4
+max_entries = 4
+SPECIFICATION Spec
+CONSTRAINT StateConstraint
+INVARIANT
+TypeOk
+ElectionSafety
+LogIsMonotonic
+LogSafety
+CommittedNotTruncated
+SYMMETRY ProposerAcceptorSymmetry
+CHECK_DEADLOCK FALSE
+ALIAS Alias