Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MinMaxLinearEquationSolverTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "test/storm_gtest.h"
5
12
13namespace {
14
15class DoubleViEnvironment {
16 public:
17 typedef double ValueType;
18 static const bool isExact = false;
19 static storm::Environment createEnvironment() {
21 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
22 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
23 return env;
24 }
25};
26
27class DoubleViRegMultEnvironment {
28 public:
29 typedef double ValueType;
30 static const bool isExact = false;
31 static storm::Environment createEnvironment() {
33 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
34 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
36 return env;
37 }
38};
39
40class DoubleSoundViEnvironment {
41 public:
42 typedef double ValueType;
43 static const bool isExact = false;
44 static storm::Environment createEnvironment() {
46 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
47 env.solver().setForceSoundness(true);
48 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
49 return env;
50 }
51};
52
53class DoubleIntervalIterationEnvironment {
54 public:
55 typedef double ValueType;
56 static const bool isExact = false;
57 static storm::Environment createEnvironment() {
59 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::IntervalIteration);
60 env.solver().setForceSoundness(true);
61 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
62 return env;
63 }
64};
65
66class DoubleOptimisticViEnvironment {
67 public:
68 typedef double ValueType;
69 static const bool isExact = false;
70 static storm::Environment createEnvironment() {
72 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::OptimisticValueIteration);
73 env.solver().setForceSoundness(true);
74 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
75 return env;
76 }
77};
78
79class DoubleTopologicalViEnvironment {
80 public:
81 typedef double ValueType;
82 static const bool isExact = false;
83 static storm::Environment createEnvironment() {
85 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological);
86 env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::ValueIteration);
87 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
88 return env;
89 }
90};
91
92class DoublePIEnvironment {
93 public:
94 typedef double ValueType;
95 static const bool isExact = false;
96 static storm::Environment createEnvironment() {
98 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
99 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
100 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
101 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi);
103 return env;
104 }
105};
106class RationalPIEnvironment {
107 public:
108 typedef storm::RationalNumber ValueType;
109 static const bool isExact = true;
110 static storm::Environment createEnvironment() {
112 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
113 return env;
114 }
115};
116class RationalRationalSearchEnvironment {
117 public:
118 typedef storm::RationalNumber ValueType;
119 static const bool isExact = true;
120 static storm::Environment createEnvironment() {
122 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
123 return env;
124 }
125};
126
127template<typename TestType>
128class MinMaxLinearEquationSolverTest : public ::testing::Test {
129 public:
130 typedef typename TestType::ValueType ValueType;
131 MinMaxLinearEquationSolverTest() : _environment(TestType::createEnvironment()) {}
132 storm::Environment const& env() const {
133 return _environment;
134 }
135 ValueType precision() const {
136 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
137 }
138 ValueType parseNumber(std::string const& input) const {
139 return storm::utility::convertNumber<ValueType>(input);
140 }
141
142 private:
143 storm::Environment _environment;
144};
145
146typedef ::testing::Types<DoubleViEnvironment, DoubleViRegMultEnvironment, DoubleSoundViEnvironment, DoubleIntervalIterationEnvironment,
147 DoubleOptimisticViEnvironment, DoubleTopologicalViEnvironment, DoublePIEnvironment, RationalPIEnvironment,
148 RationalRationalSearchEnvironment>
150
151TYPED_TEST_SUITE(MinMaxLinearEquationSolverTest, TestingTypes, );
152
153TYPED_TEST(MinMaxLinearEquationSolverTest, SolveEquations) {
154 typedef typename TestFixture::ValueType ValueType;
155
156 storm::storage::SparseMatrixBuilder<ValueType> builder(0, 0, 0, false, true);
157 ASSERT_NO_THROW(builder.newRowGroup(0));
158 ASSERT_NO_THROW(builder.addNextValue(0, 0, this->parseNumber("0.9")));
159
161 ASSERT_NO_THROW(A = builder.build(2));
162
163 std::vector<ValueType> x(1);
164 std::vector<ValueType> b = {this->parseNumber("0.099"), this->parseNumber("0.5")};
165
167 auto solver = factory.create(this->env(), A);
168 solver->setHasUniqueSolution(true);
169 solver->setHasNoEndComponents(true);
170 solver->setBounds(this->parseNumber("0"), this->parseNumber("2"));
171 storm::solver::MinMaxLinearEquationSolverRequirements req = solver->getRequirements(this->env());
172 req.clearBounds();
173 ASSERT_FALSE(req.hasEnabledRequirement());
174 ASSERT_NO_THROW(solver->solveEquations(this->env(), storm::OptimizationDirection::Minimize, x, b));
175 EXPECT_NEAR(x[0], this->parseNumber("0.5"), this->precision());
176
177 ASSERT_NO_THROW(solver->solveEquations(this->env(), storm::OptimizationDirection::Maximize, x, b));
178 EXPECT_NEAR(x[0], this->parseNumber("0.99"), this->precision());
179}
180} // namespace
SolverEnvironment & solver()
void setMultiplicationStyle(storm::solver::MultiplicationStyle value)
storm::RationalNumber const & getPrecision() const
void setPrecision(storm::RationalNumber value)
void setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault=false)
void setMethod(storm::solver::NativeLinearEquationSolverMethod value)
TopologicalSolverEnvironment & topological()
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
MinMaxSolverEnvironment & minMax()
void setLinearEquationSolverPrecision(boost::optional< storm::RationalNumber > const &newPrecision, boost::optional< bool > const &relativePrecision=boost::none)
NativeSolverEnvironment & native()
void setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod value)
A class that can be used to build a sparse matrix by adding value by value.
A class that holds a possibly non-square matrix in the compressed row storage format.
SFTBDDChecker::ValueType ValueType
NumberType parseNumber(std::string const &value)
Parse number from string.
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46