Added Lp Solver class for glpk and added it as an option in CMakeLists.txt.

Former-commit-id: e5c5215a29

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)

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<ValueType> x(numberOfStatesNotInMecs + mecDecomposition.size());
-                    std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>();
-                    nondeterministiclinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b, sspNondeterministicChoiceIndices);
+                    nondeterministicLinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b, sspNondeterministicChoiceIndices);
                     
                     // Prepare result vector.
                     std::vector<ValueType> 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<ValueType> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec) {
+                static ValueType computeLraForMaximalEndComponent(bool min, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec, uint_fast64_t mecIndex = 0) {
                     std::shared_ptr<storm::solver::LpSolver> solver = storm::utility::solver::getLpSolver("LRA for MEC");
                     solver->setModelSense(min ? storm::solver::LpSolver::MAXIMIZE : storm::solver::LpSolver::MINIMIZE);
                     

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<Type>(A.getRowCount());

src/solver/GlpkLpSolver.cpp

@@ -0,0 +1,172 @@
+#include "src/solver/GlpkLpSolver.h"
+
+#ifdef STORM_HAVE_GLPK
+
+#include <iostream>
+
+#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<uint_fast64_t> const& variables, std::vector<double> 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<int>(variableIndex));
+            
+            if (std::abs(value - static_cast<int>(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<int_fast64_t>(value);
+        }
+        
+        bool GlpkLpSolver::getBinaryValue(uint_fast64_t variableIndex) const {
+            double value = glp_get_col_prim(this->lp, static_cast<int>(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<bool>(value);
+        }
+        
+        double GlpkLpSolver::getContinuousValue(uint_fast64_t variableIndex) const {
+            return glp_get_col_prim(this->lp, static_cast<int>(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

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 <glpk.h>
+#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<uint_fast64_t> const& variables, std::vector<double> 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<int> rowIndices;
+            std::vector<int> columnIndices;
+            std::vector<double> 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<uint_fast64_t> const& variables, std::vector<double> 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_ */

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()) {

src/storm.cpp

@@ -465,8 +465,8 @@ int main(const int argc, const char* argv[]) {
                     storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker<double> mc(*markovAutomaton, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::AbstractNondeterministicLinearEquationSolver<double>()));
                     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:

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<std::string> 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<std::string> 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<std::string> 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;
 });

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<storm::solver::LpSolver> getLpSolver(std::string const& name) {
-                return std::shared_ptr<storm::solver::LpSolver>(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<storm::solver::LpSolver>(new storm::solver::GurobiLpSolver(name));
+                } else if (lpSolver == "glpk") {
+                    return std::shared_ptr<storm::solver::LpSolver>(new storm::solver::GlpkLpSolver(name));
+                }
+                
+                throw storm::exceptions::InvalidSettingsException() << "No suitable LP-solver selected.";
             }
             
             template<typename ValueType>

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"
 

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