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

LP solver support #536

Merged
merged 10 commits into from
Jun 1, 2024
Merged

LP solver support #536

merged 10 commits into from
Jun 1, 2024

Conversation

sjunges
Copy link
Contributor

@sjunges sjunges commented May 19, 2024

This PR adds four features towards better support for LP based MDP model checking:

  • Soplex version output in CMAKE
  • Gurobi 11.0.2 support (which is the current version)
  • Disabling gurobi tests from the command line to ensure that we can run CI even if we compile storm with support for Gurobi (but the CI will not have a valid license).
  • Dockerfile updates

and gurobi version 11.0.2 support
M
…bi tests in case storm was compiled with gurobi but there is no valid license available
…cal images on a mac and options to build with soplex/gurobi
@sjunges sjunges requested a review from volkm May 21, 2024 12:55
Copy link
Contributor

@volkm volkm left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, LGTM. Only two smaller comments.

inline void initialize() {
extern bool noGurobi;

inline void initialize(int* argc, char** argv) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I had to lookup how gtest arguments are handled. Maybe add a comment:
// GoogleTest-specific commandline arguments were already processed before and removed from argc/argv

Dockerfile Outdated
@@ -19,6 +20,9 @@ ARG build_type=Release
ARG no_threads=1
# Specify CMake arguments for Storm
ARG cmake_args="-DSTORM_PORTABLE=ON"
# Can be ON/OFF
ARG gurobi_support="ON"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see the point of providing some convenience flags, but could we not use cmake_args instead? Then we have more flexibility to provide any CMake flags. We are also already using cmake_args to define the configurations in the CI.
The other option would be to add more on/off switches for all relevant configurations (spot, MathSAT, Cln, ...)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I dislike the default then, because you need to carefully mimic what is already in the default. But maybe we can add the arguments hardcoded and one may overwrite them (as far as i understand, cmake takes the rightmost definition as the actual one). What do you think?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We only need the PORTABLE flag as default argument to ensure platform independence. Should we simply hard-code this cmake flag and leave cmake_args empty? Then users can always provide their own flags.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

but how do we then set that the default is to include spot, soplex, etc in this build?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah okay, you want to have the dependencies enabled by default. Then I agree that it is better to have separate flags for it.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

After this merge, I will create a new PR for some additional configurations: Spot, MathSat etc. I think it is better to have the changes to the Dockerfile in a separate PR because I should also adapt the deployed CI image then.

@sjunges
Copy link
Contributor Author

sjunges commented May 22, 2024

@volkm As this now seems to compile with Gurobi, we need to add the --noGurobi flag to the tests. How do we do that?

I will make sure that the MILP test also listens to the noGurobi flag.

@volkm
Copy link
Contributor

volkm commented May 22, 2024

One issue: ctest does not forward the arguments to googletest. We are currently using ctest to run all the tests and have a make target "test". There seems to be some workaround for supporting arguments. Another possibility would be to define the extra arguments in cmake when defining the googletest.

One additional small note: warnings on unknown arguments are currently not printed because the log level is set to ERROR.

@sjunges
Copy link
Contributor Author

sjunges commented May 22, 2024

Hmm. I am not so sure how to properly handle this then...

@volkm
Copy link
Contributor

volkm commented May 22, 2024

Maybe not so nice, but we could add a CMake flag DISABLE_GUROBI_TESTS and use that instead of the --nogurobi cmdline flag. We loose flexibility because we have to set the flag at build time, but at least it is working.

Another idea could be to use labels and then exclude tests based on the label.

Even another idea is to use environment variables.

volkm added a commit to volkm/storm that referenced this pull request May 23, 2024
Gurobi should be enabled through PR moves-rwth#536 again.
volkm added a commit to volkm/storm that referenced this pull request May 23, 2024
Gurobi should be enabled through PR moves-rwth#536 again.
sjunges pushed a commit that referenced this pull request May 23, 2024
* Added configuration options to Dockerfile

* Disabled Gurobi in CI such that tests run.

Gurobi should be enabled through PR #536 again.
@sjunges
Copy link
Contributor Author

sjunges commented May 24, 2024

@volkm i now check for the license at the start of every test suite. That also includes test suites which do not need that test, but hey...

@volkm
Copy link
Contributor

volkm commented May 29, 2024

I think it looks good for now. It is a bit overkill to check the license for every test suite, but I agree that it is currently the easiest way to handle the Gurobi license.

@sjunges sjunges merged commit 7390f75 into moves-rwth:master Jun 1, 2024
15 checks passed
@sjunges sjunges deleted the lpsolversupport branch June 1, 2024 20:49
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.

None yet

2 participants