Browse Source

Added functional tests for nondeterministic linear equation solvers. Added functional tests for LPs in addition to the existing MILP tests.

Former-commit-id: 8c0fa08f2d
tempestpy_adaptions
dehnert 11 years ago
parent
commit
36fb44e206
  1. 4
      src/solver/GlpkLpSolver.cpp
  2. 2
      src/solver/GmmxxLinearEquationSolver.cpp
  3. 2
      src/solver/GmmxxNondeterministicLinearEquationSolver.cpp
  4. 2
      src/solver/NativeLinearEquationSolver.cpp
  5. 2
      src/solver/NativeNondeterministicLinearEquationSolver.cpp
  6. 16
      test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
  7. 181
      test/functional/solver/GlpkLpSolverTest.cpp
  8. 68
      test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp
  9. 175
      test/functional/solver/GurobiLpSolverTest.cpp
  10. 23
      test/functional/solver/NativeLinearEquationSolverTest.cpp
  11. 68
      test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp

4
src/solver/GlpkLpSolver.cpp

@ -162,6 +162,8 @@ namespace storm {
} else if (error == GLP_ENODFS) {
this->isUnboundedFlag = true;
error = 0;
} else if (error == GLP_EBOUND) {
throw storm::exceptions::InvalidStateException() << "The bounds of some variables are illegal. Note that glpk only accepts integer bounds for integer variables.";
}
} else {
error = glp_simplex(this->lp, nullptr);
@ -183,7 +185,7 @@ namespace storm {
if (this->modelContainsIntegerVariables) {
return isInfeasibleFlag;
} else {
return glp_get_status(this->lp) == GLP_INFEAS;
return glp_get_status(this->lp) == GLP_INFEAS || glp_get_status(this->lp) == GLP_NOFEAS;
}
}

2
src/solver/GmmxxLinearEquationSolver.cpp

@ -58,7 +58,7 @@ namespace storm {
// Get appropriate settings.
maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger();
precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
relative = settings->isSet("absolute");
relative = !settings->isSet("absolute");
restart = settings->getOptionByLongName("gmmrestart").getArgument(0).getValueAsUnsignedInteger();
// Determine the method to be used.

2
src/solver/GmmxxNondeterministicLinearEquationSolver.cpp

@ -24,7 +24,7 @@ namespace storm {
// Get appropriate settings.
maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger();
precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
relative = settings->isSet("absolute");
relative = !settings->isSet("absolute");
}
template<typename ValueType>

2
src/solver/NativeLinearEquationSolver.cpp

@ -34,7 +34,7 @@ namespace storm {
// Get appropriate settings.
maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger();
precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
relative = settings->isSet("absolute");
relative = !settings->isSet("absolute");
// Determine the method to be used.
std::string const& methodAsString = settings->getOptionByLongName("nativelin").getArgument(0).getValueAsString();

2
src/solver/NativeNondeterministicLinearEquationSolver.cpp

@ -23,7 +23,7 @@ namespace storm {
// Get appropriate settings.
maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger();
precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble();
relative = settings->isSet("absolute");
relative = !settings->isSet("absolute");
}
template<typename ValueType>

16
test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@ -85,7 +85,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*rewardFormula);
ASSERT_LT(std::abs(result[0] - 7.3333323), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done");
@ -94,7 +94,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = mc.checkNoBoundOperator(*rewardFormula);;
ASSERT_LT(std::abs(result[0] - 7.3333323), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
storm::parser::AutoParser<double> stateRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "");
@ -111,7 +111,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
ASSERT_LT(std::abs(result[0] - 7.3333323), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done");
@ -120,7 +120,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
ASSERT_LT(std::abs(result[0] - 7.3333323), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
storm::parser::AutoParser<double> stateAndTransitionRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
@ -137,7 +137,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
ASSERT_LT(std::abs(result[0] - 14.66666611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done");
@ -146,7 +146,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
ASSERT_LT(std::abs(result[0] - 14.66666611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
}
@ -209,7 +209,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*rewardFormula);;
ASSERT_LT(std::abs(result[0] - 4.285709145), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
@ -218,6 +218,6 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = mc.checkNoBoundOperator(*rewardFormula);;
ASSERT_LT(std::abs(result[0] - 4.285709145), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
}

181
test/functional/solver/GlpkLpSolverTest.cpp

@ -5,7 +5,77 @@
#include "src/exceptions/InvalidStateException.h"
#include "src/settings/Settings.h"
TEST(GlpkLpSolver, Optimize) {
TEST(GlpkLpSolver, LPOptimizeMax) {
#ifdef STORM_HAVE_GLPK
storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
ASSERT_NO_THROW(xIndex = solver.createContinuousVariable("x", storm::solver::LpSolver::VariableType::BOUNDED, 0, 1, -1));
uint_fast64_t yIndex;
ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2));
uint_fast64_t zIndex;
ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1));
ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::EQUAL, 5));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5));
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
ASSERT_FALSE(solver.isUnbounded());
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue(xIndex));
ASSERT_LT(std::abs(xValue - 1), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue(yIndex));
ASSERT_LT(std::abs(yValue - 6.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue(zIndex));
ASSERT_LT(std::abs(zValue - 2.75), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_TRUE(false, "StoRM built without glpk support.");
#endif
}
TEST(GlpkLpSolver, LPOptimizeMin) {
#ifdef STORM_HAVE_GLPK
storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::MINIMIZE);
uint_fast64_t xIndex;
ASSERT_NO_THROW(xIndex = solver.createContinuousVariable("x", storm::solver::LpSolver::VariableType::BOUNDED, 0, 1, -1));
uint_fast64_t yIndex;
ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2));
uint_fast64_t zIndex;
ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::BOUNDED, 1, 5.7, -1));
ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5));
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
ASSERT_FALSE(solver.isUnbounded());
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue(xIndex));
ASSERT_LT(std::abs(xValue - 1), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue(yIndex));
ASSERT_LT(std::abs(yValue - 0), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue(zIndex));
ASSERT_LT(std::abs(zValue - 5.7), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_TRUE(false, "StoRM built without glpk support.");
#endif
}
TEST(GlpkLpSolver, MILPOptimizeMax) {
#ifdef STORM_HAVE_GLPK
storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
@ -36,11 +106,78 @@ TEST(GlpkLpSolver, Optimize) {
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - 14), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_TRUE(false, "StoRM built without Gurobi support.");
ASSERT_TRUE(false, "StoRM built without glpk support.");
#endif
}
TEST(GlpkLpSolver, MILPOptimizeMin) {
#ifdef STORM_HAVE_GLPK
storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::MINIMIZE);
uint_fast64_t xIndex;
ASSERT_NO_THROW(xIndex = solver.createBinaryVariable("x", -1));
uint_fast64_t yIndex;
ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2));
uint_fast64_t zIndex;
ASSERT_NO_THROW(zIndex = solver.createIntegerVariable("z", storm::solver::LpSolver::VariableType::BOUNDED, 0, 5, -1));
ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5));
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
ASSERT_FALSE(solver.isUnbounded());
ASSERT_FALSE(solver.isInfeasible());
bool xValue = false;
ASSERT_NO_THROW(xValue = solver.getBinaryValue(xIndex));
ASSERT_EQ(true, xValue);
int_fast64_t yValue = 0;
ASSERT_NO_THROW(yValue = solver.getIntegerValue(yIndex));
ASSERT_EQ(0, yValue);
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue(zIndex));
ASSERT_LT(std::abs(zValue - 5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_TRUE(false, "StoRM built without glpk support.");
#endif
}
TEST(GlpkLpSolver, LPInfeasible) {
#ifdef STORM_HAVE_GLPK
storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
ASSERT_NO_THROW(xIndex = solver.createContinuousVariable("x", storm::solver::LpSolver::VariableType::BOUNDED, 0, 1, -1));
uint_fast64_t yIndex;
ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2));
uint_fast64_t zIndex;
ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1));
ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::EQUAL, 5));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex}, {1}, storm::solver::LpSolver::BoundType::GREATER_EQUAL, 7));
ASSERT_NO_THROW(solver.optimize());
ASSERT_FALSE(solver.isOptimal());
ASSERT_FALSE(solver.isUnbounded());
ASSERT_TRUE(solver.isInfeasible());
double xValue = 0;
ASSERT_THROW(xValue = solver.getContinuousValue(xIndex), storm::exceptions::InvalidStateException);
double yValue = 0;
ASSERT_THROW(yValue = solver.getContinuousValue(yIndex), storm::exceptions::InvalidStateException);
double zValue = 0;
ASSERT_THROW(zValue = solver.getContinuousValue(zIndex), storm::exceptions::InvalidStateException);
double objectiveValue = 0;
ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidStateException);
#else
ASSERT_TRUE(false, "StoRM built without glpk support.");
#endif
}
TEST(GlpkLpSolver, Infeasible) {
TEST(GlpkLpSolver, MILPInfeasible) {
#ifdef STORM_HAVE_GLPK
storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
@ -68,11 +205,41 @@ TEST(GlpkLpSolver, Infeasible) {
double objectiveValue = 0;
ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidStateException);
#else
ASSERT_TRUE(false, "StoRM built without Gurobi support.");
ASSERT_TRUE(false, "StoRM built without glpk support.");
#endif
}
TEST(GlpkLpSolver, Unbounded) {
TEST(GlpkLpSolver, LPUnbounded) {
#ifdef STORM_HAVE_GLPK
storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
ASSERT_NO_THROW(xIndex = solver.createContinuousVariable("x", storm::solver::LpSolver::VariableType::BOUNDED, 0, 1, -1));
uint_fast64_t yIndex;
ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2));
uint_fast64_t zIndex;
ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1));
ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5));
ASSERT_NO_THROW(solver.optimize());
ASSERT_FALSE(solver.isOptimal());
ASSERT_TRUE(solver.isUnbounded());
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_THROW(xValue = solver.getContinuousValue(xIndex), storm::exceptions::InvalidStateException);
double yValue = 0;
ASSERT_THROW(yValue = solver.getContinuousValue(yIndex), storm::exceptions::InvalidStateException);
double zValue = 0;
ASSERT_THROW(zValue = solver.getContinuousValue(zIndex), storm::exceptions::InvalidStateException);
double objectiveValue = 0;
ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidStateException);
#else
ASSERT_TRUE(false, "StoRM built without glpk support.");
#endif
}
TEST(GlpkLpSolver, MILPUnbounded) {
#ifdef STORM_HAVE_GLPK
storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
@ -98,6 +265,6 @@ TEST(GlpkLpSolver, Unbounded) {
double objectiveValue = 0;
ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidStateException);
#else
ASSERT_TRUE(false, "StoRM built without Gurobi support.");
ASSERT_TRUE(false, "StoRM built without glpk support.");
#endif
}
}

68
test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp

@ -0,0 +1,68 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
#include "src/settings/Settings.h"
TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<double> builder);
storm::storage::SparseMatrixBuilder<double> builder;
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
storm::storage::SparseMatrix<double> A;
ASSERT_NO_THROW(A = builder.build(2));
std::vector<uint_fast64_t> nondeterministicChoiceIndices = {0, 2};
std::vector<double> x(1);
std::vector<double> b = {0.099, 0.5};
ASSERT_NO_THROW(storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver);
storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(true, A, x, b, nondeterministicChoiceIndices));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_NO_THROW(solver.solveEquationSystem(false, A, x, b, nondeterministicChoiceIndices));
ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
}
TEST(GmmxxNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<double> builder);
storm::storage::SparseMatrixBuilder<double> builder;
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099));
ASSERT_NO_THROW(builder.addNextValue(0, 2, 0.001));
ASSERT_NO_THROW(builder.addNextValue(1, 1, 0.5));
ASSERT_NO_THROW(builder.addNextValue(1, 2, 0.5));
ASSERT_NO_THROW(builder.addNextValue(2, 1, 1));
ASSERT_NO_THROW(builder.addNextValue(3, 2, 1));
storm::storage::SparseMatrix<double> A;
ASSERT_NO_THROW(A = builder.build());
std::vector<uint_fast64_t> nondeterministicChoiceIndices = {0, 2, 3, 4};
std::vector<double> x = {0, 1, 0};
ASSERT_NO_THROW(storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver);
storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 2));
ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nondeterministicChoiceIndices, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nondeterministicChoiceIndices, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
}

175
test/functional/solver/GurobiLpSolverTest.cpp

@ -5,7 +5,77 @@
#include "src/exceptions/InvalidStateException.h"
#include "src/settings/Settings.h"
TEST(GurobiLpSolver, Optimize) {
TEST(GurobiLpSolver, LPOptimizeMax) {
#ifdef STORM_HAVE_GUROBI
storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
ASSERT_NO_THROW(xIndex = solver.createContinuousVariable("x", storm::solver::LpSolver::VariableType::BOUNDED, 0, 1, -1));
uint_fast64_t yIndex;
ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2));
uint_fast64_t zIndex;
ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1));
ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::EQUAL, 5));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5));
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
ASSERT_FALSE(solver.isUnbounded());
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue(xIndex));
ASSERT_LT(std::abs(xValue - 1), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue(yIndex));
ASSERT_LT(std::abs(yValue - 6.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue(zIndex));
ASSERT_LT(std::abs(zValue - 2.75), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_TRUE(false, "StoRM built without Gurobi support.");
#endif
}
TEST(GurobiLpSolver, LPOptimizeMin) {
#ifdef STORM_HAVE_GUROBI
storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::MINIMIZE);
uint_fast64_t xIndex;
ASSERT_NO_THROW(xIndex = solver.createContinuousVariable("x", storm::solver::LpSolver::VariableType::BOUNDED, 0, 1, -1));
uint_fast64_t yIndex;
ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2));
uint_fast64_t zIndex;
ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::BOUNDED, 1, 5.7, -1));
ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5));
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
ASSERT_FALSE(solver.isUnbounded());
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue(xIndex));
ASSERT_LT(std::abs(xValue - 1), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue(yIndex));
ASSERT_LT(std::abs(yValue - 0), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue(zIndex));
ASSERT_LT(std::abs(zValue - 5.7), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_TRUE(false, "StoRM built without Gurobi support.");
#endif
}
TEST(GurobiLpSolver, MILPOptimizeMax) {
#ifdef STORM_HAVE_GUROBI
storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
@ -40,7 +110,74 @@ TEST(GurobiLpSolver, Optimize) {
#endif
}
TEST(GurobiLpSolver, Infeasible) {
TEST(GurobiLpSolver, MILPOptimizeMin) {
#ifdef STORM_HAVE_GUROBI
storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::MINIMIZE);
uint_fast64_t xIndex;
ASSERT_NO_THROW(xIndex = solver.createBinaryVariable("x", -1));
uint_fast64_t yIndex;
ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2));
uint_fast64_t zIndex;
ASSERT_NO_THROW(zIndex = solver.createIntegerVariable("z", storm::solver::LpSolver::VariableType::BOUNDED, 0, 5.7, -1));
ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5));
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
ASSERT_FALSE(solver.isUnbounded());
ASSERT_FALSE(solver.isInfeasible());
bool xValue = false;
ASSERT_NO_THROW(xValue = solver.getBinaryValue(xIndex));
ASSERT_EQ(true, xValue);
int_fast64_t yValue = 0;
ASSERT_NO_THROW(yValue = solver.getIntegerValue(yIndex));
ASSERT_EQ(0, yValue);
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue(zIndex));
ASSERT_LT(std::abs(zValue - 5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else
ASSERT_TRUE(false, "StoRM built without Gurobi support.");
#endif
}
TEST(GurobiLpSolver, LPInfeasible) {
#ifdef STORM_HAVE_GUROBI
storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
ASSERT_NO_THROW(xIndex = solver.createContinuousVariable("x", storm::solver::LpSolver::VariableType::BOUNDED, 0, 1, -1));
uint_fast64_t yIndex;
ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2));
uint_fast64_t zIndex;
ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1));
ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::EQUAL, 5));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex}, {1}, storm::solver::LpSolver::BoundType::GREATER_EQUAL, 7));
ASSERT_NO_THROW(solver.optimize());
ASSERT_FALSE(solver.isOptimal());
ASSERT_FALSE(solver.isUnbounded());
ASSERT_TRUE(solver.isInfeasible());
double xValue = 0;
ASSERT_THROW(xValue = solver.getContinuousValue(xIndex), storm::exceptions::InvalidStateException);
double yValue = 0;
ASSERT_THROW(yValue = solver.getContinuousValue(yIndex), storm::exceptions::InvalidStateException);
double zValue = 0;
ASSERT_THROW(zValue = solver.getContinuousValue(zIndex), storm::exceptions::InvalidStateException);
double objectiveValue = 0;
ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidStateException);
#else
ASSERT_TRUE(false, "StoRM built without Gurobi support.");
#endif
}
TEST(GurobiLpSolver, MILPInfeasible) {
#ifdef STORM_HAVE_GUROBI
storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
@ -72,7 +209,37 @@ TEST(GurobiLpSolver, Infeasible) {
#endif
}
TEST(GurobiLpSolver, Unbounded) {
TEST(GurobiLpSolver, LPUnbounded) {
#ifdef STORM_HAVE_GUROBI
storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
ASSERT_NO_THROW(xIndex = solver.createContinuousVariable("x", storm::solver::LpSolver::VariableType::BOUNDED, 0, 1, -1));
uint_fast64_t yIndex;
ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2));
uint_fast64_t zIndex;
ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1));
ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12));
ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5));
ASSERT_NO_THROW(solver.optimize());
ASSERT_FALSE(solver.isOptimal());
ASSERT_TRUE(solver.isUnbounded());
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_THROW(xValue = solver.getContinuousValue(xIndex), storm::exceptions::InvalidStateException);
double yValue = 0;
ASSERT_THROW(yValue = solver.getContinuousValue(yIndex), storm::exceptions::InvalidStateException);
double zValue = 0;
ASSERT_THROW(zValue = solver.getContinuousValue(zIndex), storm::exceptions::InvalidStateException);
double objectiveValue = 0;
ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidStateException);
#else
ASSERT_TRUE(false, "StoRM built without Gurobi support.");
#endif
}
TEST(GurobiLpSolver, MILPUnbounded) {
#ifdef STORM_HAVE_GUROBI
storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::MAXIMIZE);
uint_fast64_t xIndex;
@ -100,4 +267,4 @@ TEST(GurobiLpSolver, Unbounded) {
#else
ASSERT_TRUE(false, "StoRM built without Gurobi support.");
#endif
}
}

23
test/functional/solver/NativeLinearEquationSolverTest.cpp

@ -30,4 +30,27 @@ TEST(NativeLinearEquationSolver, SolveWithStandardOptions) {
ASSERT_LT(std::abs(x[0] - 1), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
}
TEST(NativeLinearEquationSolver, MatrixVectorMultplication) {
ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<double> builder);
storm::storage::SparseMatrixBuilder<double> builder;
ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.5));
ASSERT_NO_THROW(builder.addNextValue(0, 4, 0.5));
ASSERT_NO_THROW(builder.addNextValue(1, 2, 0.5));
ASSERT_NO_THROW(builder.addNextValue(1, 4, 0.5));
ASSERT_NO_THROW(builder.addNextValue(2, 3, 0.5));
ASSERT_NO_THROW(builder.addNextValue(2, 4, 0.5));
ASSERT_NO_THROW(builder.addNextValue(3, 4, 1));
ASSERT_NO_THROW(builder.addNextValue(4, 4, 1));
storm::storage::SparseMatrix<double> A;
ASSERT_NO_THROW(A = builder.build());
std::vector<double> x(5);
x[4] = 1;
storm::solver::NativeLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(A, x, nullptr, 4));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
}

68
test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp

@ -0,0 +1,68 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/solver/NativeNondeterministicLinearEquationSolver.h"
#include "src/settings/Settings.h"
TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<double> builder);
storm::storage::SparseMatrixBuilder<double> builder;
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
storm::storage::SparseMatrix<double> A;
ASSERT_NO_THROW(A = builder.build(2));
std::vector<uint_fast64_t> nondeterministicChoiceIndices = {0, 2};
std::vector<double> x(1);
std::vector<double> b = {0.099, 0.5};
ASSERT_NO_THROW(storm::solver::NativeNondeterministicLinearEquationSolver<double> solver);
storm::solver::NativeNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(true, A, x, b, nondeterministicChoiceIndices));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_NO_THROW(solver.solveEquationSystem(false, A, x, b, nondeterministicChoiceIndices));
ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
}
TEST(NativeNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<double> builder);
storm::storage::SparseMatrixBuilder<double> builder;
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099));
ASSERT_NO_THROW(builder.addNextValue(0, 2, 0.001));
ASSERT_NO_THROW(builder.addNextValue(1, 1, 0.5));
ASSERT_NO_THROW(builder.addNextValue(1, 2, 0.5));
ASSERT_NO_THROW(builder.addNextValue(2, 1, 1));
ASSERT_NO_THROW(builder.addNextValue(3, 2, 1));
storm::storage::SparseMatrix<double> A;
ASSERT_NO_THROW(A = builder.build());
std::vector<uint_fast64_t> nondeterministicChoiceIndices = {0, 2, 3, 4};
std::vector<double> x = {0, 1, 0};
ASSERT_NO_THROW(storm::solver::NativeNondeterministicLinearEquationSolver<double> solver);
storm::solver::NativeNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 2));
ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nondeterministicChoiceIndices, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nondeterministicChoiceIndices, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
}
Loading…
Cancel
Save