Revert log editing in ccfraft, pre-process traces accordingly

tests/raft_scenarios_runner.py

@@ -3,9 +3,12 @@
 import argparse
 import sys
 import os
+import json
 from subprocess import Popen, PIPE
 from raft_scenarios_gen import generate_scenarios
 from contextlib import contextmanager
+from collections import defaultdict
+from heapq import merge
 
 
 @contextmanager
@@ -33,6 +36,23 @@ def write_error_report(errors=None):
         print("??? success \n")
 
 
+def remove_reconfiguration_replicates(log):
+    log_by_node = defaultdict(list)
+    for line in log:
+        entry = json.loads(line)
+        node = entry["msg"]["state"]["node_id"]
+        if entry["msg"]["function"] == "add_configuration":
+            removed = log_by_node[node].pop()
+            assert removed["msg"]["function"] in (
+                "replicate",
+                "execute_append_entries_sync",
+            ), removed
+        log_by_node[node].append(entry)
+    return [
+        json.dumps(e) for e in merge(*log_by_node.values(), key=lambda e: e["h_ts"])
+    ]
+
+
 def separate_log_lines(text):
     mermaid = []
     log = []
@@ -41,7 +61,10 @@ def separate_log_lines(text):
             mermaid.append(line[len("<RaftDriver>") :])
         elif '"raft_trace"' in line:
             log.append(line)
-    return (os.linesep.join(mermaid) + os.linesep, os.linesep.join(log) + os.linesep)
+    return (
+        os.linesep.join(mermaid) + os.linesep,
+        os.linesep.join(remove_reconfiguration_replicates(log)) + os.linesep,
+    )
 
 
 def expand_files(files):

tla/consensus/ccfraft.tla

@@ -658,11 +658,6 @@ ChangeConfigurationInt(i, newConfiguration) ==
     /\ newConfiguration \subseteq Servers
     \* Configuration is not equal to the previous configuration
     /\ newConfiguration /= MaxConfiguration(i)
-    \* The previous entry in the log is a regular entry, since we are
-    \* going to replace it. We don't want replace a signature entry,
-    \* or another reconfiguration.
-    /\ Len(log[i]) > 0
-    /\ log[i][Len(log[i])].contentType = TypeEntry
     \* Keep track of running reconfigurations to limit state space
     /\ reconfigurationCount' = reconfigurationCount + 1
     /\ removedFromConfiguration' = removedFromConfiguration \cup (CurrentConfiguration(i) \ newConfiguration)
@@ -671,7 +666,7 @@ ChangeConfigurationInt(i, newConfiguration) ==
             term |-> currentTerm[i],
             configuration |-> newConfiguration,
             contentType |-> TypeReconfiguration]
-        newLog == [log[i] EXCEPT ![Len(log[i])] = entry]
+        newLog == Append(log[i], entry)
         \* Remove the ghost configuration at index 0, there's no index 0 in the log
         validConfigurationPrefix == [ci \in DOMAIN configurations[i] \ {0} |-> configurations[i]]
         IN
@@ -1339,8 +1334,7 @@ PermittedLogChangesProp ==
             \/ /\ state[i] = Leader
                /\ state[i]' = Leader
                /\ Len(log[i]') >= Len(log[i])
-               \* Reconfiguration replaces the last entry
-               \* /\ IsPrefix(log[i], log[i]')
+               /\ IsPrefix(log[i], log[i]')
             \* Newly elected leader is truncating its log
             \/ /\ state[i] = Candidate
                /\ state[i]' = Leader