Add to quint workflow a step to generate traces, including Script/tra…

…ce-remove-stuttering-steps.sh

.github/workflows/quint.yml

@@ -34,3 +34,27 @@ jobs:
       - run: npm install -g @informalsystems/quint
       - run: bash Scripts/quint-forall.sh test Specs/Quint/*Test.qnt
 
+  quint-traces:
+    name: Generate trace files
+    runs-on: ubuntu-latest
+    env:
+      fixture_dir: Code/itf/tests/fixtures/votekeeper
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v3
+        with:
+          node-version: "18"
+      - run: npm install -g @informalsystems/quint
+      - name: Generate traces 
+        working-directory: Spec/Quint
+        run: |
+          quint test --output ../../$fixture_dir/voteBookkeeper_{}.itf.json voteBookkeeperTest.qnt 
+      # This step is needed as a hack to clean the generated traces of repeated steps. The problem
+      # is that `quint test --output ...` on `run` statements registers in the traces the
+      # `allUnchanged` actions that are used when checking properties (see
+      # https://github.com/informalsystems/quint/issues/1252).
+      - name: Remove stuttering steps
+        run: find $fixture_dir -maxdepth 1 -type f -exec ./Scripts/trace-remove-stuttering-steps.sh {} \; 
+      # This step removes trace files generated from tests defined in imported modules.
+      - name: Remove tests
+        run: rm $fixture_dir/*voteBookkeeperTest::*.*

Scripts/trace-remove-stuttering-steps.sh

@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+FILE=$1
+[[ ! -f "$FILE" ]] && echo "Error: $FILE does not exist" && exit 1
+
+# The following jq command removes all stuttering steps on an ITF trace file. A stuttering step
+# happens in a trace when a state is followed by the same state.
+#
+# Note that for comparing states we remove from all states the "#meta" field, which is different for
+# each state as it includes a sequential index number. This information is not needed for displaying
+# or doing MBT on the trace.
+#
+# TODO: For completeness, include the state #meta field in the resulting trace file.
+echo $(cat $1 | jq -c '{"#meta":."#meta", vars:.vars, states: (.states | del(.[]."#meta") | reduce .[] as $a ([]; if IN(.[]; $a) then . else . += [$a] end))}') > $1