Counting witnesses

CHANGELOG.md

@@ -8,6 +8,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## UNRELEASED
 
 ### Added
+
+- Added a `--witnesses` option to `quint run` that enables counting for how many explored traces each of the given predicates (witnesses) were true (#1562)
+
 ### Changed
 ### Deprecated
 ### Removed

docs/pages/docs/quint.md

@@ -235,6 +235,8 @@ Options:
   --invariant    invariant to check: a definition name or an expression
                                                     [string] [default: ["true"]]
   --seed         random seed to use for non-deterministic choice        [string]
+  --witnesses    space separated list of witnesses to report on (counting for
+                 how many traces the witness is true)      [array] [default: []]
   --mbt          (experimental) whether to produce metadata to be used by
                  model-based testing                  [boolean] [default: false]
 ```

examples/games/tictactoe/tictactoe.qnt

@@ -127,7 +127,7 @@ module tictactoe {
 
   action MoveX = all {
     nextTurn == X,
-    not(won(O)),
+    not(gameOver),
     if (boardEmpty) StartInCorner else
     if (canWin) Win else
     if (canBlock) Block else
@@ -139,7 +139,7 @@ module tictactoe {
 
   action MoveO = all {
     nextTurn == O,
-    not(won(X)),
+    not(gameOver),
     MoveToEmpty(O),
     nextTurn' = X,
   }

quint/io-cli-tests.md

@@ -1463,3 +1463,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/cli.ts

@@ -273,6 +273,11 @@ const runCmd = {
         type: 'string',
         default: 'true',
       })
+      .option('witnesses', {
+        desc: 'space separated list of witnesses to report on (counting for how many traces the witness is true)',
+        type: 'array',
+        default: [],
+      })
       .option('seed', {
         desc: 'random seed to use for non-deterministic choice',
         type: 'string',

quint/src/cliCommands.ts

@@ -37,7 +37,7 @@ import { DocumentationEntry, produceDocs, toMarkdown } from './docs'
 import { QuintError, quintErrorToString } from './quintError'
 import { TestOptions, TestResult } from './runtime/testing'
 import { IdGenerator, newIdGenerator, zerog } from './idGenerator'
-import { Outcome, SimulatorOptions } from './simulation'
+import { Outcome, SimulationResult, SimulatorOptions } from './simulation'
 import { ofItf, toItf } from './itf'
 import { printExecutionFrameRec, printTrace, terminalWidth } from './graphics'
 import { verbosity } from './verbosity'
@@ -480,6 +480,21 @@ function maybePrintCounterExample(verbosityLevel: number, states: QuintEx[], fra
   }
 }
 
+function maybePrintWitnesses(
+  verbosityLevel: number,
+  evalResult: Either<QuintError, SimulationResult>,
+  witnesses: string[]
+) {
+  if (verbosity.hasWitnessesOutput(verbosityLevel)) {
+    evalResult.map(r => {
+      if (r.witnessingTraces.length > 0) {
+        console.log(chalk.green('Witnesses:'))
+      }
+      r.witnessingTraces.forEach((n, i) => console.log(chalk.yellow(witnesses[i]), 'was witnessed in', n, 'traces'))
+    })
+  }
+}
+
 /**
  * Run the simulator.
  *
@@ -545,20 +560,23 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
     return right(parseResult.expr)
   }
 
-  const argsParsingResult = mergeInMany([prev.args.init, prev.args.step, prev.args.invariant].map(toExpr))
+  const argsParsingResult = mergeInMany(
+    [prev.args.init, prev.args.step, prev.args.invariant, ...prev.args.witnesses].map(toExpr)
+  )
   if (argsParsingResult.isLeft()) {
     return cliErr('Argument error', {
       ...simulator,
       errors: argsParsingResult.value.map(mkErrorMessage(new Map())),
     })
   }
-  const [init, step, invariant] = argsParsingResult.value
+  const [init, step, invariant, ...witnesses] = argsParsingResult.value
 
   const evaluator = new Evaluator(prev.resolver.table, recorder, options.rng, options.storeMetadata)
   const evalResult = evaluator.simulate(
     init,
     step,
     invariant,
+    witnesses,
     prev.args.maxSamples,
     prev.args.maxSteps,
     prev.args.nTraces ?? 1
@@ -567,7 +585,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
   const elapsedMs = Date.now() - startMs
 
   const outcome: Outcome = evalResult.isRight()
-    ? { status: (evalResult.value as QuintBool).value ? 'ok' : 'violation' }
+    ? { status: (evalResult.value.result as QuintBool).value ? 'ok' : 'violation' }
     : { status: 'error', errors: [evalResult.value] }
 
   const states = recorder.bestTraces[0]?.frame?.args?.map(e => e.toQuintEx(zerog))
@@ -609,6 +627,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
           console.log(chalk.gray('Use --verbosity to produce more (or less) output.'))
         }
       }
+      maybePrintWitnesses(verbosityLevel, evalResult, prev.args.witnesses)
 
       return right({
         ...simulator,
@@ -625,6 +644,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
           console.log(chalk.gray('Use --verbosity=3 to show executions.'))
         }
       }
+      maybePrintWitnesses(verbosityLevel, evalResult, prev.args.witnesses)
 
       return cliErr('Invariant violated', {
         ...simulator,

quint/src/runtime/impl/evaluator.ts

@@ -28,6 +28,7 @@ import { zerog } from '../../idGenerator'
 import { List } from 'immutable'
 import { Builder, buildDef, buildExpr, nameWithNamespaces } from './builder'
 import { Presets, SingleBar } from 'cli-progress'
+import { SimulationResult } from '../../simulation'
 
 /**
  * An evaluator for Quint in Node TS runtime.
@@ -141,10 +142,11 @@ export class Evaluator {
     init: QuintEx,
     step: QuintEx,
     inv: QuintEx,
+    witnesses: QuintEx[],
     nruns: number,
     nsteps: number,
     ntraces: number
-  ): Either<QuintError, QuintEx> {
+  ): Either<QuintError, SimulationResult> {
     let errorsFound = 0
     let failure: QuintError | undefined = undefined
 
@@ -161,9 +163,12 @@ export class Evaluator {
     const initEval = buildExpr(this.builder, init)
     const stepEval = buildExpr(this.builder, step)
     const invEval = buildExpr(this.builder, inv)
+    const witnessesEvals = witnesses.map(w => buildExpr(this.builder, w))
+    const witnessingTraces = new Array(witnesses.length).fill(0)
 
     for (let runNo = 0; errorsFound < ntraces && !failure && runNo < nruns; runNo++) {
       progressBar.update(runNo)
+      const traceWitnessed = new Array(witnesses.length).fill(false)
 
       this.recorder.onRunCall()
       this.reset()
@@ -208,12 +213,25 @@ export class Evaluator {
 
             this.shift()
 
+            witnessesEvals.forEach((witnessEval, i) => {
+              const witnessResult = witnessEval(this.ctx)
+              if (isTrue(witnessResult)) {
+                traceWitnessed[i] = true
+              }
+            })
+
             const invResult = invEval(this.ctx).mapLeft(error => (failure = error))
             if (!isTrue(invResult)) {
               errorsFound++
             }
             this.recorder.onUserOperatorReturn(stepApp, [], invResult)
           }
+
+          traceWitnessed.forEach((witnessed, i) => {
+            if (witnessed) {
+              witnessingTraces[i] = witnessingTraces[i] + 1
+            }
+          })
         }
       }
 
@@ -222,11 +240,9 @@ export class Evaluator {
     }
     progressBar.stop()
 
-    const outcome: Either<QuintError, QuintEx> = failure
+    return failure
       ? left(failure)
-      : right({ id: 0n, kind: 'bool', value: errorsFound == 0 })
-
-    return outcome
+      : right({ result: { id: 0n, kind: 'bool', value: errorsFound == 0 }, witnessingTraces })
   }
 
   /**
@@ -386,10 +402,10 @@ export class Evaluator {
   private evaluateSimulation(expr: QuintApp): Either<QuintError, QuintEx> {
     if (expr.opcode === 'q::testOnce') {
       const [nsteps, ntraces, init, step, inv] = expr.args
-      return this.simulate(init, step, inv, 1, toNumber(nsteps), toNumber(ntraces))
+      return this.simulate(init, step, inv, [], 1, toNumber(nsteps), toNumber(ntraces)).map(r => r.result)
     } else {
       const [nruns, nsteps, ntraces, init, step, inv] = expr.args
-      return this.simulate(init, step, inv, toNumber(nruns), toNumber(nsteps), toNumber(ntraces))
+      return this.simulate(init, step, inv, [], toNumber(nruns), toNumber(nsteps), toNumber(ntraces)).map(r => r.result)
     }
   }
 }

quint/src/simulation.ts

@@ -9,7 +9,6 @@
  */
 
 import { QuintEx } from './ir/quintIr'
-import { ExecutionFrame } from './runtime/trace'
 import { Rng } from './rng'
 import { QuintError } from './quintError'
 
@@ -39,10 +38,7 @@ export type Outcome =
 /**
  * A result returned by the simulator.
  */
-export interface SimulatorResult {
-  outcome: Outcome
-  vars: string[]
-  states: QuintEx[]
-  frames: ExecutionFrame[]
-  seed: bigint
+export interface SimulationResult {
+  result: QuintEx
+  witnessingTraces: number[]
 }

quint/src/verbosity.ts

@@ -63,6 +63,13 @@ export const verbosity = {
     return level >= 2
   },
 
+  /**
+   * Shall the tool output witnesses counts.
+   */
+  hasWitnessesOutput: (level: number): boolean => {
+    return level >= 1
+  },
+
   /**
    * Shall the tool track and output actions that were executed.
    */