diff options
Diffstat (limited to 'src/mongo/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg')
| -rw-r--r-- | src/mongo/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/src/mongo/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg b/src/mongo/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg new file mode 100644 index 00000000000..beb09332519 --- /dev/null +++ b/src/mongo/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg @@ -0,0 +1,34 @@ +\* 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} + +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 + +\* The number of commit points advanced during model-checking. +MaxCommittedEntries = 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 |