Exclude messagesSent variable s.t. two states are considered equal if they only differ in the number of messages sent. (#4471)

tla/MCccfraft.cfg

@@ -35,6 +35,7 @@ CONSTANTS
     NodeFive = n5
 
 SYMMETRY Symmetry
+VIEW View
 
 CHECK_DEADLOCK 
     FALSE

tla/MCccfraft.tla

@@ -45,6 +45,9 @@ mc_spec == Spec
 \* via the Symmetry option in cfg file.
 Symmetry == Permutations(Servers_mc)
 
+\* Include all variables in the view, which is similar to defining no view.
+View == vars
+
 ----
 
 \* Returns true if server i has committed value v, false otherwise

tla/MCccfraftWithReconfig.tla

@@ -45,4 +45,7 @@ mc_spec == Spec
 \* via the Symmetry option in cfg file.
 Symmetry == Permutations(Servers_mc)
 
+\* Exclude messagesSent variable s.t. two states are considered equal if they only differ in the number of messages sent.
+View == << reconfigurationVars, <<messages, commitsNotified>>, serverVars, candidateVars, leaderVars, logVars >>
+
 ===================================