From 36fb44e206111367e3f1cb21c7af62bba9ec85a2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 17 Dec 2013 11:39:50 +0100 Subject: [PATCH] Added functional tests for nondeterministic linear equation solvers. Added functional tests for LPs in addition to the existing MILP tests. Former-commit-id: 8c0fa08f2d30375a90aaca6d490573f55a600741 --- src/solver/GlpkLpSolver.cpp | 4 +- src/solver/GmmxxLinearEquationSolver.cpp | 2 +- ...xxNondeterministicLinearEquationSolver.cpp | 2 +- src/solver/NativeLinearEquationSolver.cpp | 2 +- ...veNondeterministicLinearEquationSolver.cpp | 2 +- .../SparseMdpPrctlModelCheckerTest.cpp | 16 +- test/functional/solver/GlpkLpSolverTest.cpp | 181 +++++++++++++++++- ...ndeterministicLinearEquationSolverTest.cpp | 68 +++++++ test/functional/solver/GurobiLpSolverTest.cpp | 175 ++++++++++++++++- .../solver/NativeLinearEquationSolverTest.cpp | 23 +++ ...ndeterministicLinearEquationSolverTest.cpp | 68 +++++++ 11 files changed, 519 insertions(+), 24 deletions(-) create mode 100644 test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp create mode 100644 test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp index a9d2b4da0..f7bed4476 100644 --- a/src/solver/GlpkLpSolver.cpp +++ b/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; } } diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index dd6845659..2cb466059 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/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. diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp index f66c520fe..3b7b65341 100644 --- a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp +++ b/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 diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index 21f09203c..959126631 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/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(); diff --git a/src/solver/NativeNondeterministicLinearEquationSolver.cpp b/src/solver/NativeNondeterministicLinearEquationSolver.cpp index 6f7459ef7..78efa5b7c 100644 --- a/src/solver/NativeNondeterministicLinearEquationSolver.cpp +++ b/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 diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 418044ac6..83b4afdb2 100644 --- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/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("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 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("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 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("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("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; } diff --git a/test/functional/solver/GlpkLpSolverTest.cpp b/test/functional/solver/GlpkLpSolverTest.cpp index 72d6311a0..b4dfebe57 100644 --- a/test/functional/solver/GlpkLpSolverTest.cpp +++ b/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 -} +} \ No newline at end of file diff --git a/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp new file mode 100644 index 000000000..58bf724b1 --- /dev/null +++ b/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 builder); + storm::storage::SparseMatrixBuilder builder; + ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); + + storm::storage::SparseMatrix A; + ASSERT_NO_THROW(A = builder.build(2)); + + std::vector nondeterministicChoiceIndices = {0, 2}; + + std::vector x(1); + std::vector b = {0.099, 0.5}; + + ASSERT_NO_THROW(storm::solver::GmmxxNondeterministicLinearEquationSolver solver); + + storm::solver::GmmxxNondeterministicLinearEquationSolver 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 builder); + storm::storage::SparseMatrixBuilder 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 A; + ASSERT_NO_THROW(A = builder.build()); + + std::vector nondeterministicChoiceIndices = {0, 2, 3, 4}; + std::vector x = {0, 1, 0}; + + ASSERT_NO_THROW(storm::solver::GmmxxNondeterministicLinearEquationSolver solver); + + storm::solver::GmmxxNondeterministicLinearEquationSolver 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()); +} \ No newline at end of file diff --git a/test/functional/solver/GurobiLpSolverTest.cpp b/test/functional/solver/GurobiLpSolverTest.cpp index d1cca8e08..06d9bfb33 100644 --- a/test/functional/solver/GurobiLpSolverTest.cpp +++ b/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 -} +} \ No newline at end of file diff --git a/test/functional/solver/NativeLinearEquationSolverTest.cpp b/test/functional/solver/NativeLinearEquationSolverTest.cpp index 3ccfbbf08..9effe7199 100644 --- a/test/functional/solver/NativeLinearEquationSolverTest.cpp +++ b/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 builder); + storm::storage::SparseMatrixBuilder 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 A; + ASSERT_NO_THROW(A = builder.build()); + + std::vector x(5); + x[4] = 1; + + storm::solver::NativeLinearEquationSolver 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()); } \ No newline at end of file diff --git a/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp new file mode 100644 index 000000000..246da6fdf --- /dev/null +++ b/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 builder); + storm::storage::SparseMatrixBuilder builder; + ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); + + storm::storage::SparseMatrix A; + ASSERT_NO_THROW(A = builder.build(2)); + + std::vector nondeterministicChoiceIndices = {0, 2}; + + std::vector x(1); + std::vector b = {0.099, 0.5}; + + ASSERT_NO_THROW(storm::solver::NativeNondeterministicLinearEquationSolver solver); + + storm::solver::NativeNondeterministicLinearEquationSolver 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 builder); + storm::storage::SparseMatrixBuilder 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 A; + ASSERT_NO_THROW(A = builder.build()); + + std::vector nondeterministicChoiceIndices = {0, 2, 3, 4}; + std::vector x = {0, 1, 0}; + + ASSERT_NO_THROW(storm::solver::NativeNondeterministicLinearEquationSolver solver); + + storm::solver::NativeNondeterministicLinearEquationSolver 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()); +} \ No newline at end of file