Align the _logline in a TLA+ counterexample with its corresponding en…

…try in the JSON log, from which the TLA+ state has been constructed. There's an issue in VScode's "TLA+ model checking" view. Expanding the _logline record fails when the current step is "add_configuration", as VScode struggles with "new_configurations: ...".
microsoft · Nov 3, 2023 · fdba7d5 · fdba7d5
1 parent 4fc9ad2
commit fdba7d5
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
@@ -473,9 +473,7 @@ TraceDifferentialInv ==
 TraceAlias ==
     DebugAlias @@
     [
-        lvl |-> l,
-        ts |-> ts,
-        logline |-> logline.msg
+        _logline |-> TraceLog[l-1]
 
         \* Uncomment _ENABLED when debugging the enablement state of ccfraft's actions.
         \* ,_ENABLED |->