storm
storm copied to clipboard
moves-rwth
added the soplex LP solver
The Soplex LP solver allows exact and numeric LP solving and has an academic license.
This commit also shows what to to do if you want to add a new LP solver. The procedure should be similar for SMT solvers.
BTW: I tested the use of Soplex on some benchmarks. I did not yet include options to configure Soplex from command line. We can delay merging until a point where I added those.
I changed the include_soplex.cmake to fix linking on a linux system I tested this on.
If you agree with my changes, this can be merged!
There currently seems to be a bug in Soplex which leads to an error and a confusing message in storm.
For the record, the bug report is here:
https://github.com/scipopt/soplex/issues/7
Using consensus.6.prism from QVBS and the command line
./storm --prism consensus.6.prism --prop 'R{"steps"}min=? [ F "finished"]' --constants K=2 --topological:minmax lp --lpsolver soplex
(i.e. no --exact) I get
Model checking property "steps_min": R[exp]{"steps"}min=? [F "finished"] ...
ERROR (LpMinMaxLinearEquationSolver.cpp:132): Unable to find optimal solution for MinMax equation system.
WARN (model-handling.h:982): Cannot handle property: UnexpectedException: Unable to find optimal solution for MinMax equation system.
Given that consensus is known to be challenging, I assume that soplex is trying to tell us that it detected numerical problems. Can / should we convert this into a warning instead?
So far, our wrapper for soplex behaves as the wrapper for gurobi and expects that the solver converges. However, it may very well be that SoPlex is more precise in notifying us that no precise solution is found.
We can change that behavior for both wrappers, of course. I think that at least a more precise error (or warning) should be emitted.
iirc, we check for some return code. Maybe STORM_LOG_ERROR that code? (or convert it into a human readable string if soplex can do that?)