Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SchedulerGenerationMdpPrctlModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-conv/api/storm-conv.h"
5#include "storm-parsers/api/model_descriptions.h"
6#include "storm-parsers/api/properties.h"
7#include "storm/api/builder.h"
8#include "storm/api/properties.h"
9
10#include "storm/logic/Formulas.h"
11#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
12#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.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
18#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
19#include "storm/environment/solver/MinMaxSolverEnvironment.h"
20
21namespace {
22class DoubleViEnvironment {
23 public:
24 typedef double ValueType;
25 static storm::Environment createEnvironment() {
26 storm::Environment env;
27 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
28 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
29 env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::ValueIteration);
30 return env;
31 }
32};
33class DoubleSoundViEnvironment {
34 public:
35 typedef double ValueType;
36 static storm::Environment createEnvironment() {
37 storm::Environment env;
38 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
39 env.solver().setForceSoundness(true);
40 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
41 env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::ValueIteration);
42 return env;
43 }
44};
45class DoublePIEnvironment {
46 public:
47 typedef double ValueType;
48 static storm::Environment createEnvironment() {
49 storm::Environment env;
50 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
51 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
52 env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::ValueIteration);
53 return env;
54 }
55};
56class RationalPIEnvironment {
57 public:
58 typedef storm::RationalNumber ValueType;
59 static storm::Environment createEnvironment() {
60 storm::Environment env;
61 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
62 return env;
63 }
64};
65// class RationalRationalSearchEnvironment {
66// public:
67// typedef storm::RationalNumber ValueType;
68// static storm::Environment createEnvironment() {
69// storm::Environment env;
70// env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
71// return env;
72// }
73// };
74
75template<typename TestType>
76class SchedulerGenerationMdpPrctlModelCheckerTest : public ::testing::Test {
77 public:
78 typedef typename TestType::ValueType ValueType;
79 SchedulerGenerationMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
80
81 void SetUp() override {
82#ifndef STORM_HAVE_Z3
83 GTEST_SKIP() << "Z3 not available.";
84#endif
85 }
86
87 storm::Environment const& env() const {
88 return _environment;
89 }
90
91 std::pair<std::shared_ptr<storm::models::sparse::Mdp<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> buildModelFormulas(
92 std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
93 std::pair<std::shared_ptr<storm::models::sparse::Mdp<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
94 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
95 program = storm::utility::prism::preprocess(program, constantDefinitionString);
96 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
97 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<storm::models::sparse::Mdp<ValueType>>();
98 return result;
99 }
100
101 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
102 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
103 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
104 for (auto const& f : formulas) {
105 result.emplace_back(*f);
106 result.back().setProduceSchedulers(true);
107 }
108 return result;
109 }
110
111 ValueType parseNumber(std::string const& input) const {
112 return storm::utility::convertNumber<ValueType>(input);
113 }
114
115 private:
116 storm::Environment _environment;
117};
118
119typedef ::testing::Types<DoubleViEnvironment, DoubleSoundViEnvironment, DoublePIEnvironment, RationalPIEnvironment
120 // RationalRationalSearchEnvironment
121 >
122 TestingTypes;
123
124TYPED_TEST_SUITE(SchedulerGenerationMdpPrctlModelCheckerTest, TestingTypes, );
125
126TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, reachability) {
127 typedef typename TestFixture::ValueType ValueType;
128
129 std::string formulasString = "Pmin=? [F \"target\"]; Pmax=? [F \"target\"];";
130 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString);
131 auto mdp = std::move(modelFormulas.first);
132 auto tasks = this->getTasks(modelFormulas.second);
133 EXPECT_EQ(4ull, mdp->getNumberOfStates());
134 EXPECT_EQ(11ull, mdp->getNumberOfTransitions());
135 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
136 EXPECT_EQ(7ull, mdp->getNumberOfChoices());
137
138 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
139
140 auto result = checker.check(this->env(), tasks[0]);
141 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
142 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
143 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
144 EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice());
145 EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice());
146 EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice());
147 EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice());
148
149 result = checker.check(tasks[1]);
150 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
151 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
152 storm::storage::Scheduler<ValueType> const& scheduler2 = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
153 EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice());
154 EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice());
155 EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice());
156 EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice());
157}
158
159TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, total_reward) {
160 typedef typename TestFixture::ValueType ValueType;
161
162 std::string formulasString = "Rmin=? [ C ];";
163
164 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", formulasString);
165 auto mdp = std::move(modelFormulas.first);
166 auto tasks = this->getTasks(modelFormulas.second);
167 EXPECT_EQ(3ul, mdp->getNumberOfStates());
168 EXPECT_EQ(4ul, mdp->getNumberOfTransitions());
169 EXPECT_EQ(4ul, mdp->getNumberOfChoices());
170 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
171 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
172
173 {
174 auto result = checker.check(this->env(), tasks[0]);
175 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
176 EXPECT_NEAR(this->parseNumber("0"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
177 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
178 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
179 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
180 EXPECT_TRUE(scheduler.isDeterministicScheduler());
181 EXPECT_TRUE(scheduler.isMemorylessScheduler());
182 EXPECT_TRUE(!scheduler.isPartialScheduler());
183
184 auto inducedModel = mdp->applyScheduler(scheduler);
185 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
186 auto const& inducedDtmc = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
187 EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates());
188 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedDtmc);
189 auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
190 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
191 EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
192 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
193 }
194}
195
196TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, reach_reward) {
197 // Test case taken from https://github.com/moves-rwth/storm/issues/297
198 typedef typename TestFixture::ValueType ValueType;
199
200 std::string formulasString = "Rmax=? [ F \"goal\" ];";
201
202 auto [mdp, formulas] = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards2.nm", formulasString);
203 auto tasks = this->getTasks(formulas);
204 EXPECT_EQ(4ul, mdp->getNumberOfStates());
205 EXPECT_EQ(7ul, mdp->getNumberOfChoices());
206 EXPECT_EQ(12ul, mdp->getNumberOfTransitions());
207 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
208 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
209
210 {
211 auto result = checker.check(this->env(), tasks[0]);
212 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
213 ASSERT_TRUE(storm::utility::isInfinity(result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()]));
214 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
215 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
216 EXPECT_TRUE(scheduler.isDeterministicScheduler());
217 EXPECT_TRUE(scheduler.isMemorylessScheduler());
218 EXPECT_TRUE(!scheduler.isPartialScheduler());
219
220 auto inducedModel = mdp->applyScheduler(scheduler);
221 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
222 auto const& inducedDtmc = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
223 EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates());
224 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedDtmc);
225 auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
226 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
227 EXPECT_TRUE(storm::utility::isInfinity(inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()]));
228 }
229}
230
231TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, reach_reward2) {
232 // Test case taken from https://github.com/moves-rwth/storm/issues/683
233 typedef typename TestFixture::ValueType ValueType;
234
235 std::string formulasString = "Rmax=? [ F \"goal\" ];";
236
237 auto [mdp, formulas] = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards3.nm", formulasString);
238 auto tasks = this->getTasks(formulas);
239 EXPECT_EQ(4ul, mdp->getNumberOfStates());
240 EXPECT_EQ(5ul, mdp->getNumberOfChoices());
241 EXPECT_EQ(6ul, mdp->getNumberOfTransitions());
242 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
243 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
244
245 {
246 auto result = checker.check(this->env(), tasks[0]);
247 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
248 ASSERT_TRUE(storm::utility::isInfinity(result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()]));
249 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
250 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
251 EXPECT_TRUE(scheduler.isDeterministicScheduler());
252 EXPECT_TRUE(scheduler.isMemorylessScheduler());
253 EXPECT_TRUE(!scheduler.isPartialScheduler());
254
255 auto inducedModel = mdp->applyScheduler(scheduler);
256 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
257 auto const& inducedDtmc = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
258 EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates());
259 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedDtmc);
260 auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
261 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
262 EXPECT_TRUE(storm::utility::isInfinity(inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()]));
263 }
264}
265
266TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, lra) {
267 typedef typename TestFixture::ValueType ValueType;
268
269 std::string formulasString = "R{\"grants\"}max=? [ MP ]; R{\"grants\"}min=? [ MP ];";
270
271 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/cs_nfail3.nm", formulasString);
272 auto mdp = std::move(modelFormulas.first);
273 auto tasks = this->getTasks(modelFormulas.second);
274 EXPECT_EQ(184ul, mdp->getNumberOfStates());
275 EXPECT_EQ(541ul, mdp->getNumberOfTransitions());
276 EXPECT_EQ(439ul, mdp->getNumberOfChoices());
277 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
278 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
279
280 if (!std::is_same<ValueType, double>::value) {
281 GTEST_SKIP() << "Lra scheduler extraction not supported for LP based method";
282 }
283 {
284 auto result = checker.check(this->env(), tasks[0]);
285 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
286 EXPECT_NEAR(this->parseNumber("333/1000"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
287 storm::utility::convertNumber<ValueType>(this->env().solver().lra().getPrecision()));
288 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
289 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
290 EXPECT_TRUE(scheduler.isDeterministicScheduler());
291 EXPECT_TRUE(scheduler.isMemorylessScheduler());
292 EXPECT_TRUE(!scheduler.isPartialScheduler());
293
294 auto inducedModel = mdp->applyScheduler(scheduler);
295 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
296 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
297 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
298 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedMdp);
299 auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
300 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
301 EXPECT_NEAR(this->parseNumber("333/1000"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
302 storm::utility::convertNumber<ValueType>(this->env().solver().lra().getPrecision()));
303 }
304 {
305 auto result = checker.check(this->env(), tasks[1]);
306 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
307 EXPECT_NEAR(this->parseNumber("0"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
308 storm::utility::convertNumber<ValueType>(this->env().solver().lra().getPrecision()));
309 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
310 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
311 EXPECT_TRUE(scheduler.isDeterministicScheduler());
312 EXPECT_TRUE(scheduler.isMemorylessScheduler());
313 EXPECT_TRUE(!scheduler.isPartialScheduler());
314 auto inducedModel = mdp->applyScheduler(scheduler);
315 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
316 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
317 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
318 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedMdp);
319 auto inducedResult = inducedChecker.check(this->env(), tasks[1]);
320 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
321 EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
322 storm::utility::convertNumber<ValueType>(this->env().solver().lra().getPrecision()));
323 }
324}
325
326TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl) {
327 typedef typename TestFixture::ValueType ValueType;
328
329#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
330 std::string formulasString = "Pmax=? [X X s=0]; Pmin=? [G F \"target\"]; Pmax=? [(G F s>2) & (F G !(s=3))];";
331 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString);
332 auto mdp = std::move(modelFormulas.first);
333 auto tasks = this->getTasks(modelFormulas.second);
334 EXPECT_EQ(4ull, mdp->getNumberOfStates());
335 EXPECT_EQ(11ull, mdp->getNumberOfTransitions());
336 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
337 EXPECT_EQ(7ull, mdp->getNumberOfChoices());
338
339 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
340
341 {
342 tasks[0].setOnlyInitialStatesRelevant(true);
343 auto result = checker.check(this->env(), tasks[0]);
344 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
345 EXPECT_NEAR(this->parseNumber("81/100"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
346 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
347 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
348 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
349
350 EXPECT_TRUE(scheduler.isDeterministicScheduler());
351 EXPECT_TRUE(!scheduler.isMemorylessScheduler());
352 EXPECT_TRUE(!scheduler.isPartialScheduler());
353 auto inducedModel = mdp->applyScheduler(scheduler);
354
355 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
356 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
357 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
358
359 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
360 auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
361 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
362 EXPECT_NEAR(this->parseNumber("81/100"),
363 inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],
364 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
365 }
366 {
367 tasks[1].setOnlyInitialStatesRelevant(true);
368 auto result = checker.check(this->env(), tasks[1]);
369 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
370 EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
371 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
372 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
373 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
374
375 EXPECT_TRUE(scheduler.isDeterministicScheduler());
376 EXPECT_TRUE(!scheduler.isMemorylessScheduler());
377 EXPECT_TRUE(!scheduler.isPartialScheduler());
378 auto inducedModel = mdp->applyScheduler(scheduler);
379
380 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
381 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
382 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
383
384 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
385 auto inducedResult = inducedChecker.check(this->env(), tasks[1]);
386 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
387
388 EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],
389 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
390 }
391 {
392 tasks[2].setOnlyInitialStatesRelevant(false);
393 auto result = checker.check(this->env(), tasks[2]);
394 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
395 EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
396 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
397 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
398 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
399
400 EXPECT_TRUE(scheduler.isDeterministicScheduler());
401 EXPECT_TRUE(!scheduler.isMemorylessScheduler());
402 EXPECT_TRUE(!scheduler.isPartialScheduler());
403 auto inducedModel = mdp->applyScheduler(scheduler);
404
405 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
406 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
407 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
408
409 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
410 auto inducedResult = inducedChecker.check(this->env(), tasks[2]);
411 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
412
413 auto test = inducedResult->template asExplicitQuantitativeCheckResult<ValueType>().getValueVector();
414 EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[0],
415 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
416 EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[1],
417 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
418 EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[2],
419 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
420 }
421#else
422 GTEST_SKIP();
423#endif
424}
425
426TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltlNondetChoice) {
427 typedef typename TestFixture::ValueType ValueType;
428#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
429 // Nondeterministic choice in an accepting EC.
430 std::string formulasString = "Pmax=? [X X !(x=0)];";
431 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example1.nm", formulasString);
432
433 auto mdp = std::move(modelFormulas.first);
434 auto tasks = this->getTasks(modelFormulas.second);
435 EXPECT_EQ(3ull, mdp->getNumberOfStates());
436 EXPECT_EQ(5ull, mdp->getNumberOfTransitions());
437 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
438 EXPECT_EQ(4ull, mdp->getNumberOfChoices());
439
440 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
441
442 {
443 tasks[0].setOnlyInitialStatesRelevant(true);
444 auto result = checker.check(this->env(), tasks[0]);
445 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
446 EXPECT_NEAR(this->parseNumber("1"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
447 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
448 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
449 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
450
451 EXPECT_TRUE(scheduler.isDeterministicScheduler());
452 EXPECT_TRUE(!scheduler.isMemorylessScheduler());
453 EXPECT_TRUE(!scheduler.isPartialScheduler());
454 auto inducedModel = mdp->applyScheduler(scheduler);
455
456 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
457 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
458 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
459
460 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
461 auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
462 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
463 EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],
464 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
465 }
466#else
467 GTEST_SKIP();
468#endif
469}
470
471TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltlUnsat) {
472 typedef typename TestFixture::ValueType ValueType;
473#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
474 // Nondeterministic choice in an accepting EC, Pmax unsatisfiable, Pmin tautology (compute 1-Pmax(!phi))
475 std::string formulasString = "Pmax=? [(X X !(s=0)) & (X X (s=0))]; Pmin=? [(X X !(s=0)) | (X X (s=0))];";
476 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString);
477
478 auto mdp = std::move(modelFormulas.first);
479 auto tasks = this->getTasks(modelFormulas.second);
480 EXPECT_EQ(4ull, mdp->getNumberOfStates());
481 EXPECT_EQ(11ull, mdp->getNumberOfTransitions());
482 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
483 EXPECT_EQ(7ull, mdp->getNumberOfChoices());
484
485 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
486
487 {
488 tasks[0].setOnlyInitialStatesRelevant(true);
489 auto result = checker.check(this->env(), tasks[0]);
490 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
491 EXPECT_NEAR(this->parseNumber("0"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
492 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
493 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
494 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
495
496 EXPECT_TRUE(scheduler.isDeterministicScheduler());
497 EXPECT_TRUE(scheduler.isMemorylessScheduler());
498 EXPECT_TRUE(!scheduler.isPartialScheduler());
499 auto inducedModel = mdp->applyScheduler(scheduler);
500
501 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
502 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
503 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
504
505 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedMdp);
506 auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
507 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
508 EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],
509 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
510 }
511
512 {
513 tasks[1].setOnlyInitialStatesRelevant(true);
514 auto result = checker.check(this->env(), tasks[1]);
515 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
516 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
517 EXPECT_NEAR(this->parseNumber("1"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
518 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
519 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
520
521 EXPECT_TRUE(scheduler.isDeterministicScheduler());
522 EXPECT_TRUE(scheduler.isMemorylessScheduler());
523 EXPECT_TRUE(!scheduler.isPartialScheduler());
524 auto inducedModel = mdp->applyScheduler(scheduler);
525
526 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
527 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
528 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
529
530 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedMdp);
531 auto inducedResult = inducedChecker.check(this->env(), tasks[1]);
532 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
533 EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],
534 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
535 }
536#else
537 GTEST_SKIP();
538#endif
539}
540} // namespace
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:25
storm::LongRunAverageSolverEnvironment::setNondetLraMethod
void setNondetLraMethod(storm::solver::LraMethod value, bool isSetFromDefault=false)
Definition LongRunAverageSolverEnvironment.cpp:49
storm::MinMaxSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition MinMaxSolverEnvironment.cpp:60
storm::MinMaxSolverEnvironment::setMethod
void setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault=false)
Definition MinMaxSolverEnvironment.cpp:43
storm::SolverEnvironment::minMax
MinMaxSolverEnvironment & minMax()
Definition SolverEnvironment.cpp:43
storm::SolverEnvironment::lra
LongRunAverageSolverEnvironment & lra()
Definition SolverEnvironment.cpp:27
storm::storage::Scheduler
This class defines which action is chosen in a particular state of a non-deterministic model.
Definition Scheduler.h:18
storm::storage::Scheduler::isDeterministicScheduler
bool isDeterministicScheduler() const
Retrieves whether all defined choices are deterministic.
Definition Scheduler.cpp:150
storm::storage::Scheduler::isPartialScheduler
bool isPartialScheduler() const
Retrieves whether there is a reachable pair of model and memory state for which the choice is undefin...
Definition Scheduler.cpp:145
storm::storage::Scheduler::getChoice
SchedulerChoice< ValueType > const & getChoice(uint_fast64_t modelState, uint_fast64_t memoryState=0) const
Gets the choice defined by the scheduler for the given model and memory state.
Definition Scheduler.cpp:86
storm::storage::Scheduler::isMemorylessScheduler
bool isMemorylessScheduler() const
Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with j...
Definition Scheduler.cpp:155
model_descriptions.h
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:13
storm::parser::parseNumber
NumberType parseNumber(std::string const &value)
Parse number from string.
Definition ValueParser.cpp:53
storm::utility::prism::preprocess
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:19
storm::utility::isInfinity
bool isInfinity(ValueType const &a)
Definition constants.cpp:71
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h