diff options
Diffstat (limited to 'src/mongo/tla_plus/RaftMongo/MCRaftMongo.tla')
| -rw-r--r-- | src/mongo/tla_plus/RaftMongo/MCRaftMongo.tla | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/mongo/tla_plus/RaftMongo/MCRaftMongo.tla b/src/mongo/tla_plus/RaftMongo/MCRaftMongo.tla new file mode 100644 index 00000000000..057e3dd7a91 --- /dev/null +++ b/src/mongo/tla_plus/RaftMongo/MCRaftMongo.tla @@ -0,0 +1,13 @@ +---- MODULE MCRaftMongo ---- +\* This module defines RaftMongo.tla constants/constraints for model-checking. +\* See RaftMongo.tla for instructions. + +EXTENDS RaftMongo + +CONSTANT MaxTerm +CONSTANT MaxLogLen + +StateConstraint == + /\ GlobalCurrentTerm <= MaxTerm + /\ \forall i \in Server: Len(log[i]) <= MaxLogLen +============================================================================= |