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