diff --git a/quint/src/runtime/impl/runtimeValue.ts b/quint/src/runtime/impl/runtimeValue.ts index 0957b1dfd..8e6afe323 100644 --- 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 index 96068135c..4c08b801b 100644 --- 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')