Storm
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<GBGmmxxDoubleGmresEnvironment, GBEigenDoubleDGmresEnvironment, GBEigenRationalLUEnvironment, GBNativeSorEnvironment,
178 GBNativeWalkerChaeEnvironment, DistrGmmxxDoubleGmresEnvironment, DistrEigenRationalLUEnvironment, DistrNativeWalkerChaeEnvironment,
179 ValueIterationEnvironment>
180 TestingTypes;
181
182TYPED_TEST_SUITE(LraDtmcPrctlModelCheckerTest, TestingTypes, );
183
184TYPED_TEST(LraDtmcPrctlModelCheckerTest, LRASingleBscc) {
185 typedef typename TestFixture::ValueType ValueType;
186
187 storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
188 std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc;
189
190 // A parser that we use for conveniently constructing the formulas.
191 storm::parser::FormulaParser formulaParser;
192
193 {
194 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 2);
195 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
196 matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
197 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
198
199 storm::models::sparse::StateLabeling ap(2);
200 ap.addLabel("a");
201 ap.addLabelToState("a", 1);
202
203 dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
204
205 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
206
207 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
208
209 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
210 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
211
212 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
213 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
214 }
215 {
216 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 4);
217 matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5"));
218 matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5"));
219 matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5"));
220 matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5"));
221 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
222
223 storm::models::sparse::StateLabeling ap(2);
224 ap.addLabel("a");
225 ap.addLabelToState("a", 1);
226
227 dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
228
229 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
230
231 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
232
233 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
234 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
235
236 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
237 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
238 }
239
240 {
241 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(3, 3, 3);
242 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
243 matrixBuilder.addNextValue(1, 2, this->parseNumber("1"));
244 matrixBuilder.addNextValue(2, 0, this->parseNumber("1"));
245 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
246
247 storm::models::sparse::StateLabeling ap(3);
248 ap.addLabel("a");
249 ap.addLabelToState("a", 2);
250
251 dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
252
253 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
254
255 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
256
257 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
258 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
259
260 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision());
261 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision());
262 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision());
263 }
264}
265
266TYPED_TEST(LraDtmcPrctlModelCheckerTest, LRA) {
267 typedef typename TestFixture::ValueType ValueType;
268
269 storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
270 std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc;
271
272 // A parser that we use for conveniently constructing the formulas.
273 storm::parser::FormulaParser formulaParser;
274
275 {
276 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(15, 15, 20, true);
277 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
278 matrixBuilder.addNextValue(1, 4, this->parseNumber("0.7"));
279 matrixBuilder.addNextValue(1, 6, this->parseNumber("0.3"));
280 matrixBuilder.addNextValue(2, 0, this->parseNumber("1"));
281
282 matrixBuilder.addNextValue(3, 5, this->parseNumber("0.8"));
283 matrixBuilder.addNextValue(3, 9, this->parseNumber("0.2"));
284 matrixBuilder.addNextValue(4, 3, this->parseNumber("1"));
285 matrixBuilder.addNextValue(5, 3, this->parseNumber("1"));
286
287 matrixBuilder.addNextValue(6, 7, this->parseNumber("1"));
288 matrixBuilder.addNextValue(7, 8, this->parseNumber("1"));
289 matrixBuilder.addNextValue(8, 6, this->parseNumber("1"));
290
291 matrixBuilder.addNextValue(9, 10, this->parseNumber("1"));
292 matrixBuilder.addNextValue(10, 9, this->parseNumber("1"));
293 matrixBuilder.addNextValue(11, 9, this->parseNumber("1"));
294
295 matrixBuilder.addNextValue(12, 5, this->parseNumber("0.4"));
296 matrixBuilder.addNextValue(12, 8, this->parseNumber("0.3"));
297 matrixBuilder.addNextValue(12, 11, this->parseNumber("0.3"));
298
299 matrixBuilder.addNextValue(13, 7, this->parseNumber("0.7"));
300 matrixBuilder.addNextValue(13, 12, this->parseNumber("0.3"));
301
302 matrixBuilder.addNextValue(14, 12, this->parseNumber("1"));
303
304 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
305
306 storm::models::sparse::StateLabeling ap(15);
307 ap.addLabel("a");
308 ap.addLabelToState("a", 1);
309 ap.addLabelToState("a", 4);
310 ap.addLabelToState("a", 5);
311 ap.addLabelToState("a", 7);
312 ap.addLabelToState("a", 11);
313 ap.addLabelToState("a", 13);
314 ap.addLabelToState("a", 14);
315
316 dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
317
318 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
319
320 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
321
322 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
323 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
324
325 EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[0], this->precision());
326 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[3], this->precision());
327 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[6], this->precision());
328 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[9], this->precision());
329 EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[12], this->precision());
330 EXPECT_NEAR(this->parseNumber("79/300"), quantitativeResult1[13], this->precision());
331 EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[14], this->precision());
332 }
333}
334} // 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:137
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:332
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:13
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