apalache-mc/apalache

Operator overriding in annotations

konnov opened this issue · 0 comments

This feature request was brought in the discussion.

Currently, Apalache allows the user to specify operator overrides as explained here. For example:

OVERRIDE_BIRTH_YEAR == 80
OVERRIDE_LICENSE_AGE == 18

As Markus suggested, this could look much better if annotations were used, e.g.:

\* @overrides("BIRTH_YEAR")
MY_BIRTH_YEAR == 80
\* @overrides("LICENSE_AGE")
MY_LICENSE_AGE == 18