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