Change placeholders to {test} and {seq}, stop enforcing .itf.json extension, rename test --output to test --out-itf

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)

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",
@@ -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
 ```

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', {
@@ -180,11 +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
-{} 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',
@@ -210,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
@@ -225,7 +235,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_{seq}.itf.json where {seq} is the trace sequence number (suppresses all console output)',
         type: 'string',
       })
       .option('max-samples', {
@@ -290,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', {
@@ -349,17 +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.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: {}, {#}`)
-    }
-  }
-
+const validate = (_argv: any) => {
   return true
 }
 

quint/src/cliCommands.ts

@@ -327,8 +327,8 @@ 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')) {
-        const filename = outputTemplate.replaceAll('{}', name).replaceAll('{#}', index)
+      if (outputTemplate) {
+        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)
@@ -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()
@@ -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
@@ -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)
@@ -551,7 +552,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 = 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)
@@ -726,7 +727,19 @@ 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) {
+    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
+        )}, but this has no effect since at most a single trace will be produced.`
+      )
+    }
+  }
 
   let loadedConfig: any = {}
   try {
@@ -957,6 +970,63 @@ 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 = {
+  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 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,
+  options: { autoAppend: boolean }
+): string {
+  return expandOutputTemplate(template.replaceAll(PLACEHOLDERS.test, name), index, options)
+}
+
+/**
+ * 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())
+  }
+
+  if (options.autoAppend) {
+    const parts = template.split('.')
+    parts[0] += `${index}`
+    return parts.join('.')
+  }
+
+  return template
 }