diff options
| author | Siyuan Zhou <siyuan.zhou@mongodb.com> | 2020-02-06 21:47:44 +0000 |
|---|---|---|
| committer | evergreen <evergreen@mongodb.com> | 2020-02-06 21:47:44 +0000 |
| commit | dfccd546055fdbfa0401e67e4f0e5bc9e89ef358 (patch) | |
| tree | 12fd7dc9ba126c79cbee21751c0fb8cd55a282f2 | |
| parent | e5b21a774777fd1a1d89959b9e78c6eb18580c32 (diff) | |
| download | mongo-dfccd546055fdbfa0401e67e4f0e5bc9e89ef358.tar.gz | |
SERVER-44851 Constrain commit points for model-checking.
| -rw-r--r-- | src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg | 3 | ||||
| -rw-r--r-- | src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla | 3 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg b/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg index 22ce4314040..110de894de4 100644 --- a/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg +++ b/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg @@ -20,6 +20,9 @@ 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. diff --git a/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla b/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla index 4c36b333523..5ebe4859678 100644 --- a/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla +++ b/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla @@ -7,12 +7,13 @@ EXTENDS MongoReplReconfig (* State Constraint. Used for model checking only. *) (**************************************************************************************************) -CONSTANTS MaxTerm, MaxLogLen, MaxConfigVersion +CONSTANTS MaxTerm, MaxLogLen, MaxConfigVersion, MaxCommittedEntries StateConstraint == \A s \in Server : /\ currentTerm[s] <= MaxTerm /\ Len(log[s]) <= MaxLogLen /\ configVersion[s] <= MaxConfigVersion + /\ Cardinality(immediatelyCommitted) <= MaxCommittedEntries ServerSymmetry == Permutations(Server) ============================================================================= |