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