[FEATURE] Assignment annotations

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint

https://apalache-mc.org/

Apache License 2.0

440 stars 40 forks source link

[FEATURE] Assignment annotations #181

Closed konnov closed 4 years ago

konnov commented 4 years ago

Sometimes the assignment finder fails to find assignments because it is buggy: #157

Apart from fixing the bug in #157, we should introduce assignment annotations and let the assignment solver consume them. This will give the users a way to work around bugs. Moreover, some users may find it more convenient to label some expressions as assignments.

konnov commented 4 years ago

See the Apalche operators in https://github.com/informalsystems/apalache/blob/unstable/src/tla/Apalache.tla

konnov commented 4 years ago

@Kukovec when shall we expect the PR?