Storm 1.10.0.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
176class GmmGmresIluEnvironment {
177 public:
178 typedef double ValueType;
179 static const bool isExact = false;
180 static storm::Environment createEnvironment() {
182 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
183 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
184 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
185 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
186 return env;
187 }
188};
189
190class GmmGmresDiagonalEnvironment {
191 public:
192 typedef double ValueType;
193 static const bool isExact = false;
194 static storm::Environment createEnvironment() {
196 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
197 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
198 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Diagonal);
199 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
200 return env;
201 }
202};
203
204class GmmGmresNoneEnvironment {
205 public:
206 typedef double ValueType;
207 static const bool isExact = false;
208 static storm::Environment createEnvironment() {
210 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
211 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
212 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::None);
213 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
214 return env;
215 }
216};
217
218class GmmBicgstabIluEnvironment {
219 public:
220 typedef double ValueType;
221 static const bool isExact = false;
222 static storm::Environment createEnvironment() {
224 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
225 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Bicgstab);
226 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
227 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
228 return env;
229 }
230};
231
232class GmmQmrDiagonalEnvironment {
233 public:
234 typedef double ValueType;
235 static const bool isExact = false;
236 static storm::Environment createEnvironment() {
238 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
239 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Qmr);
240 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Diagonal);
241 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
242 return env;
243 }
244};
245
246class EigenDGmresDiagonalEnvironment {
247 public:
248 typedef double ValueType;
249 static const bool isExact = false;
250 static storm::Environment createEnvironment() {
252 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
253 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
254 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Diagonal);
255 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
256 return env;
257 }
258};
259
260class EigenGmresIluEnvironment {
261 public:
262 typedef double ValueType;
263 static const bool isExact = false;
264 static storm::Environment createEnvironment() {
266 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
267 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::Gmres);
268 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
269 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
270 return env;
271 }
272};
273
274class EigenBicgstabNoneEnvironment {
275 public:
276 typedef double ValueType;
277 static const bool isExact = false;
278 static storm::Environment createEnvironment() {
280 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
281 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::Bicgstab);
282 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::None);
283 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber, std::string>("1e-8"));
284 return env;
285 }
286};
287
288class EigenDoubleLUEnvironment {
289 public:
290 typedef double ValueType;
291 static const bool isExact = false;
292 static storm::Environment createEnvironment() {
294 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
295 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
296 return env;
297 }
298};
299
300class EigenRationalLUEnvironment {
301 public:
302 typedef storm::RationalNumber ValueType;
303 static const bool isExact = true;
304 static storm::Environment createEnvironment() {
306 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
307 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
308 return env;
309 }
310};
311
312class TopologicalEigenRationalLUEnvironment {
313 public:
314 typedef storm::RationalNumber ValueType;
315 static const bool isExact = true;
316 static storm::Environment createEnvironment() {
318 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological);
319 env.solver().topological().setUnderlyingEquationSolverType(storm::solver::EquationSolverType::Eigen);
320 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
321 return env;
322 }
323};
324
325template<typename TestType>
326class LinearEquationSolverTest : public ::testing::Test {
327 public:
328 typedef typename TestType::ValueType ValueType;
329 LinearEquationSolverTest() : _environment(TestType::createEnvironment()) {}
330 storm::Environment const& env() const {
331 return _environment;
332 }
333 ValueType precision() const {
334 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
335 }
336 ValueType parseNumber(std::string const& input) const {
337 return storm::utility::convertNumber<ValueType>(input);
338 }
339
340 private:
341 storm::Environment _environment;
342};
343
344typedef ::testing::Types<NativeDoublePowerEnvironment, NativeDoublePowerRegMultEnvironment, NativeDoubleSoundValueIterationEnvironment,
345 NativeDoubleOptimisticValueIterationEnvironment, NativeDoubleGuessingViEnvironment, NativeDoubleIntervalIterationEnvironment,
346 NativeDoubleJacobiEnvironment, NativeDoubleGaussSeidelEnvironment, NativeDoubleSorEnvironment, NativeDoubleWalkerChaeEnvironment,
347 NativeRationalRationalSearchEnvironment, EliminationRationalEnvironment,
348#ifdef STORM_HAVE_GMM
349 GmmGmresIluEnvironment, GmmGmresDiagonalEnvironment, GmmGmresNoneEnvironment, GmmBicgstabIluEnvironment, GmmQmrDiagonalEnvironment,
350#endif
351 EigenDGmresDiagonalEnvironment, EigenGmresIluEnvironment, EigenBicgstabNoneEnvironment, EigenDoubleLUEnvironment,
352 EigenRationalLUEnvironment, TopologicalEigenRationalLUEnvironment>
354
355TYPED_TEST_SUITE(LinearEquationSolverTest, TestingTypes, );
356
357TYPED_TEST(LinearEquationSolverTest, solveEquationSystem) {
358 typedef typename TestFixture::ValueType ValueType;
359 ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<ValueType> builder);
361 ASSERT_NO_THROW(builder.addNextValue(0, 0, this->parseNumber("1/5")));
362 ASSERT_NO_THROW(builder.addNextValue(0, 1, this->parseNumber("2/5")));
363 ASSERT_NO_THROW(builder.addNextValue(0, 2, this->parseNumber("2/5")));
364 ASSERT_NO_THROW(builder.addNextValue(1, 0, this->parseNumber("1/50")));
365 ASSERT_NO_THROW(builder.addNextValue(1, 1, this->parseNumber("48/50")));
366 ASSERT_NO_THROW(builder.addNextValue(1, 2, this->parseNumber("1/50")));
367 ASSERT_NO_THROW(builder.addNextValue(2, 0, this->parseNumber("4/10")));
368 ASSERT_NO_THROW(builder.addNextValue(2, 1, this->parseNumber("3/10")));
369 ASSERT_NO_THROW(builder.addNextValue(2, 2, this->parseNumber("0")));
370
372 ASSERT_NO_THROW(A = builder.build());
373
374 std::vector<ValueType> x(3);
375 std::vector<ValueType> b = {this->parseNumber("3"), this->parseNumber("-0.01"), this->parseNumber("12")};
376
378 if (factory.getEquationProblemFormat(this->env()) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem) {
380 }
381
382 auto requirements = factory.getRequirements(this->env());
383 requirements.clearUpperBounds();
384 requirements.clearLowerBounds();
385 ASSERT_FALSE(requirements.hasEnabledRequirement());
386 auto solver = factory.create(this->env(), A);
387 solver->setBounds(this->parseNumber("-100"), this->parseNumber("100"));
388 ASSERT_NO_THROW(solver->solveEquations(this->env(), x, b));
389 EXPECT_NEAR(x[0], this->parseNumber("481/9"), this->precision());
390 EXPECT_NEAR(x[1], this->parseNumber("457/9"), this->precision());
391 EXPECT_NEAR(x[2], this->parseNumber("875/18"), this->precision());
392}
393} // 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