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