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 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..b081a0a5c 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') { 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' }, }, ], }