TV args

microsoft · Sep 30, 2024 · 7970fd0 · 7970fd0
1 parent 748094f
commit 7970fd0
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 15 deletions.
diff --git a/.github/workflows/ci-verification.yml b/.github/workflows/ci-verification.yml
@@ -27,7 +27,8 @@ jobs:
 
     steps:
       - uses: actions/checkout@v4
-      - run: |
+      - name: Install TLC dependencies
+        run: |
           sudo apt update
           sudo apt install -y default-jre
           python3 ./tla/install_deps.py
@@ -72,7 +73,11 @@ jobs:
 
     steps:
       - uses: actions/checkout@v4
-      - run: python3 ./tla/install_deps.py
+      - name: Install TLC dependencies
+        run: |
+          sudo apt update
+          sudo apt install -y default-jre
+          python3 ./tla/install_deps.py
 
       - name: consistency/MCSingleNodeCommitReachability.cfg
         run: |
@@ -100,7 +105,11 @@ jobs:
 
     steps:
       - uses: actions/checkout@v4
-      - run: python3 ./tla/install_deps.py
+      - name: Install TLC dependencies
+        run: |
+          sudo apt update
+          sudo apt install -y default-jre
+          python3 ./tla/install_deps.py
 
       - name: consistency/MultiNodeReads.cfg
         run: |
@@ -124,7 +133,8 @@ jobs:
 
     steps:
       - uses: actions/checkout@v4
-      - run: |
+      - name: Install TLC dependencies
+        run: |
           sudo apt update
           sudo apt install -y default-jre
           python3 ./tla/install_deps.py
@@ -162,7 +172,8 @@ jobs:
 
     steps:
       - uses: actions/checkout@v4
-      - run: |
+      - name: Install TLC dependencies
+        run: |
           sudo apt update
           sudo apt install -y default-jre
           python3 ./tla/install_deps.py
@@ -193,11 +204,11 @@ jobs:
       - uses: actions/checkout@v4
         with:
           fetch-depth: 0
-      - run: |
+      - name: Install TLC dependencies
+        run: |
           sudo apt update
           sudo apt install -y default-jre parallel
           python3 ./tla/install_deps.py
-        shell: bash
 
       - name: "Build"
         run: |
@@ -223,7 +234,7 @@ jobs:
           cd tla/
           mkdir -p traces/consensus
           mv ../build/consensus traces/
-          parallel 'JSON={} ./tlc.py --workers 1 --dfs --dot --trace-name {} consensus/Traceccfraft.tla' ::: $(ls traces/consensus/*.ndjson)
+          parallel './tlc.py --workers 1 --dfs --driver-trace {} --dot --trace-name {} consensus/Traceccfraft.tla' ::: $(ls traces/consensus/*.ndjson)
         shell: bash
 
       - name: Upload artifacts.

diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
@@ -77,12 +77,12 @@ IsMessage(msg, dst, src, logline) ==
 ASSUME TLCGet("config").mode = "bfs"
 
 JsonFile ==
-    IF "JSON" \in DOMAIN IOEnv THEN IOEnv.JSON ELSE "../traces/consensus/append.ndjson"
+    IF "DRIVER_TRACE" \in DOMAIN IOEnv THEN IOEnv.DRIVER_TRACE ELSE "../traces/consensus/append.ndjson"
 
 JsonLog ==
     \* Deserialize the System log as a sequence of records from the log file.
     \* Run TLC from under the tla/ directory with:
-    \* $ JSON=../build/startup.ndjson ./tlc.sh consensus/Traceccfraft.tla
+    \* $ DRIVER_TRACE=../build/startup.ndjson ./tlc.sh consensus/Traceccfraft.tla
     \* Traces can be generated with: ./make_traces.sh, also under the tla/ directory.
     ndJsonDeserialize(JsonFile)
 

diff --git a/tla/tlc.py b/tla/tlc.py
@@ -40,11 +40,6 @@ def cli():
         action="store_true",
         help="Print out command and environment before running",
     )
-    parser.add_argument(
-        "--dfs",
-        action="store_true",
-        help="Set TLC to use depth-first search",
-    )
     parser.add_argument(
         "--workers",
         type=str,
@@ -79,6 +74,19 @@ def cli():
     parser.add_argument(
         "spec", type=pathlib.Path, help="Path to the TLA+ specification"
     )
+
+    trace_validation = parser.add_argument_group(title="trace validation arguments")
+    trace_validation.add_argument(
+        "--dfs",
+        action="store_true",
+        help="Set TLC to use depth-first search",
+    )
+    trace_validation.add_argument(
+        "--driver-trace",
+        type=pathlib.Path,
+        default=None,
+        help="Path to a CCF Raft driver trace .ndjson file, produced by make_traces.sh",
+    )
     return parser
 
 
@@ -125,6 +133,9 @@ def cli():
             ["-dump", "dot,constrained,colorize,actionlabels", f"{trace_name}.dot"]
         )
 
+    if args.driver_trace:
+        env["DRIVER_TRACE"] = args.driver_trace
+
     cmd = ["java"] + jvm_args + cp_args + ["tlc2.TLC"] + tlc_args + [args.spec]
     if args.v:
         pprint.pprint(env)