From 5384d23393fd2dbc45c4afeaecfe6b9cf4cac97b Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 23 Oct 2023 13:04:31 -0700 Subject: [PATCH] Recreating longer counterexamples such as those coming out of the simulator is significantly faster when deserialized from TLC's binary format as opposed to the textual record in TTrace.tla. --- .github/workflows/tlaplus.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml index 03d5d028f265..d2a58898bf92 100644 --- a/.github/workflows/tlaplus.yml +++ b/.github/workflows/tlaplus.yml @@ -40,6 +40,7 @@ jobs: name: tlc path: | tla/consensus/*_TTrace_*.tla + tla/consensus/*_TTrace_*.bin tla/*.trace.tla tla/*.json @@ -63,6 +64,7 @@ jobs: name: tlc path: | tla/consensus/*_TTrace_*.tla + tla/consensus/*_TTrace_*.bin tla/*.trace.tla tla/*.json