Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
LinearEquationSolverTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
9
11namespace {
12
13class NativeDoublePowerEnvironment {
14 public:
15 typedef double ValueType;
16 static const bool isExact = false;
17 static storm::Environment createEnvironment() {
19 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
20 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
21 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-10"));
22 return env;
23 }
24};
25
26class NativeDoublePowerRegMultEnvironment {
27 public:
28 typedef double ValueType;
29 static const bool isExact = false;
30 static storm::Environment createEnvironment() {
32 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
33 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
34 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-10"));
36 return env;
37 }
38};
39
40class NativeDoubleSoundValueIterationEnvironment {
41 public:
42 typedef double ValueType;
43 static const bool isExact = false;
44 static storm::Environment createEnvironment() {
46 env.solver().setForceSoundness(true);
47 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
48 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration);
50 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-6"));
51 return env;
52 }
53};
54
55class NativeDoubleOptimisticValueIterationEnvironment {
56 public:
57 typedef double ValueType;
58 static const bool isExact = false;
59 static storm::Environment createEnvironment() {
61 env.solver().setForceSoundness(true);
62 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
63 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::OptimisticValueIteration);
65 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-6"));
66 return env;
67 }
68};
69
70class NativeDoubleIntervalIterationEnvironment {
71 public:
72 typedef double ValueType;
73 static const bool isExact = false;
74 static storm::Environment createEnvironment() {
76 env.solver().setForceSoundness(true);
77 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
78 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::IntervalIteration);
80 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-6"));
81 return env;
82 }
83};
84
85class NativeDoubleJacobiEnvironment {
86 public:
87 typedef double ValueType;
88 static const bool isExact = false;
89 static storm::Environment createEnvironment() {
91 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
92 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi);
93 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-10"));
94 return env;
95 }
96};
97
98class NativeDoubleGaussSeidelEnvironment {
99 public:
100 typedef double ValueType;
101 static const bool isExact = false;
102 static storm::Environment createEnvironment() {
104 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
105 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::GaussSeidel);
106 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-10"));
107 return env;
108 }
109};
110
111class NativeDoubleSorEnvironment {
112 public:
113 typedef double ValueType;
114 static const bool isExact = false;
115 static storm::Environment createEnvironment() {
117 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
118 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
119 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-10"));
120 return env;
121 }
122};
123
124class NativeDoubleWalkerChaeEnvironment {
125 public:
126 typedef double ValueType;
127 static const bool isExact = false;
128 static storm::Environment createEnvironment() {
130 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
131 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
132 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
134 return env;
135 }
136};
137
138class NativeRationalRationalSearchEnvironment {
139 public:
140 typedef storm::RationalNumber ValueType;
141 static const bool isExact = true;
142 static storm::Environment createEnvironment() {
144 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
145 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
146 return env;
147 }
148};
149
150class EliminationRationalEnvironment {
151 public:
152 typedef storm::RationalNumber ValueType;
153 static const bool isExact = true;
154 static storm::Environment createEnvironment() {
156 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Elimination);
157 return env;
158 }
159};
160
161class GmmGmresIluEnvironment {
162 public:
163 typedef double ValueType;
164 static const bool isExact = false;
165 static storm::Environment createEnvironment() {
167 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
168 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
169 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
170 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
171 return env;
172 }
173};
174
175class GmmGmresDiagonalEnvironment {
176 public:
177 typedef double ValueType;
178 static const bool isExact = false;
179 static storm::Environment createEnvironment() {
181 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
182 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
183 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Diagonal);
184 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
185 return env;
186 }
187};
188
189class GmmGmresNoneEnvironment {
190 public:
191 typedef double ValueType;
192 static const bool isExact = false;
193 static storm::Environment createEnvironment() {
195 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
196 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
197 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::None);
198 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
199 return env;
200 }
201};
202
203class GmmBicgstabIluEnvironment {
204 public:
205 typedef double ValueType;
206 static const bool isExact = false;
207 static storm::Environment createEnvironment() {
209 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
210 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Bicgstab);
211 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
212 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
213 return env;
214 }
215};
216
217class GmmQmrDiagonalEnvironment {
218 public:
219 typedef double ValueType;
220 static const bool isExact = false;
221 static storm::Environment createEnvironment() {
223 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
224 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Qmr);
225 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Diagonal);
226 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
227 return env;
228 }
229};
230
231class EigenDGmresDiagonalEnvironment {
232 public:
233 typedef double ValueType;
234 static const bool isExact = false;
235 static storm::Environment createEnvironment() {
237 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
238 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
239 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Diagonal);
240 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
241 return env;
242 }
243};
244
245class EigenGmresIluEnvironment {
246 public:
247 typedef double ValueType;
248 static const bool isExact = false;
249 static storm::Environment createEnvironment() {
251 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
252 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::Gmres);
253 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
254 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
255 return env;
256 }
257};
258
259class EigenBicgstabNoneEnvironment {
260 public:
261 typedef double ValueType;
262 static const bool isExact = false;
263 static storm::Environment createEnvironment() {
265 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
266 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::Bicgstab);
267 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::None);
268 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
269 return env;
270 }
271};
272
273class EigenDoubleLUEnvironment {
274 public:
275 typedef double ValueType;
276 static const bool isExact = false;
277 static storm::Environment createEnvironment() {
279 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
280 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
281 return env;
282 }
283};
284
285class EigenRationalLUEnvironment {
286 public:
287 typedef storm::RationalNumber ValueType;
288 static const bool isExact = true;
289 static storm::Environment createEnvironment() {
291 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
292 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
293 return env;
294 }
295};
296
297class TopologicalEigenRationalLUEnvironment {
298 public:
299 typedef storm::RationalNumber ValueType;
300 static const bool isExact = true;
301 static storm::Environment createEnvironment() {
303 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological);
304 env.solver().topological().setUnderlyingEquationSolverType(storm::solver::EquationSolverType::Eigen);
305 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
306 return env;
307 }
308};
309
310template<typename TestType>
311class LinearEquationSolverTest : public ::testing::Test {
312 public:
313 typedef typename TestType::ValueType ValueType;
314 LinearEquationSolverTest() : _environment(TestType::createEnvironment()) {}
315 storm::Environment const& env() const {
316 return _environment;
317 }
318 ValueType precision() const {
319 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
320 }
321 ValueType parseNumber(std::string const& input) const {
322 return storm::utility::convertNumber<ValueType>(input);
323 }
324
325 private:
326 storm::Environment _environment;
327};
328
329typedef ::testing::Types<NativeDoublePowerEnvironment, NativeDoublePowerRegMultEnvironment, NativeDoubleSoundValueIterationEnvironment,
330 NativeDoubleOptimisticValueIterationEnvironment, NativeDoubleIntervalIterationEnvironment, NativeDoubleJacobiEnvironment,
331 NativeDoubleGaussSeidelEnvironment, NativeDoubleSorEnvironment, NativeDoubleWalkerChaeEnvironment,
332 NativeRationalRationalSearchEnvironment, EliminationRationalEnvironment, GmmGmresIluEnvironment, GmmGmresDiagonalEnvironment,
333 GmmGmresNoneEnvironment, GmmBicgstabIluEnvironment, GmmQmrDiagonalEnvironment, EigenDGmresDiagonalEnvironment,
334 EigenGmresIluEnvironment, EigenBicgstabNoneEnvironment, EigenDoubleLUEnvironment, EigenRationalLUEnvironment,
335 TopologicalEigenRationalLUEnvironment>
337
338TYPED_TEST_SUITE(LinearEquationSolverTest, TestingTypes, );
339
340TYPED_TEST(LinearEquationSolverTest, solveEquationSystem) {
341 typedef typename TestFixture::ValueType ValueType;
342 ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<ValueType> builder);
344 ASSERT_NO_THROW(builder.addNextValue(0, 0, this->parseNumber("1/5")));
345 ASSERT_NO_THROW(builder.addNextValue(0, 1, this->parseNumber("2/5")));
346 ASSERT_NO_THROW(builder.addNextValue(0, 2, this->parseNumber("2/5")));
347 ASSERT_NO_THROW(builder.addNextValue(1, 0, this->parseNumber("1/50")));
348 ASSERT_NO_THROW(builder.addNextValue(1, 1, this->parseNumber("48/50")));
349 ASSERT_NO_THROW(builder.addNextValue(1, 2, this->parseNumber("1/50")));
350 ASSERT_NO_THROW(builder.addNextValue(2, 0, this->parseNumber("4/10")));
351 ASSERT_NO_THROW(builder.addNextValue(2, 1, this->parseNumber("3/10")));
352 ASSERT_NO_THROW(builder.addNextValue(2, 2, this->parseNumber("0")));
353
355 ASSERT_NO_THROW(A = builder.build());
356
357 std::vector<ValueType> x(3);
358 std::vector<ValueType> b = {this->parseNumber("3"), this->parseNumber("-0.01"), this->parseNumber("12")};
359
361 if (factory.getEquationProblemFormat(this->env()) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem) {
363 }
364
365 auto requirements = factory.getRequirements(this->env());
366 requirements.clearUpperBounds();
367 requirements.clearLowerBounds();
368 ASSERT_FALSE(requirements.hasEnabledRequirement());
369 auto solver = factory.create(this->env(), A);
370 solver->setBounds(this->parseNumber("-100"), this->parseNumber("100"));
371 ASSERT_NO_THROW(solver->solveEquations(this->env(), x, b));
372 EXPECT_NEAR(x[0], this->parseNumber("481/9"), this->precision());
373 EXPECT_NEAR(x[1], this->parseNumber("457/9"), this->precision());
374 EXPECT_NEAR(x[2], this->parseNumber("875/18"), this->precision());
375}
376} // namespace
void setPrecision(storm::RationalNumber value)
void setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner value)
void setMethod(storm::solver::EigenLinearEquationSolverMethod value)
SolverEnvironment & solver()
void setMethod(storm::solver::GmmxxLinearEquationSolverMethod value)
void setPrecision(storm::RationalNumber value)
void setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner value)
void setPowerMethodMultiplicationStyle(storm::solver::MultiplicationStyle value)
void setMaximalNumberOfIterations(uint64_t value)
void setMethod(storm::solver::NativeLinearEquationSolverMethod value)
void setPrecision(storm::RationalNumber value)
TopologicalSolverEnvironment & topological()
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
EigenSolverEnvironment & eigen()
NativeSolverEnvironment & native()
GmmxxSolverEnvironment & gmmxx()
void setUnderlyingEquationSolverType(storm::solver::EquationSolverType value)
A class that can be used to build a sparse matrix by adding value by value.
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
A class that holds a possibly non-square matrix in the compressed row storage format.
void convertToEquationSystem()
Transforms the matrix into an equation system.
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