traces

microsoft · Oct 1, 2024 · a64ff54 · a64ff54
1 parent 0a2535c
commit a64ff54
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 5 deletions.
diff --git a/.github/workflows/ci-verification.yml b/.github/workflows/ci-verification.yml
@@ -193,7 +193,7 @@ jobs:
           cd tla/
           mkdir -p traces/consensus
           mv ../build/consensus traces/
-          parallel './tlc.py --workers 1 --dot --trace-name {} tv --driver-trace {} consensus/Traceccfraft.tla' ::: $(ls traces/consensus/*.ndjson)
+          parallel './tlc.py --workers 1 --dot --trace-name {} tv --ccf-raft-trace {} consensus/Traceccfraft.tla' ::: $(ls traces/consensus/*.ndjson)
         shell: bash
 
       - name: Upload artifacts.

diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
@@ -82,7 +82,7 @@ JsonFile ==
 JsonLog ==
     \* Deserialize the System log as a sequence of records from the log file.
     \* Run TLC from under the tla/ directory with:
-    \* ./tlc.py --driver-trace ../build/startup.ndjson consensus/Traceccfraft.tla
+    \* ./tlc.py --ccf-raft-trace ../build/startup.ndjson consensus/Traceccfraft.tla
     \* Traces can be generated with: ./make_traces.sh, also under the tla/ directory.
     ndJsonDeserialize(JsonFile)
 

diff --git a/tla/consistency/TraceMultiNodeReads.tla b/tla/consistency/TraceMultiNodeReads.tla
@@ -17,7 +17,7 @@ JsonFile ==
 JsonLog ==
     \* Deserialize the System log as a sequence of records from the log file.
     \* Run TLC from under the tla/ directory with:
-    \* ./tlc.py --driver-trace ../build/consistency/trace.ndjson consistency/TraceMultiNodeReads.tla
+    \* ./tlc.py --ccf-raft-trace ../build/consistency/trace.ndjson consistency/TraceMultiNodeReads.tla
     \* Traces can be generated by running ./tests.sh -VV -R consistency_trace_validation under build/
     \* The clients execute transactions sequentially, and so the log is ordered by tx
     ndJsonDeserialize(JsonFile)

diff --git a/tla/tlc.py b/tla/tlc.py
@@ -119,10 +119,10 @@ def cli():
         help="Set TLC to use depth-first search",
     )
     tv.add_argument(
-        "--driver-trace",
+        "--ccf-raft-trace",
         type=pathlib.Path,
         default=None,
-        help="Path to a CCF Raft driver trace .ndjson file, produced by make_traces.sh",
+        help="Path to a CCF Raft trace .ndjson file, for example produced by make_traces.sh",
     )
 
     # Simulation