From afb4d9fa6b16f7cc3417c499a306fac6f1a1f792 Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Wed, 21 Aug 2024 08:26:09 +0200
Subject: [PATCH 01/15] Allow `{#}` placeholder in `run` commands `--out-itf`
 option, regardless of whether it ends with `.itf.json`

---
 quint/src/cli.ts         |  5 ++---
 quint/src/cliCommands.ts | 15 +++++++++++++--
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/quint/src/cli.ts b/quint/src/cli.ts
index c22ec696f..8846671d4 100755
--- a/quint/src/cli.ts
+++ b/quint/src/cli.ts
@@ -181,8 +181,7 @@ const testCmd = {
         type: 'string',
       })
       .option('output', {
-        desc: `write a trace for every test, e.g., out{#}{}.itf.json
-{} is the name of a test, {#} is the test sequence number`,
+        desc: 'write a trace for every test, e.g., out{#}{}.itf.json where {} is the name of a test, {#} is the test sequence number',
         type: 'string',
       })
       .option('max-samples', {
@@ -225,7 +224,7 @@ const runCmd = {
         type: 'string',
       })
       .option('out-itf', {
-        desc: 'output the trace in the Informal Trace Format to file (suppresses all console output)',
+        desc: 'output the trace in the Informal Trace Format to file, e.g., out{#}.itf.json where {#} is the trace sequence number (suppresses all console output)',
         type: 'string',
       })
       .option('max-samples', {
diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
index ca2c8d76a..e65c689ed 100644
--- a/quint/src/cliCommands.ts
+++ b/quint/src/cliCommands.ts
@@ -327,7 +327,7 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
     rng,
     verbosity: verbosityLevel,
     onTrace: (index: number, name: string, status: string, vars: string[], states: QuintEx[]) => {
-      if (outputTemplate && outputTemplate.endsWith('.itf.json')) {
+      if (outputTemplate) {
         const filename = outputTemplate.replaceAll('{}', name).replaceAll('{#}', index)
         const trace = toItf(vars, states)
         if (trace.isRight()) {
@@ -551,7 +551,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
     onTrace: (index: number, status: string, vars: string[], states: QuintEx[]) => {
       const itfFile: string | undefined = prev.args.outItf
       if (itfFile) {
-        const filename = prev.args.nTraces > 1 ? itfFile.replaceAll('.itf.json', `${index}.itf.json`) : itfFile
+        const filename = itfFile.replaceAll('{#}', `${index}`)
         const trace = toItf(vars, states)
         if (trace.isRight()) {
           const jsonObj = addItfHeader(prev.args.input, status, trace.value)
@@ -728,6 +728,17 @@ export async function verifySpec(prev: CompiledStage): Promise<CLIProcedure<Trac
   const args = verifying.args
   const verbosityLevel = deriveVerbosity(args)
 
+  const itfFile: string | undefined = prev.args.outItf
+  if (itfFile) {
+    if (itfFile.includes('{}') || itfFile.includes('{#}')) {
+      console.log(
+        `${chalk.yellow('[warning]')} the output file contains ${chalk.grey('{}')} or ${chalk.grey(
+          '{#}'
+        )}, but this has no effect since at most a single trace will be produced.`
+      )
+    }
+  }
+
   let loadedConfig: any = {}
   try {
     if (args.apalacheConfig) {

From 6091d81dd66fea2b344e38461b94c79c61eaf16e Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Wed, 21 Aug 2024 08:38:41 +0200
Subject: [PATCH 02/15] Remove restriction on `itf.json` extension in `test`
 commands `--output` argument

---
 quint/src/cli.ts | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/quint/src/cli.ts b/quint/src/cli.ts
index 8846671d4..63acba210 100755
--- a/quint/src/cli.ts
+++ b/quint/src/cli.ts
@@ -351,9 +351,6 @@ const docsCmd = {
 const validate = (argv: any) => {
   if (argv.output && typeof argv.output === 'string') {
     const output = argv.output
-    if (!output.endsWith('.itf.json')) {
-      throw new Error(`Unexpected format in --output: ${output}`)
-    }
     if (!output.includes('{}') && !output.includes('{#}')) {
       throw new Error(`The output should contain at least one of variables: {}, {#}`)
     }

From 766a249ff6441ba8403367fede01ccdbec6f5a66 Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Wed, 21 Aug 2024 08:38:59 +0200
Subject: [PATCH 03/15] Fix `--invariant` help message

---
 quint/src/cli.ts | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/quint/src/cli.ts b/quint/src/cli.ts
index 63acba210..37b8f3ccf 100755
--- a/quint/src/cli.ts
+++ b/quint/src/cli.ts
@@ -57,7 +57,7 @@ const compileOpts = (yargs: any) =>
       default: 'step',
     })
     .option('invariant', {
-      desc: 'the invariants to check, separated by commas (e.g.)',
+      desc: 'the invariants to check, separated by commas',
       type: 'string',
     })
     .option('temporal', {

From 6434789d6503ab63f36cd4271a2cd691839cdbdf Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Wed, 21 Aug 2024 13:36:00 +0200
Subject: [PATCH 04/15] Fix tests

---
 quint/io-cli-tests.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md
index 7697d5228..573ca4d91 100644
--- a/quint/io-cli-tests.md
+++ b/quint/io-cli-tests.md
@@ -864,7 +864,7 @@ rm out-itf-example.itf.json
 
 <!-- !test in run with n-traces itf -->
 ```
-quint run --out-itf=out-itf-example.itf.json --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
+quint run --out-itf='out-itf-example{#}.itf.json' --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
 cat out-itf-example0.itf.json | jq '.["#meta"].status'
 rm out-itf-example*.itf.json
 ```
@@ -878,7 +878,7 @@ rm out-itf-example*.itf.json
 
 <!-- !test in run with n-traces itf violation -->
 ```
-quint run --out-itf=out-itf-example.itf.json --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt \
+quint run --out-itf='out-itf-example{#}.itf.json' --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt \
    --invariant=totalSupplyDoesNotOverflowInv 
 cat out-itf-example0.itf.json | jq '.["#meta"].status'
 cat out-itf-example1.itf.json | jq '.["#meta"].status'

From 09c44e15869ca4f643e4ef5bf16ba31d2162b5bd Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Wed, 21 Aug 2024 13:36:10 +0200
Subject: [PATCH 05/15] Fix typos

---
 quint/io-cli-tests.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md
index 573ca4d91..e573c2205 100644
--- a/quint/io-cli-tests.md
+++ b/quint/io-cli-tests.md
@@ -843,14 +843,14 @@ rm out-itf-mbt-example.itf.json
 
 ### Run without violation outputs ITF
 
-<!-- !test in sucessful run itf -->
+<!-- !test in successful run itf -->
 ```
 quint run --out-itf=out-itf-example.itf.json --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
 cat out-itf-example.itf.json | jq '.states[0]."balances"."#map"[0]'
 rm out-itf-example.itf.json
 ```
 
-<!-- !test out sucessful run itf -->
+<!-- !test out successful run itf -->
 ```
 [
   "alice",

From 6bc8e0c9b84d29bdcadb9dcc5451d1d7911253b1 Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Tue, 27 Aug 2024 11:04:56 +0200
Subject: [PATCH 06/15] Rename `test --output` to `test --out-itf` and add a
 hidden alias for the former

---
 quint/src/cli.ts         | 17 ++++++++++++++---
 quint/src/cliCommands.ts |  2 +-
 2 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/quint/src/cli.ts b/quint/src/cli.ts
index 37b8f3ccf..3db5a4329 100755
--- a/quint/src/cli.ts
+++ b/quint/src/cli.ts
@@ -180,10 +180,15 @@ const testCmd = {
         desc: 'name of the main module (by default, computed from filename)',
         type: 'string',
       })
+      .option('out-itf', {
+        desc: 'write a trace for every test, e.g., out_{test}_{seq}.itf.json where {test} is the name of a test, and {seq} is the test sequence number',
+        type: 'string',
+      })
+      // Hidden alias for `--out-itf`
       .option('output', {
-        desc: 'write a trace for every test, e.g., out{#}{}.itf.json where {} is the name of a test, {#} is the test sequence number',
         type: 'string',
       })
+      .hide('output')
       .option('max-samples', {
         desc: 'the maximum number of successful runs to try for every randomized test',
         type: 'number',
@@ -209,8 +214,14 @@ const testCmd = {
         desc: 'a string or regex that selects names to use as tests',
         type: 'string',
       }),
-  handler: (args: any) =>
-    load(args).then(chainCmd(parse)).then(chainCmd(typecheck)).then(chainCmd(runTests)).then(outputResult),
+  handler: (args: any) => {
+    if (args.output != null) {
+      args.outItf = args['out-itf'] = args.output
+      delete args.output
+    }
+
+    load(args).then(chainCmd(parse)).then(chainCmd(typecheck)).then(chainCmd(runTests)).then(outputResult)
+  },
 }
 
 // construct run commands with yargs
diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
index e65c689ed..9191d637a 100644
--- a/quint/src/cliCommands.ts
+++ b/quint/src/cliCommands.ts
@@ -342,7 +342,7 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
 
   const out = console.log
 
-  const outputTemplate = testing.args.output
+  const outputTemplate = testing.args.outItf
 
   // Start the Timer and being running the tests
   const startMs = Date.now()

From 9a5971f495fa5f58a828ed547e47b7ac06217473 Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Tue, 27 Aug 2024 11:05:32 +0200
Subject: [PATCH 07/15] Change placeholders from {} to {test} and from {#} to
 {seq}

---
 quint/io-cli-tests.md    | 12 ++++----
 quint/src/cli.ts         | 13 ++------
 quint/src/cliCommands.ts | 64 ++++++++++++++++++++++++++++++++++++----
 3 files changed, 67 insertions(+), 22 deletions(-)

diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md
index e573c2205..83cffc661 100644
--- a/quint/io-cli-tests.md
+++ b/quint/io-cli-tests.md
@@ -864,7 +864,7 @@ rm out-itf-example.itf.json
 
 <!-- !test in run with n-traces itf -->
 ```
-quint run --out-itf='out-itf-example{#}.itf.json' --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
+quint run --out-itf='out-itf-example{seq}.itf.json' --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
 cat out-itf-example0.itf.json | jq '.["#meta"].status'
 rm out-itf-example*.itf.json
 ```
@@ -878,7 +878,7 @@ rm out-itf-example*.itf.json
 
 <!-- !test in run with n-traces itf violation -->
 ```
-quint run --out-itf='out-itf-example{#}.itf.json' --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt \
+quint run --out-itf='out-itf-example{seq}.itf.json' --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt \
    --invariant=totalSupplyDoesNotOverflowInv 
 cat out-itf-example0.itf.json | jq '.["#meta"].status'
 cat out-itf-example1.itf.json | jq '.["#meta"].status'
@@ -899,7 +899,7 @@ TODO: output states after fix: https://github.com/informalsystems/quint/issues/2
 
 <!-- !test in test itf -->
 ```
-output=$(quint test --output='coin_{#}_{}.itf.json' \
+output=$(quint test --out-itf='coin_{seq}_{test}.itf.json' \
   ../examples/tutorials/coin.qnt)
 exit_code=$?
 echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' -e 's#^.*coin.qnt#      HOME/coin.qnt#g'
@@ -961,7 +961,7 @@ FIXME: fix the traces found by the simulator once #1133 is resolved.
 
 <!-- !test in test1133 -->
 ```
-output=$(quint test --match='(t1|t2)' --output='out_{#}_{}.itf.json' \
+output=$(quint test --match='(t1|t2)' --out-itf='out_{seq}_{test}.itf.json' \
   ./testFixture/simulator/lastActionInRun.qnt)
 exit_code=$?
 echo "BEGIN"
@@ -1268,7 +1268,7 @@ See [#1264](https://github.com/informalsystems/quint/pull/1264).
 
 <!-- !test in multiple jsons -->
 ```
-quint test --output {}.itf.json ./testFixture/_1051manyTests.qnt >/dev/null
+quint test --out-itf {test}.itf.json ./testFixture/_1051manyTests.qnt >/dev/null
 cat firstTest.itf.json secondTest.itf.json | jq -c .states
 rm firstTest.itf.json secondTest.itf.json
 ```
@@ -1285,7 +1285,7 @@ See [#1281](https://github.com/informalsystems/quint/issues/1281)
 
 <!-- !test in variants in itf -->
 ```
-quint test --output {}.itf.json ./testFixture/_1054sumTypesInItf.qnt >/dev/null
+quint test --out-itf {test}.itf.json ./testFixture/_1054sumTypesInItf.qnt >/dev/null
 cat xTest.itf.json | jq -c .states
 rm xTest.itf.json
 ```
diff --git a/quint/src/cli.ts b/quint/src/cli.ts
index 3db5a4329..210361b15 100755
--- a/quint/src/cli.ts
+++ b/quint/src/cli.ts
@@ -235,7 +235,7 @@ const runCmd = {
         type: 'string',
       })
       .option('out-itf', {
-        desc: 'output the trace in the Informal Trace Format to file, e.g., out{#}.itf.json where {#} is the trace sequence number (suppresses all console output)',
+        desc: 'output the trace in the Informal Trace Format to file, e.g., out_{seq}.itf.json where {seq} is the trace sequence number (suppresses all console output)',
         type: 'string',
       })
       .option('max-samples', {
@@ -300,7 +300,7 @@ const verifyCmd = {
   builder: (yargs: any) =>
     compileOpts(yargs)
       .option('out-itf', {
-        desc: 'output the trace in the Informal Trace Format to file (suppresses all console output)',
+        desc: 'output the trace in the Informal Trace Format to file, e.g., out.itf.json (suppresses all console output)',
         type: 'string',
       })
       .option('max-steps', {
@@ -359,14 +359,7 @@ const docsCmd = {
   handler: (args: any) => load(args).then(chainCmd(docs)).then(outputResult),
 }
 
-const validate = (argv: any) => {
-  if (argv.output && typeof argv.output === 'string') {
-    const output = argv.output
-    if (!output.includes('{}') && !output.includes('{#}')) {
-      throw new Error(`The output should contain at least one of variables: {}, {#}`)
-    }
-  }
-
+const validate = (_argv: any) => {
   return true
 }
 
diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
index 9191d637a..ac45721b7 100644
--- a/quint/src/cliCommands.ts
+++ b/quint/src/cliCommands.ts
@@ -328,7 +328,7 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
     verbosity: verbosityLevel,
     onTrace: (index: number, name: string, status: string, vars: string[], states: QuintEx[]) => {
       if (outputTemplate) {
-        const filename = outputTemplate.replaceAll('{}', name).replaceAll('{#}', index)
+        const filename = expandNamedOutputTemplate(outputTemplate, name, index)
         const trace = toItf(vars, states)
         if (trace.isRight()) {
           const jsonObj = addItfHeader(prev.args.input, status, trace.value)
@@ -352,7 +352,7 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
   }
 
   // TODO: This block is a workaround for the fact that flattening removes any defs
-  // not refernced in the main module. We'd instead like way to just instruct it
+  // not referenced in the main module. We'd instead like way to just instruct it
   // to keep some defs.
   //
   // Find tests that are not used in the main module. We need to add references to them in the main module so flattening
@@ -551,7 +551,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
     onTrace: (index: number, status: string, vars: string[], states: QuintEx[]) => {
       const itfFile: string | undefined = prev.args.outItf
       if (itfFile) {
-        const filename = itfFile.replaceAll('{#}', `${index}`)
+        const filename = expandOutputTemplate(itfFile, index, { autoAppend: prev.args.nTraces > 1 })
         const trace = toItf(vars, states)
         if (trace.isRight()) {
           const jsonObj = addItfHeader(prev.args.input, status, trace.value)
@@ -730,10 +730,10 @@ export async function verifySpec(prev: CompiledStage): Promise<CLIProcedure<Trac
 
   const itfFile: string | undefined = prev.args.outItf
   if (itfFile) {
-    if (itfFile.includes('{}') || itfFile.includes('{#}')) {
+    if (itfFile.includes(Placeholders.test) || itfFile.includes(Placeholders.seq)) {
       console.log(
-        `${chalk.yellow('[warning]')} the output file contains ${chalk.grey('{}')} or ${chalk.grey(
-          '{#}'
+        `${chalk.yellow('[warning]')} the output file contains ${chalk.grey(Placeholders.test)} or ${chalk.grey(
+          Placeholders.seq
         )}, but this has no effect since at most a single trace will be produced.`
       )
     }
@@ -971,3 +971,55 @@ function isMatchingTest(match: string | undefined, name: string) {
 function deriveVerbosity(args: { out: string | undefined; outItf: string | undefined; verbosity: number }): number {
   return !args.out && !args.outItf ? args.verbosity : 0
 }
+
+const Placeholders = {
+  test: '{test}',
+  seq: '{seq}',
+}
+
+/**
+ * Expand the output template with the name of the test and the index of the trace.
+ *
+ * Possible placeholders:
+ * - {test} is replaced with the name of the test
+ * - {seq} is replaced with the index of the trace
+ *
+ * If {seq} is not present, the index is appended to the filename, before the extension.
+ *
+ * @param template the output template
+ * @param name the name of the test
+ * @param index the index of the trace
+ * @returns the expanded output template
+ */
+function expandNamedOutputTemplate(template: string, name: string, index: number): string {
+  return expandOutputTemplate(template.replaceAll(Placeholders.test, name), index, { autoAppend: true })
+}
+
+/**
+ * Expand the output template with the index of the trace.
+ *
+ * The {seq} placeholder is replaced with the index of the trace.
+ *
+ * If {seq} is not present and `options.autoAppend` is true,
+ * the index is appended to the filename, before the extension.
+ *
+ * @param template the output template
+ * @param index the index of the trace
+ * @param options An object of the form `{ autoAppend: boolean }`
+ * @returns the expanded output template
+ */
+function expandOutputTemplate(template: string, index: number, options: { autoAppend: boolean }): string {
+  if (template.includes(Placeholders.seq)) {
+    return template.replaceAll(Placeholders.seq, index.toString())
+  } else if (template.endsWith('.itf.json')) {
+    // Special case for the recommended extension, to avoid adding the index in between `itf` and `json`
+    return template.replace('.itf.json', `${index}.itf.json`)
+  } else if (options.autoAppend) {
+    // Append the index to the filename, before the extension
+    const parts = template.split('.')
+    const ext = parts.pop()
+    return `${parts.join('.')}${index}.${ext}`
+  } else {
+    return template
+  }
+}

From 130503486a946ac46b139433bbb22a12b88b9c44 Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Tue, 27 Aug 2024 11:14:16 +0200
Subject: [PATCH 08/15] Update changelog

---
 CHANGELOG.md | 12 ++++++++++++
 check.sh     | 20 ++++++++++++++++++++
 2 files changed, 32 insertions(+)
 create mode 100644 check.sh

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 370c15e24..32df82b74 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,12 +8,24 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## UNRELEASED
 
 ### Added
+
+- In the `verify` command, add warning if `--out-itf` option contains `{test}` or `{seq}` as those have no effect since Apalache only produces a single trace (#1485)
+
 ### Changed
 
 - Performance of incrementally checking types (i.e. in REPL) was improved (#1483).
+- In the `run` and `test` commands, change placeholders from `{}` to `{test}` and from `{#}` to `{seq}` (#1485)
+- In the `run` command, auto-append trace sequence number to filename if more than one trace is present and `{seq}` is not specified (#1485)
+- In the `test` command, rename `--output` to `--out-itf`
 
 ### Deprecated
+
+- In the `test` command, deprecate `--output` option in favour of `--out-itf`, add hidden alias for the former (#1485)
+
 ### Removed
+
+- In the `test` command, stop enforcing `.itf.json` extension (#1485)
+
 ### Fixed
 
  - Bumped GRPC message sizes to 1G (#1480)
diff --git a/check.sh b/check.sh
new file mode 100644
index 000000000..17e4cadfa
--- /dev/null
+++ b/check.sh
@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+
+# Find all .qnt files
+qnt_files=$(find examples -type f -name "*.qnt")
+
+# Initialize a flag to track if any file fails the check
+all_files_valid=true
+
+# Loop through each .qnt file and check its header
+for file in $qnt_files; do
+  if [[ "$(head -n 1 "$file")" != "// -*- mode: Bluespec; -*-" ]]; then
+    echo "File $file does not start with // -*- mode: Bluespec; -*-"
+    all_files_valid=false
+  fi
+done
+
+# If any file failed the check, exit with a non-zero status
+if [ "$all_files_valid" = false ]; then
+  exit 1
+fi

From 6f2847784219bdc219363e2ae3da9062a4a0acac Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Tue, 27 Aug 2024 13:31:00 +0200
Subject: [PATCH 09/15] Fix bug in `test` command where sequence number would
 always be appended, even when not needed

---
 quint/src/cliCommands.ts | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
index ac45721b7..312dfe92c 100644
--- a/quint/src/cliCommands.ts
+++ b/quint/src/cliCommands.ts
@@ -328,7 +328,7 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
     verbosity: verbosityLevel,
     onTrace: (index: number, name: string, status: string, vars: string[], states: QuintEx[]) => {
       if (outputTemplate) {
-        const filename = expandNamedOutputTemplate(outputTemplate, name, index)
+        const filename = expandNamedOutputTemplate(outputTemplate, name, index, { autoAppend: prev.args.nTraces > 1 })
         const trace = toItf(vars, states)
         if (trace.isRight()) {
           const jsonObj = addItfHeader(prev.args.input, status, trace.value)
@@ -984,15 +984,22 @@ const Placeholders = {
  * - {test} is replaced with the name of the test
  * - {seq} is replaced with the index of the trace
  *
- * If {seq} is not present, the index is appended to the filename, before the extension.
+ * If {seq} is not present and `options.autoAppend` is true,
+ * the index is appended to the filename, before the extension.
  *
  * @param template the output template
  * @param name the name of the test
  * @param index the index of the trace
+ * @param options An object of the form `{ autoAppend: boolean }`
  * @returns the expanded output template
  */
-function expandNamedOutputTemplate(template: string, name: string, index: number): string {
-  return expandOutputTemplate(template.replaceAll(Placeholders.test, name), index, { autoAppend: true })
+function expandNamedOutputTemplate(
+  template: string,
+  name: string,
+  index: number,
+  options: { autoAppend: boolean }
+): string {
+  return expandOutputTemplate(template.replaceAll(Placeholders.test, name), index, options)
 }
 
 /**
@@ -1011,7 +1018,7 @@ function expandNamedOutputTemplate(template: string, name: string, index: number
 function expandOutputTemplate(template: string, index: number, options: { autoAppend: boolean }): string {
   if (template.includes(Placeholders.seq)) {
     return template.replaceAll(Placeholders.seq, index.toString())
-  } else if (template.endsWith('.itf.json')) {
+  } else if (options.autoAppend && template.endsWith('.itf.json')) {
     // Special case for the recommended extension, to avoid adding the index in between `itf` and `json`
     return template.replace('.itf.json', `${index}.itf.json`)
   } else if (options.autoAppend) {

From 6e0c3042b60a56a63c11f5356c65b73b51454019 Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Tue, 27 Aug 2024 14:51:58 +0200
Subject: [PATCH 10/15] Show output of `test` command, even when `--out-itf` is
 specified

---
 quint/src/cliCommands.ts | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
index 312dfe92c..d3ce71935 100644
--- a/quint/src/cliCommands.ts
+++ b/quint/src/cliCommands.ts
@@ -529,7 +529,8 @@ function maybePrintCounterExample(verbosityLevel: number, states: QuintEx[], fra
  */
 export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure<TracingStage>> {
   const simulator = { ...prev, stage: 'running' as stage }
-  const verbosityLevel = deriveVerbosity(prev.args)
+  // Force disable output if `--out-itf` is set
+  const verbosityLevel = prev.args.outItf ? 0 : deriveVerbosity(prev.args)
   const mainName = guessMainModule(prev)
 
   const rngOrError = mkRng(prev.args.seed)
@@ -968,8 +969,8 @@ function isMatchingTest(match: string | undefined, name: string) {
 }
 
 // Derive the verbosity for simulation and verification routines
-function deriveVerbosity(args: { out: string | undefined; outItf: string | undefined; verbosity: number }): number {
-  return !args.out && !args.outItf ? args.verbosity : 0
+function deriveVerbosity(args: { out: string | undefined; verbosity: number }): number {
+  return args.out ? 0 : args.verbosity
 }
 
 const Placeholders = {

From cf3df7ce99640a49028b702e5b98c60fbd1bade8 Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Wed, 28 Aug 2024 10:10:59 +0200
Subject: [PATCH 11/15] Disable output of `verify` command if `--out-itf` is
 set

---
 quint/src/cliCommands.ts | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
index d3ce71935..ffe193aed 100644
--- a/quint/src/cliCommands.ts
+++ b/quint/src/cliCommands.ts
@@ -727,7 +727,8 @@ export async function outputCompilationTarget(compiled: CompiledStage): Promise<
 export async function verifySpec(prev: CompiledStage): Promise<CLIProcedure<TracingStage>> {
   const verifying = { ...prev, stage: 'verifying' as stage }
   const args = verifying.args
-  const verbosityLevel = deriveVerbosity(args)
+  // Force disable output if `--out-itf` is set
+  const verbosityLevel = prev.args.outItf ? 0 : deriveVerbosity(prev.args)
 
   const itfFile: string | undefined = prev.args.outItf
   if (itfFile) {

From 25de4982b6c0c4e91d1e9adb5fbca4e88d13b922 Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Thu, 29 Aug 2024 10:37:59 +0200
Subject: [PATCH 12/15] Remove unrelated file

---
 check.sh | 20 --------------------
 1 file changed, 20 deletions(-)
 delete mode 100644 check.sh

diff --git a/check.sh b/check.sh
deleted file mode 100644
index 17e4cadfa..000000000
--- a/check.sh
+++ /dev/null
@@ -1,20 +0,0 @@
-#!/usr/bin/env bash
-
-# Find all .qnt files
-qnt_files=$(find examples -type f -name "*.qnt")
-
-# Initialize a flag to track if any file fails the check
-all_files_valid=true
-
-# Loop through each .qnt file and check its header
-for file in $qnt_files; do
-  if [[ "$(head -n 1 "$file")" != "// -*- mode: Bluespec; -*-" ]]; then
-    echo "File $file does not start with // -*- mode: Bluespec; -*-"
-    all_files_valid=false
-  fi
-done
-
-# If any file failed the check, exit with a non-zero status
-if [ "$all_files_valid" = false ]; then
-  exit 1
-fi

From 6988f0e0c35dc810b8af001adde2cf98ae6373e5 Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Thu, 29 Aug 2024 10:39:13 +0200
Subject: [PATCH 13/15] Revert unnecessary changes in CLI tests

---
 quint/io-cli-tests.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md
index 83cffc661..3f5e8a317 100644
--- a/quint/io-cli-tests.md
+++ b/quint/io-cli-tests.md
@@ -864,7 +864,7 @@ rm out-itf-example.itf.json
 
 <!-- !test in run with n-traces itf -->
 ```
-quint run --out-itf='out-itf-example{seq}.itf.json' --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
+quint run --out-itf=out-itf-example.itf.json --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
 cat out-itf-example0.itf.json | jq '.["#meta"].status'
 rm out-itf-example*.itf.json
 ```
@@ -878,7 +878,7 @@ rm out-itf-example*.itf.json
 
 <!-- !test in run with n-traces itf violation -->
 ```
-quint run --out-itf='out-itf-example{seq}.itf.json' --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt \
+quint run --out-itf=out-itf-example.itf.json --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt \
    --invariant=totalSupplyDoesNotOverflowInv 
 cat out-itf-example0.itf.json | jq '.["#meta"].status'
 cat out-itf-example1.itf.json | jq '.["#meta"].status'

From 463d19fe41daadeef4b51cf3d982b3548689d03b Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Thu, 29 Aug 2024 10:40:11 +0200
Subject: [PATCH 14/15] Change constant to uppercase

---
 quint/src/cliCommands.ts | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
index ffe193aed..d4632e5aa 100644
--- a/quint/src/cliCommands.ts
+++ b/quint/src/cliCommands.ts
@@ -732,10 +732,10 @@ export async function verifySpec(prev: CompiledStage): Promise<CLIProcedure<Trac
 
   const itfFile: string | undefined = prev.args.outItf
   if (itfFile) {
-    if (itfFile.includes(Placeholders.test) || itfFile.includes(Placeholders.seq)) {
+    if (itfFile.includes(PLACEHOLDERS.test) || itfFile.includes(PLACEHOLDERS.seq)) {
       console.log(
-        `${chalk.yellow('[warning]')} the output file contains ${chalk.grey(Placeholders.test)} or ${chalk.grey(
-          Placeholders.seq
+        `${chalk.yellow('[warning]')} the output file contains ${chalk.grey(PLACEHOLDERS.test)} or ${chalk.grey(
+          PLACEHOLDERS.seq
         )}, but this has no effect since at most a single trace will be produced.`
       )
     }
@@ -974,7 +974,7 @@ function deriveVerbosity(args: { out: string | undefined; verbosity: number }):
   return args.out ? 0 : args.verbosity
 }
 
-const Placeholders = {
+const PLACEHOLDERS = {
   test: '{test}',
   seq: '{seq}',
 }
@@ -1001,7 +1001,7 @@ function expandNamedOutputTemplate(
   index: number,
   options: { autoAppend: boolean }
 ): string {
-  return expandOutputTemplate(template.replaceAll(Placeholders.test, name), index, options)
+  return expandOutputTemplate(template.replaceAll(PLACEHOLDERS.test, name), index, options)
 }
 
 /**
@@ -1018,8 +1018,8 @@ function expandNamedOutputTemplate(
  * @returns the expanded output template
  */
 function expandOutputTemplate(template: string, index: number, options: { autoAppend: boolean }): string {
-  if (template.includes(Placeholders.seq)) {
-    return template.replaceAll(Placeholders.seq, index.toString())
+  if (template.includes(PLACEHOLDERS.seq)) {
+    return template.replaceAll(PLACEHOLDERS.seq, index.toString())
   } else if (options.autoAppend && template.endsWith('.itf.json')) {
     // Special case for the recommended extension, to avoid adding the index in between `itf` and `json`
     return template.replace('.itf.json', `${index}.itf.json`)

From ce713fe4a71117c835dd21e40ff582e36c489f36 Mon Sep 17 00:00:00 2001
From: Romain Ruetschi <romain@informal.systems>
Date: Thu, 29 Aug 2024 10:46:15 +0200
Subject: [PATCH 15/15] Remove special case for `.itf.json` trace files, always
 append index to filename, before any extension

---
 quint/src/cliCommands.ts | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
index d4632e5aa..e26622641 100644
--- a/quint/src/cliCommands.ts
+++ b/quint/src/cliCommands.ts
@@ -1020,15 +1020,13 @@ function expandNamedOutputTemplate(
 function expandOutputTemplate(template: string, index: number, options: { autoAppend: boolean }): string {
   if (template.includes(PLACEHOLDERS.seq)) {
     return template.replaceAll(PLACEHOLDERS.seq, index.toString())
-  } else if (options.autoAppend && template.endsWith('.itf.json')) {
-    // Special case for the recommended extension, to avoid adding the index in between `itf` and `json`
-    return template.replace('.itf.json', `${index}.itf.json`)
-  } else if (options.autoAppend) {
-    // Append the index to the filename, before the extension
+  }
+
+  if (options.autoAppend) {
     const parts = template.split('.')
-    const ext = parts.pop()
-    return `${parts.join('.')}${index}.${ext}`
-  } else {
-    return template
+    parts[0] += `${index}`
+    return parts.join('.')
   }
+
+  return template
 }