Remove state counter and add integration test

quint/io-cli-tests.md

@@ -1461,3 +1461,22 @@ exit $exit_code
 
 error: parsing failed
 ```
+### Prints witnesses counts
+
+<!-- !test exit 0 -->
+<!-- !test in witnesses -->
+```
+output=$(quint run ../examples/games/tictactoe/tictactoe.qnt --witnesses="won(X)" stalemate --max-samples=100 --seed=0x2b442ab439177 --verbosity=1)
+exit_code=$?
+echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g'
+exit $exit_code
+```
+
+<!-- !test out witnesses -->
+```
+[ok] No violation found (duration).
+Witnesses:
+won(X) was witnessed in 98 traces
+stalemate was witnessed in 2 traces
+Use --seed=0x2b442ab439177 to reproduce.
+```

quint/src/cliCommands.ts

@@ -487,12 +487,10 @@ function maybePrintWitnesses(
 ) {
   if (verbosity.hasWitnessesOutput(verbosityLevel)) {
     evalResult.map(r => {
-      if (r.witnessResults.states.length > 0) {
+      if (r.witnessingTraces.length > 0) {
         console.log(chalk.green('Witnesses:'))
       }
-      r.witnessResults.states.forEach((c, i) =>
-        console.log(chalk.yellow(witnesses[i]), 'was true for', c, 'states and', r.witnessResults.traces[i], 'traces')
-      )
+      r.witnessingTraces.forEach((n, i) => console.log(chalk.yellow(witnesses[i]), 'was witnessed in', n, 'traces'))
     })
   }
 }

quint/src/runtime/impl/evaluator.ts

@@ -164,8 +164,7 @@ export class Evaluator {
     const stepEval = buildExpr(this.builder, step)
     const invEval = buildExpr(this.builder, inv)
     const witnessesEvals = witnesses.map(w => buildExpr(this.builder, w))
-    const stateCounters = new Array(witnesses.length).fill(0)
-    const traceCounters = new Array(witnesses.length).fill(0)
+    const witnessingTraces = new Array(witnesses.length).fill(0)
 
     for (let runNo = 0; errorsFound < ntraces && !failure && runNo < nruns; runNo++) {
       progressBar.update(runNo)
@@ -217,7 +216,6 @@ export class Evaluator {
             witnessesEvals.forEach((witnessEval, i) => {
               const witnessResult = witnessEval(this.ctx)
               if (isTrue(witnessResult)) {
-                stateCounters[i] = stateCounters[i] + 1
                 traceWitnessed[i] = true
               }
             })
@@ -231,7 +229,7 @@ export class Evaluator {
 
           traceWitnessed.forEach((witnessed, i) => {
             if (witnessed) {
-              traceCounters[i] = traceCounters[i] + 1
+              witnessingTraces[i] = witnessingTraces[i] + 1
             }
           })
         }
@@ -242,11 +240,9 @@ export class Evaluator {
     }
     progressBar.stop()
 
-    const witnessResults = { states: stateCounters, traces: traceCounters }
-
     return failure
       ? left(failure)
-      : right({ result: { id: 0n, kind: 'bool', value: errorsFound == 0 }, witnessResults })
+      : right({ result: { id: 0n, kind: 'bool', value: errorsFound == 0 }, witnessingTraces })
   }
 
   /**

quint/src/simulation.ts

@@ -41,5 +41,5 @@ export type Outcome =
  */
 export interface SimulationResult {
   result: QuintEx
-  witnessResults: { states: number[]; traces: number[] }
+  witnessingTraces: number[]
 }