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