From 9c0807c0088cfc0b7e7253394295bcac9460a571 Mon Sep 17 00:00:00 2001 From: bugarela Date: Wed, 13 Nov 2024 14:29:37 -0300 Subject: [PATCH 1/9] Add witnesses argument to quint run --- quint/src/cli.ts | 5 +++++ quint/src/cliCommands.ts | 16 +++++++++++++--- quint/src/runtime/impl/evaluator.ts | 20 +++++++++++++++----- 3 files changed, 33 insertions(+), 8 deletions(-) diff --git a/quint/src/cli.ts b/quint/src/cli.ts index 0acbcd42f..6df55eb89 100755 --- a/quint/src/cli.ts +++ b/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 samples the witness is true)', + type: 'array', + default: '[]', + }) .option('seed', { desc: 'random seed to use for non-deterministic choice', type: 'string', diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index a692e490a..462159fa4 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -545,20 +545,23 @@ export async function runSimulator(prev: TypecheckedStage): Promise e.toQuintEx(zerog)) @@ -609,6 +612,12 @@ export async function runSimulator(prev: TypecheckedStage): Promise { + if (r.counters.length > 0) { + console.log(chalk.green('Witnesses:')) + } + r.counters.forEach((c, i) => console.log(chalk.yellow(prev.args.witnesses[i]), 'was true for', c, 'samples')) + }) return right({ ...simulator, @@ -618,6 +627,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise r.counters.forEach((c, i) => console.log(prev.args.witnesses[i], c))) if (verbosity.hasResults(verbosityLevel)) { console.log(chalk.red(`[violation]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`)) diff --git a/quint/src/runtime/impl/evaluator.ts b/quint/src/runtime/impl/evaluator.ts index 5001d522d..37f9b14b1 100644 --- a/quint/src/runtime/impl/evaluator.ts +++ b/quint/src/runtime/impl/evaluator.ts @@ -141,10 +141,11 @@ export class Evaluator { init: QuintEx, step: QuintEx, inv: QuintEx, + witnesses: QuintEx[], nruns: number, nsteps: number, ntraces: number - ): Either { + ): Either { let errorsFound = 0 let failure: QuintError | undefined = undefined @@ -161,6 +162,8 @@ 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 counters = new Array(witnesses.length).fill(0) for (let runNo = 0; errorsFound < ntraces && !failure && runNo < nruns; runNo++) { progressBar.update(runNo) @@ -208,6 +211,13 @@ export class Evaluator { this.shift() + witnessesEvals.forEach((witnessEval, i) => { + const witnessResult = witnessEval(this.ctx) + if (isTrue(witnessResult)) { + counters[i] = counters[i] + 1 + } + }) + const invResult = invEval(this.ctx).mapLeft(error => (failure = error)) if (!isTrue(invResult)) { errorsFound++ @@ -222,9 +232,9 @@ export class Evaluator { } progressBar.stop() - const outcome: Either = failure + const outcome: Either = failure ? left(failure) - : right({ id: 0n, kind: 'bool', value: errorsFound == 0 }) + : right({ result: { id: 0n, kind: 'bool', value: errorsFound == 0 }, counters: counters }) return outcome } @@ -386,10 +396,10 @@ export class Evaluator { private evaluateSimulation(expr: QuintApp): Either { 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) } } } From 6ab474477c792a4c70598e2348ec1d70e88ded2f Mon Sep 17 00:00:00 2001 From: bugarela Date: Wed, 13 Nov 2024 14:52:40 -0300 Subject: [PATCH 2/9] Fix descriptions to match behavior --- quint/src/cli.ts | 2 +- quint/src/cliCommands.ts | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/quint/src/cli.ts b/quint/src/cli.ts index 6df55eb89..223a19372 100755 --- a/quint/src/cli.ts +++ b/quint/src/cli.ts @@ -274,7 +274,7 @@ const runCmd = { default: 'true', }) .option('witnesses', { - desc: 'space separated list of witnesses to report on (counting for how many samples the witness is true)', + desc: 'space separated list of witnesses to report on (counting for how many states the witness is true)', type: 'array', default: '[]', }) diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index 462159fa4..3a30f93c9 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -616,7 +616,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise 0) { console.log(chalk.green('Witnesses:')) } - r.counters.forEach((c, i) => console.log(chalk.yellow(prev.args.witnesses[i]), 'was true for', c, 'samples')) + r.counters.forEach((c, i) => console.log(chalk.yellow(prev.args.witnesses[i]), 'was true for', c, 'states')) }) return right({ From 9ec2ab2de3233dab7064b94daeb4bef906162ef0 Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 18 Nov 2024 15:05:31 -0300 Subject: [PATCH 3/9] Count wintessing traces as well --- quint/src/cliCommands.ts | 15 ++++++++++++--- quint/src/runtime/impl/evaluator.ts | 24 +++++++++++++++++------- quint/src/simulation.ts | 9 +++------ 3 files changed, 32 insertions(+), 16 deletions(-) diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index 3a30f93c9..d616d6aac 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -613,10 +613,19 @@ export async function runSimulator(prev: TypecheckedStage): Promise { - if (r.counters.length > 0) { + if (r.witnessResults.states.length > 0) { console.log(chalk.green('Witnesses:')) } - r.counters.forEach((c, i) => console.log(chalk.yellow(prev.args.witnesses[i]), 'was true for', c, 'states')) + r.witnessResults.states.forEach((c, i) => + console.log( + chalk.yellow(prev.args.witnesses[i]), + 'was true for', + c, + 'states and', + r.witnessResults.traces[i], + 'traces' + ) + ) }) return right({ @@ -627,7 +636,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise r.counters.forEach((c, i) => console.log(prev.args.witnesses[i], c))) + // TODO: print witnesses if (verbosity.hasResults(verbosityLevel)) { console.log(chalk.red(`[violation]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`)) diff --git a/quint/src/runtime/impl/evaluator.ts b/quint/src/runtime/impl/evaluator.ts index 37f9b14b1..2e8005449 100644 --- a/quint/src/runtime/impl/evaluator.ts +++ b/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. @@ -145,7 +146,7 @@ export class Evaluator { nruns: number, nsteps: number, ntraces: number - ): Either { + ): Either { let errorsFound = 0 let failure: QuintError | undefined = undefined @@ -163,10 +164,12 @@ 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 counters = new Array(witnesses.length).fill(0) + const stateCounters = new Array(witnesses.length).fill(0) + const traceCounters = 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() @@ -214,7 +217,8 @@ export class Evaluator { witnessesEvals.forEach((witnessEval, i) => { const witnessResult = witnessEval(this.ctx) if (isTrue(witnessResult)) { - counters[i] = counters[i] + 1 + stateCounters[i] = stateCounters[i] + 1 + traceWitnessed[i] = true } }) @@ -224,6 +228,12 @@ export class Evaluator { } this.recorder.onUserOperatorReturn(stepApp, [], invResult) } + + traceWitnessed.forEach((witnessed, i) => { + if (witnessed) { + traceCounters[i] = traceCounters[i] + 1 + } + }) } } @@ -232,11 +242,11 @@ export class Evaluator { } progressBar.stop() - const outcome: Either = failure - ? left(failure) - : right({ result: { id: 0n, kind: 'bool', value: errorsFound == 0 }, counters: counters }) + const witnessResults = { states: stateCounters, traces: traceCounters } - return outcome + return failure + ? left(failure) + : right({ result: { id: 0n, kind: 'bool', value: errorsFound == 0 }, witnessResults }) } /** diff --git a/quint/src/simulation.ts b/quint/src/simulation.ts index ea2221e79..0019c8d4c 100644 --- a/quint/src/simulation.ts +++ b/quint/src/simulation.ts @@ -39,10 +39,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 + witnessResults: { states: number[]; traces: number[] } } From 050a7b03ee30deaadb8a992dd6c2ba286e9b67ed Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 13 Dec 2024 11:20:23 -0300 Subject: [PATCH 4/9] Fix issue on default and organize --- quint/src/cli.ts | 2 +- quint/src/cliCommands.ts | 37 ++++++++++++++++++++----------------- quint/src/verbosity.ts | 7 +++++++ 3 files changed, 28 insertions(+), 18 deletions(-) diff --git a/quint/src/cli.ts b/quint/src/cli.ts index 223a19372..eebefd88b 100755 --- a/quint/src/cli.ts +++ b/quint/src/cli.ts @@ -276,7 +276,7 @@ const runCmd = { .option('witnesses', { desc: 'space separated list of witnesses to report on (counting for how many states the witness is true)', type: 'array', - default: '[]', + default: [], }) .option('seed', { desc: 'random seed to use for non-deterministic choice', diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index d616d6aac..94b313038 100644 --- a/quint/src/cliCommands.ts +++ b/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, SimulatorOptions, SimulationResult } from './simulation' import { ofItf, toItf } from './itf' import { printExecutionFrameRec, printTrace, terminalWidth } from './graphics' import { verbosity } from './verbosity' @@ -480,6 +480,23 @@ function maybePrintCounterExample(verbosityLevel: number, states: QuintEx[], fra } } +function maybePrintWitnesses( + verbosityLevel: number, + evalResult: Either, + witnesses: string[] +) { + if (verbosity.hasWitnessesOutput(verbosityLevel)) { + evalResult.map(r => { + if (r.witnessResults.states.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') + ) + }) + } +} + /** * Run the simulator. * @@ -612,21 +629,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise { - if (r.witnessResults.states.length > 0) { - console.log(chalk.green('Witnesses:')) - } - r.witnessResults.states.forEach((c, i) => - console.log( - chalk.yellow(prev.args.witnesses[i]), - 'was true for', - c, - 'states and', - r.witnessResults.traces[i], - 'traces' - ) - ) - }) + maybePrintWitnesses(verbosityLevel, evalResult, prev.args.witnesses) return right({ ...simulator, @@ -636,7 +639,6 @@ export async function runSimulator(prev: TypecheckedStage): Promise= 2 }, + /** + * Shall the tool output witnesses counts. + */ + hasWitnessesOutput: (level: number): boolean => { + return level >= 1 + }, + /** * Shall the tool track and output actions that were executed. */ From 11341bfd30a13c372a4109362ca817ede357c7a2 Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 13 Dec 2024 15:23:09 -0300 Subject: [PATCH 5/9] Fix problem on the Tic-Tac-Toe example --- examples/games/tictactoe/tictactoe.qnt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/games/tictactoe/tictactoe.qnt b/examples/games/tictactoe/tictactoe.qnt index 4c272e087..6bfe583ae 100644 --- a/examples/games/tictactoe/tictactoe.qnt +++ b/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, } From 1a6ad1f1a8e73e9e26378e54a0ae57a2fafacb8c Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 13 Dec 2024 15:23:33 -0300 Subject: [PATCH 6/9] Remove state counter and add integration test --- quint/io-cli-tests.md | 19 +++++++++++++++++++ quint/src/cliCommands.ts | 6 ++---- quint/src/runtime/impl/evaluator.ts | 10 +++------- quint/src/simulation.ts | 2 +- 4 files changed, 25 insertions(+), 12 deletions(-) diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index d9777549f..904ad6192 100644 --- a/quint/io-cli-tests.md +++ b/quint/io-cli-tests.md @@ -1461,3 +1461,22 @@ exit $exit_code error: parsing failed ``` +### Prints witnesses counts + + + +``` +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 +``` + + +``` +[ok] No violation found (duration). +Witnesses: +won(X) was witnessed in 98 traces +stalemate was witnessed in 2 traces +Use --seed=0x2b442ab439177 to reproduce. +``` diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index 94b313038..990df07dd 100644 --- a/quint/src/cliCommands.ts +++ b/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')) }) } } diff --git a/quint/src/runtime/impl/evaluator.ts b/quint/src/runtime/impl/evaluator.ts index 2e8005449..4c126b8ff 100644 --- a/quint/src/runtime/impl/evaluator.ts +++ b/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 }) } /** diff --git a/quint/src/simulation.ts b/quint/src/simulation.ts index 0019c8d4c..afcd20757 100644 --- a/quint/src/simulation.ts +++ b/quint/src/simulation.ts @@ -41,5 +41,5 @@ export type Outcome = */ export interface SimulationResult { result: QuintEx - witnessResults: { states: number[]; traces: number[] } + witnessingTraces: number[] } From d7af57e4b589d0576b6da82a2895815969d02e07 Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 16 Dec 2024 16:50:16 -0300 Subject: [PATCH 7/9] Fix linter issues --- quint/src/cliCommands.ts | 2 +- quint/src/simulation.ts | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index 990df07dd..984e83a68 100644 --- a/quint/src/cliCommands.ts +++ b/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, SimulationResult } from './simulation' +import { Outcome, SimulationResult, SimulatorOptions } from './simulation' import { ofItf, toItf } from './itf' import { printExecutionFrameRec, printTrace, terminalWidth } from './graphics' import { verbosity } from './verbosity' diff --git a/quint/src/simulation.ts b/quint/src/simulation.ts index afcd20757..36a612f28 100644 --- a/quint/src/simulation.ts +++ b/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' From ee26adbd1c39d3c52d7cd84d379da465022beff5 Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 16 Dec 2024 16:55:55 -0300 Subject: [PATCH 8/9] Add documentation --- docs/pages/docs/quint.md | 2 ++ quint/src/cli.ts | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/pages/docs/quint.md b/docs/pages/docs/quint.md index 8947bb038..4e3c2ca3a 100644 --- a/docs/pages/docs/quint.md +++ b/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] ``` diff --git a/quint/src/cli.ts b/quint/src/cli.ts index eebefd88b..d3e89f259 100755 --- a/quint/src/cli.ts +++ b/quint/src/cli.ts @@ -274,7 +274,7 @@ const runCmd = { default: 'true', }) .option('witnesses', { - desc: 'space separated list of witnesses to report on (counting for how many states the witness is true)', + desc: 'space separated list of witnesses to report on (counting for how many traces the witness is true)', type: 'array', default: [], }) From 62ab7b8c70d06f717ae9aabee111427cf3bf3774 Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 16 Dec 2024 16:57:49 -0300 Subject: [PATCH 9/9] Add CHANGELOG entry --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index ff4031a4c..ab9110809 100644 --- a/CHANGELOG.md +++ b/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