Compute node count from a single pass over the JSON log file, elimina…

…ting the need for separate 'nodes' file.

tests/raft_scenarios_runner.py

@@ -37,21 +37,15 @@ def write_error_report(errors=None):
 def separate_log_lines(text):
     mermaid = []
     log = []
-    nodes = set()
     for line in text.split(os.linesep):
         if line.startswith("<RaftDriver>"):
             mermaid.append(line[len("<RaftDriver>") :])
         elif '"raft_trace"' in line:
             line_ = json.loads(line)
-            if "msg" in line_:
-                if "configurations" in line_["msg"]:
-                    for config in line_["msg"]["configurations"]:
-                        nodes.update(config["nodes"].keys())
             log.append(line)
     return (
         os.linesep.join(mermaid) + os.linesep,
-        os.linesep.join(log) + os.linesep,
-        len(nodes),
+        os.linesep.join(log) + os.linesep
     )
 
 
@@ -105,19 +99,14 @@ def expand_files(files):
             with block(ostream, "stderr", 3):
                 ostream.write(err.decode())
 
-        mermaid, log, max_nodes = separate_log_lines(out.decode())
+        mermaid, log = separate_log_lines(out.decode())
 
         with block(ostream, "diagram", 3, "mermaid", ["sequenceDiagram"]):
             ostream.write(mermaid)
 
         with open(f"{os.path.basename(scenario)}.ndjson", "w", encoding="utf-8") as f:
             f.write(log)
 
-        with open(
-            f"{os.path.basename(scenario)}.ndjson.nodes", "w", encoding="utf-8"
-        ) as f:
-            f.write(str(max_nodes))
-
     write_error_report(err_list)
 
     if not test_result or err_list:

tla/Traceccfraft.tla

@@ -73,7 +73,7 @@ TraceLog ==
 ASSUME PrintT(<< "Trace:", JsonFile, "Length:", Len(TraceLog)>>)
 
 JsonServers ==
-    atoi(Deserialize(JsonFile \o ".nodes", [format |-> "TXT", charset |-> "UTF-8"]).stdout)
+    Cardinality({ TraceLog[i].msg.state.node_id: i \in DOMAIN TraceLog })
 ASSUME JsonServers \in Nat \ {0}
 
 TraceServers ==