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