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