Convert "U_OF_UNIT" from Apalache to the empty tuple

Author: bugarela

quint/src/itf.ts

@@ -189,6 +189,12 @@ 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.

quint/test/itf.test.ts

@@ -88,4 +88,28 @@ describe('toItf', () => {
       `round trip conversion of trace failed`
     )
   })
+
+  it('converts unit type from Apalache', () => {
+    const text = '{ a: () }'
+
+    const trace = [buildExpression(text)]
+    const vars = ['a']
+    const itfTrace = {
+      vars: vars,
+      states: [
+        {
+          '#meta': {
+            index: 0,
+          },
+          a: 'U_OF_UNIT',
+        },
+      ],
+    }
+
+    const roundTripTrace = ofItf(itfTrace)
+    assert(
+      zip(roundTripTrace, trace).every(([a, b]) => quintExAreEqual(a, b)),
+      `round trip conversion of trace failed`
+    )
+  })
 })