Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GraphTest.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/builder/DdPrismModelBuilder.h"
8#include "storm/builder/ExplicitModelBuilder.h"
9#include "storm/models/sparse/Dtmc.h"
10#include "storm/models/sparse/Mdp.h"
11#include "storm/models/sparse/StandardRewardModel.h"
12#include "storm/models/symbolic/Dtmc.h"
13#include "storm/models/symbolic/Mdp.h"
14#include "storm/models/symbolic/StandardRewardModel.h"
15#include "storm/storage/SymbolicModelDescription.h"
16#include "storm/storage/dd/Add.h"
17#include "storm/storage/dd/Bdd.h"
18#include "storm/storage/dd/DdManager.h"
19#include "storm/storage/expressions/Expression.h"
20#include "storm/utility/graph.h"
21#include "storm/utility/solver.h"
22
23class Cudd {
24 public:
25 static const storm::dd::DdType DdType = storm::dd::DdType::CUDD;
26};
27
28class Sylvan {
29 public:
30 static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan;
31};
32
33template<typename TestType>
34class GraphTestAR : public ::testing::Test {
35 public:
36 static const storm::dd::DdType DdType = TestType::DdType;
37
38 protected:
39 void SetUp() override {
40#ifndef STORM_HAVE_MSAT
41 GTEST_SKIP() << "MathSAT not available.";
42#endif
43 }
44};
45
46typedef ::testing::Types<Cudd, Sylvan> TestingTypes;
47TYPED_TEST_SUITE(GraphTestAR, TestingTypes, );
48
49TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall) {
50 const storm::dd::DdType DdType = TestFixture::DdType;
51 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
52
53 std::vector<storm::expressions::Expression> initialPredicates;
54 storm::expressions::ExpressionManager& manager = program.getManager();
55
56 initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
57
58 auto smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
59 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(program, smtSolverFactory);
60 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
61 refiner.refine(initialPredicates);
62
63 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
64
65 // The target states are those states where !(s < 3).
66 storm::dd::Bdd<DdType> targetStates = !abstractor.getStates(initialPredicates[0]) && game.getReachableStates();
67
68 storm::utility::graph::SymbolicGameProb01Result<DdType> result =
69 storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
70 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
71 EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
72 EXPECT_TRUE(result.hasPlayer1Strategy());
73 EXPECT_TRUE(result.hasPlayer2Strategy());
74
75 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
76 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
77 EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
78
79 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
80 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
81 EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
82
83 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
84 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
85 EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
86
87 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
88 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
89 EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
90
91 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
92 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
93 EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
94
95 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
96 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
97 EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
98
99 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
100 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
101 EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
102 EXPECT_TRUE(result.hasPlayer1Strategy());
103 EXPECT_TRUE(result.hasPlayer2Strategy());
104
105 refiner.refine({manager.getVariableExpression("s") < manager.integer(2)});
106 game = abstractor.abstract();
107
108 // We need to create a new BDD for the target states since the reachable states might have changed.
109 targetStates = !abstractor.getStates(initialPredicates[0]) && game.getReachableStates();
110
111 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
112 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
113 EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
114 ASSERT_TRUE(result.hasPlayer1Strategy());
115 ASSERT_TRUE(result.hasPlayer2Strategy());
116
117 // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy.
118 storm::dd::Bdd<DdType> nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
119 EXPECT_TRUE(nonProb0StatesWithStrategy.isZero());
120
121 // Proceed by checking whether they select exactly one action in each state.
122 storm::dd::Add<DdType, double> stateDistributionsUnderStrategies =
123 (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>())
124 .sumAbstract(game.getColumnVariables());
125 EXPECT_EQ(0ull, stateDistributionsUnderStrategies.getNonZeroCount());
126
127 // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states).
128 storm::dd::Add<DdType> stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
129 EXPECT_EQ(0.0, stateDistributionCount.getMax());
130
131 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
132 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
133 EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
134
135 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
136 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
137 EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
138
139 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
140 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
141 EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
142
143 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
144 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
145 EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
146
147 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
148 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
149 EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
150
151 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
152 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
153 EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount());
154
155 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
156 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
157 EXPECT_EQ(8ull, result.getPlayer1States().getNonZeroCount());
158 EXPECT_TRUE(result.hasPlayer1Strategy());
159 EXPECT_TRUE(result.hasPlayer2Strategy());
160
161 // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy.
162 storm::dd::Bdd<DdType> nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
163 EXPECT_TRUE(nonProb1StatesWithStrategy.isZero());
164
165 // Proceed by checking whether they select exactly one action in each state.
166 stateDistributionsUnderStrategies =
167 (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>())
168 .sumAbstract(game.getColumnVariables());
169 EXPECT_EQ(8ull, stateDistributionsUnderStrategies.getNonZeroCount());
170
171 // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states).
172 stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
173 EXPECT_EQ(1.0, stateDistributionCount.getMax());
174}
175
176TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameTwoDice) {
177 const storm::dd::DdType DdType = TestFixture::DdType;
178 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
179 program = program.substituteConstantsFormulas();
180 program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
181
182 std::vector<storm::expressions::Expression> initialPredicates;
183 storm::expressions::ExpressionManager& manager = program.getManager();
184
185 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(0));
186 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1));
187 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2));
188 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3));
189 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4));
190 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5));
191 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6));
192 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7));
193
194 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(0));
195 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(1));
196 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(2));
197 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(3));
198 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(4));
199 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(5));
200 initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(6));
201
202 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
203 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1));
204 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2));
205 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3));
206 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4));
207 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5));
208 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6));
209 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7));
210
211 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(0));
212 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(1));
213 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(2));
214 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(3));
215 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(4));
216 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5));
217 initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6));
218
219 auto smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
220 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(program, smtSolverFactory);
221 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
222 refiner.refine(initialPredicates);
223
224 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
225
226 // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 2.
227 storm::dd::Bdd<DdType> targetStates = abstractor.getStates(initialPredicates[7]) && abstractor.getStates(initialPredicates[22]) &&
228 abstractor.getStates(initialPredicates[9]) && abstractor.getStates(initialPredicates[24]) &&
229 game.getReachableStates();
230
231 storm::utility::graph::SymbolicGameProb01Result<DdType> result =
232 storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
233 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
234 EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount());
235 ASSERT_TRUE(result.hasPlayer1Strategy());
236 ASSERT_TRUE(result.hasPlayer2Strategy());
237
238 // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy.
239 storm::dd::Bdd<DdType> nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
240 EXPECT_TRUE(nonProb0StatesWithStrategy.isZero());
241
242 // Proceed by checking whether they select exactly one exaction in each state.
243 storm::dd::Add<DdType, double> stateDistributionsUnderStrategies =
244 (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>())
245 .sumAbstract(game.getColumnVariables());
246 EXPECT_EQ(153ull, stateDistributionsUnderStrategies.getNonZeroCount());
247
248 storm::dd::Add<DdType> stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
249 EXPECT_EQ(1.0, stateDistributionCount.getMax());
250
251 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
252 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
253 EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount());
254
255 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
256 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
257 EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount());
258
259 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
260 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
261 EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount());
262
263 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
264 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
265 EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount());
266
267 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
268 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
269 EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount());
270
271 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
272 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
273 EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount());
274
275 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
276 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
277 EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount());
278 EXPECT_TRUE(result.hasPlayer1Strategy());
279 EXPECT_TRUE(result.hasPlayer2Strategy());
280
281 // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy.
282 storm::dd::Bdd<DdType> nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
283 EXPECT_TRUE(nonProb1StatesWithStrategy.isZero());
284
285 // Proceed by checking whether they select exactly one action in each state.
286 stateDistributionsUnderStrategies =
287 (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>())
288 .sumAbstract(game.getColumnVariables());
289 EXPECT_EQ(1ull, stateDistributionsUnderStrategies.getNonZeroCount());
290
291 // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states).
292 stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
293 EXPECT_EQ(1.0, stateDistributionCount.getMax());
294}
295
296TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameWlan) {
297 const storm::dd::DdType DdType = TestFixture::DdType;
298 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm");
299 program = program.substituteConstantsFormulas();
300 program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
301
302 std::vector<storm::expressions::Expression> initialPredicates;
303 storm::expressions::ExpressionManager& manager = program.getManager();
304
305 initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(0));
306 initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(1));
307 initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(2));
308
309 initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(0));
310 initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(1));
311 initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(2));
312
313 initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(0));
314 initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(1));
315 initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(2));
316
317 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(0));
318 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(1));
319 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(2));
320 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(3));
321 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(4));
322 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(5));
323 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(6));
324 initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(7));
325
326 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1));
327 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2));
328 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3));
329 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4));
330 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5));
331 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6));
332 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7));
333 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(8));
334 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(9));
335 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(10));
336 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(11));
337 initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(12));
338
339 initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(0));
340 initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(1));
341
342 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(0));
343 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(1));
344 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(2));
345 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(3));
346 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(4));
347 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(5));
348 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(6));
349 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(7));
350 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(8));
351 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(9));
352 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(10));
353 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(11));
354 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(12));
355 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(13));
356 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(14));
357 initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(15));
358
359 initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
360 initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(1));
361
362 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(0));
363 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(1));
364 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(2));
365 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(3));
366 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(4));
367 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(5));
368 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(6));
369 initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(7));
370
371 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1));
372 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2));
373 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3));
374 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4));
375 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5));
376 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6));
377 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7));
378 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(8));
379 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(9));
380 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(10));
381 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(11));
382 initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(12));
383
384 initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(0));
385 initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(1));
386
387 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(0));
388 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(1));
389 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(2));
390 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(3));
391 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(4));
392 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(5));
393 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(6));
394 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(7));
395 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(8));
396 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(9));
397 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(10));
398 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(11));
399 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(12));
400 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(13));
401 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(14));
402 initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(15));
403
404 initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0));
405 initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1));
406
407 auto smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
408 storm::gbar::abstraction::prism::PrismMenuGameAbstractor<DdType, double> abstractor(program, smtSolverFactory);
409 storm::gbar::abstraction::MenuGameRefiner<DdType, double> refiner(abstractor, smtSolverFactory->create(manager));
410 refiner.refine(initialPredicates);
411
412 storm::gbar::abstraction::MenuGame<DdType, double> game = abstractor.abstract();
413
414 // The target states are those states where col == 2.
415 storm::dd::Bdd<DdType> targetStates = abstractor.getStates(initialPredicates[2]) && game.getReachableStates();
416
417 storm::utility::graph::SymbolicGameProb01Result<DdType> result =
418 storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
419 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
420 EXPECT_EQ(2831ull, result.getPlayer1States().getNonZeroCount());
421 EXPECT_TRUE(result.hasPlayer1Strategy());
422 EXPECT_TRUE(result.hasPlayer2Strategy());
423
424 // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy.
425 storm::dd::Bdd<DdType> nonProb0StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
426 EXPECT_TRUE(nonProb0StatesWithStrategy.isZero());
427
428 // Proceed by checking whether they select exactly one action in each state.
429 storm::dd::Add<DdType, double> stateDistributionsUnderStrategies =
430 (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>())
431 .sumAbstract(game.getColumnVariables());
432 ;
433 EXPECT_EQ(2831ull, stateDistributionsUnderStrategies.getNonZeroCount());
434
435 // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states).
436 storm::dd::Add<DdType> stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
437 EXPECT_EQ(1.0, stateDistributionCount.getMax());
438
439 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
440 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
441 EXPECT_EQ(2692ull, result.getPlayer1States().getNonZeroCount());
442
443 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
444 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
445 EXPECT_EQ(2831ull, result.getPlayer1States().getNonZeroCount());
446
447 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
448 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
449 EXPECT_EQ(2692ull, result.getPlayer1States().getNonZeroCount());
450
451 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
452 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
453 EXPECT_EQ(2064ull, result.getPlayer1States().getNonZeroCount());
454
455 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
456 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
457 EXPECT_EQ(2884ull, result.getPlayer1States().getNonZeroCount());
458
459 result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
460 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
461 EXPECT_EQ(2064ull, result.getPlayer1States().getNonZeroCount());
462
463 result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates,
464 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
465 EXPECT_EQ(2884ull, result.getPlayer1States().getNonZeroCount());
466 EXPECT_TRUE(result.hasPlayer1Strategy());
467 EXPECT_TRUE(result.hasPlayer2Strategy());
468
469 // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy.
470 storm::dd::Bdd<DdType> nonProb1StatesWithStrategy = !result.getPlayer1States() && result.player1Strategy.get();
471 EXPECT_TRUE(nonProb1StatesWithStrategy.isZero());
472
473 // Proceed by checking whether they select exactly one action in each state.
474 stateDistributionsUnderStrategies =
475 (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>())
476 .sumAbstract(game.getColumnVariables());
477 EXPECT_EQ(2884ull, stateDistributionsUnderStrategies.getNonZeroCount());
478
479 // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states).
480 stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
481 EXPECT_EQ(1.0, stateDistributionCount.getMax());
482}
Cudd::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:25
GraphTestAR::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:36
GraphTestAR::SetUp
void SetUp() override
Definition GraphTest.cpp:39
Sylvan::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:30
storm::dd::Add::getMax
ValueType getMax() const
Retrieves the highest function value of any encoding.
Definition Add.cpp:475
storm::dd::Add::getNonZeroCount
virtual uint_fast64_t getNonZeroCount() const override
Retrieves the number of encodings that are mapped to a non-zero value.
Definition Add.cpp:451
storm::dd::Add::sumAbstract
Add< LibraryType, ValueType > sumAbstract(std::set< storm::expressions::Variable > const &metaVariables) const
Sum-abstracts from the given meta variables.
Definition Add.cpp:178
storm::dd::Bdd::isZero
bool isZero() const
Retrieves whether this DD represents the constant zero function.
Definition Bdd.cpp:547
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::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::gbar::abstraction::prism::PrismMenuGameAbstractor::getStates
storm::dd::Bdd< DdType > getStates(storm::expressions::Expression const &expression) override
Retrieves a BDD that characterizes the states corresponding to the given expression.
Definition PrismMenuGameAbstractor.cpp:167
storm::models::symbolic::Model::getTransitionMatrix
storm::dd::Add< Type, ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:177
storm::models::symbolic::Model::getColumnVariables
std::set< storm::expressions::Variable > const & getColumnVariables() const
Retrieves the meta variables used to encode the columns of the transition matrix and the vector indic...
Definition Model.cpp:197
storm::models::symbolic::Model::getReachableStates
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
Definition Model.cpp:102
storm::models::symbolic::NondeterministicModel::getNondeterminismVariables
virtual std::set< storm::expressions::Variable > const & getNondeterminismVariables() const override
Retrieves the meta variables used to encode the nondeterminism in the model.
Definition NondeterministicModel.cpp:60
storm::models::symbolic::NondeterministicModel::getQualitativeTransitionMatrix
virtual storm::dd::Bdd< Type > getQualitativeTransitionMatrix(bool keepNondeterminism=true) const override
Retrieves the matrix qualitatively (i.e.
Definition NondeterministicModel.cpp:106
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::utility::graph::performProb0
ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint64_t > const &player1Groups, storm::storage::SparseMatrix< ValueType > const &player1BackwardTransitions, std::vector< uint64_t > const &player2BackwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::OptimizationDirection const &player1Direction, storm::OptimizationDirection const &player2Direction, storm::storage::ExplicitGameStrategyPair *strategyPair)
Computes the set of states that have probability 0 given the strategies of the two players.
Definition graph.cpp:1308
storm::utility::graph::performProb1
storm::storage::BitVector performProb1(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &, storm::storage::BitVector const &psiStates, storm::storage::BitVector const &statesWithProbabilityGreater0)
Computes the set of states of the given model for which all paths lead to the given set of target sta...
Definition graph.cpp:383
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h
storm::utility::graph::SymbolicGameProb01Result::player1Strategy
boost::optional< storm::dd::Bdd< Type > > player1Strategy
Definition graph.h:709
storm::utility::graph::SymbolicGameProb01Result::player2Strategy
boost::optional< storm::dd::Bdd< Type > > player2Strategy
Definition graph.h:710
storm::utility::graph::SymbolicGameProb01Result::getPlayer1States
storm::dd::Bdd< Type > const & getPlayer1States() const
Definition graph.h:699