diff --git a/CHANGELOG.md b/CHANGELOG.md index ab9110809..7cd1dade3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -17,6 +17,20 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Fixed ### Security +## v0.22.4 -- 2024-11-19 + +### Added +### Changed +### 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 ### Added diff --git a/docs/README.md b/docs/README.md index 97e4ef5cf..3b49ed1d2 100644 --- a/docs/README.md +++ b/docs/README.md @@ -4,7 +4,7 @@ - [Language tutorials](../tutorials/README.md) - [Syntax specification](./lang.md) -- [Cheatsheet](./quint-cheatsheet.pdf) +- [Cheatsheet](./public/quint-cheatsheet.pdf) - [API documentation for built-in operators](./builtin.md) ## Tooling diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index 904ad6192..5aacec869 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/package-lock.json b/quint/package-lock.json index b572f4418..d88ada13a 100644 --- a/quint/package-lock.json +++ b/quint/package-lock.json @@ -1,12 +1,12 @@ { "name": "@informalsystems/quint", - "version": "0.22.3", + "version": "0.22.4", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "@informalsystems/quint", - "version": "0.22.3", + "version": "0.22.4", "license": "Apache 2.0", "dependencies": { "@grpc/grpc-js": "^1.11.1", diff --git a/quint/package.json b/quint/package.json index 937cc7853..a6a1a9824 100644 --- a/quint/package.json +++ b/quint/package.json @@ -1,6 +1,6 @@ { "name": "@informalsystems/quint", - "version": "0.22.3", + "version": "0.22.4", "description": "Core tool for the Quint specification language", "keywords": [ "temporal", 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) + }) + } } /** diff --git a/quint/src/runtime/impl/runtimeValue.ts b/quint/src/runtime/impl/runtimeValue.ts index 0957b1dfd..8e6afe323 100644 --- a/quint/src/runtime/impl/runtimeValue.ts +++ b/quint/src/runtime/impl/runtimeValue.ts @@ -1475,10 +1475,18 @@ class RuntimeValueMapSet extends RuntimeValueBase implements RuntimeValue { const nindices = domainArr.length const nvalues = rangeArr.length function* gen() { - if (domainArr.length === 0 || rangeArr.length === 0) { - // yield nothing as an empty set produces the empty product + if (domainArr.length === 0) { + // To reflect the behaviour of TLC, an empty domain needs to give Set(Map()) + yield rv.mkMap([]) + return + } + + if (rangeArr.length === 0) { + // To reflect the behaviour of TLC, an empty range needs to give Set() + // yields nothing return } + // generate `nmaps` maps by using number increments const nmaps = nvalues ** nindices for (let i = 0; i < nmaps; i++) { @@ -1539,7 +1547,12 @@ class RuntimeValueMapSet extends RuntimeValueBase implements RuntimeValue { } const domainSize = domainSizeResult.value - if (domainSize === 0n || (rangeSizeResult.isRight() && rangeSizeResult.value === 0n)) { + if (domainSize === 0n) { + // To reflect the behaviour of TLC, an empty domain needs to give Set(Map()) + return right(rv.mkMap([])) + } + + if (rangeSizeResult.isRight() && rangeSizeResult.value === 0n) { // the set of maps is empty, no way to pick a value return left({ code: 'QNT501', message: 'Empty set of maps' }) } diff --git a/quint/src/version.ts b/quint/src/version.ts index 12f4b8264..077c8d29c 100644 --- a/quint/src/version.ts +++ b/quint/src/version.ts @@ -1,2 +1,2 @@ // Generated by genversion. -export const version = '0.22.3' +export const version = '0.22.4' diff --git a/quint/test/runtime/compile.test.ts b/quint/test/runtime/compile.test.ts index 96068135c..4c08b801b 100644 --- a/quint/test/runtime/compile.test.ts +++ b/quint/test/runtime/compile.test.ts @@ -898,6 +898,12 @@ describe('compiling specs to runtime values', () => { Map(2 -> 6, 3 -> 6))`, 'true' ) + assertResultAsString('Set().setOfMaps(Set(3, 5))', 'Set(Map())') + + assertResultAsString('Set().setOfMaps(Set())', 'Set(Map())') + + assertResultAsString('Set(1, 2).setOfMaps(Set())', 'Set()') + assertResultAsString('Set(2).setOfMaps(5.to(6))', 'Set(Map(Tup(2, 5)), Map(Tup(2, 6)))') assertResultAsString('2.to(3).setOfMaps(Set(5))', 'Set(Map(Tup(2, 5), Tup(3, 5)))') assertResultAsString('2.to(4).setOfMaps(5.to(8)).size()', '64')