Bump Apalache to 0.47.2 and update UNIT representation

informalsystems · Dec 17, 2024 · d730aca · d730aca
1 parent acdd6fb
commit d730aca
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 11 deletions.
diff --git 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 | \
 
 <!-- !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).
 ```
diff --git 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
@@ -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
@@ -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') {