Merge pull request #1664 from markopiers/out-itf-should-not-supress-output

Allow --verbosity to override default suppression by --out-itf (#1571)

Author: bugarela

CHANGELOG.md

@@ -9,6 +9,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 ### Changed
+
+- `--out-itf` does not suppress outputs anymore. Shown output amount only depends on `--verbosity` now (#1664) 
+
 ### Deprecated
 ### Removed
 ### Fixed

docs/pages/docs/quint.md

@@ -229,7 +229,7 @@ Options:
                                                                         [string]
   --out-itf      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)                        [string]
+                                                                        [string]
   --max-samples  the maximum number of runs to attempt before giving up
                                                        [number] [default: 10000]
   --n-traces     how many traces to generate (only affects output to out-itf)

quint/io-cli-tests.md

@@ -1,4 +1,3 @@
-
 This is a suite of blackbox integration tests for the `quint` executable.
 The tests in this file check that particular output is produced when
 particular input is received.
@@ -778,6 +777,7 @@ error: Invariant violated
 ```
 quint run --out-itf=out-itf-example.itf.json --max-steps=5 --seed=123 \
   --invariant=totalSupplyDoesNotOverflowInv \
+  --verbosity=0 \
   ../examples/tutorials/coin.qnt
 cat out-itf-example.itf.json | jq '.states[0]."balances"."#map"[0]'
 rm out-itf-example.itf.json
@@ -799,6 +799,7 @@ rm out-itf-example.itf.json
 ```
 quint run --out-itf=out-itf-mbt-example.itf.json --max-steps=5 --seed=123 \
   --invariant=totalSupplyDoesNotOverflowInv --mbt\
+  --verbosity=0 \
   ../examples/tutorials/coin.qnt
 cat out-itf-mbt-example.itf.json | jq '.states[1]'
 rm out-itf-mbt-example.itf.json
@@ -869,7 +870,7 @@ rm out-itf-mbt-example.itf.json
 
 <!-- !test in successful run itf -->
 ```
-quint run --out-itf=out-itf-example.itf.json --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
+quint run --out-itf=out-itf-example.itf.json --max-steps=5 --seed=123  --verbosity=0 ../examples/tutorials/coin.qnt
 cat out-itf-example.itf.json | jq '.states[0]."balances"."#map"[0]'
 rm out-itf-example.itf.json
 ```
@@ -888,7 +889,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 --mbt --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
+quint run --out-itf=out-itf-example.itf.json --n-traces=3 --mbt --max-steps=5 --seed=123 --verbosity=0 ../examples/tutorials/coin.qnt
 cat out-itf-example0.itf.json | jq '.["#meta"].status'
 cat out-itf-example1.itf.json | jq '.states[0]["mbt::actionTaken"]'
 rm out-itf-example*.itf.json
@@ -904,7 +905,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 --verbosity=0  ../examples/tutorials/coin.qnt \
    --invariant=totalSupplyDoesNotOverflowInv 
 cat out-itf-example0.itf.json | jq '.["#meta"].status'
 cat out-itf-example1.itf.json | jq '.["#meta"].status'
@@ -1476,3 +1477,31 @@ won(X) was witnessed in 99 trace(s) out of 100 explored (99.00%)
 stalemate was witnessed in 1 trace(s) out of 100 explored (1.00%)
 Use --seed=0x2b442ab439177 to reproduce.
 ```
+
+### Run produces normal output on `--out-itf` with default verbosity
+
+<!-- !test exit 1 -->
+<!-- !test in run itf default verbosity -->
+```
+output=$(quint run --out-itf=out.itf.json --max-steps=5 --seed=123 \
+  --invariant=totalSupplyDoesNotOverflowInv \
+  ../examples/tutorials/coin.qnt 2>&1)
+exit_code=$?
+rm out.itf.json
+echo "$output" | head
+exit $exit_code
+```
+
+<!-- !test out run itf default verbosity -->
+```
+An example execution:
+
+[State 0]
+{
+  balances:
+    Map("alice" -> 0, "bob" -> 0, "charlie" -> 0, "eve" -> 0, "null" -> 0),
+  minter: "null"
+}
+
+[State 1]
+```

quint/src/cli.ts

@@ -238,7 +238,7 @@ const runCmd = {
         type: 'string',
       })
       .option('out-itf', {
-        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)',
+        desc: 'output the trace in the Informal Trace Format to file, e.g., out_{seq}.itf.json where {seq} is the trace sequence number',
         type: 'string',
       })
       .option('max-samples', {

quint/src/cliCommands.ts

@@ -517,8 +517,8 @@ function maybePrintWitnesses(verbosityLevel: number, outcome: Outcome, witnesses
 export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure<TracingStage>> {
   const simulator = { ...prev, stage: 'running' as stage }
   const startMs = Date.now()
-  // Force disable output if `--out-itf` is set
-  const verbosityLevel = prev.args.outItf ? 0 : deriveVerbosity(prev.args)
+  // Verboity level controls how much of the output is shown
+  const verbosityLevel = deriveVerbosity(prev.args)
   const mainName = guessMainModule(prev)
   const main = prev.modules.find(m => m.name === mainName)
   if (!main) {