Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ConditionalMdpPrctlModelCheckerTest.cpp
Go to the documentation of this file.
1#include "test/storm_gtest.h"
2
3#include "storm-config.h"
4
7#include "storm/api/builder.h"
9
12
15
16namespace {
17
18class SparseDoubleRestartEnvironment {
19 public:
20 static const bool isExact = false;
21 typedef double ValueType;
23 static storm::Environment createEnvironment() {
26 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10)); // restart algorithm requires a higher precision
27 return env;
28 }
29};
30
31class SparseDoubleBisectionEnvironment {
32 public:
33 static const bool isExact = false;
34 typedef double ValueType;
36 static storm::Environment createEnvironment() {
39 return env;
40 }
41};
42
43class SparseDoubleBisectionAdvancedEnvironment {
44 public:
45 static const bool isExact = false;
46 typedef double ValueType;
48 static storm::Environment createEnvironment() {
51 return env;
52 }
53};
54
55class SparseDoublePiEnvironment {
56 public:
57 static const bool isExact = false;
58 typedef double ValueType;
60 static storm::Environment createEnvironment() {
63 return env;
64 }
65};
66
67class SparseRationalNumberRestartEnvironment {
68 public:
69 static const bool isExact = true;
70 typedef storm::RationalNumber ValueType;
72 static storm::Environment createEnvironment() {
75 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10)); // restart algorithm requires a higher precision
76 return env;
77 }
78};
79
80class SparseRationalNumberBisectionEnvironment {
81 public:
82 static const bool isExact = true;
83 typedef storm::RationalNumber ValueType;
85 static storm::Environment createEnvironment() {
88 return env;
89 }
90};
91
92class SparseRationalNumberBisectionAdvancedEnvironment {
93 public:
94 static const bool isExact = true;
95 typedef storm::RationalNumber ValueType;
97 static storm::Environment createEnvironment() {
100 return env;
101 }
102};
103
104class SparseRationalNumberPiEnvironment {
105 public:
106 static const bool isExact = true;
107 typedef storm::RationalNumber ValueType;
109 static storm::Environment createEnvironment() {
112 return env;
113 }
114};
115
116template<typename TestType>
117class ConditionalMdpPrctlModelCheckerTest : public ::testing::Test {
118 public:
119 typedef typename TestType::ValueType ValueType;
120 typedef typename storm::models::sparse::Mdp<ValueType> SparseModelType;
121
122 ConditionalMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
123
124 void SetUp() override {
125#ifndef STORM_HAVE_Z3
126 GTEST_SKIP() << "Z3 not available.";
127#endif
128 }
129
130 storm::Environment const& env() const {
131 return _environment;
132 }
133 ValueType parseNumber(std::string const& input) const {
134 return storm::utility::convertNumber<ValueType>(input);
135 }
136 ValueType precision() const {
137 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
138 }
139 bool isSparseModel() const {
140 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
141 }
142
143 std::pair<std::shared_ptr<SparseModelType>, std::vector<std::shared_ptr<storm::logic::Formula const>>> buildModelFormulas(
144 storm::prism::Program const& inputProgram, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
145 std::pair<std::shared_ptr<SparseModelType>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
146 auto program = storm::utility::prism::preprocess(inputProgram, constantDefinitionString);
148 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<SparseModelType>();
149 return result;
150 }
151
152 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
153 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
154 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
155 for (auto const& f : formulas) {
156 result.emplace_back(*f, true); // Set onlyInitialStatesRelevant to true for conditional tasks
157 }
158 return result;
159 }
160
161 private:
162 storm::Environment _environment;
163};
164
165typedef ::testing::Types<SparseDoubleRestartEnvironment, SparseDoubleBisectionEnvironment, SparseDoubleBisectionAdvancedEnvironment, SparseDoublePiEnvironment,
166 SparseRationalNumberRestartEnvironment, SparseRationalNumberBisectionEnvironment, SparseRationalNumberBisectionAdvancedEnvironment,
167 SparseRationalNumberPiEnvironment>
169
170TYPED_TEST_SUITE(ConditionalMdpPrctlModelCheckerTest, TestingTypes, );
171
172TYPED_TEST(ConditionalMdpPrctlModelCheckerTest, two_dice) {
173 typedef typename TestFixture::ValueType ValueType;
174
175 std::string const formulasString =
176 "Pmax=? [F \"twelve\" || F d1=6];"
177 "Pmin=? [F \"twelve\" || F d1=6];"
178 "Pmax=? [F \"seven\" || F d2=4];"
179 "Pmin=? [F \"seven\" || F d2=4];"
180 "Pmax=? [F \"two\" || F d2=2];"
181 "Pmin=? [F \"two\" || F d2=2];"
182 "Pmax=? [F d1=6 || F \"twelve\"];"
183 "Pmin=? [F d1=6 || F \"twelve\"];";
184
185 auto program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
186 auto modelFormulas = this->buildModelFormulas(program, formulasString);
187 auto model = std::move(modelFormulas.first);
188 auto tasks = this->getTasks(modelFormulas.second);
189 EXPECT_EQ(169ul, model->getNumberOfStates());
190 EXPECT_EQ(436ul, model->getNumberOfTransitions());
191 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
192 auto mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
194
195 auto result = checker.check(this->env(), tasks[0])->template asExplicitQuantitativeCheckResult<ValueType>();
196 EXPECT_NEAR(this->parseNumber("1/6"), result[*mdp->getInitialStates().begin()], this->precision());
197 result = checker.check(this->env(), tasks[1])->template asExplicitQuantitativeCheckResult<ValueType>();
198 EXPECT_NEAR(this->parseNumber("1/6"), result[*mdp->getInitialStates().begin()], this->precision());
199 result = checker.check(this->env(), tasks[2])->template asExplicitQuantitativeCheckResult<ValueType>();
200 EXPECT_NEAR(this->parseNumber("1/6"), result[*mdp->getInitialStates().begin()], this->precision());
201 result = checker.check(this->env(), tasks[3])->template asExplicitQuantitativeCheckResult<ValueType>();
202 EXPECT_NEAR(this->parseNumber("1/6"), result[*mdp->getInitialStates().begin()], this->precision());
203 result = checker.check(this->env(), tasks[4])->template asExplicitQuantitativeCheckResult<ValueType>();
204 EXPECT_NEAR(this->parseNumber("0"), result[*mdp->getInitialStates().begin()], this->precision());
205 result = checker.check(this->env(), tasks[5])->template asExplicitQuantitativeCheckResult<ValueType>();
206 EXPECT_NEAR(this->parseNumber("0"), result[*mdp->getInitialStates().begin()], this->precision());
207 result = checker.check(this->env(), tasks[6])->template asExplicitQuantitativeCheckResult<ValueType>();
208 EXPECT_NEAR(this->parseNumber("1"), result[*mdp->getInitialStates().begin()], this->precision());
209 result = checker.check(this->env(), tasks[7])->template asExplicitQuantitativeCheckResult<ValueType>();
210 EXPECT_NEAR(this->parseNumber("1"), result[*mdp->getInitialStates().begin()], this->precision());
211}
212
213TYPED_TEST(ConditionalMdpPrctlModelCheckerTest, consensus) {
214 typedef typename TestFixture::ValueType ValueType;
215
216 std::string const formulasString =
217 "Pmax=? [F \"all_coins_equal_0\" & \"finished\" || F \"agree\" & \"finished\"];"
218 "Pmin=? [F \"all_coins_equal_0\" & \"finished\" || F \"agree\" & \"finished\"];"
219 "Pmax=? [F \"all_coins_equal_1\" & \"finished\" || F \"agree\" & \"finished\"];"
220 "Pmin=? [F \"all_coins_equal_1\" & \"finished\" || F \"agree\" & \"finished\"];";
221
222 auto program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
223 auto modelFormulas = this->buildModelFormulas(program, formulasString);
224 auto model = std::move(modelFormulas.first);
225 auto tasks = this->getTasks(modelFormulas.second);
226 EXPECT_EQ(272ul, model->getNumberOfStates());
227 EXPECT_EQ(492ul, model->getNumberOfTransitions());
228 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
229 auto mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
231
232 auto result = checker.check(this->env(), tasks[0])->template asExplicitQuantitativeCheckResult<ValueType>();
233 EXPECT_NEAR(this->parseNumber("561/953"), result[*mdp->getInitialStates().begin()], this->precision());
234 result = checker.check(this->env(), tasks[1])->template asExplicitQuantitativeCheckResult<ValueType>();
235 EXPECT_NEAR(this->parseNumber("392/953"), result[*mdp->getInitialStates().begin()], this->precision());
236 result = checker.check(this->env(), tasks[2])->template asExplicitQuantitativeCheckResult<ValueType>();
237 EXPECT_NEAR(this->parseNumber("561/953"), result[*mdp->getInitialStates().begin()], this->precision());
238 result = checker.check(this->env(), tasks[3])->template asExplicitQuantitativeCheckResult<ValueType>();
239 EXPECT_NEAR(this->parseNumber("392/953"), result[*mdp->getInitialStates().begin()], this->precision());
240}
241
242TYPED_TEST(ConditionalMdpPrctlModelCheckerTest, simple) {
243 typedef typename TestFixture::ValueType ValueType;
244
245 std::string const programAsString = R"(mdp
246module main
247 x : [0..2];
248 [] x=0 -> 0.7 : (x'=1) + 0.3 : (x'=2);
249 [] x=1 -> 1 : (x'=1);
250 [] x=2 -> 1 : (x'=1);
251endmodule
252)";
253
254 std::string const formulasString =
255 "Pmin=? [F x=2 || F x=1];"
256 "Pmax=? [F x=2 || F x=1];";
257
258 auto program = storm::parser::PrismParser::parseFromString(programAsString, "<no filename>");
259 auto modelFormulas = this->buildModelFormulas(program, formulasString);
260 auto model = std::move(modelFormulas.first);
261 auto tasks = this->getTasks(modelFormulas.second);
262 EXPECT_EQ(3ul, model->getNumberOfStates());
263 EXPECT_EQ(4ul, model->getNumberOfTransitions());
264 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
265 auto mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
267
268 auto result = checker.check(this->env(), tasks[0])->template asExplicitQuantitativeCheckResult<ValueType>();
269 EXPECT_NEAR(this->parseNumber("3/10"), result[*mdp->getInitialStates().begin()], this->precision());
270 result = checker.check(this->env(), tasks[1])->template asExplicitQuantitativeCheckResult<ValueType>();
271 EXPECT_NEAR(this->parseNumber("3/10"), result[*mdp->getInitialStates().begin()], this->precision());
272}
273
274} // namespace
SolverEnvironment & solver()
ModelCheckerEnvironment & modelchecker()
void setPrecision(storm::RationalNumber value)
void setConditionalAlgorithmSetting(ConditionalAlgorithmSetting value)
MinMaxSolverEnvironment & minMax()
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
static storm::prism::Program parseFromString(std::string const &input, std::string const &filename, bool prismCompatability=false)
Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM synt...
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
SFTBDDChecker::ValueType ValueType
NumberType parseNumber(std::string const &value)
Parse number from string.
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:19
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46