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

Finite invariants #152

Draft
wants to merge 34 commits into
base: main
Choose a base branch
from
Draft

Finite invariants #152

wants to merge 34 commits into from

Conversation

Alex-Fischman
Copy link
Collaborator

This was an experiment to use the BDD checker's ability to generate the set of all backwards-reachable states to try and come up with an invariant that would hold for any sort sizes. It currently works for lockserver, but the BDD checker is too slow to test it on longer examples. (Also, the current invariant inference part of the implementation can only generate forall invariants.)

Alex-Fischman and others added 30 commits August 7, 2023 12:14
@Alex-Fischman
Add test that shows the nesting bug
42ccd5b 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman @wilcoxjay
Add finite invariant inference module
d6ace41 
Co-authored-by: Alex Fischman <[email protected]>
Co-authored-by: James R. Wilcox <[email protected]>
Signed-off-by: Alex Fischman <[email protected]>
Signed-off-by: James R. Wilcox <[email protected]>
@Alex-Fischman
Autoformat
209a35a 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Add unit test for finite
34651f2 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Return Context with Bdd
95deab9 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Take an initial universe as input
9778909 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Convert BDD to Term
42be606 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Build forall term
1ff3c90 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Remove verify_module, now blocked on transition system extraction
98bd113 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Add MaybeSpannedTerm, plug finite into verify
669e865 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Change no-arg Apps to Ids
fa37794 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Move bdd_to_term into bdd.rs instead of finite.rs
483d150 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Make test not fail
f25e969 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Remove finite.rs
01b255f 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Remove finite from lib.rs
d93154c 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Add finite.rs
22cb416 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Add finite to lib.rs
767977d 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Add underapproximate(), add better error reporting for verify
7c176b8 
Signed-off-by: Alex Fischman <[email protected]>
@wilcoxjay @Alex-Fischman
Handle full traces in finite.rs
625333d 
Co-authored-by: Alex Fischman <[email protected]>
Co-authored-by: James R. Wilcox <[email protected]>
Signed-off-by: Alex Fischman <[email protected]>
Signed-off-by: James R. Wilcox <[email protected]>
@Alex-Fischman
Update finite counterexample printing
ed95d5b 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Figured out bug
7b094e6 
The problem is that it normally isn't possible for no one to have the lock

Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Ignore finite test for now
8f0f060 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Reversed works! Remove underapproximate and unignore test
0950766 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Reference existing lockserver file instead of copy-paste
0dc0dac 
Signed-off-by: Alex Fischman <[email protected]>
@wilcoxjay @Alex-Fischman
Add print_timing bool, add consensus test (that hasn't terminated)
c4cf478 
Co-authored-by: Alex Fischman <[email protected]>
Co-authored-by: James R. Wilcox <[email protected]>
Signed-off-by: Alex Fischman <[email protected]>
Signed-off-by: James R. Wilcox <[email protected]>
@Alex-Fischman
Fix finite tests assertions
82cbeaf 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Add finite CLI, add finite::invariant doc comments
c30fb7f 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Improve invariant() return type, remember that consensus doesn't have…
410615d 
… a universal invariant

Signed-off-by: Alex Fischman <[email protected]>
@wilcoxjay @Alex-Fischman
Inline defs for finite.rs
ccb7e74 
Co-authored-by: Alex Fischman <[email protected]>
Co-authored-by: James R. Wilcox <[email protected]>
Signed-off-by: Alex Fischman <[email protected]>
Signed-off-by: James R. Wilcox <[email protected]>
@Alex-Fischman
Make finite return counterexamples instead of printing
a81f4d2 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Update finite code to use model back-conversion
8d4da5c 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Fix errors after rebase
a4e1f3f 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Fix print {}s
1a2f246 
Signed-off-by: Alex Fischman <[email protected]>
@Alex-Fischman
Fix errors after rebasing
dddcec0 
Signed-off-by: Alex Fischman <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@Alex-Fischman @wilcoxjay