Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ExplicitMdpPrctlModelCheckerTest.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-parsers/parser/PrismParser.h"
7#include "storm/builder/ExplicitModelBuilder.h"
8#include "storm/environment/solver/MinMaxSolverEnvironment.h"
9#include "storm/logic/Formulas.h"
10#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
11#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
12#include "storm/models/sparse/StandardRewardModel.h"
13#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
14
15TEST(ExplicitMdpPrctlModelCheckerTest, Dice) {
16 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel =
17 storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "",
18 STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew");
19 storm::Environment env;
20 double const precision = 1e-6;
21 // Increase precision a little to get more accurate results
22 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
23
24 // A parser that we use for conveniently constructing the formulas.
25 storm::parser::FormulaParser formulaParser;
26
27 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
28
29 std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
30
31 ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
32 ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
33
34 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
35
36 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
37
38 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
39 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
40
41 EXPECT_NEAR(1.0 / 36.0, quantitativeResult1[0], precision);
42
43 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
44
45 result = checker.check(env, *formula);
46 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
47
48 EXPECT_NEAR(1.0 / 36.0, quantitativeResult2[0], precision);
49
50 formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
51
52 result = checker.check(env, *formula);
53 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
54
55 EXPECT_NEAR(2.0 / 36.0, quantitativeResult3[0], precision);
56
57 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
58
59 result = checker.check(env, *formula);
60 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
61
62 EXPECT_NEAR(2.0 / 36.0, quantitativeResult4[0], precision);
63
64 formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
65
66 result = checker.check(env, *formula);
67 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
68
69 EXPECT_NEAR(3.0 / 36.0, quantitativeResult5[0], precision);
70
71 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
72
73 result = checker.check(env, *formula);
74 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
75
76 EXPECT_NEAR(3.0 / 36.0, quantitativeResult6[0], precision);
77
78 formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
79
80 result = checker.check(env, *formula);
81 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
82
83 EXPECT_NEAR(22.0 / 3.0, quantitativeResult7[0], precision);
84
85 formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
86
87 result = checker.check(env, *formula);
88 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
89
90 EXPECT_NEAR(22.0 / 3.0, quantitativeResult8[0], precision);
91
92 abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab",
93 STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", "");
94
95 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
96
97 std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
98
99 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp);
100
101 formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
102
103 result = stateRewardModelChecker.check(env, *formula);
104 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
105
106 EXPECT_NEAR(22.0 / 3.0, quantitativeResult9[0], precision);
107
108 formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
109
110 result = stateRewardModelChecker.check(env, *formula);
111 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
112
113 EXPECT_NEAR(22.0 / 3.0, quantitativeResult10[0], precision);
114
115 abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab",
116 STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew",
117 STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew");
118
119 ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
120
121 std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
122
123 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
124
125 formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
126
127 result = stateAndTransitionRewardModelChecker.check(env, *formula);
128 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
129
130 EXPECT_NEAR(44.0 / 3.0, quantitativeResult11[0], precision);
131
132 formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
133
134 result = stateAndTransitionRewardModelChecker.check(env, *formula);
135 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
136
137 EXPECT_NEAR(44.0 / 3.0, quantitativeResult12[0], precision);
138}
139
140TEST(ExplicitMdpPrctlModelCheckerTest, AsynchronousLeader) {
141 storm::Environment env;
142 double const precision = 1e-6;
143 // Increase precision a little to get more accurate results
144 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
145
146 std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(
147 STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew");
148
149 // A parser that we use for conveniently constructing the formulas.
150 storm::parser::FormulaParser formulaParser;
151
152 ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType());
153
154 std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
155
156 ASSERT_EQ(3172ull, mdp->getNumberOfStates());
157 ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
158
159 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
160
161 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
162
163 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
164 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
165
166 EXPECT_NEAR(1.0, quantitativeResult1[0], precision);
167
168 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
169
170 result = checker.check(env, *formula);
171 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
172
173 EXPECT_NEAR(1.0, quantitativeResult2[0], precision);
174
175 formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
176
177 result = checker.check(env, *formula);
178 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
179
180 EXPECT_NEAR(1.0 / 16.0, quantitativeResult3[0], precision);
181
182 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
183
184 result = checker.check(env, *formula);
185 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
186
187 EXPECT_NEAR(1.0 / 16.0, quantitativeResult4[0], precision);
188
189 formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
190
191 result = checker.check(env, *formula);
192 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
193
194 EXPECT_NEAR(30.0 / 7.0, quantitativeResult5[0], precision);
195
196 formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
197
198 result = checker.check(env, *formula);
199 storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
200
201 EXPECT_NEAR(30.0 / 7.0, quantitativeResult6[0], precision);
202}
TEST
TEST(ExplicitMdpPrctlModelCheckerTest, Dice)
Definition ExplicitMdpPrctlModelCheckerTest.cpp:15
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:25
storm::MinMaxSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition MinMaxSolverEnvironment.cpp:60
storm::SolverEnvironment::minMax
MinMaxSolverEnvironment & minMax()
Definition SolverEnvironment.cpp:43
storm::modelchecker::AbstractModelChecker::check
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
Definition AbstractModelChecker.cpp:51
storm::modelchecker::CheckResult::asExplicitQuantitativeCheckResult
ExplicitQuantitativeCheckResult< ValueType > & asExplicitQuantitativeCheckResult()
Definition CheckResult.cpp:94
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:13
storm::parser::AutoParser::parseModel
static std::shared_ptr< storm::models::sparse::Model< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > > > parseModel(std::string const &transitionsFilename, std::string const &labelingFilename, std::string const &stateRewardFilename="", std::string const &transitionRewardFilename="", std::string const &choiceLabelingFilename="")
Checks the given files and parses the model within these files.
Definition AutoParser.cpp:25
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_gtest.h