Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[FEATURE] Support for ENABLED #800

Open
konnov opened this issue May 4, 2021 · 0 comments
Open

[FEATURE] Support for ENABLED #800

konnov opened this issue May 4, 2021 · 0 comments
Assignees
@p-offtermatt
Labels
effort-medium Can be completed within about 3 days Fliveness Feature: liveness checking impact-medium Incremental improvement | unblocks non-critical work | saves some time
Milestone
X12: Temporal pro...

Comments

@konnov
Copy link
Collaborator

konnov commented May 4, 2021

This is not a priority issue. However, it would help us in making progress towards #488 and #712. From the implementation point of view, the general form of ENABLED A is hard to implement, as it requires an additional existential quantifier and thus may easily lead to quantifier alternation in SMT (which is hard to solve). In practice, it is easy to convert ENABLED A to a predicate over non-primed variables.
@konnov konnov added new New issue to be triaged. Fliveness Feature: liveness checking labels May 4, 2021
@konnov konnov added this to the backlog2021 milestone May 4, 2021
This was referenced May 4, 2021
Open
Open
@p-offtermatt p-offtermatt added impact-medium Incremental improvement | unblocks non-critical work | saves some time effort-medium Can be completed within about 3 days and removed new New issue to be triaged. labels Jun 2, 2022
@p-offtermatt p-offtermatt self-assigned this Jun 2, 2022
@p-offtermatt p-offtermatt linked a pull request Jun 20, 2022 that will close this issue
800 feature support for enabled #1861
Closed
4 tasks
@Kukovec Kukovec mentioned this issue Jul 4, 2022
Closed
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@p-offtermatt p-offtermatt

Labels
effort-medium Can be completed within about 3 days Fliveness Feature: liveness checking impact-medium Incremental improvement | unblocks non-critical work | saves some time
Projects
None yet
Milestone
X12: Temporal properties
Development

Successfully merging a pull request may close this issue.

800 feature support for enabled apalache-mc/apalache
Rewrite enabled apalache-mc/apalache
2 participants
@konnov @p-offtermatt