From d730acac14cbdbe8dc5ff6a29da5b6776426e7c7 Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 17 Dec 2024 17:46:18 -0300 Subject: [PATCH 1/3] Bump Apalache to 0.47.2 and update UNIT representation --- quint/apalache-dist-tests.md | 2 +- quint/apalache-tests.md | 6 +++--- quint/src/apalache.ts | 3 ++- quint/src/itf.ts | 11 +++++------ 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/quint/apalache-dist-tests.md b/quint/apalache-dist-tests.md index 8fecfac7d..a9895777c 100644 --- a/quint/apalache-dist-tests.md +++ b/quint/apalache-dist-tests.md @@ -31,7 +31,7 @@ quint verify --verbosity=1 ../examples/language-features/booleans.qnt | \ ``` -Downloading Apalache distribution 0.46.1... done. +Downloading Apalache distribution 0.47.2... done. [ok] No violation found (duration). [ok] No violation found (duration). ``` diff --git a/quint/apalache-tests.md b/quint/apalache-tests.md index 88709f0e2..94043605f 100644 --- a/quint/apalache-tests.md +++ b/quint/apalache-tests.md @@ -249,12 +249,12 @@ VARIABLE x (* - @type: (() => A(UNIT) | B(Int)); + @type: (() => A({ tag: Str }) | B(Int)); *) -A == Variant("A", "U_OF_UNIT") +A == Variant("A", [tag |-> "UNIT"]) (* - @type: ((Int) => A(UNIT) | B(Int)); + @type: ((Int) => A({ tag: Str })) | B(Int)); *) B(__BParam_31) == Variant("B", __BParam_31) diff --git a/quint/src/apalache.ts b/quint/src/apalache.ts index abb44398c..a2aafc7b1 100644 --- a/quint/src/apalache.ts +++ b/quint/src/apalache.ts @@ -75,7 +75,7 @@ export function serverEndpointToConnectionString(endpoint: ServerEndpoint): stri return `${endpoint.hostname}:${endpoint.port}` } -export const DEFAULT_APALACHE_VERSION_TAG = '0.46.1' +export const DEFAULT_APALACHE_VERSION_TAG = '0.47.2' // TODO: used by GitHub api approach: https://github.com/informalsystems/quint/issues/1124 // const APALACHE_TGZ = 'apalache.tgz' @@ -437,6 +437,7 @@ export async function connect( const connectionResult = await tryConnect(serverEndpoint) // We managed to connect, simply return this connection if (connectionResult.isRight()) { + debugLog(verbosityLevel, 'Connecting with existing Apalache server') return connectionResult } diff --git a/quint/src/itf.ts b/quint/src/itf.ts index 51a8723f6..b7d5bb6d4 100644 --- a/quint/src/itf.ts +++ b/quint/src/itf.ts @@ -189,12 +189,6 @@ export function ofItf(itf: ItfTrace): QuintEx[] { if (typeof value === 'boolean') { return { id, kind: 'bool', value } } else if (typeof value === 'string') { - if (value === 'U_OF_UNIT') { - // Apalache converts empty tuples to its unit value, "U_OF_UNIT". - // We need to convert it back to Quint's unit value, the empty tuple. - return { id, kind: 'app', opcode: 'Tup', args: [] } - } - return { id, kind: 'str', value } } else if (isBigint(value)) { // this is the standard way of encoding an integer in ITF. @@ -226,6 +220,11 @@ export function ofItf(itf: ItfTrace): QuintEx[] { } } else if (isVariant(value)) { const l = ofItfValue(value.tag) + if (l.kind === 'str' && l.value === 'UNIT') { + // Apalache converts empty tuples to its unit value, { tag: "UNIT" }. + // We need to convert it back to Quint's unit value, the empty tuple. + return { id, kind: 'app', opcode: 'Tup', args: [] } + } const v = ofItfValue(value.value) return { id, kind: 'app', opcode: 'variant', args: [l, v] } } else if (typeof value === 'object') { From 7bd5c325c244a0e4100b064c5e1b7e79f36b38bf Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 17 Dec 2024 17:51:31 -0300 Subject: [PATCH 2/3] Add CHANGELOG entry --- CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index ffcfb5ec0..b9c3de7fa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,9 +9,15 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Added ### Changed + +- Bumped Apalache to 0.47.2 (#1565) + ### Deprecated ### Removed ### Fixed + +- Fixed a problem where calling `setOfMaps()` on empty sets resulted in errors in the simulator (#1561) + ### Security ## v0.22.4 -- 2024-11-19 From a137bb32f9b0f771ce45ee5496cd0bb71d367148 Mon Sep 17 00:00:00 2001 From: bugarela Date: Wed, 18 Dec 2024 09:19:42 -0300 Subject: [PATCH 3/3] Fix failing tests --- quint/apalache-tests.md | 2 +- quint/test/itf.test.ts | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/quint/apalache-tests.md b/quint/apalache-tests.md index 94043605f..b081a0a5c 100644 --- a/quint/apalache-tests.md +++ b/quint/apalache-tests.md @@ -254,7 +254,7 @@ VARIABLE A == Variant("A", [tag |-> "UNIT"]) (* - @type: ((Int) => A({ tag: Str })) | B(Int)); + @type: ((Int) => A({ tag: Str }) | B(Int)); *) B(__BParam_31) == Variant("B", __BParam_31) diff --git a/quint/test/itf.test.ts b/quint/test/itf.test.ts index 03d490211..f8305e78c 100644 --- a/quint/test/itf.test.ts +++ b/quint/test/itf.test.ts @@ -101,7 +101,7 @@ describe('toItf', () => { '#meta': { index: 0, }, - a: 'U_OF_UNIT', + a: { tag: 'UNIT' }, }, ], }