You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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()
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
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.
The text was updated successfully, but these errors were encountered:
konnov
changed the title
Incompatibility of the Quint simulator with TLA+ on empty sets of maps
Incompatibility of the Quint simulator with TLA+ on empty sets
Oct 3, 2024
This may seem a bit exotic, but it actually happens in practical specs. Consider the following MWE:
Run all combinations with the simulator v0.22.1:
Now, compare it with the TLC REPL:
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.
The text was updated successfully, but these errors were encountered: