From 0e9217eb435b44cd3da8027f44238b14359382d6 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Thu, 2 Nov 2023 18:46:28 -0700
Subject: [PATCH] Align the _logline in a TLA+ counterexample with its
 corresponding entry 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: ...".
---
 tla/consensus/Traceccfraft.tla | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
index 4f99e39556e7..86d49c39e3de 100644
--- 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 |->