diff options
Diffstat (limited to 'src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg')
| -rw-r--r-- | src/mongo/db/repl/tla_plus/RaftMongo/MCRaftMongo.cfg | 22 |
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 |