Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
LraDtmcPrctlModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-parsers/parser/FormulaParser.h"
5#include "storm/logic/Formulas.h"
6#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
7#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
8#include "storm/models/sparse/StandardRewardModel.h"
9#include "storm/settings/SettingMemento.h"
10#include "storm/settings/SettingsManager.h"
11#include "storm/settings/modules/GeneralSettings.h"
12#include "storm/solver/NativeLinearEquationSolver.h"
13
14#include "storm/environment/solver/EigenSolverEnvironment.h"
15#include "storm/environment/solver/GmmxxSolverEnvironment.h"
16#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
17#include "storm/environment/solver/NativeSolverEnvironment.h"
18
19#include "storm-parsers/parser/AutoParser.h"
20#include "storm/builder/ExplicitModelBuilder.h"
21
22namespace {
23
24#ifdef STORM_HAVE_GMM
25class GBGmmxxDoubleGmresEnvironment {
26 public:
27 typedef double ValueType;
28 static const bool isExact = false;
29 static storm::Environment createEnvironment() {
30 storm::Environment env;
31 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
32 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
33 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
34 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
35 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
36 env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
37 return env;
38 }
39};
40
41class GBEigenDoubleDGmresEnvironment {
42 public:
43 typedef double ValueType;
44 static const bool isExact = false;
45 static storm::Environment createEnvironment() {
46 storm::Environment env;
47 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
48 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
49 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
50 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
51 env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
52 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
53 return env;
54 }
55};
56#endif
57
58class GBEigenRationalLUEnvironment {
59 public:
60 typedef storm::RationalNumber ValueType;
61 static const bool isExact = true;
62 static storm::Environment createEnvironment() {
63 storm::Environment env;
64 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
65 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
66 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
67 return env;
68 }
69};
70
71class GBNativeSorEnvironment {
72 public:
73 typedef double ValueType;
74 static const bool isExact = false;
75 static storm::Environment createEnvironment() {
76 storm::Environment env;
77 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
78 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
79 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
80 env.solver().native().setSorOmega(storm::utility::convertNumber<storm::RationalNumber>(0.8)); // A test fails if this is set to 0.9...
81 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
82 env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
83 return env;
84 }
85};
86
87class GBNativeWalkerChaeEnvironment {
88 public:
89 typedef double ValueType;
90 static const bool isExact = false;
91 static storm::Environment createEnvironment() {
92 storm::Environment env;
93 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
94 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
95 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
96 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
97 env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
98 env.solver().native().setMaximalNumberOfIterations(50000);
99 return env;
100 }
101};
102
103#ifdef STORM_HAVE_GMM
104class DistrGmmxxDoubleGmresEnvironment {
105 public:
106 typedef double ValueType;
107 static const bool isExact = false;
108 static storm::Environment createEnvironment() {
109 storm::Environment env;
110 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::LraDistributionEquations);
111 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
112 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
113 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
114 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
115 env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
116 return env;
117 }
118};
119#endif
120
121class DistrEigenRationalLUEnvironment {
122 public:
123 typedef storm::RationalNumber ValueType;
124 static const bool isExact = true;
125 static storm::Environment createEnvironment() {
126 storm::Environment env;
127 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::LraDistributionEquations);
128 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
129 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
130 return env;
131 }
132};
133
134class DistrNativeWalkerChaeEnvironment {
135 public:
136 typedef double ValueType;
137 static const bool isExact = false;
138 static storm::Environment createEnvironment() {
139 storm::Environment env;
140 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
141 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
142 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
143 env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
144 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
145 env.solver().native().setMaximalNumberOfIterations(50000);
146 return env;
147 }
148};
149
150class ValueIterationEnvironment {
151 public:
152 typedef double ValueType;
153 static const bool isExact = false;
154 static storm::Environment createEnvironment() {
155 storm::Environment env;
156 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::ValueIteration);
157 env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
158 return env;
159 }
160};
161
162template<typename TestType>
163class LraDtmcPrctlModelCheckerTest : public ::testing::Test {
164 public:
165 typedef typename TestType::ValueType ValueType;
166 LraDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
167 storm::Environment const& env() const {
168 return _environment;
169 }
170 ValueType parseNumber(std::string const& input) const {
171 return storm::utility::convertNumber<ValueType>(input);
172 }
173 ValueType precision() const {
174 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
175 }
176
177 private:
178 storm::Environment _environment;
179};
180
181typedef ::testing::Types<
182#ifdef STORM_HAVE_GMM
183 GBGmmxxDoubleGmresEnvironment, GBEigenDoubleDGmresEnvironment, DistrGmmxxDoubleGmresEnvironment,
184#endif
185 GBEigenRationalLUEnvironment, GBNativeSorEnvironment, GBNativeWalkerChaeEnvironment, DistrEigenRationalLUEnvironment, DistrNativeWalkerChaeEnvironment,
186 ValueIterationEnvironment>
187 TestingTypes;
188
189TYPED_TEST_SUITE(LraDtmcPrctlModelCheckerTest, TestingTypes, );
190
191TYPED_TEST(LraDtmcPrctlModelCheckerTest, LRASingleBscc) {
192 typedef typename TestFixture::ValueType ValueType;
193
194 storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
195 std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc;
196
197 // A parser that we use for conveniently constructing the formulas.
198 storm::parser::FormulaParser formulaParser;
199
200 {
201 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 2);
202 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
203 matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
204 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
205
206 storm::models::sparse::StateLabeling ap(2);
207 ap.addLabel("a");
208 ap.addLabelToState("a", 1);
209
210 dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
211
212 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
213
214 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
215
216 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
217 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
218
219 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
220 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
221 }
222 {
223 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 4);
224 matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5"));
225 matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5"));
226 matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5"));
227 matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5"));
228 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
229
230 storm::models::sparse::StateLabeling ap(2);
231 ap.addLabel("a");
232 ap.addLabelToState("a", 1);
233
234 dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
235
236 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
237
238 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
239
240 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
241 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
242
243 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
244 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
245 }
246
247 {
248 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(3, 3, 3);
249 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
250 matrixBuilder.addNextValue(1, 2, this->parseNumber("1"));
251 matrixBuilder.addNextValue(2, 0, this->parseNumber("1"));
252 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
253
254 storm::models::sparse::StateLabeling ap(3);
255 ap.addLabel("a");
256 ap.addLabelToState("a", 2);
257
258 dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
259
260 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
261
262 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
263
264 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
265 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
266
267 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision());
268 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision());
269 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision());
270 }
271}
272
273TYPED_TEST(LraDtmcPrctlModelCheckerTest, LRA) {
274 typedef typename TestFixture::ValueType ValueType;
275
276 storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
277 std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc;
278
279 // A parser that we use for conveniently constructing the formulas.
280 storm::parser::FormulaParser formulaParser;
281
282 {
283 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(15, 15, 20, true);
284 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
285 matrixBuilder.addNextValue(1, 4, this->parseNumber("0.7"));
286 matrixBuilder.addNextValue(1, 6, this->parseNumber("0.3"));
287 matrixBuilder.addNextValue(2, 0, this->parseNumber("1"));
288
289 matrixBuilder.addNextValue(3, 5, this->parseNumber("0.8"));
290 matrixBuilder.addNextValue(3, 9, this->parseNumber("0.2"));
291 matrixBuilder.addNextValue(4, 3, this->parseNumber("1"));
292 matrixBuilder.addNextValue(5, 3, this->parseNumber("1"));
293
294 matrixBuilder.addNextValue(6, 7, this->parseNumber("1"));
295 matrixBuilder.addNextValue(7, 8, this->parseNumber("1"));
296 matrixBuilder.addNextValue(8, 6, this->parseNumber("1"));
297
298 matrixBuilder.addNextValue(9, 10, this->parseNumber("1"));
299 matrixBuilder.addNextValue(10, 9, this->parseNumber("1"));
300 matrixBuilder.addNextValue(11, 9, this->parseNumber("1"));
301
302 matrixBuilder.addNextValue(12, 5, this->parseNumber("0.4"));
303 matrixBuilder.addNextValue(12, 8, this->parseNumber("0.3"));
304 matrixBuilder.addNextValue(12, 11, this->parseNumber("0.3"));
305
306 matrixBuilder.addNextValue(13, 7, this->parseNumber("0.7"));
307 matrixBuilder.addNextValue(13, 12, this->parseNumber("0.3"));
308
309 matrixBuilder.addNextValue(14, 12, this->parseNumber("1"));
310
311 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
312
313 storm::models::sparse::StateLabeling ap(15);
314 ap.addLabel("a");
315 ap.addLabelToState("a", 1);
316 ap.addLabelToState("a", 4);
317 ap.addLabelToState("a", 5);
318 ap.addLabelToState("a", 7);
319 ap.addLabelToState("a", 11);
320 ap.addLabelToState("a", 13);
321 ap.addLabelToState("a", 14);
322
323 dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
324
325 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
326
327 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
328
329 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
330 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
331
332 EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[0], this->precision());
333 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[3], this->precision());
334 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[6], this->precision());
335 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[9], this->precision());
336 EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[12], this->precision());
337 EXPECT_NEAR(this->parseNumber("79/300"), quantitativeResult1[13], this->precision());
338 EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[14], this->precision());
339 }
340}
341} // namespace
storm::EigenSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition EigenSolverEnvironment.cpp:70
storm::EigenSolverEnvironment::setPreconditioner
void setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner value)
Definition EigenSolverEnvironment.cpp:46
storm::EigenSolverEnvironment::setMethod
void setMethod(storm::solver::EigenLinearEquationSolverMethod value)
Definition EigenSolverEnvironment.cpp:37
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:25
storm::GmmxxSolverEnvironment::setMethod
void setMethod(storm::solver::GmmxxLinearEquationSolverMethod value)
Definition GmmxxSolverEnvironment.cpp:32
storm::GmmxxSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition GmmxxSolverEnvironment.cpp:64
storm::GmmxxSolverEnvironment::setPreconditioner
void setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner value)
Definition GmmxxSolverEnvironment.cpp:40
storm::LongRunAverageSolverEnvironment::setDetLraMethod
void setDetLraMethod(storm::solver::LraMethod value, bool isSetFromDefault=false)
Definition LongRunAverageSolverEnvironment.cpp:36
storm::NativeSolverEnvironment::setSorOmega
void setSorOmega(storm::RationalNumber const &value)
Definition NativeSolverEnvironment.cpp:84
storm::NativeSolverEnvironment::setMaximalNumberOfIterations
void setMaximalNumberOfIterations(uint64_t value)
Definition NativeSolverEnvironment.cpp:52
storm::NativeSolverEnvironment::setMethod
void setMethod(storm::solver::NativeLinearEquationSolverMethod value)
Definition NativeSolverEnvironment.cpp:43
storm::NativeSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition NativeSolverEnvironment.cpp:60
storm::SolverEnvironment::setLinearEquationSolverType
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
Definition SolverEnvironment.cpp:127
storm::SolverEnvironment::eigen
EigenSolverEnvironment & eigen()
Definition SolverEnvironment.cpp:59
storm::SolverEnvironment::native
NativeSolverEnvironment & native()
Definition SolverEnvironment.cpp:75
storm::SolverEnvironment::gmmxx
GmmxxSolverEnvironment & gmmxx()
Definition SolverEnvironment.cpp:67
storm::SolverEnvironment::lra
LongRunAverageSolverEnvironment & lra()
Definition SolverEnvironment.cpp:27
storm::modelchecker::CheckResult::asExplicitQuantitativeCheckResult
ExplicitQuantitativeCheckResult< ValueType > & asExplicitQuantitativeCheckResult()
Definition CheckResult.cpp:94
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
storm::models::sparse::StateLabeling
This class manages the labeling of the state space with a number of (atomic) labels.
Definition StateLabeling.h:19
storm::parser::FormulaParser::parseSingleFormulaFromString
std::shared_ptr< storm::logic::Formula const > parseSingleFormulaFromString(std::string const &formulaString) const
Parses the formula given by the provided string.
Definition FormulaParser.cpp:55
storm::storage::SparseMatrixBuilder
A class that can be used to build a sparse matrix by adding value by value.
Definition SparseMatrix.h:133
storm::storage::SparseMatrixBuilder::addNextValue
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.
Definition SparseMatrix.cpp:156
storm::storage::SparseMatrixBuilder::build
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
Definition SparseMatrix.cpp:281
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:328
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:12
storm::parser::parseNumber
NumberType parseNumber(std::string const &value)
Parse number from string.
Definition ValueParser.cpp:53
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h