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