blob: 5ebe485967804d853ab0d22a7653b79fe676bd48 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
---- 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, MaxCommittedEntries
StateConstraint == \A s \in Server :
/\ currentTerm[s] <= MaxTerm
/\ Len(log[s]) <= MaxLogLen
/\ configVersion[s] <= MaxConfigVersion
/\ Cardinality(immediatelyCommitted) <= MaxCommittedEntries
ServerSymmetry == Permutations(Server)
=============================================================================
|
