Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Counting witnesses #1562

Open
wants to merge 10 commits into
base: main
Choose a base branch
from
Next Next commit
Add witnesses argument to quint run
bugarela committed Nov 13, 2024

Verified

This commit was signed with the committer’s verified signature.
bugarela Gabriela Moreira
commit 9c0807c0088cfc0b7e7253394295bcac9460a571
5 changes: 5 additions & 0 deletions quint/src/cli.ts
Original file line number Diff line number Diff line change
@@ -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',
16 changes: 13 additions & 3 deletions quint/src/cliCommands.ts
Original file line number Diff line number Diff line change
@@ -545,20 +545,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 +570,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 +612,12 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
console.log(chalk.gray('Use --verbosity to produce more (or less) output.'))
}
}
evalResult.map(r => {
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<CLIProcedure

case 'violation':
maybePrintCounterExample(verbosityLevel, states, frames)
evalResult.map(r => 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).`))

20 changes: 15 additions & 5 deletions quint/src/runtime/impl/evaluator.ts
Original file line number Diff line number Diff line change
@@ -141,10 +141,11 @@ export class Evaluator {
init: QuintEx,
step: QuintEx,
inv: QuintEx,
witnesses: QuintEx[],
nruns: number,
nsteps: number,
ntraces: number
): Either<QuintError, QuintEx> {
): Either<QuintError, { result: QuintEx; counters: number[] }> {
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<QuintError, QuintEx> = failure
const outcome: Either<QuintError, { result: QuintEx; counters: number[] }> = 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<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)
}
}
}