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, lra) {
197 typedef typename TestFixture::ValueType ValueType;
198
199 std::string formulasString = "R{\"grants\"}max=? [ MP ]; R{\"grants\"}min=? [ MP ];";
200
201 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/cs_nfail3.nm", formulasString);
202 auto mdp = std::move(modelFormulas.first);
203 auto tasks = this->getTasks(modelFormulas.second);
204 EXPECT_EQ(184ul, mdp->getNumberOfStates());
205 EXPECT_EQ(541ul, mdp->getNumberOfTransitions());
206 EXPECT_EQ(439ul, mdp->getNumberOfChoices());
207 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
208 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
209
210 if (!std::is_same<ValueType, double>::value) {
211 GTEST_SKIP() << "Lra scheduler extraction not supported for LP based method";
212 }
213 {
214 auto result = checker.check(this->env(), tasks[0]);
215 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
216 EXPECT_NEAR(this->parseNumber("333/1000"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
217 storm::utility::convertNumber<ValueType>(this->env().solver().lra().getPrecision()));
218 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
219 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
220 EXPECT_TRUE(scheduler.isDeterministicScheduler());
221 EXPECT_TRUE(scheduler.isMemorylessScheduler());
222 EXPECT_TRUE(!scheduler.isPartialScheduler());
223
224 auto inducedModel = mdp->applyScheduler(scheduler);
225 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
226 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
227 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
228 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedMdp);
229 auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
230 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
231 EXPECT_NEAR(this->parseNumber("333/1000"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
232 storm::utility::convertNumber<ValueType>(this->env().solver().lra().getPrecision()));
233 }
234 {
235 auto result = checker.check(this->env(), tasks[1]);
236 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
237 EXPECT_NEAR(this->parseNumber("0"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
238 storm::utility::convertNumber<ValueType>(this->env().solver().lra().getPrecision()));
239 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
240 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
241 EXPECT_TRUE(scheduler.isDeterministicScheduler());
242 EXPECT_TRUE(scheduler.isMemorylessScheduler());
243 EXPECT_TRUE(!scheduler.isPartialScheduler());
244 auto inducedModel = mdp->applyScheduler(scheduler);
245 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
246 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
247 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
248 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedMdp);
249 auto inducedResult = inducedChecker.check(this->env(), tasks[1]);
250 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
251 EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
252 storm::utility::convertNumber<ValueType>(this->env().solver().lra().getPrecision()));
253 }
254}
255
256TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl) {
257 typedef typename TestFixture::ValueType ValueType;
258
259#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
260 std::string formulasString = "Pmax=? [X X s=0]; Pmin=? [G F \"target\"]; Pmax=? [(G F s>2) & (F G !(s=3))];";
261 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString);
262 auto mdp = std::move(modelFormulas.first);
263 auto tasks = this->getTasks(modelFormulas.second);
264 EXPECT_EQ(4ull, mdp->getNumberOfStates());
265 EXPECT_EQ(11ull, mdp->getNumberOfTransitions());
266 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
267 EXPECT_EQ(7ull, mdp->getNumberOfChoices());
268
269 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
270
271 {
272 tasks[0].setOnlyInitialStatesRelevant(true);
273 auto result = checker.check(this->env(), tasks[0]);
274 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
275 EXPECT_NEAR(this->parseNumber("81/100"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
276 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
277 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
278 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
279
280 EXPECT_TRUE(scheduler.isDeterministicScheduler());
281 EXPECT_TRUE(!scheduler.isMemorylessScheduler());
282 EXPECT_TRUE(!scheduler.isPartialScheduler());
283 auto inducedModel = mdp->applyScheduler(scheduler);
284
285 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
286 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
287 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
288
289 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
290 auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
291 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
292 EXPECT_NEAR(this->parseNumber("81/100"),
293 inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],
294 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
295 }
296 {
297 tasks[1].setOnlyInitialStatesRelevant(true);
298 auto result = checker.check(this->env(), tasks[1]);
299 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
300 EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
301 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
302 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
303 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
304
305 EXPECT_TRUE(scheduler.isDeterministicScheduler());
306 EXPECT_TRUE(!scheduler.isMemorylessScheduler());
307 EXPECT_TRUE(!scheduler.isPartialScheduler());
308 auto inducedModel = mdp->applyScheduler(scheduler);
309
310 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
311 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
312 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
313
314 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
315 auto inducedResult = inducedChecker.check(this->env(), tasks[1]);
316 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
317
318 EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],
319 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
320 }
321 {
322 tasks[2].setOnlyInitialStatesRelevant(false);
323 auto result = checker.check(this->env(), tasks[2]);
324 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
325 EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
326 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
327 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
328 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
329
330 EXPECT_TRUE(scheduler.isDeterministicScheduler());
331 EXPECT_TRUE(!scheduler.isMemorylessScheduler());
332 EXPECT_TRUE(!scheduler.isPartialScheduler());
333 auto inducedModel = mdp->applyScheduler(scheduler);
334
335 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
336 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
337 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
338
339 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
340 auto inducedResult = inducedChecker.check(this->env(), tasks[2]);
341 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
342
343 auto test = inducedResult->template asExplicitQuantitativeCheckResult<ValueType>().getValueVector();
344 EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[0],
345 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
346 EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[1],
347 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
348 EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[2],
349 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
350 }
351#else
352 GTEST_SKIP();
353#endif
354}
355
356TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltlNondetChoice) {
357 typedef typename TestFixture::ValueType ValueType;
358#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
359 // Nondeterministic choice in an accepting EC.
360 std::string formulasString = "Pmax=? [X X !(x=0)];";
361 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example1.nm", formulasString);
362
363 auto mdp = std::move(modelFormulas.first);
364 auto tasks = this->getTasks(modelFormulas.second);
365 EXPECT_EQ(3ull, mdp->getNumberOfStates());
366 EXPECT_EQ(5ull, mdp->getNumberOfTransitions());
367 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
368 EXPECT_EQ(4ull, mdp->getNumberOfChoices());
369
370 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
371
372 {
373 tasks[0].setOnlyInitialStatesRelevant(true);
374 auto result = checker.check(this->env(), tasks[0]);
375 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
376 EXPECT_NEAR(this->parseNumber("1"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
377 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
378 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
379 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
380
381 EXPECT_TRUE(scheduler.isDeterministicScheduler());
382 EXPECT_TRUE(!scheduler.isMemorylessScheduler());
383 EXPECT_TRUE(!scheduler.isPartialScheduler());
384 auto inducedModel = mdp->applyScheduler(scheduler);
385
386 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
387 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
388 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
389
390 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
391 auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
392 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
393 EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],
394 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
395 }
396#else
397 GTEST_SKIP();
398#endif
399}
400
401TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltlUnsat) {
402 typedef typename TestFixture::ValueType ValueType;
403#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
404 // Nondeterministic choice in an accepting EC, Pmax unsatisfiable, Pmin tautology (compute 1-Pmax(!phi))
405 std::string formulasString = "Pmax=? [(X X !(s=0)) & (X X (s=0))]; Pmin=? [(X X !(s=0)) | (X X (s=0))];";
406 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString);
407
408 auto mdp = std::move(modelFormulas.first);
409 auto tasks = this->getTasks(modelFormulas.second);
410 EXPECT_EQ(4ull, mdp->getNumberOfStates());
411 EXPECT_EQ(11ull, mdp->getNumberOfTransitions());
412 ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
413 EXPECT_EQ(7ull, mdp->getNumberOfChoices());
414
415 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
416
417 {
418 tasks[0].setOnlyInitialStatesRelevant(true);
419 auto result = checker.check(this->env(), tasks[0]);
420 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
421 EXPECT_NEAR(this->parseNumber("0"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
422 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
423 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
424 storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
425
426 EXPECT_TRUE(scheduler.isDeterministicScheduler());
427 EXPECT_TRUE(scheduler.isMemorylessScheduler());
428 EXPECT_TRUE(!scheduler.isPartialScheduler());
429 auto inducedModel = mdp->applyScheduler(scheduler);
430
431 ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
432 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
433 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
434
435 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedMdp);
436 auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
437 ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
438 EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],
439 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
440 }
441
442 {
443 tasks[1].setOnlyInitialStatesRelevant(true);
444 auto result = checker.check(this->env(), tasks[1]);
445 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
446 ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
447 EXPECT_NEAR(this->parseNumber("1"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
448 storm::utility::convertNumber<ValueType>(this->env().solver().minMax().getPrecision()));
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::Dtmc);
457 auto const& inducedMdp = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
458 EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
459
460 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedMdp);
461 auto inducedResult = inducedChecker.check(this->env(), tasks[1]);
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} // 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
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