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