Merge pull request #1565 from informalsystems/gabriela/bump-apalache

Bump Apalache to 0.47.2 and update UNIT representation

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

quint/apalache-dist-tests.md

@@ -31,7 +31,7 @@ quint verify --verbosity=1 ../examples/language-features/booleans.qnt | \
 
 <!-- !test out server not running -->
 ```
-Downloading Apalache distribution 0.46.1... done.
+Downloading Apalache distribution 0.47.2... done.
 [ok] No violation found (duration).
 [ok] No violation found (duration).
 ```

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)
 

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
   }
 

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') {

quint/test/itf.test.ts

@@ -101,7 +101,7 @@ describe('toItf', () => {
           '#meta': {
             index: 0,
           },
-          a: 'U_OF_UNIT',
+          a: { tag: 'UNIT' },
         },
       ],
     }