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