From 82a8bb7a4bba137be92776e5dddb84f7cebb5867 Mon Sep 17 00:00:00 2001 From: OakenKnight Date: Wed, 13 Nov 2024 18:40:32 +0100 Subject: [PATCH 1/7] fixed broken link for quint-cheatsheet.pdf in README.md --- docs/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From ab8299f1f7e426d22f26b1ef06d2ddf58a503431 Mon Sep 17 00:00:00 2001 From: bugarela Date: Mon, 18 Nov 2024 16:35:51 -0300 Subject: [PATCH 2/7] Properly reset metadata variables --- quint/src/runtime/impl/VarStorage.ts | 6 ++++++ 1 file changed, 6 insertions(+) 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) + }) + } } /** From 40cc216a0bd5c792d4b353b3dcf975727e5b9728 Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 19 Nov 2024 11:36:14 -0300 Subject: [PATCH 3/7] Add test coverage --- quint/io-cli-tests.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 From 28486b1798b39b47f977fc0be1ef7a0289b6c447 Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 19 Nov 2024 11:39:01 -0300 Subject: [PATCH 4/7] Add CHANGELOG entry --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) 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 From 63c79006cd07404f8b012e3200e22631845a865b Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 19 Nov 2024 11:53:24 -0300 Subject: [PATCH 5/7] Release v0.22.4 --- CHANGELOG.md | 9 +++++++++ quint/package-lock.json | 4 ++-- quint/package.json | 2 +- quint/src/version.ts | 2 +- 4 files changed, 13 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 40fde10af..ffcfb5ec0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,15 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## UNRELEASED +### Added +### Changed +### Deprecated +### Removed +### Fixed +### Security + +## v0.22.4 -- 2024-11-19 + ### Added ### Changed ### Deprecated 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/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' From d9009a130e202647d3b00747ad82f08ef0d08586 Mon Sep 17 00:00:00 2001 From: Amyr14 Date: Wed, 11 Dec 2024 17:42:57 -0300 Subject: [PATCH 6/7] Fixed --- quint/src/runtime/impl/runtimeValue.ts | 19 ++++++++++++++++--- quint/test/runtime/compile.test.ts | 4 ++++ 2 files changed, 20 insertions(+), 3 deletions(-) diff --git a/quint/src/runtime/impl/runtimeValue.ts b/quint/src/runtime/impl/runtimeValue.ts index 0957b1dfd..e5cd3c509 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/test/runtime/compile.test.ts b/quint/test/runtime/compile.test.ts index 96068135c..08c666d49 100644 --- a/quint/test/runtime/compile.test.ts +++ b/quint/test/runtime/compile.test.ts @@ -898,6 +898,10 @@ describe('compiling specs to runtime values', () => { Map(2 -> 6, 3 -> 6))`, 'true' ) + assertResultAsString('Set().setOfMaps(Set(3, 5)) == Set(Map())', 'true') + assertResultAsString('Set().setOfMaps(Set()) == Set(Map())', 'true') + assertResultAsString('Set(1, 2).setOfMaps(Set()) == Set()', 'true') + 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') From 7619ce7c02e46bb7de493fbd7b0a458f78f00962 Mon Sep 17 00:00:00 2001 From: Amyr14 Date: Fri, 13 Dec 2024 17:29:26 -0300 Subject: [PATCH 7/7] Suggestions --- quint/src/runtime/impl/runtimeValue.ts | 2 +- quint/test/runtime/compile.test.ts | 8 +++++--- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/quint/src/runtime/impl/runtimeValue.ts b/quint/src/runtime/impl/runtimeValue.ts index e5cd3c509..8e6afe323 100644 --- a/quint/src/runtime/impl/runtimeValue.ts +++ b/quint/src/runtime/impl/runtimeValue.ts @@ -1486,7 +1486,7 @@ class RuntimeValueMapSet extends RuntimeValueBase implements RuntimeValue { // yields nothing return } - + // generate `nmaps` maps by using number increments const nmaps = nvalues ** nindices for (let i = 0; i < nmaps; i++) { diff --git a/quint/test/runtime/compile.test.ts b/quint/test/runtime/compile.test.ts index 08c666d49..4c08b801b 100644 --- a/quint/test/runtime/compile.test.ts +++ b/quint/test/runtime/compile.test.ts @@ -898,9 +898,11 @@ describe('compiling specs to runtime values', () => { Map(2 -> 6, 3 -> 6))`, 'true' ) - assertResultAsString('Set().setOfMaps(Set(3, 5)) == Set(Map())', 'true') - assertResultAsString('Set().setOfMaps(Set()) == Set(Map())', 'true') - assertResultAsString('Set(1, 2).setOfMaps(Set()) == Set()', '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)))')