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