Warning: The variable messages was changed while it is specified as U…

…NCHANGED at line 227, col 5 to line 227, col 12 of module ccfraft
microsoft · Oct 6, 2023 · d348bec · d348bec
1 parent 438ff87
commit d348bec
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/tla/ccfraft.tla b/tla/ccfraft.tla
@@ -755,10 +755,10 @@ AdvanceCommitIndex(i) ==
                         IN Send(msg)
                     /\ UNCHANGED << currentTerm, votedFor, reconfigurationCount, removedFromConfiguration >>
                  \* Otherwise, states remain unchanged
-                 ELSE UNCHANGED <<serverVars, reconfigurationCount, removedFromConfiguration>>
+                 ELSE UNCHANGED <<messages, serverVars, reconfigurationCount, removedFromConfiguration>>
            \* Otherwise, Configuration and states remain unchanged
-           ELSE UNCHANGED <<serverVars, reconfigurationVars>>
-    /\ UNCHANGED <<messageVars, candidateVars, leaderVars, log>>
+           ELSE UNCHANGED <<messages, serverVars, reconfigurationVars>>
+    /\ UNCHANGED <<commitsNotified, candidateVars, leaderVars, log>>
 
 \* CCF: RetiredLeader server i notifies the current commit level to server j
 \*  This allows to retire gracefully instead of deadlocking the system through removing itself from the network.