diff --git a/CHANGELOG.md b/CHANGELOG.md index 675c1f1bb..aceb4790b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -28,6 +28,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Deprecated ### Removed ### Fixed + +- The seed was not being properly printed when the simulator found some runtime errors (#1524). + ### Security ## v0.22.1 -- 2024-09-25 diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index 27b0cb256..953cf9761 100644 --- a/quint/io-cli-tests.md +++ b/quint/io-cli-tests.md @@ -101,7 +101,7 @@ in the lookup table for the expression with ID 7: ``` -quint typecheck --out typecheck-out-example.json ../examples/language-features/tuples.qnt > /dev/null +quint typecheck --out typecheck-out-example.json ../examples/language-features/tuples.qnt printf "first type: " && cat typecheck-out-example.json | jq '.types."7".type.kind' printf "first effect: " && cat typecheck-out-example.json | jq '.effects."8".effect.kind' rm typecheck-out-example.json @@ -443,8 +443,8 @@ An example execution: [State 4] { n: 12 } [violation] Found an issue (duration). -Use --seed=0x308623f2a48e7 to reproduce. Use --verbosity=3 to show executions. +Use --seed=0x308623f2a48e7 to reproduce. error: Invariant violated ``` @@ -477,8 +477,8 @@ An example execution: [State 4] { action_taken: "OnDivByThree", n: 12, nondet_picks: { } } [violation] Found an issue (duration). -Use --seed=0x308623f2a48e7 to reproduce. Use --verbosity=3 to show executions. +Use --seed=0x308623f2a48e7 to reproduce. error: Invariant violated ``` @@ -508,9 +508,9 @@ An example execution: [State 4] { n: 12 } [ok] No violation found (duration). -Use --seed=0x11 to reproduce. You may increase --max-samples and --max-steps. Use --verbosity to produce more (or less) output. +Use --seed=0x11 to reproduce. ``` ### Repl evaluates coin @@ -589,8 +589,8 @@ An example execution: } [violation] Found an issue (duration). -Use --seed=0x1e352e160ffbb3 to reproduce. Use --verbosity=3 to show executions. +Use --seed=0x1e352e160ffbb3 to reproduce. error: Invariant violated ``` @@ -721,8 +721,8 @@ q::stepAndInvariant => false } [violation] Found an issue (duration). -Use --seed=0x1786e678d460fe to reproduce. Use --verbosity=3 to show executions. +Use --seed=0x1786e678d460fe to reproduce. error: Invariant violated ``` @@ -1164,9 +1164,11 @@ error: Tests failed ### Fail on run with uninitialized constants +FIXME: this should not be a runtime error + ``` -output=$(quint run testFixture/_1041compileConst.qnt 2>&1) +output=$(quint run testFixture/_1041compileConst.qnt --seed=1 2>&1) exit_code=$? echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' \ -e 's#^.*_1041compileConst.qnt#HOME/_1041compileConst.qnt#g' @@ -1180,6 +1182,7 @@ HOME/_1041compileConst.qnt:5:24 - error: [QNT500] Uninitialized const N. Use: im 5: action init = { x' = N } ^ +Use --seed=0x1 to reproduce. error: Runtime error ``` diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index 18616cb2a..a692e490a 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -81,6 +81,7 @@ interface OutputStage { // Possible results from 'run' status?: 'ok' | 'violation' | 'failure' | 'error' trace?: QuintEx[] + seed?: bigint /* Docstrings by definition name by module name */ documentation?: Map> errors?: ErrorMessage[] @@ -104,6 +105,7 @@ const pickOutputStage = ({ ignored, status, trace, + seed, }: ProcedureStage) => { return { stage, @@ -119,6 +121,7 @@ const pickOutputStage = ({ ignored, status, trace, + seed, } } @@ -567,6 +570,10 @@ export async function runSimulator(prev: TypecheckedStage): Promise e.toQuintEx(zerog)) + const frames = recorder.bestTraces[0]?.frame?.subframes + simulator.seed = recorder.bestTraces[0]?.seed + recorder.bestTraces.forEach((trace, index) => { const maybeEvalResult = trace.frame.result if (maybeEvalResult.isLeft()) { @@ -584,9 +591,6 @@ export async function runSimulator(prev: TypecheckedStage): Promise e.toQuintEx(zerog)) - const frames = recorder.bestTraces[0]?.frame?.subframes - const seed = recorder.bestTraces[0]?.seed switch (outcome.status) { case 'error': return cliErr('Runtime error', { @@ -600,7 +604,6 @@ export async function runSimulator(prev: TypecheckedStage): Promise) { result .map(stage => { + const verbosityLevel = deriveVerbosity(stage.args) const outputData = pickOutputStage(stage) if (stage.args.out) { writeToJson(stage.args.out, outputData) + } else if (!stage.args.outItf && outputData.seed && verbosity.hasResults(verbosityLevel)) { + console.log(chalk.gray(`Use --seed=0x${outputData.seed.toString(16)} to reproduce.`)) } process.exit(0) }) .mapLeft(({ msg, stage }) => { const { args, errors, sourceCode } = stage + const verbosityLevel = deriveVerbosity(args) const outputData = pickOutputStage(stage) if (args.out) { writeToJson(args.out, outputData) } else { const finders = createFinders(sourceCode!) uniqWith(errors, isEqual).forEach(err => console.error(formatError(sourceCode, finders, err))) + if (!stage.args.outItf && outputData.seed && verbosity.hasResults(verbosityLevel)) { + console.log(chalk.gray(`Use --seed=0x${outputData.seed.toString(16)} to reproduce.`)) + } console.error(`error: ${msg}`) } process.exit(1)