diff options
Diffstat (limited to 'src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla')
| -rw-r--r-- | src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla b/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla new file mode 100644 index 00000000000..4c36b333523 --- /dev/null +++ b/src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.tla @@ -0,0 +1,18 @@ +---- MODULE MCMongoReplReconfig ---- +\* This module defines MCMongoReplReconfig.tla constants/constraints for model-checking. + +EXTENDS MongoReplReconfig + +(**************************************************************************************************) +(* State Constraint. Used for model checking only. *) +(**************************************************************************************************) + +CONSTANTS MaxTerm, MaxLogLen, MaxConfigVersion + +StateConstraint == \A s \in Server : + /\ currentTerm[s] <= MaxTerm + /\ Len(log[s]) <= MaxLogLen + /\ configVersion[s] <= MaxConfigVersion + +ServerSymmetry == Permutations(Server) +============================================================================= |