blob: 3724efb7f0b607c0d943389094d64c8b5ca14fc4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
\* 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}
INVARIANT NoTwoPrimariesInSameTerm
\* NeverRollbackCommitted and NeverRollbackBeforeCommitPoint can be violated,
\* although it's not ultimately a safety issue: SERVER-39626. The issue
\* requires at least 5 servers, 3 terms, and oplogs of length 4+, which are
\* larger limits than we can easily model-check.
INVARIANT NeverRollbackCommitted
INVARIANT NeverRollbackBeforeCommitPoint
PROPERTY CommitPointEventuallyPropagates
\* Not configurable.
CONSTRAINT StateConstraint
SPECIFICATION Spec
|
