Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
PrismMenuGameTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-gamebased-ar/abstraction/MenuGameRefiner.h"
5#include "storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.h"
6#include "storm-parsers/parser/PrismParser.h"
7#include "storm/environment/Environment.h"
8#include "storm/models/symbolic/StandardRewardModel.h"
9#include "storm/settings/SettingsManager.h"
10#include "storm/settings/modules/AbstractionSettings.h"
11#include "storm/storage/dd/Bdd.h"
12#include "storm/storage/expressions/Expression.h"
13#include "storm/utility/solver.h"
14
15class Cudd {
16 public:
17 static void checkLibraryAvailable() {
18#ifndef STORM_HAVE_CUDD
19 GTEST_SKIP() << "Library CUDD not available.";
20#endif
21 }
22
23 static const storm::dd::DdType DdType = storm::dd::DdType::CUDD;
24};
25
26class Sylvan {
27 public:
28 static void checkLibraryAvailable() {
29#ifndef STORM_HAVE_SYLVAN
30 GTEST_SKIP() << "Library Sylvan not available.";
31#endif
32 }
33
34 static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan;
35};
36
37template<typename TestType>
38class PrismMenuGame : public ::testing::Test {
39 public:
40 static const storm::dd::DdType DdType = TestType::DdType;
41
42 protected:
43 void SetUp() override {
44#ifndef STORM_HAVE_MATHSAT
45 GTEST_SKIP() << "MathSAT not available.";
46#endif
47 TestType::checkLibraryAvailable();
48 }
49};
50
51typedef ::testing::Types<Cudd, Sylvan> TestingTypes;
52TYPED_TEST_SUITE(PrismMenuGame, TestingTypes, );
53
54TYPED_TEST(PrismMenuGame, DieAbstractionTest) {
55 const storm::dd::DdType DdType = TestFixture::DdType;
56 auto& settings = storm::settings::mutableAbstractionSettings();
57 settings.setAddAllGuards(false);
58 settings.setAddAllInitialExpressions(false);
59
60 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
61
62 std::vector<storm::expressions::Expression> initialPredicates;
63 storm::expressions::ExpressionManager& manager = program.getManager();
64
65 initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
66 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
67
68 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
69 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
70 refiner.refine(initialPredicates);
71
72 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
73
74 EXPECT_EQ(26ull, game.getNumberOfTransitions());
75 EXPECT_EQ(4ull, game.getNumberOfStates());
76 EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount());
77
78 storm::settings::mutableAbstractionSettings().restoreDefaults();
79}
80
81TYPED_TEST(PrismMenuGame, DieAbstractionAndRefinementTest) {
82 const storm::dd::DdType DdType = TestFixture::DdType;
83 auto& settings = storm::settings::mutableAbstractionSettings();
84 settings.setAddAllGuards(false);
85 settings.setAddAllInitialExpressions(false);
86
87 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
88
89 std::vector<storm::expressions::Expression> initialPredicates;
90 storm::expressions::ExpressionManager& manager = program.getManager();
91
92 initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
93
94 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
95
96 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
97 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
98 refiner.refine(initialPredicates);
99
100 ASSERT_NO_THROW(refiner.refine({manager.getVariableExpression("s") == manager.integer(7)}));
101
102 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
103
104 EXPECT_EQ(24ull, game.getNumberOfTransitions());
105 EXPECT_EQ(5ull, game.getNumberOfStates());
106 EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount());
107
108 storm::settings::mutableAbstractionSettings().restoreDefaults();
109}
110
111TYPED_TEST(PrismMenuGame, DieFullAbstractionTest) {
112 const storm::dd::DdType DdType = TestFixture::DdType;
113 auto& settings = storm::settings::mutableAbstractionSettings();
114 settings.setAddAllGuards(false);
115 settings.setAddAllInitialExpressions(false);
116
117 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
118
119 std::vector<storm::expressions::Expression> initialPredicates;
120 storm::expressions::ExpressionManager& manager = program.getManager();
121
122 initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(0));
123 initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(1));
124 initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(2));
125 initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(3));
126 initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(4));
127 initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(5));
128 initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(6));
129 initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(7));
130
131 initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(0));
132 initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(1));
133 initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(2));
134 initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(3));
135 initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(4));
136 initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(5));
137 initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(6));
138
139 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
140
141 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
142 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
143 refiner.refine(initialPredicates);
144
145 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
146
147 EXPECT_EQ(20ull, game.getNumberOfTransitions());
148 EXPECT_EQ(13ull, game.getNumberOfStates());
149 EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
150
151 storm::settings::mutableAbstractionSettings().restoreDefaults();
152}
153
154TYPED_TEST(PrismMenuGame, CrowdsAbstractionTest) {
155 const storm::dd::DdType DdType = TestFixture::DdType;
156 auto& settings = storm::settings::mutableAbstractionSettings();
157 settings.setAddAllGuards(false);
158 settings.setAddAllInitialExpressions(false);
159
160 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
161 program = program.substituteConstantsFormulas();
162
163 std::vector<storm::expressions::Expression> initialPredicates;
164 storm::expressions::ExpressionManager& manager = program.getManager();
165
166 initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
167
168 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
169
170 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
171 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
172 refiner.refine(initialPredicates);
173
174 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
175
176 EXPECT_EQ(31ull, game.getNumberOfTransitions());
177 EXPECT_EQ(4ull, game.getNumberOfStates());
178 EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount());
179
180 storm::settings::mutableAbstractionSettings().restoreDefaults();
181}
182
183TYPED_TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) {
184 const storm::dd::DdType DdType = TestFixture::DdType;
185 auto& settings = storm::settings::mutableAbstractionSettings();
186 settings.setAddAllGuards(false);
187 settings.setAddAllInitialExpressions(false);
188
189 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
190 program = program.substituteConstantsFormulas();
191
192 std::vector<storm::expressions::Expression> initialPredicates;
193 storm::expressions::ExpressionManager& manager = program.getManager();
194
195 initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
196
197 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
198
199 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
200 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
201 refiner.refine(initialPredicates);
202
203 ASSERT_NO_THROW(
204 refiner.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") +
205 manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <=
206 manager.getVariableExpression("runCount")}));
207
208 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
209
210 EXPECT_EQ(68ull, game.getNumberOfTransitions());
211 EXPECT_EQ(8ull, game.getNumberOfStates());
212 EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount());
213
214 storm::settings::mutableAbstractionSettings().restoreDefaults();
215}
216
217TYPED_TEST(PrismMenuGame, CrowdsFullAbstractionTest) {
218 const storm::dd::DdType DdType = TestFixture::DdType;
219 auto& settings = storm::settings::mutableAbstractionSettings();
220 settings.setAddAllGuards(false);
221 settings.setAddAllInitialExpressions(false);
222
223 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
224 program = program.substituteConstantsFormulas();
225
226 std::vector<storm::expressions::Expression> initialPredicates;
227 storm::expressions::ExpressionManager& manager = program.getManager();
228
229 initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(0));
230 initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(1));
231 initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(2));
232 initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(3));
233 initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(4));
234
235 initialPredicates.push_back(manager.getVariableExpression("good"));
236
237 initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(0));
238 initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(1));
239 initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(2));
240 initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(3));
241 initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(4));
242 initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(5));
243
244 initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(0));
245 initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(1));
246 initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(2));
247 initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(3));
248 initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(4));
249 initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(5));
250
251 initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(0));
252 initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(1));
253 initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(2));
254 initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(3));
255 initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(4));
256 initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(5));
257
258 initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(0));
259 initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(1));
260 initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(2));
261 initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(3));
262 initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(4));
263 initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(5));
264
265 initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(0));
266 initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(1));
267 initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(2));
268 initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(3));
269 initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(4));
270 initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(5));
271
272 initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(0));
273 initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(1));
274 initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(2));
275 initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(3));
276 initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(4));
277 initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(5));
278
279 initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(0));
280 initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(1));
281 initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(2));
282 initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(3));
283 initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(4));
284
285 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
286
287 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
288 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
289 refiner.refine(initialPredicates);
290
291 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
292
293 EXPECT_EQ(15113ull, game.getNumberOfTransitions());
294 EXPECT_EQ(8607ull, game.getNumberOfStates());
295 EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
296
297 storm::settings::mutableAbstractionSettings().restoreDefaults();
298}
299
300TYPED_TEST(PrismMenuGame, TwoDiceAbstractionTest) {
301 const storm::dd::DdType DdType = TestFixture::DdType;
302 auto& settings = storm::settings::mutableAbstractionSettings();
303 settings.setAddAllGuards(false);
304 settings.setAddAllInitialExpressions(false);
305
306 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
307 program = program.substituteConstantsFormulas();
308 program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
309
310 std::vector<storm::expressions::Expression> initialPredicates;
311 storm::expressions::ExpressionManager& manager = program.getManager();
312
313 initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
314 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
315
316 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
317
318 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
319 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
320 refiner.refine(initialPredicates);
321
322 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
323
324 EXPECT_EQ(90ull, game.getNumberOfTransitions());
325 EXPECT_EQ(8ull, game.getNumberOfStates());
326 EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount());
327
328 storm::settings::mutableAbstractionSettings().restoreDefaults();
329}
330TYPED_TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) {
331 const storm::dd::DdType DdType = TestFixture::DdType;
332 auto& settings = storm::settings::mutableAbstractionSettings();
333 settings.setAddAllGuards(false);
334 settings.setAddAllInitialExpressions(false);
335
336 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
337 program = program.substituteConstantsFormulas();
338 program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
339
340 std::vector<storm::expressions::Expression> initialPredicates;
341 storm::expressions::ExpressionManager& manager = program.getManager();
342
343 initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
344 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
345
346 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
347
348 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
349 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
350 refiner.refine(initialPredicates);
351
352 ASSERT_NO_THROW(refiner.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)}));
353
354 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
355
356 EXPECT_EQ(276ull, game.getNumberOfTransitions());
357 EXPECT_EQ(16ull, game.getNumberOfStates());
358 EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount());
359
360 storm::settings::mutableAbstractionSettings().restoreDefaults();
361}
362TYPED_TEST(PrismMenuGame, TwoDiceFullAbstractionTest) {
363 const storm::dd::DdType DdType = TestFixture::DdType;
364 auto& settings = storm::settings::mutableAbstractionSettings();
365 settings.setAddAllGuards(false);
366 settings.setAddAllInitialExpressions(false);
367
368 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
369 program = program.substituteConstantsFormulas();
370 program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
371
372 std::vector<storm::expressions::Expression> initialPredicates;
373 storm::expressions::ExpressionManager& manager = program.getManager();
374
375 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(0));
376 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1));
377 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2));
378 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3));
379 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4));
380 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5));
381 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6));
382 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7));
383
384 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(0));
385 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(1));
386 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(2));
387 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(3));
388 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(4));
389 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(5));
390 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(6));
391
392 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
393 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1));
394 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2));
395 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3));
396 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4));
397 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5));
398 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6));
399 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7));
400
401 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(0));
402 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(1));
403 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(2));
404 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(3));
405 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(4));
406 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5));
407 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6));
408
409 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
410
411 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
412 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
413 refiner.refine(initialPredicates);
414
415 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
416
417 EXPECT_EQ(436ull, game.getNumberOfTransitions());
418 EXPECT_EQ(169ull, game.getNumberOfStates());
419 EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
420
421 storm::settings::mutableAbstractionSettings().restoreDefaults();
422}
423
424TYPED_TEST(PrismMenuGame, WlanAbstractionTest) {
425 const storm::dd::DdType DdType = TestFixture::DdType;
426 auto& settings = storm::settings::mutableAbstractionSettings();
427 settings.setAddAllGuards(false);
428 settings.setAddAllInitialExpressions(false);
429
430 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
431 program = program.substituteConstantsFormulas();
432 program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
433
434 std::vector<storm::expressions::Expression> initialPredicates;
435 storm::expressions::ExpressionManager& manager = program.getManager();
436
437 initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(5));
438 initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
439 initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
440
441 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
442
443 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
444 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
445 refiner.refine(initialPredicates);
446
447 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
448
449 EXPECT_EQ(903ull, game.getNumberOfTransitions());
450 EXPECT_EQ(8ull, game.getNumberOfStates());
451 EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount());
452
453 storm::settings::mutableAbstractionSettings().restoreDefaults();
454}
455
456TYPED_TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
457 const storm::dd::DdType DdType = TestFixture::DdType;
458 auto& settings = storm::settings::mutableAbstractionSettings();
459 settings.setAddAllGuards(false);
460 settings.setAddAllInitialExpressions(false);
461
462 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
463 program = program.substituteConstantsFormulas();
464 program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
465
466 std::vector<storm::expressions::Expression> initialPredicates;
467 storm::expressions::ExpressionManager& manager = program.getManager();
468
469 initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(5));
470 initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
471 initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
472
473 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
474
475 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
476 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
477 refiner.refine(initialPredicates);
478
479 ASSERT_NO_THROW(refiner.refine({manager.getVariableExpression("backoff1") < manager.integer(7)}));
480
481 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
482
483 EXPECT_EQ(1800ull, game.getNumberOfTransitions());
484 EXPECT_EQ(16ull, game.getNumberOfStates());
485 EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount());
486
487 storm::settings::mutableAbstractionSettings().restoreDefaults();
488}
489
490TYPED_TEST(PrismMenuGame, WlanFullAbstractionTest) {
491 const storm::dd::DdType DdType = TestFixture::DdType;
492 auto& settings = storm::settings::mutableAbstractionSettings();
493 settings.setAddAllGuards(false);
494 settings.setAddAllInitialExpressions(false);
495
496 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
497 program = program.substituteConstantsFormulas();
498 program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
499
500 std::vector<storm::expressions::Expression> initialPredicates;
501 storm::expressions::ExpressionManager& manager = program.getManager();
502
503 initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(0));
504 initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(1));
505 initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(2));
506
507 initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(0));
508 initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(1));
509 initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(2));
510
511 initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(0));
512 initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(1));
513 initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(2));
514
515 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(0));
516 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(1));
517 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(2));
518 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(3));
519 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(4));
520 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(5));
521 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(6));
522 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(7));
523
524 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1));
525 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2));
526 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3));
527 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4));
528 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5));
529 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6));
530 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7));
531 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(8));
532 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(9));
533 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(10));
534 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(11));
535 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(12));
536
537 initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(0));
538 initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(1));
539
540 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(0));
541 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(1));
542 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(2));
543 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(3));
544 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(4));
545 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(5));
546 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(6));
547 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(7));
548 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(8));
549 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(9));
550 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(10));
551 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(11));
552 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(12));
553 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(13));
554 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(14));
555 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(15));
556
557 initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
558 initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(1));
559
560 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(0));
561 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(1));
562 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(2));
563 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(3));
564 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(4));
565 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(5));
566 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(6));
567 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(7));
568
569 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1));
570 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2));
571 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3));
572 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4));
573 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5));
574 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6));
575 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7));
576 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(8));
577 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(9));
578 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(10));
579 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(11));
580 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(12));
581
582 initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(0));
583 initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(1));
584
585 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(0));
586 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(1));
587 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(2));
588 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(3));
589 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(4));
590 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(5));
591 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(6));
592 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(7));
593 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(8));
594 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(9));
595 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(10));
596 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(11));
597 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(12));
598 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(13));
599 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(14));
600 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(15));
601
602 initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0));
603 initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1));
604
605 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
606
607 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(storm::Environment(), program, smtSolverFactory);
608 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
609 refiner.refine(initialPredicates);
610
611 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
612
613 EXPECT_EQ(9503ull, game.getNumberOfTransitions());
614 EXPECT_EQ(5523ull, game.getNumberOfStates());
615 EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount());
616
617 storm::settings::mutableAbstractionSettings().restoreDefaults();
618}
TYPED_TEST_SUITE
TYPED_TEST_SUITE(PrismMenuGame, TestingTypes,)
TYPED_TEST
TYPED_TEST(PrismMenuGame, DieAbstractionTest)
Definition PrismMenuGameTest.cpp:54
Cudd::checkLibraryAvailable
static void checkLibraryAvailable()
Definition PrismMenuGameTest.cpp:17
Cudd::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:33
PrismMenuGame::DdType
static const storm::dd::DdType DdType
Definition PrismMenuGameTest.cpp:40
PrismMenuGame::SetUp
void SetUp() override
Definition PrismMenuGameTest.cpp:43
Sylvan::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:44
Sylvan::checkLibraryAvailable
static void checkLibraryAvailable()
Definition PrismMenuGameTest.cpp:28
storm::dd::Bdd::getNonZeroCount
virtual uint_fast64_t getNonZeroCount() const override
Retrieves the number of encodings that are mapped to a non-zero value.
Definition Bdd.cpp:507
storm::expressions::ExpressionManager
This class is responsible for managing a set of typed variables and all expressions using these varia...
Definition ExpressionManager.h:71
storm::gbar::abstraction::MenuGame
This class represents a discrete-time stochastic two-player game.
Definition MenuGame.h:14
storm::gbar::abstraction::MenuGame::getBottomStates
storm::dd::Bdd< Type > getBottomStates() const
Retrieves the bottom states of the model.
Definition MenuGame.cpp:64
storm::gbar::abstraction::MenuGameRefiner::refine
void refine(std::vector< storm::expressions::Expression > const &predicates, bool allowInjection=true) const
Refines the abstractor with the given predicates.
Definition MenuGameRefiner.cpp:107
storm::gbar::abstraction::prism::PrismMenuGameAbstractor::abstract
MenuGame< DdType, ValueType > abstract() override
Uses the current set of predicates to derive the abstract menu game in the form of an ADD.
Definition PrismMenuGameAbstractor.cpp:113
storm::models::symbolic::Model::getNumberOfTransitions
virtual uint_fast64_t getNumberOfTransitions() const override
Returns the number of (non-zero) transitions of the model.
Definition Model.cpp:78
storm::models::symbolic::Model::getNumberOfStates
virtual uint_fast64_t getNumberOfStates() const override
Returns the number of states of the model.
Definition Model.cpp:73
storm::parser::PrismParser::parse
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
Definition PrismParser.cpp:5
storm::prism::Program::substituteConstantsFormulas
Program substituteConstantsFormulas(bool substituteConstants=true, bool substituteFormulas=true) const
Substitutes all constants and/or formulas appearing in the expressions of the program by their defini...
Definition Program.cpp:1096
storm::prism::Program::getManager
storm::expressions::ExpressionManager & getManager() const
Retrieves the manager responsible for the expressions of this program.
Definition Program.cpp:2388
storm::prism::Program::flattenModules
Program flattenModules(std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &smtSolverFactory=std::shared_ptr< storm::utility::solver::SmtSolverFactory >(new storm::utility::solver::SmtSolverFactory())) const
Creates an equivalent program that contains exactly one module.
Definition Program.cpp:1980
storm::settings::modules::ModuleSettings::restoreDefaults
void restoreDefaults()
Restores the default values for all arguments of all options.
Definition ModuleSettings.cpp:66
storm::settings::mutableAbstractionSettings
storm::settings::modules::AbstractionSettings & mutableAbstractionSettings()
Retrieves the abstraction settings in a mutable form.
Definition SettingsManager.cpp:693
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:61
storm_gtest.h