From b3601782a968e01a12a15538dd8045727022cf82 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 2 Dec 2013 17:06:09 +0100 Subject: [PATCH] Added Lp Solver class for glpk and added it as an option in CMakeLists.txt. Former-commit-id: e5c5215a293fbecaf49442e5ca80c7905d5f7c12 --- CMakeLists.txt | 20 ++ .../SparseMarkovAutomatonCslModelChecker.h | 21 ++- ...ractNondeterministicLinearEquationSolver.h | 3 - src/solver/GlpkLpSolver.cpp | 172 ++++++++++++++++++ src/solver/GlpkLpSolver.h | 113 ++++++++++++ src/solver/GurobiLpSolver.cpp | 1 - src/storm.cpp | 4 +- src/utility/StormOptions.cpp | 13 +- src/utility/solver.cpp | 13 +- src/utility/solver.h | 3 +- storm-config.h.in | 3 + 11 files changed, 343 insertions(+), 23 deletions(-) create mode 100644 src/solver/GlpkLpSolver.cpp create mode 100644 src/solver/GlpkLpSolver.h diff --git a/CMakeLists.txt b/CMakeLists.txt index 89615eb3a..31d82172c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -32,6 +32,7 @@ option(USE_INTELTBB "Sets whether the Intel TBB Extensions should be used." OFF) option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precompiled headers)." OFF) option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF) option(USE_LIBCXX "Sets whether the standard library is libc++." OFF) +option(ENABLE_GLPK "Sets whether StoRM is built with support for glpk." OFF) set(GUROBI_ROOT "" CACHE STRING "The root directory of Gurobi (if available).") set(Z3_ROOT "" CACHE STRING "The root directory of Z3 (if available).") set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") @@ -184,6 +185,13 @@ else() set(STORM_CPP_GUROBI_DEF "undef") endif() +# glpk defines +if (ENABLE_GLPK) + set(STORM_CPP_GLPK_DEF "define") +else() + set(STORM_CPP_GLPK_DEF "undef") +endif() + # Z3 Defines if (ENABLE_Z3) set(STORM_CPP_Z3_DEF "define") @@ -359,6 +367,18 @@ if (ENABLE_GUROBI) target_link_libraries(storm-performance-tests "gurobi56") endif(ENABLE_GUROBI) +############################################################# +## +## glpk (optional) +## +############################################################# +if (ENABLE_GLPK) + message (STATUS "StoRM - Linking with glpk") + target_link_libraries(storm "glpk") + target_link_libraries(storm-functional-tests "glpk") + target_link_libraries(storm-performance-tests "glpk") +endif(ENABLE_GLPK) + ############################################################# ## ## Z3 (optional) diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 123503cac..c040b92ed 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -274,9 +274,9 @@ namespace storm { } // Compute the LRA value for the current MEC. - lraValuesForEndComponents.push_back(this->computeLraForMaximalEndComponent(min, transitionMatrix, nondeterministicChoiceIndices, this->getModel().getMarkovianStates(), this->getModel().getExitRates(), goalStates, mec)); + lraValuesForEndComponents.push_back(this->computeLraForMaximalEndComponent(min, transitionMatrix, nondeterministicChoiceIndices, this->getModel().getMarkovianStates(), this->getModel().getExitRates(), goalStates, mec, currentMecIndex)); } - + // For fast transition rewriting, we build some auxiliary data structures. storm::storage::BitVector statesNotContainedInAnyMec = ~statesInMecs; uint_fast64_t firstAuxiliaryStateIndex = statesNotContainedInAnyMec.getNumberOfSetBits(); @@ -388,23 +388,23 @@ namespace storm { // Finalize the matrix and solve the corresponding system of equations. sspMatrix.finalize(); std::vector x(numberOfStatesNotInMecs + mecDecomposition.size()); - std::shared_ptr> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver(); - nondeterministiclinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b, sspNondeterministicChoiceIndices); + nondeterministicLinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b, sspNondeterministicChoiceIndices); // Prepare result vector. std::vector result(this->getModel().getNumberOfStates()); + std::cout << "res " << result << std::endl; + // Set the values for states not contained in MECs. - uint_fast64_t stateIndex = 0; - for (auto state : statesNotContainedInAnyMec) { - result[state] = x[stateIndex]; - ++stateIndex; - } + std::cout << x << std::endl; + storm::utility::vector::setVectorValues(result, statesNotContainedInAnyMec, x); + std::cout << "res " << result << std::endl; // Set the values for all states in MECs. for (auto state : statesInMecs) { result[state] = lraValuesForEndComponents[stateToMecIndexMap[state]]; } + std::cout << "res " << result << std::endl; return result; } @@ -428,9 +428,10 @@ namespace storm { * @param exitRates A vector with exit rates for all states. Exit rates of probabilistic states are assumed to be zero. * @param goalStates A bit vector indicating which states are to be considered as goal states. * @param mec The maximal end component to consider for computing the long-run average. + * @param mecIndex The index of the MEC. * @return The long-run average of being in a goal state for the given MEC. */ - static ValueType computeLraForMaximalEndComponent(bool min, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec) { + static ValueType computeLraForMaximalEndComponent(bool min, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec, uint_fast64_t mecIndex = 0) { std::shared_ptr solver = storm::utility::solver::getLpSolver("LRA for MEC"); solver->setModelSense(min ? storm::solver::LpSolver::MAXIMIZE : storm::solver::LpSolver::MINIMIZE); diff --git a/src/solver/AbstractNondeterministicLinearEquationSolver.h b/src/solver/AbstractNondeterministicLinearEquationSolver.h index 4ab08cf90..2929bb695 100644 --- a/src/solver/AbstractNondeterministicLinearEquationSolver.h +++ b/src/solver/AbstractNondeterministicLinearEquationSolver.h @@ -83,9 +83,6 @@ namespace storm { // LOG4CPLUS_INFO(logger, "Starting iterative solver."); // Set up the environment for the power method. -// auto startTime = std::chrono::high_resolution_clock::now(); -// std::chrono::nanoseconds totalTime(0); - bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { multiplyResult = new std::vector(A.getRowCount()); diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp new file mode 100644 index 000000000..0d51fb590 --- /dev/null +++ b/src/solver/GlpkLpSolver.cpp @@ -0,0 +1,172 @@ +#include "src/solver/GlpkLpSolver.h" + +#ifdef STORM_HAVE_GLPK + +#include + +#include "src/exceptions/InvalidStateException.h" +#include "src/settings/Settings.h" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +namespace storm { + namespace solver { + GlpkLpSolver::GlpkLpSolver(std::string const& name, ModelSense const& modelSense) : LpSolver(modelSense), lp(nullptr), nextVariableIndex(1), nextConstraintIndex(1), isOptimal(false), rowIndices(), columnIndices(), coefficientValues() { + // Create the LP problem for glpk. + lp = glp_create_prob(); + + // Set its name and model sense. + glp_set_prob_name(lp, name.c_str()); + this->setModelSense(modelSense); + + // Because glpk uses 1-based indexing (wtf!?), we need to put dummy elements into the matrix vectors. + rowIndices.push_back(0); + columnIndices.push_back(0); + coefficientValues.push_back(0); + } + + GlpkLpSolver::GlpkLpSolver(std::string const& name) : GlpkLpSolver(name, MINIMIZE) { + // Intentionally left empty. + } + + GlpkLpSolver::~GlpkLpSolver() { + glp_delete_prob(this->lp); + glp_free_env(); + } + + uint_fast64_t GlpkLpSolver::createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { + glp_add_cols(this->lp, 1); + glp_set_col_name(this->lp, nextVariableIndex, name.c_str()); + switch (variableType) { + case LpSolver::BOUNDED: + glp_set_col_bnds(lp, nextVariableIndex, GLP_DB, lowerBound, upperBound); + break; + case LpSolver::UNBOUNDED: + glp_set_col_bnds(lp, nextVariableIndex, GLP_FR, 0, 0); + break; + case LpSolver::UPPER_BOUND: + glp_set_col_bnds(lp, nextVariableIndex, GLP_UP, 0, upperBound); + break; + case LpSolver::LOWER_BOUND: + glp_set_col_bnds(lp, nextVariableIndex, GLP_LO, lowerBound, 0); + break; + } + glp_set_col_kind(this->lp, nextVariableIndex, GLP_CV); + glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient); + ++nextVariableIndex; + + this->isOptimal = false; + + return nextVariableIndex - 1; + } + + uint_fast64_t GlpkLpSolver::createIntegerVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { + uint_fast64_t index = this->createContinuousVariable(name, variableType, lowerBound, upperBound, objectiveFunctionCoefficient); + glp_set_col_kind(this->lp, index, GLP_IV); + return index; + } + + uint_fast64_t GlpkLpSolver::createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) { + uint_fast64_t index = this->createContinuousVariable(name, UNBOUNDED, 0, 1, objectiveFunctionCoefficient); + glp_set_col_kind(this->lp, index, GLP_BV); + return index; + } + + void GlpkLpSolver::addConstraint(std::string const& name, std::vector const& variables, std::vector const& coefficients, BoundType const& boundType, double rightHandSideValue) { + if (variables.size() != coefficients.size()) { + LOG4CPLUS_ERROR(logger, "Sizes of variable indices vector and coefficients vector do not match."); + throw storm::exceptions::InvalidStateException() << "Sizes of variable indices vector and coefficients vector do not match."; + } + + // Add the row that will represent this constraint. + glp_add_rows(this->lp, 1); + glp_set_row_name(this->lp, nextConstraintIndex, name.c_str()); + + // Determine the type of the constraint and add it properly. + bool isUpperBound = boundType == LESS || boundType == LESS_EQUAL; + bool isStrict = boundType == LESS || boundType == GREATER; + switch (boundType) { + case LESS: + glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightHandSideValue - storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + break; + case LESS_EQUAL: + glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightHandSideValue); + break; + case GREATER: + glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightHandSideValue + storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble(), 0); + break; + case GREATER_EQUAL: + glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_LO, rightHandSideValue, 0); + break; + case EQUAL: + glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_FX, rightHandSideValue, rightHandSideValue); + break; + } + + // Record the variables and coefficients in the coefficient matrix. + rowIndices.insert(rowIndices.end(), variables.size(), nextConstraintIndex); + columnIndices.insert(columnIndices.end(), variables.begin(), variables.end()); + coefficientValues.insert(coefficientValues.end(), coefficients.begin(), coefficients.end()); + + ++nextConstraintIndex; + this->isOptimal = false; + } + + void GlpkLpSolver::setModelSense(ModelSense const& newModelSense) { + glp_set_obj_dir(this->lp, newModelSense == MINIMIZE ? GLP_MIN : GLP_MAX); + this->isOptimal = false; + } + + void GlpkLpSolver::optimize() const { + glp_load_matrix(this->lp, rowIndices.size() - 1, rowIndices.data(), columnIndices.data(), coefficientValues.data()); + int error = glp_simplex(this->lp, nullptr); + + if (error != 0) { + LOG4CPLUS_ERROR(logger, "Unable to optimize glpk model (" << error << ")."); + throw storm::exceptions::InvalidStateException() << "Unable to optimize glpk model (" << error << ")."; + } + + this->isOptimal = true; + } + + int_fast64_t GlpkLpSolver::getIntegerValue(uint_fast64_t variableIndex) const { + double value = glp_get_col_prim(this->lp, static_cast(variableIndex)); + + if (std::abs(value - static_cast(value)) <= storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { + // Nothing to do in this case. + } else if (std::abs(value) > storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { + LOG4CPLUS_ERROR(logger, "Illegal value for integer variable in glpk solution (" << value << ")."); + throw storm::exceptions::InvalidStateException() << "Illegal value for integer variable in glpk solution (" << value << ")."; + } + + return static_cast(value); + } + + bool GlpkLpSolver::getBinaryValue(uint_fast64_t variableIndex) const { + double value = glp_get_col_prim(this->lp, static_cast(variableIndex)); + + if (std::abs(value - 1) <= storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { + // Nothing to do in this case. + } else if (std::abs(value) > storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { + LOG4CPLUS_ERROR(logger, "Illegal value for binary variable in Gurobi solution (" << value << ")."); + throw storm::exceptions::InvalidStateException() << "Illegal value for binary variable in Gurobi solution (" << value << ")."; + } + + return static_cast(value); + } + + double GlpkLpSolver::getContinuousValue(uint_fast64_t variableIndex) const { + return glp_get_col_prim(this->lp, static_cast(variableIndex)); + } + + void GlpkLpSolver::writeModelToFile(std::string const& filename) const { + glp_load_matrix(this->lp, rowIndices.size() - 1, rowIndices.data(), columnIndices.data(), coefficientValues.data()); + glp_write_lp(this->lp, 0, filename.c_str()); + } + } +} + +#endif \ No newline at end of file diff --git a/src/solver/GlpkLpSolver.h b/src/solver/GlpkLpSolver.h new file mode 100644 index 000000000..5576b1111 --- /dev/null +++ b/src/solver/GlpkLpSolver.h @@ -0,0 +1,113 @@ +#ifndef STORM_SOLVER_GLPKLPSOLVER_H_ +#define STORM_SOLVER_GLPKLPSOLVER_H_ + +#include "src/solver/LpSolver.h" +#include "src/exceptions/NotImplementedException.h" + +// To detect whether the usage of glpk is possible, this include is neccessary. +#include "storm-config.h" + +#ifdef STORM_HAVE_GLPK +#include +#endif + +namespace storm { + namespace solver { +#ifdef STORM_HAVE_GLPK + class GlpkLpSolver : public LpSolver { + public: + GlpkLpSolver(std::string const& name, ModelSense const& modelSense); + GlpkLpSolver(std::string const& name); + virtual ~GlpkLpSolver(); + + virtual uint_fast64_t createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override; + virtual uint_fast64_t createIntegerVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override; + virtual uint_fast64_t createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override; + + virtual void addConstraint(std::string const& name, std::vector const& variables, std::vector const& coefficients, BoundType const& boundType, double rightHandSideValue) override; + + virtual void setModelSense(ModelSense const& newModelSense) override; + virtual void optimize() const override; + + virtual int_fast64_t getIntegerValue(uint_fast64_t variableIndex) const override; + virtual bool getBinaryValue(uint_fast64_t variableIndex) const override; + virtual double getContinuousValue(uint_fast64_t variableIndex) const override; + + virtual void writeModelToFile(std::string const& filename) const override; + + private: + // The glpk LP problem. + glp_prob* lp; + + // A counter that keeps track of the next free variable index. + uint_fast64_t nextVariableIndex; + + // A counter that keeps track of the next free constraint index. + uint_fast64_t nextConstraintIndex; + + // A flag that stores whether the model was optimized properly. + mutable bool isOptimal; + + // The arrays that store the coefficient matrix of the problem. + std::vector rowIndices; + std::vector columnIndices; + std::vector coefficientValues; + }; +#else + // If glpk is not available, we provide a stub implementation that emits an error if any of its methods is called. + class GlpkLpSolver : public LpSolver { + public: + + GlpkLpSolver(std::string const& name) : LpSolver(MINIMIZE) { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + + virtual GlpkLpSolver() { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + + virtual uint_fast64_t createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + + virtual uint_fast64_t createIntegerVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + + virtual uint_fast64_t createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + + virtual void addConstraint(std::string const& name, std::vector const& variables, std::vector const& coefficients, BoundType const& boundType, double rightHandSideValue) override { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + + virtual void setModelSense(ModelSense const& newModelSense) { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + + virtual void optimize() const override { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + + virtual int_fast64_t getIntegerValue(uint_fast64_t variableIndex) const override { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + + virtual bool getBinaryValue(uint_fast64_t variableIndex) const override { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + + virtual double getContinuousValue(uint_fast64_t variableIndex) const override { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + + virtual void writeModelToFile(std::string const& filename) const override { + throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; + } + }; +#endif + } +} + +#endif /* STORM_SOLVER_GLPKLPSOLVER_H_ */ diff --git a/src/solver/GurobiLpSolver.cpp b/src/solver/GurobiLpSolver.cpp index 6ef9b130d..5b143fe9c 100644 --- a/src/solver/GurobiLpSolver.cpp +++ b/src/solver/GurobiLpSolver.cpp @@ -233,7 +233,6 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ")."; } - bool returnValue = false; if (std::abs(value - 1) <= storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { // Nothing to do in this case. } else if (std::abs(value) > storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { diff --git a/src/storm.cpp b/src/storm.cpp index 6aee44050..0babe7612 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -465,8 +465,8 @@ int main(const int argc, const char* argv[]) { storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(*markovAutomaton, std::shared_ptr>(new storm::solver::AbstractNondeterministicLinearEquationSolver())); std::cout << mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal")) << std::endl; std::cout << mc.checkLongRunAverage(true, markovAutomaton->getLabeledStates("goal")) << std::endl; - std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 0, 1) << std::endl; - std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 1, 2) << std::endl; + // std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 0, 1) << std::endl; + // std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 1, 2) << std::endl; break; } case storm::models::Unknown: diff --git a/src/utility/StormOptions.cpp b/src/utility/StormOptions.cpp index b8985c9c9..39e57a6b9 100644 --- a/src/utility/StormOptions.cpp +++ b/src/utility/StormOptions.cpp @@ -34,10 +34,15 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "If the model contains deadlock states, setting this option will insert self-loops for these states.").build()); - std::vector matrixLibrarys; - matrixLibrarys.push_back("gmm++"); - matrixLibrarys.push_back("native"); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "matrixLibrary", "m", "Sets which matrix library is preferred for numerical operations.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("matrixLibraryName", "The name of a matrix library. Valid values are gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(matrixLibrarys)).setDefaultValueString("gmm++").build()).build()); + std::vector matrixLibraries; + matrixLibraries.push_back("gmm++"); + matrixLibraries.push_back("native"); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "matrixLibrary", "m", "Sets which matrix library is preferred for numerical operations.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("matrixLibraryName", "The name of a matrix library. Valid values are gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(matrixLibraries)).setDefaultValueString("gmm++").build()).build()); + std::vector lpSolvers; + lpSolvers.push_back("gurobi"); + lpSolvers.push_back("glpk"); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "lpSolver", "", "Sets which LP solver is preferred.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("LP solver name", "The name of an available LP solver. Valid values are gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build()); + return true; }); diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 16578aaf8..b6036ae58 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -1,10 +1,21 @@ #include "src/utility/solver.h" +#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" +#include "src/solver/GurobiLpSolver.h" +#include "src/solver/GlpkLpSolver.h" + namespace storm { namespace utility { namespace solver { std::shared_ptr getLpSolver(std::string const& name) { - return std::shared_ptr(new storm::solver::GurobiLpSolver(name)); + std::string const& lpSolver = storm::settings::Settings::getInstance()->getOptionByLongName("lpSolver").getArgument(0).getValueAsString(); + if (lpSolver == "gurobi") { + return std::shared_ptr(new storm::solver::GurobiLpSolver(name)); + } else if (lpSolver == "glpk") { + return std::shared_ptr(new storm::solver::GlpkLpSolver(name)); + } + + throw storm::exceptions::InvalidSettingsException() << "No suitable LP-solver selected."; } template diff --git a/src/utility/solver.h b/src/utility/solver.h index 165ba9c00..0122a49f3 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -2,8 +2,7 @@ #define STORM_UTILITY_SOLVER_H_ #include "src/solver/AbstractNondeterministicLinearEquationSolver.h" -#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" -#include "src/solver/GurobiLpSolver.h" +#include "src/solver/LpSolver.h" #include "src/exceptions/InvalidSettingsException.h" diff --git a/storm-config.h.in b/storm-config.h.in index 08bf0ca38..d44ae122c 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -19,6 +19,9 @@ // Whether Gurobi is available and to be used (define/undef) #@STORM_CPP_GUROBI_DEF@ STORM_HAVE_GUROBI +// Whether GLPK is available and to be used (define/undef) +#@STORM_CPP_GLPK_DEF@ STORM_HAVE_GLPK + // Whether Z3 is available and to be used (define/undef) #@STORM_CPP_Z3_DEF@ STORM_HAVE_Z3