diff --git a/CHANGELOG.md b/CHANGELOG.md index ff4031a4c..40fde10af 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Deprecated ### Removed ### Fixed + +- Fixed a problem where traces other than the first one when `--n-traces` > 1 + and `--mbt` is true had the incorrect `action_taken` and `nondet_picks` values + (#1553). + ### Security ## v0.22.3 -- 2024-10-28 diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index d9777549f..46e7d4910 100644 --- a/quint/io-cli-tests.md +++ b/quint/io-cli-tests.md @@ -894,14 +894,16 @@ rm out-itf-example.itf.json ``` -quint run --out-itf=out-itf-example.itf.json --n-traces=3 --max-steps=5 --seed=123 ../examples/tutorials/coin.qnt +quint run --out-itf=out-itf-example.itf.json --n-traces=3 --mbt --max-steps=5 --seed=123 ../examples/tutorials/coin.qnt cat out-itf-example0.itf.json | jq '.["#meta"].status' +cat out-itf-example1.itf.json | jq '.states[0].action_taken' rm out-itf-example*.itf.json ``` ``` "ok" +"init" ``` ### Run to generate multiple ITF traces with violation diff --git a/quint/src/runtime/impl/VarStorage.ts b/quint/src/runtime/impl/VarStorage.ts index d3b16c71d..78a975f0f 100644 --- a/quint/src/runtime/impl/VarStorage.ts +++ b/quint/src/runtime/impl/VarStorage.ts @@ -140,6 +140,12 @@ export class VarStorage { reset() { this.vars.forEach(reg => (reg.value = initialRegisterValue(reg.name))) this.nextVars.forEach(reg => (reg.value = initialRegisterValue(reg.name))) + if (this.storeMetadata) { + this.actionTaken = undefined + this.nondetPicks.forEach((_, key) => { + this.nondetPicks.set(key, undefined) + }) + } } /**