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

Don't check Inv in state 0 with --init=Inv #1825

Open
nano-o opened this issue May 25, 2022 · 3 comments
Open

Don't check Inv in state 0 with --init=Inv #1825

nano-o opened this issue May 25, 2022 · 3 comments
Labels
feature A new feature or functionality impact-medium Incremental improvement | unblocks non-critical work | saves some time product-owner-triage This should be triaged by the product owner usability UX improvements

Comments

@nano-o
Copy link

nano-o commented May 25, 2022

Apalache checks that Inv holds in state 0 even with option --init=Inv. This is unnecessary but takes time, so I suggest skipping this check.
@nano-o nano-o added the feature A new feature or functionality label May 25, 2022
@konnov konnov added this to the X10: Bugfixing & maintenance milestone Jul 6, 2022
@konnov konnov added the product-owner-triage This should be triaged by the product owner label Jul 13, 2022
@nano-o
Copy link
Author

nano-o commented Aug 22, 2022

Ran into a variant of this again today, where it takes about 10 minutes to check that I /\ J => J... Maybe what would be needed is to first apply some basic simplification rules to discharge obviously tautological goals.

@konnov konnov added the usability UX improvements label Aug 22, 2022
@konnov
Copy link
Contributor

konnov commented Aug 22, 2022 •
edited
Loading

Yeah, totally, it annoys me all the time too. The quick workaround is to pass:

'--tuning-options=search.invariantFilter=1->.*'

@konnov konnov added the impact-medium Incremental improvement | unblocks non-critical work | saves some time label Sep 2, 2022
@will62794
Copy link

+1. I also encountered this as a minor annoyance when checking a larger inductive invariant.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
feature A new feature or functionality impact-medium Incremental improvement | unblocks non-critical work | saves some time product-owner-triage This should be triaged by the product owner usability UX improvements
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@konnov @nano-o @will62794 @shonfeder