Incompatibility of the Quint simulator with TLA+ on empty sets

[konnov]

This may seem a bit exotic, but it actually happens in practical specs. Consider the following MWE:

module t {                                                                                                                       
    var myMap: int -> int

    action init = {
        nondet f = Set(1, 2).setOfMaps(Set(4, 5)).oneOf()
        myMap' = f
    }

    action init1 = {
        nondet f = Set().setOfMaps(Set(4, 5)).oneOf()
        myMap' = f
    }

    action init2 = {
        nondet f = Set(1, 2).setOfMaps(Set()).oneOf()
        myMap' = f
    }

    action init3 = {
        nondet f = Set().setOfMaps(Set()).oneOf()
        myMap' = f
    }

    action step = {
        myMap' = myMap
    }
}

Run all combinations with the simulator v0.22.1:

$ quint run --init=init1 t.qnt
t.qnt:10:20 - error: [QNT501] Empty set of maps
10:         nondet f = Set().setOfMaps(Set(4, 5)).oneOf()
                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: Runtime error                                                                                                        /0.3s
$ quint run --init=init2 t.qnt
t.qnt:15:20 - error: [QNT509] Applied oneOf to an empty set
15:         nondet f = Set(1, 2).setOfMaps(Set()).oneOf()
                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: Runtime error                                                                                                        /0.3s
$ quint run --init=init3 t.qnt
t.qnt:20:20 - error: [QNT501] Empty set of maps
20:         nondet f = Set().setOfMaps(Set()).oneOf()
                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Now, compare it with the TLC REPL:

$ java -cp tla2tools.jar tlc2.REPL
(tla+) [{} -> {3, 5}]
{<<>>}
(tla+) [{1, 2} -> {}]
{}
(tla+) [{} -> {}]
{<<>>}

Notice that in the cases (1) and (3), TLC does not produce an empty set, but it produces a singleton set that contains a function of the empty domain, which correspond to Map() in Quint.

The behavior of the Quint simulator is stricter than that of TLC. It would be great to have the cases (1) and (3) fixed.

[bugarela]

I just hit an instance of this myself and it is annoying.

[Amyr14]

Working on it!

[bugarela]

@Amyr14 the equivalent of the behavior from TLC:

$ java -cp tla2tools.jar tlc2.REPL
(tla+) [{} -> {3, 5}]
{<<>>}
(tla+) [{1, 2} -> {}]
{}
(tla+) [{} -> {}]
{<<>>}

in Quint would be:

$ quint
>>> Set().setOfMaps(Set(3,5))
Set(Map())
>>> Set(1,2).setOfMaps(Set())
Set()
>>> Set().setOfMaps(Set())
Set(Map())