[FEATURE] Detect well-known unsupported features and point the user to workarounds

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint

https://apalache-mc.org/

Apache License 2.0

441 stars 40 forks source link

[FEATURE] Detect well-known unsupported features and point the user to workarounds #548

Closed konnov closed 2 years ago

konnov commented 3 years ago

Several language features appear quite often in our bug reports. As we cannot support these features in the near future, we should detect these patterns and point the user to the explanations and workaround in the documentation.

[x] a..b for non-constant a and b: #425
[ ] CASE without OTHER: #285
[ ] Expanding sets of functions: #540

lemmy commented 3 years ago

FWIW: You might want to propose your workaround to the PlusCal translator because it generates CASE without OTHER.

konnov commented 2 years ago

We have added a known issue on a..b. The other issues have been fixed, see #738 and #881.