MoreUpToDateCorrectInv is not an invariant, move to Debug (#5934)

tla/consensus/MCccfraft.cfg

@@ -71,7 +71,6 @@ INVARIANTS
     ElectionSafetyInv
     LogMatchingInv
     QuorumLogInv
-    MoreUpToDateCorrectInv
     LeaderCompletenessInv
     SignatureInv
     TypeInv

tla/consensus/MCccfraftAtomicReconfig.cfg

@@ -71,7 +71,6 @@ INVARIANTS
     ElectionSafetyInv
     LogMatchingInv
     QuorumLogInv
-    MoreUpToDateCorrectInv
     LeaderCompletenessInv
     SignatureInv
     TypeInv

tla/consensus/MCccfraftWithReconfig.cfg

@@ -71,7 +71,6 @@ INVARIANTS
     ElectionSafetyInv
     LogMatchingInv
     QuorumLogInv
-    MoreUpToDateCorrectInv
     LeaderCompletenessInv
     SignatureInv
     TypeInv

tla/consensus/SIMccfraft.cfg

@@ -73,7 +73,6 @@ INVARIANTS
     ElectionSafetyInv
     LogMatchingInv
     QuorumLogInv
-    MoreUpToDateCorrectInv
     LeaderCompletenessInv
     SignatureInv
 
@@ -101,4 +100,5 @@ INVARIANTS
     \* DebugInvSuccessfulCommitAfterReconfig
     \* DebugInvAllMessagesProcessable
     \* DebugInvRetirementReachable
-    \* DebugInvUpToDepth
+    \* DebugInvUpToDepth
+    \* DebugMoreUpToDateCorrectInv

tla/consensus/ccfraft.tla

@@ -1195,7 +1195,10 @@ UpToDateCheck(i, j) ==
 
 \* If a server i might request a vote from j, receives it and counts it then i 
 \* has all of j's committed entries
-MoreUpToDateCorrectInv ==
+\* This is not an invariant, it is possible for j to vote for i despite i not
+\* having all of j's committed entries. What isn't possible is for i to win
+\* an election without having all of j's committed entries.
+DebugMoreUpToDateCorrectInv ==
     \A i \in { s \in Servers : leadershipState[s] = Candidate } :
         \A j \in GetServerSet(i) :
             /\ i /= j