New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Suggested tweaks to the supported features docs #797
Conversation
docs/src/apalache/features.md
Outdated
@@ -62,7 +62,7 @@ Operator | Supported? | Milestone | Comment | |||
`f[e]` | ✔ | - | | |||
`DOMAIN f` | ✔ | - | | |||
`[ x \in S ↦ e]` | ✔ | - | | |||
`[ S -> T ]` | ✔ | - | Sometimes, the functions sets are expanded | |||
`[ S -> T ]` | ✔ | - | Sometimes, the functions sets are expanded <!-- What does this mean? --> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't know what this comment is supposed to mean or what the impact is on users.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It is confusing. It means that in some cases functions sets are treated purely symbolically, but sometimes the model checker would try to construct an explicit set of functions, which is exponential. Actually, the model checker would just fail there and will not try to construct such a set. So this sentence is not helping the user.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Cool. That helps. How about
Supported, provided the function can be interpreted symbolically
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good! A few things were out of date, so it's good you looked at this doc.
Co-authored-by: Igor Konnov <igor@informal.systems>
Co-authored-by: Igor Konnov <igor@informal.systems>
809a9ee
to
66baeac
Compare
Some clarifications and slight rewording on the documentation of supported features.
There are also two places where I am not sure what is meant, I'll call those out with comments.