Storm 1.11.1.1
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 NativeDoubleGuessingViEnvironment {
86 public:
87 typedef double ValueType;
88 static const bool isExact = false;
89 static storm::Environment createEnvironment() {
91 env.solver().setForceSoundness(true);
92 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
93 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::GuessingValueIteration);
95 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-6"));
96 return env;
97 }
98};
99
100class NativeDoubleJacobiEnvironment {
101 public:
102 typedef double ValueType;
103 static const bool isExact = false;
104 static storm::Environment createEnvironment() {
106 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
107 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi);
108 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-10"));
109 return env;
110 }
111};
112
113class NativeDoubleGaussSeidelEnvironment {
114 public:
115 typedef double ValueType;
116 static const bool isExact = false;
117 static storm::Environment createEnvironment() {
119 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
120 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::GaussSeidel);
121 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-10"));
122 return env;
123 }
124};
125
126class NativeDoubleSorEnvironment {
127 public:
128 typedef double ValueType;
129 static const bool isExact = false;
130 static storm::Environment createEnvironment() {
132 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
133 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
134 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-10"));
135 return env;
136 }
137};
138
139class NativeDoubleWalkerChaeEnvironment {
140 public:
141 typedef double ValueType;
142 static const bool isExact = false;
143 static storm::Environment createEnvironment() {
145 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
146 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
147 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
149 return env;
150 }
151};
152
153class NativeRationalRationalSearchEnvironment {
154 public:
155 typedef storm::RationalNumber ValueType;
156 static const bool isExact = true;
157 static storm::Environment createEnvironment() {
159 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
160 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
161 return env;
162 }
163};
164
165class EliminationRationalEnvironment {
166 public:
167 typedef storm::RationalNumber ValueType;
168 static const bool isExact = true;
169 static storm::Environment createEnvironment() {
171 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Elimination);
172 return env;
173 }
174};
175
176#ifdef STORM_HAVE_GMM
177class GmmGmresIluEnvironment {
178 public:
179 typedef double ValueType;
180 static const bool isExact = false;
181 static storm::Environment createEnvironment() {
183 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
184 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
185 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
186 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
187 return env;
188 }
189};
190
191class GmmGmresDiagonalEnvironment {
192 public:
193 typedef double ValueType;
194 static const bool isExact = false;
195 static storm::Environment createEnvironment() {
197 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
198 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
199 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Diagonal);
200 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
201 return env;
202 }
203};
204
205class GmmGmresNoneEnvironment {
206 public:
207 typedef double ValueType;
208 static const bool isExact = false;
209 static storm::Environment createEnvironment() {
211 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
212 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
213 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::None);
214 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
215 return env;
216 }
217};
218
219class GmmBicgstabIluEnvironment {
220 public:
221 typedef double ValueType;
222 static const bool isExact = false;
223 static storm::Environment createEnvironment() {
225 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
226 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Bicgstab);
227 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
228 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
229 return env;
230 }
231};
232
233class GmmQmrDiagonalEnvironment {
234 public:
235 typedef double ValueType;
236 static const bool isExact = false;
237 static storm::Environment createEnvironment() {
239 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
240 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Qmr);
241 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Diagonal);
242 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
243 return env;
244 }
245};
246#endif
247
248class EigenDGmresDiagonalEnvironment {
249 public:
250 typedef double ValueType;
251 static const bool isExact = false;
252 static storm::Environment createEnvironment() {
254 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
255 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
256 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Diagonal);
257 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
258 return env;
259 }
260};
261
262class EigenGmresIluEnvironment {
263 public:
264 typedef double ValueType;
265 static const bool isExact = false;
266 static storm::Environment createEnvironment() {
268 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
269 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::Gmres);
270 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
271 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
272 return env;
273 }
274};
275
276class EigenBicgstabNoneEnvironment {
277 public:
278 typedef double ValueType;
279 static const bool isExact = false;
280 static storm::Environment createEnvironment() {
282 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
283 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::Bicgstab);
284 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::None);
285 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
286 return env;
287 }
288};
289
290class EigenDoubleLUEnvironment {
291 public:
292 typedef double ValueType;
293 static const bool isExact = false;
294 static storm::Environment createEnvironment() {
296 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
297 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
298 return env;
299 }
300};
301
302class EigenRationalLUEnvironment {
303 public:
304 typedef storm::RationalNumber ValueType;
305 static const bool isExact = true;
306 static storm::Environment createEnvironment() {
308 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
309 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
310 return env;
311 }
312};
313
314class TopologicalEigenRationalLUEnvironment {
315 public:
316 typedef storm::RationalNumber ValueType;
317 static const bool isExact = true;
318 static storm::Environment createEnvironment() {
320 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological);
321 env.solver().topological().setUnderlyingEquationSolverType(storm::solver::EquationSolverType::Eigen);
322 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
323 return env;
324 }
325};
326
327template<typename TestType>
328class LinearEquationSolverTest : public ::testing::Test {
329 public:
330 typedef typename TestType::ValueType ValueType;
331 LinearEquationSolverTest() : _environment(TestType::createEnvironment()) {}
332 storm::Environment const& env() const {
333 return _environment;
334 }
335 ValueType precision() const {
336 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
337 }
338 ValueType parseNumber(std::string const& input) const {
339 return storm::utility::convertNumber<ValueType>(input);
340 }
341
342 private:
343 storm::Environment _environment;
344};
345
346typedef ::testing::Types<NativeDoublePowerEnvironment, NativeDoublePowerRegMultEnvironment, NativeDoubleSoundValueIterationEnvironment,
347 NativeDoubleOptimisticValueIterationEnvironment, NativeDoubleGuessingViEnvironment, NativeDoubleIntervalIterationEnvironment,
348 NativeDoubleJacobiEnvironment, NativeDoubleGaussSeidelEnvironment, NativeDoubleSorEnvironment, NativeDoubleWalkerChaeEnvironment,
349 NativeRationalRationalSearchEnvironment, EliminationRationalEnvironment,
350#ifdef STORM_HAVE_GMM
351 GmmGmresIluEnvironment, GmmGmresDiagonalEnvironment, GmmGmresNoneEnvironment, GmmBicgstabIluEnvironment, GmmQmrDiagonalEnvironment,
352#endif
353 EigenDGmresDiagonalEnvironment, EigenGmresIluEnvironment, EigenBicgstabNoneEnvironment, EigenDoubleLUEnvironment,
354 EigenRationalLUEnvironment, TopologicalEigenRationalLUEnvironment>
356
357TYPED_TEST_SUITE(LinearEquationSolverTest, TestingTypes, );
358
359TYPED_TEST(LinearEquationSolverTest, solveEquationSystem) {
360 typedef typename TestFixture::ValueType ValueType;
361 ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<ValueType> builder);
363 ASSERT_NO_THROW(builder.addNextValue(0, 0, this->parseNumber("1/5")));
364 ASSERT_NO_THROW(builder.addNextValue(0, 1, this->parseNumber("2/5")));
365 ASSERT_NO_THROW(builder.addNextValue(0, 2, this->parseNumber("2/5")));
366 ASSERT_NO_THROW(builder.addNextValue(1, 0, this->parseNumber("1/50")));
367 ASSERT_NO_THROW(builder.addNextValue(1, 1, this->parseNumber("48/50")));
368 ASSERT_NO_THROW(builder.addNextValue(1, 2, this->parseNumber("1/50")));
369 ASSERT_NO_THROW(builder.addNextValue(2, 0, this->parseNumber("4/10")));
370 ASSERT_NO_THROW(builder.addNextValue(2, 1, this->parseNumber("3/10")));
371 ASSERT_NO_THROW(builder.addNextValue(2, 2, this->parseNumber("0")));
372
374 ASSERT_NO_THROW(A = builder.build());
375
376 std::vector<ValueType> x(3);
377 std::vector<ValueType> b = {this->parseNumber("3"), this->parseNumber("-0.01"), this->parseNumber("12")};
378
380 if (factory.getEquationProblemFormat(this->env()) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem) {
382 }
383
384 auto requirements = factory.getRequirements(this->env());
385 requirements.clearUpperBounds();
386 requirements.clearLowerBounds();
387 ASSERT_FALSE(requirements.hasEnabledRequirement());
388 auto solver = factory.create(this->env(), A);
389 solver->setBounds(this->parseNumber("-100"), this->parseNumber("100"));
390 ASSERT_NO_THROW(solver->solveEquations(this->env(), x, b));
391 EXPECT_NEAR(x[0], this->parseNumber("481/9"), this->precision());
392 EXPECT_NEAR(x[1], this->parseNumber("457/9"), this->precision());
393 EXPECT_NEAR(x[2], this->parseNumber("875/18"), this->precision());
394}
395} // 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