Merge branch 'main' into mku-AdvanceCommitIndexOptimization

microsoft · Jan 5, 2024 · 6c53d64 · 6c53d64
2 parents bea77ab + d95a0ce
commit 6c53d64
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/doc/architecture/raft_tla.rst b/doc/architecture/raft_tla.rst
@@ -40,6 +40,8 @@ Using TLC to exhaustively check our models can take any time between minutes (fo
 Trace validation
 ----------------
 
-It is possible to produce fresh traces quickly from the driver by running the make_traces.sh`` script from the ``tla`` directory.
+It is possible to produce fresh traces quickly from the driver by running the ``make_traces.sh`` script from the ``tla`` directory.
 
-Calling the trace validation on, for example, the ``replicate`` scenario can then be done with ``JSON=../build/replicate.ndjson ./tlc.sh consensus/Traceccfraft.tla``.
+Calling the trace validation on, for example, the ``append`` scenario can then be done with ``JSON=../build/append.ndjson ./tlc.sh consensus/Traceccfraft.tla``.
+
+CCF also provides a command line trace visualizer to aid debugging, for example, the ``append`` scenario can be visualized with ``python ../tests/trace_viz.py ../build/append.ndjson``.