SERVER-44458 Model-checking files for RaftMongo.tla

1 files changed, 22 insertions, 0 deletions

diff --git a/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg b/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg
new file mode 100644
index 00000000000..c94a84e89d9
--- /dev/null
+++ b/src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg
@@ -0,0 +1,22 @@
+\* Config file to run the TLC model-checker on RaftMongo.tla.
+\* See RaftMongo.tla for instructions.
+
+\* The maximum number of oplog entries that can be created on the primary in one
+\* action. For model-checking, this can be 1 or a small number.
+CONSTANT MaxClientWriteSize = 2
+
+\* The number of election terms to simulate during model-checking.
+CONSTANT MaxTerm = 3
+
+\* The longest oplog any server can reach during model-checking.
+CONSTANT MaxLogLen = 3
+
+\* The set of server IDs. Adjust to test different replica set sizes.
+CONSTANT Server = {1, 2, 3}
+
+\* Add invariants if desired.
+INVARIANT NoTwoPrimariesInSameTerm
+
+\* Not configurable.
+CONSTRAINT StateConstraint
+SPECIFICATION Spec