There is no default trace

achamayou · Oct 25, 2023 · 020dc25 · 020dc25
1 parent 1999d94
commit 020dc25
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
@@ -60,13 +60,12 @@ IsAppendEntriesResponse(msg, dst, src, logline) ==
 ASSUME TLCGet("config").mode = "bfs"
 
 JsonFile ==
-    IF "JSON" \in DOMAIN IOEnv THEN IOEnv.JSON ELSE "traces/election.ndjson"
+    IF "JSON" \in DOMAIN IOEnv THEN IOEnv.JSON ELSE Print("The JSON environment variable is not set.", FALSE)
 
 JsonLog ==
     \* Deserialize the System log as a sequence of records from the log file.
      \* Run TLC with (assuming a suitable "tlc" shell alias):
-     \* $ JSON=../tests/raft_scenarios/4582.ndjson tlc -note Traceccfraft
-     \* Fall back to trace.ndjson if the JSON environment variable is not set.
+     \* $ JSON=../build/election.ndjson tlc -note Traceccfraft
     ndJsonDeserialize(JsonFile)
 
 TraceLog ==