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.

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

Optimize IMC with Dedicated Solvers for Reachability and Fixed-Point #335

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from

Conversation

KlevisImeri
Copy link

@KlevisImeri KlevisImeri commented Jan 27, 2025

Resolves #299

Things extra to consider:

  • The Fixed-Point solver was named imcFpSolver.

  • Added popAll() method to the SolverBase interface. This makes working with solvers easier. The user of the solver doesn't have to keep track of how many times push() was called when they just want to clear the 'stack'. This needs testing.

  • In ConfigToBoundedChecker.kt, I used the same configuration for the Fixed-Point solver as the one for the itpSolver. This may need to be separated so the Fixed-Point solver can have its own configuration.

@AdamZsofi AdamZsofi self-requested a review January 28, 2025 15:14
@AdamZsofi
Copy link
Member

Thanks for the changes!
Can you maybe mark this PR as a draft for now?
I approved the CI checks - if those work, we'll benchmark and compare the results. Let's talk about that part later in person.

@AdamZsofi
Copy link
Member

AdamZsofi commented Jan 28, 2025

Also, you can use gradlew spotlessApply locally for formatting or manually run the formatting action on github on your fork. There is also an action for bumping the version, although we can also wait with that for now.

@KlevisImeri KlevisImeri marked this pull request as draft January 29, 2025 05:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Suggestion to improve implementation of IMC
2 participants