Merge branch 'main' into ivan/mbtVars

informalsystems · Dec 16, 2024 · 8286ee6 · 8286ee6
2 parents 42825c9 + acdd6fb
commit 8286ee6
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 3 deletions.
diff --git a/quint/src/runtime/impl/runtimeValue.ts b/quint/src/runtime/impl/runtimeValue.ts
@@ -1475,10 +1475,18 @@ class RuntimeValueMapSet extends RuntimeValueBase implements RuntimeValue {
     const nindices = domainArr.length
     const nvalues = rangeArr.length
     function* gen() {
-      if (domainArr.length === 0 || rangeArr.length === 0) {
-        // yield nothing as an empty set produces the empty product
+      if (domainArr.length === 0) {
+        // To reflect the behaviour of TLC, an empty domain needs to give Set(Map())
+        yield rv.mkMap([])
+        return
+      }
+
+      if (rangeArr.length === 0) {
+        // To reflect the behaviour of TLC, an empty range needs to give Set()
+        // yields nothing
         return
       }
+
       // generate `nmaps` maps by using number increments
       const nmaps = nvalues ** nindices
       for (let i = 0; i < nmaps; i++) {
@@ -1539,7 +1547,12 @@ class RuntimeValueMapSet extends RuntimeValueBase implements RuntimeValue {
     }
 
     const domainSize = domainSizeResult.value
-    if (domainSize === 0n || (rangeSizeResult.isRight() && rangeSizeResult.value === 0n)) {
+    if (domainSize === 0n) {
+      // To reflect the behaviour of TLC, an empty domain needs to give Set(Map())
+      return right(rv.mkMap([]))
+    }
+
+    if (rangeSizeResult.isRight() && rangeSizeResult.value === 0n) {
       // the set of maps is empty, no way to pick a value
       return left({ code: 'QNT501', message: 'Empty set of maps' })
     }

diff --git a/quint/test/runtime/compile.test.ts b/quint/test/runtime/compile.test.ts
@@ -898,6 +898,12 @@ describe('compiling specs to runtime values', () => {
               Map(2 -> 6, 3 -> 6))`,
         'true'
       )
+      assertResultAsString('Set().setOfMaps(Set(3, 5))', 'Set(Map())')
+
+      assertResultAsString('Set().setOfMaps(Set())', 'Set(Map())')
+
+      assertResultAsString('Set(1, 2).setOfMaps(Set())', 'Set()')
+
       assertResultAsString('Set(2).setOfMaps(5.to(6))', 'Set(Map(Tup(2, 5)), Map(Tup(2, 6)))')
       assertResultAsString('2.to(3).setOfMaps(Set(5))', 'Set(Map(Tup(2, 5), Tup(3, 5)))')
       assertResultAsString('2.to(4).setOfMaps(5.to(8)).size()', '64')