LP solver support - Githubissues

moves-rwth / storm

A Modern Probabilistic Model Checker

https://www.stormchecker.org

GNU General Public License v3.0

135 stars 74 forks source link

LP solver support #536

Closed sjunges closed 4 months ago

sjunges commented 4 months ago

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

sjunges commented 4 months ago

@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 commented 4 months ago

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 commented 4 months ago

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

volkm commented 4 months ago

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.

sjunges commented 4 months ago

@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 commented 4 months ago

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.