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

Commits on Aug 7, 2023

  1. Add test that shows the nesting bug 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    42ccd5b View commit details
    Browse the repository at this point in the history

  2. Add finite invariant inference module 

    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 @wilcoxjay
    Alex-Fischman and wilcoxjay committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    d6ace41 View commit details
    Browse the repository at this point in the history

  3. Autoformat 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    209a35a View commit details
    Browse the repository at this point in the history

  4. Add unit test for finite 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    34651f2 View commit details
    Browse the repository at this point in the history

  5. Return Context with Bdd 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    95deab9 View commit details
    Browse the repository at this point in the history

  6. Take an initial universe as input 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    9778909 View commit details
    Browse the repository at this point in the history

  7. Convert BDD to Term 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    42be606 View commit details
    Browse the repository at this point in the history

  8. Build forall term 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    1ff3c90 View commit details
    Browse the repository at this point in the history

  9. Remove verify_module, now blocked on transition system extraction 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    98bd113 View commit details
    Browse the repository at this point in the history

  10. Add MaybeSpannedTerm, plug finite into verify 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    669e865 View commit details
    Browse the repository at this point in the history

  11. Change no-arg Apps to Ids 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    fa37794 View commit details
    Browse the repository at this point in the history

  12. Move bdd_to_term into bdd.rs instead of finite.rs 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    483d150 View commit details
    Browse the repository at this point in the history

  13. Make test not fail 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    f25e969 View commit details
    Browse the repository at this point in the history

  14. Remove finite.rs 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    01b255f View commit details
    Browse the repository at this point in the history

  15. Remove finite from lib.rs 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    d93154c View commit details
    Browse the repository at this point in the history

  16. Add finite.rs 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    22cb416 View commit details
    Browse the repository at this point in the history

  17. Add finite to lib.rs 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    767977d View commit details
    Browse the repository at this point in the history

  18. Add underapproximate(), add better error reporting for verify 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    7c176b8 View commit details
    Browse the repository at this point in the history

  19. Handle full traces in finite.rs 

    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]>
    @wilcoxjay @Alex-Fischman
    wilcoxjay and Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    625333d View commit details
    Browse the repository at this point in the history

  20. Update finite counterexample printing 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    ed95d5b View commit details
    Browse the repository at this point in the history

  21. Figured out bug 

    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
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    7b094e6 View commit details
    Browse the repository at this point in the history

  22. Ignore finite test for now 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    8f0f060 View commit details
    Browse the repository at this point in the history

  23. Reversed works! Remove underapproximate and unignore test 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    0950766 View commit details
    Browse the repository at this point in the history

  24. Reference existing lockserver file instead of copy-paste 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    0dc0dac View commit details
    Browse the repository at this point in the history

  25. Add print_timing bool, add consensus test (that hasn't terminated) 

    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]>
    @wilcoxjay @Alex-Fischman
    wilcoxjay and Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    c4cf478 View commit details
    Browse the repository at this point in the history

  26. Fix finite tests assertions 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    82cbeaf View commit details
    Browse the repository at this point in the history

  27. Add finite CLI, add finite::invariant doc comments 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    c30fb7f View commit details
    Browse the repository at this point in the history

  28. Improve invariant() return type, remember that consensus doesn't have… 

    … a universal invariant

Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    410615d View commit details
    Browse the repository at this point in the history

  29. Inline defs for finite.rs 

    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]>
    @wilcoxjay @Alex-Fischman
    wilcoxjay and Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    ccb7e74 View commit details
    Browse the repository at this point in the history

  30. Make finite return counterexamples instead of printing 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    a81f4d2 View commit details
    Browse the repository at this point in the history

  31. Update finite code to use model back-conversion 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    8d4da5c View commit details
    Browse the repository at this point in the history

  32. Fix errors after rebase 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    a4e1f3f View commit details
    Browse the repository at this point in the history

  33. Fix print {}s 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    1a2f246 View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2023

  1. Fix errors after rebasing 

    Signed-off-by: Alex Fischman <[email protected]>
    @Alex-Fischman
    Alex-Fischman committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    dddcec0 View commit details
    Browse the repository at this point in the history