blob: 22ce43140403719d0db90fe7c4c61b2b0f793d7f (
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
31
|
\* Config file to run the TLC model-checker on MongoReplReconfig.tla.
\* See MongoReplReconfig.tla for instructions.
SPECIFICATION Spec
CONSTANTS
Leader = Leader
Follower = Follower
Down = Down
\* The set of server IDs. Adjust to test different replica set sizes.
CONSTANT Server = {n1, n2, n3, n4}
CONSTANTS
\* The longest oplog any server can reach during model-checking.
MaxLogLen = 2
\* The number of election terms to simulate during model-checking.
MaxTerm = 3
\* The number of reconfigs allowed during model-checking.
MaxConfigVersion = 3
\* Constrain the model to be finite and leverage the symmetry to reduce
\* the state space.
\* Symmetry checking may invalidate liveness checking in certain cases.
SYMMETRY ServerSymmetry
CONSTRAINT StateConstraint
\* Invariants and properties checked by TLC.
INVARIANT ElectionSafety
PROPERTY NeverRollbackCommitted
|
