Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DdTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm/exceptions/InvalidArgumentException.h"
5#include "storm/settings/SettingsManager.h"
6#include "storm/storage/SparseMatrix.h"
7#include "storm/storage/dd/Add.h"
8#include "storm/storage/dd/DdManager.h"
9#include "storm/storage/dd/DdMetaVariable.h"
10#include "storm/storage/dd/Odd.h"
11#include "storm/storage/expressions/Expression.h"
12#include "storm/storage/expressions/ExpressionManager.h"
13
14class Cudd {
15 public:
16 static const storm::dd::DdType DdType = storm::dd::DdType::CUDD;
17};
18
19class Sylvan {
20 public:
21 static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan;
22};
23
24template<typename TestType>
25class Dd : public ::testing::Test {
26 public:
27 static const storm::dd::DdType DdType = TestType::DdType;
28};
29
30typedef ::testing::Types<Cudd, Sylvan> TestingTypes;
31TYPED_TEST_SUITE(Dd, TestingTypes, );
32
33TYPED_TEST(Dd, AddConstants) {
34 const storm::dd::DdType DdType = TestFixture::DdType;
35 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
36 manager->execute([&]() {
37 storm::dd::Add<DdType, double> zero;
38 ASSERT_NO_THROW(zero = manager->template getAddZero<double>());
39
40 EXPECT_EQ(0ul, zero.getNonZeroCount());
41 EXPECT_EQ(1ul, zero.getLeafCount());
42 EXPECT_EQ(1ul, zero.getNodeCount());
43 EXPECT_EQ(0, zero.getMin());
44 EXPECT_EQ(0, zero.getMax());
45
46 storm::dd::Add<DdType, double> one;
47 ASSERT_NO_THROW(one = manager->template getAddOne<double>());
48
49 EXPECT_EQ(0ul, one.getNonZeroCount());
50 EXPECT_EQ(1ul, one.getLeafCount());
51 EXPECT_EQ(1ul, one.getNodeCount());
52 EXPECT_EQ(1, one.getMin());
53 EXPECT_EQ(1, one.getMax());
54
55 storm::dd::Add<DdType, double> two;
56 ASSERT_NO_THROW(two = manager->template getConstant<double>(2));
57
58 EXPECT_EQ(0ul, two.getNonZeroCount());
59 EXPECT_EQ(1ul, two.getLeafCount());
60 EXPECT_EQ(1ul, two.getNodeCount());
61 EXPECT_EQ(2, two.getMin());
62 EXPECT_EQ(2, two.getMax());
63 });
64}
65
66TYPED_TEST(Dd, BddConstants) {
67 const storm::dd::DdType DdType = TestFixture::DdType;
68 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
69 manager->execute([&]() {
70 storm::dd::Bdd<DdType> zero;
71 ASSERT_NO_THROW(zero = manager->getBddZero());
72
73 EXPECT_EQ(0ul, zero.getNonZeroCount());
74 EXPECT_EQ(1ul, zero.getLeafCount());
75 EXPECT_EQ(1ul, zero.getNodeCount());
76
77 storm::dd::Bdd<DdType> one;
78 ASSERT_NO_THROW(one = manager->getBddOne());
79
80 EXPECT_EQ(0ul, one.getNonZeroCount());
81 EXPECT_EQ(1ul, one.getLeafCount());
82 EXPECT_EQ(1ul, one.getNodeCount());
83 });
84}
85
86TYPED_TEST(Dd, BddExistAbstractRepresentative) {
87 const storm::dd::DdType DdType = TestFixture::DdType;
88 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
89
90 manager->execute([&]() {
91 storm::dd::Bdd<DdType> zero;
92 ASSERT_NO_THROW(zero = manager->getBddZero());
93 storm::dd::Bdd<DdType> one;
94 ASSERT_NO_THROW(one = manager->getBddOne());
95
96 std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
97 std::pair<storm::expressions::Variable, storm::expressions::Variable> y;
98 std::pair<storm::expressions::Variable, storm::expressions::Variable> z;
99 ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1));
100 ASSERT_NO_THROW(y = manager->addMetaVariable("y", 0, 1));
101 ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1));
102
103 storm::dd::Bdd<DdType> bddX0 = manager->getEncoding(x.first, 0);
104 storm::dd::Bdd<DdType> bddX1 = manager->getEncoding(x.first, 1);
105 storm::dd::Bdd<DdType> bddY0 = manager->getEncoding(y.first, 0);
106 storm::dd::Bdd<DdType> bddY1 = manager->getEncoding(y.first, 1);
107 storm::dd::Bdd<DdType> bddZ0 = manager->getEncoding(z.first, 0);
108 storm::dd::Bdd<DdType> bddZ1 = manager->getEncoding(z.first, 1);
109
110 // Abstract from FALSE
111 storm::dd::Bdd<DdType> representative_false_x = zero.existsAbstractRepresentative({x.first});
112 EXPECT_EQ(0ul, representative_false_x.getNonZeroCount());
113 EXPECT_EQ(1ul, representative_false_x.getLeafCount());
114 EXPECT_EQ(1ul, representative_false_x.getNodeCount());
115 EXPECT_TRUE(representative_false_x == zero);
116
117 // Abstract from TRUE
118 storm::dd::Bdd<DdType> representative_true_x = one.existsAbstractRepresentative({x.first});
119 EXPECT_EQ(0ul, representative_true_x.getNonZeroCount());
120 EXPECT_EQ(1ul, representative_true_x.getLeafCount());
121 EXPECT_EQ(2ul, representative_true_x.getNodeCount());
122 EXPECT_TRUE(representative_true_x == bddX0);
123
124 storm::dd::Bdd<DdType> representative_true_xyz = one.existsAbstractRepresentative({x.first, y.first, z.first});
125 EXPECT_EQ(0ul, representative_true_xyz.getNonZeroCount());
126 EXPECT_EQ(1ul, representative_true_xyz.getLeafCount());
127 EXPECT_EQ(4ul, representative_true_xyz.getNodeCount());
128 EXPECT_TRUE(representative_true_xyz == ((bddX0 && bddY0) && bddZ0));
129
130 storm::dd::Bdd<DdType> bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0;
131 EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount());
132 EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount());
133 EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount());
134
135 storm::dd::Bdd<DdType> representative_x = bddX1Y0Z0.existsAbstractRepresentative({x.first});
136 EXPECT_EQ(1ul, representative_x.getNonZeroCount());
137 EXPECT_EQ(1ul, representative_x.getLeafCount());
138 EXPECT_EQ(4ul, representative_x.getNodeCount());
139 EXPECT_TRUE(bddX1Y0Z0 == representative_x);
140
141 storm::dd::Bdd<DdType> representative_y = bddX1Y0Z0.existsAbstractRepresentative({y.first});
142 EXPECT_EQ(1ul, representative_y.getNonZeroCount());
143 EXPECT_EQ(1ul, representative_y.getLeafCount());
144 EXPECT_EQ(4ul, representative_y.getNodeCount());
145 EXPECT_TRUE(bddX1Y0Z0 == representative_y);
146
147 storm::dd::Bdd<DdType> representative_z = bddX1Y0Z0.existsAbstractRepresentative({z.first});
148 EXPECT_EQ(1ul, representative_z.getNonZeroCount());
149 EXPECT_EQ(1ul, representative_z.getLeafCount());
150 EXPECT_EQ(4ul, representative_z.getNodeCount());
151 EXPECT_TRUE(bddX1Y0Z0 == representative_z);
152
153 storm::dd::Bdd<DdType> representative_xyz = bddX1Y0Z0.existsAbstractRepresentative({x.first, y.first, z.first});
154 EXPECT_EQ(1ul, representative_xyz.getNonZeroCount());
155 EXPECT_EQ(1ul, representative_xyz.getLeafCount());
156 EXPECT_EQ(4ul, representative_xyz.getNodeCount());
157 EXPECT_TRUE(bddX1Y0Z0 == representative_xyz);
158
159 storm::dd::Bdd<DdType> bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0;
160 storm::dd::Bdd<DdType> bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1;
161
162 storm::dd::Bdd<DdType> bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1;
163
164 representative_x = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first});
165 EXPECT_EQ(2ul, representative_x.getNonZeroCount());
166 EXPECT_EQ(1ul, representative_x.getLeafCount());
167 EXPECT_EQ(5ul, representative_x.getNodeCount());
168 EXPECT_TRUE(bddAllTrueOrAllFalse == representative_x);
169
170 representative_y = bddAllTrueOrAllFalse.existsAbstractRepresentative({y.first});
171 EXPECT_EQ(2ul, representative_y.getNonZeroCount());
172 EXPECT_EQ(1ul, representative_y.getLeafCount());
173 EXPECT_EQ(5ul, representative_y.getNodeCount());
174 EXPECT_TRUE(bddAllTrueOrAllFalse == representative_y);
175
176 representative_z = bddAllTrueOrAllFalse.existsAbstractRepresentative({z.first});
177 EXPECT_EQ(2ul, representative_z.getNonZeroCount());
178 EXPECT_EQ(1ul, representative_z.getLeafCount());
179 EXPECT_EQ(5ul, representative_z.getNodeCount());
180 EXPECT_TRUE(bddAllTrueOrAllFalse == representative_z);
181
182 representative_xyz = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first, y.first, z.first});
183 EXPECT_EQ(1ul, representative_xyz.getNonZeroCount());
184 EXPECT_EQ(1ul, representative_xyz.getLeafCount());
185 EXPECT_EQ(4ul, representative_xyz.getNodeCount());
186 EXPECT_TRUE(bddX0Y0Z0 == representative_xyz);
187 });
188}
189
190TYPED_TEST(Dd, AddMinExistAbstractRepresentative) {
191 const storm::dd::DdType DdType = TestFixture::DdType;
192 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
193
194 manager->execute([&]() {
195 storm::dd::Bdd<DdType> bddZero;
196 ASSERT_NO_THROW(bddZero = manager->getBddZero());
197 storm::dd::Bdd<DdType> bddOne;
198 ASSERT_NO_THROW(bddOne = manager->getBddOne());
199
200 storm::dd::Add<DdType, double> addZero;
201 ASSERT_NO_THROW(addZero = manager->template getAddZero<double>());
202 storm::dd::Add<DdType, double> addOne;
203 ASSERT_NO_THROW(addOne = manager->template getAddOne<double>());
204
205 std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
206 std::pair<storm::expressions::Variable, storm::expressions::Variable> y;
207 std::pair<storm::expressions::Variable, storm::expressions::Variable> z;
208 ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1));
209 ASSERT_NO_THROW(y = manager->addMetaVariable("y", 0, 1));
210 ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1));
211
212 storm::dd::Bdd<DdType> bddX0 = manager->getEncoding(x.first, 0);
213 storm::dd::Bdd<DdType> bddX1 = manager->getEncoding(x.first, 1);
214 storm::dd::Bdd<DdType> bddY0 = manager->getEncoding(y.first, 0);
215 storm::dd::Bdd<DdType> bddY1 = manager->getEncoding(y.first, 1);
216 storm::dd::Bdd<DdType> bddZ0 = manager->getEncoding(z.first, 0);
217 storm::dd::Bdd<DdType> bddZ1 = manager->getEncoding(z.first, 1);
218
219 storm::dd::Add<DdType, double> complexAdd = ((bddX1 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.4)) +
220 ((bddX1 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.7)) +
221 ((bddX1 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.3)) +
222 ((bddX1 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.3)) +
223 ((bddX0 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.9)) +
224 ((bddX0 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.5)) +
225 ((bddX0 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(1.0)) +
226 ((bddX0 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.0));
227
228 // Abstract from FALSE
229 storm::dd::Bdd<DdType> representative_false_x = addZero.minAbstractRepresentative({x.first});
230 EXPECT_EQ(0ul, representative_false_x.getNonZeroCount());
231 EXPECT_EQ(1ul, representative_false_x.getLeafCount());
232 EXPECT_EQ(2ul, representative_false_x.getNodeCount());
233 EXPECT_TRUE(representative_false_x == bddX0);
234
235 // Abstract from TRUE
236 storm::dd::Bdd<DdType> representative_true_x = addOne.minAbstractRepresentative({x.first});
237 EXPECT_EQ(0ul, representative_true_x.getNonZeroCount());
238 EXPECT_EQ(1ul, representative_true_x.getLeafCount());
239 EXPECT_EQ(2ul, representative_true_x.getNodeCount());
240 EXPECT_TRUE(representative_true_x == bddX0);
241
242 storm::dd::Bdd<DdType> representative_true_xyz = addOne.minAbstractRepresentative({x.first, y.first, z.first});
243 EXPECT_EQ(0ul, representative_true_xyz.getNonZeroCount());
244 EXPECT_EQ(1ul, representative_true_xyz.getLeafCount());
245 EXPECT_EQ(4ul, representative_true_xyz.getNodeCount());
246 EXPECT_TRUE(representative_true_xyz == ((bddX0 && bddY0) && bddZ0));
247
248 // Abstract x
249 storm::dd::Bdd<DdType> representative_complex_x = complexAdd.minAbstractRepresentative({x.first});
250 storm::dd::Bdd<DdType> comparison_complex_x =
251 (((bddX0 && (bddY0 && bddZ0))) || ((bddX1 && (bddY0 && bddZ1))) || ((bddX0 && (bddY1 && bddZ0))) || ((bddX1 && (bddY1 && bddZ1))));
252 EXPECT_EQ(4ul, representative_complex_x.getNonZeroCount());
253 EXPECT_EQ(1ul, representative_complex_x.getLeafCount());
254 EXPECT_EQ(3ul, representative_complex_x.getNodeCount());
255 EXPECT_TRUE(representative_complex_x == comparison_complex_x);
256
257 // Abstract y
258 storm::dd::Bdd<DdType> representative_complex_y = complexAdd.minAbstractRepresentative({y.first});
259 storm::dd::Bdd<DdType> comparison_complex_y =
260 (((bddX0 && (bddY0 && bddZ0))) || ((bddX0 && (bddY1 && bddZ1))) || ((bddX1 && (bddY0 && bddZ0))) || ((bddX1 && (bddY0 && bddZ1))));
261 EXPECT_EQ(4ul, representative_complex_y.getNonZeroCount());
262 EXPECT_EQ(1ul, representative_complex_y.getLeafCount());
263 EXPECT_EQ(5ul, representative_complex_y.getNodeCount());
264 EXPECT_TRUE(representative_complex_y == comparison_complex_y);
265
266 // Abstract z
267 storm::dd::Bdd<DdType> representative_complex_z = complexAdd.minAbstractRepresentative({z.first});
268 storm::dd::Bdd<DdType> comparison_complex_z =
269 (((bddX0 && (bddY0 && bddZ0))) || ((bddX0 && (bddY1 && bddZ0))) || ((bddX1 && (bddY0 && bddZ0))) || ((bddX1 && (bddY1 && bddZ1))));
270 EXPECT_EQ(4ul, representative_complex_z.getNonZeroCount());
271 EXPECT_EQ(1ul, representative_complex_z.getLeafCount());
272 EXPECT_EQ(4ul, representative_complex_z.getNodeCount());
273 EXPECT_TRUE(representative_complex_z == comparison_complex_z);
274
275 // Abstract x, y, z
276 storm::dd::Bdd<DdType> representative_complex_xyz = complexAdd.minAbstractRepresentative({x.first, y.first, z.first});
277 storm::dd::Bdd<DdType> comparison_complex_xyz = (bddX0 && (bddY0 && bddZ0));
278 EXPECT_EQ(1ul, representative_complex_xyz.getNonZeroCount());
279 EXPECT_EQ(1ul, representative_complex_xyz.getLeafCount());
280 EXPECT_EQ(4ul, representative_complex_xyz.getNodeCount());
281 EXPECT_TRUE(representative_complex_xyz == comparison_complex_xyz);
282 });
283}
284
285TYPED_TEST(Dd, AddMaxExistAbstractRepresentative) {
286 const storm::dd::DdType DdType = TestFixture::DdType;
287 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
288
289 manager->execute([&]() {
290 storm::dd::Bdd<DdType> bddZero;
291 ASSERT_NO_THROW(bddZero = manager->getBddZero());
292 storm::dd::Bdd<DdType> bddOne;
293 ASSERT_NO_THROW(bddOne = manager->getBddOne());
294
295 storm::dd::Add<DdType, double> addZero;
296 ASSERT_NO_THROW(addZero = manager->template getAddZero<double>());
297 storm::dd::Add<DdType, double> addOne;
298 ASSERT_NO_THROW(addOne = manager->template getAddOne<double>());
299
300 std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
301 std::pair<storm::expressions::Variable, storm::expressions::Variable> y;
302 std::pair<storm::expressions::Variable, storm::expressions::Variable> z;
303 ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1));
304 ASSERT_NO_THROW(y = manager->addMetaVariable("y", 0, 1));
305 ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1));
306
307 storm::dd::Bdd<DdType> bddX0 = manager->getEncoding(x.first, 0);
308 storm::dd::Bdd<DdType> bddX1 = manager->getEncoding(x.first, 1);
309 storm::dd::Bdd<DdType> bddY0 = manager->getEncoding(y.first, 0);
310 storm::dd::Bdd<DdType> bddY1 = manager->getEncoding(y.first, 1);
311 storm::dd::Bdd<DdType> bddZ0 = manager->getEncoding(z.first, 0);
312 storm::dd::Bdd<DdType> bddZ1 = manager->getEncoding(z.first, 1);
313
314 storm::dd::Add<DdType, double> complexAdd = ((bddX1 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.4)) +
315 ((bddX1 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.7)) +
316 ((bddX1 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.3)) +
317 ((bddX1 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.3)) +
318 ((bddX0 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.9)) +
319 ((bddX0 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.5)) +
320 ((bddX0 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(1.0)) +
321 ((bddX0 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.0));
322
323 // Abstract from FALSE
324 storm::dd::Bdd<DdType> representative_false_x = addZero.maxAbstractRepresentative({x.first});
325 EXPECT_EQ(0ul, representative_false_x.getNonZeroCount());
326 EXPECT_EQ(1ul, representative_false_x.getLeafCount());
327 EXPECT_EQ(2ul, representative_false_x.getNodeCount());
328 EXPECT_TRUE(representative_false_x == bddX0);
329
330 // Abstract from TRUE
331 storm::dd::Bdd<DdType> representative_true_x = addOne.maxAbstractRepresentative({x.first});
332 EXPECT_EQ(0ul, representative_true_x.getNonZeroCount());
333 EXPECT_EQ(1ul, representative_true_x.getLeafCount());
334 EXPECT_EQ(2ul, representative_true_x.getNodeCount());
335 EXPECT_TRUE(representative_true_x == bddX0);
336
337 storm::dd::Bdd<DdType> representative_true_xyz = addOne.maxAbstractRepresentative({x.first, y.first, z.first});
338 EXPECT_EQ(0ul, representative_true_xyz.getNonZeroCount());
339 EXPECT_EQ(1ul, representative_true_xyz.getLeafCount());
340 EXPECT_EQ(4ul, representative_true_xyz.getNodeCount());
341 EXPECT_TRUE(representative_true_xyz == ((bddX0 && bddY0) && bddZ0));
342
343 // Abstract x
344 storm::dd::Bdd<DdType> representative_complex_x = complexAdd.maxAbstractRepresentative({x.first});
345 storm::dd::Bdd<DdType> comparison_complex_x =
346 (((bddX1 && (bddY0 && bddZ0))) || ((bddX0 && (bddY0 && bddZ1))) || ((bddX1 && (bddY1 && bddZ0))) || ((bddX0 && (bddY1 && bddZ1))));
347 EXPECT_EQ(4ul, representative_complex_x.getNonZeroCount());
348 EXPECT_EQ(1ul, representative_complex_x.getLeafCount());
349 EXPECT_EQ(3ul, representative_complex_x.getNodeCount());
350 EXPECT_TRUE(representative_complex_x == comparison_complex_x);
351
352 // Abstract y
353 storm::dd::Bdd<DdType> representative_complex_y = complexAdd.maxAbstractRepresentative({y.first});
354 storm::dd::Bdd<DdType> comparison_complex_y =
355 (((bddX0 && (bddY1 && bddZ0))) || ((bddX0 && (bddY0 && bddZ1))) || ((bddX1 && (bddY1 && bddZ0))) || ((bddX1 && (bddY1 && bddZ1))));
356 EXPECT_EQ(4ul, representative_complex_y.getNonZeroCount());
357 EXPECT_EQ(1ul, representative_complex_y.getLeafCount());
358 EXPECT_EQ(5ul, representative_complex_y.getNodeCount());
359 EXPECT_TRUE(representative_complex_y == comparison_complex_y);
360
361 // Abstract z
362 storm::dd::Bdd<DdType> representative_complex_z = complexAdd.maxAbstractRepresentative({z.first});
363 storm::dd::Bdd<DdType> comparison_complex_z =
364 (((bddX0 && (bddY0 && bddZ1))) || ((bddX0 && (bddY1 && bddZ1))) || ((bddX1 && (bddY0 && bddZ0))) || ((bddX1 && (bddY1 && bddZ0))));
365 EXPECT_EQ(4ul, representative_complex_z.getNonZeroCount());
366 EXPECT_EQ(1ul, representative_complex_z.getLeafCount());
367 EXPECT_EQ(3ul, representative_complex_z.getNodeCount());
368 EXPECT_TRUE(representative_complex_z == comparison_complex_z);
369
370 // Abstract x, y, z
371 storm::dd::Bdd<DdType> representative_complex_xyz = complexAdd.maxAbstractRepresentative({x.first, y.first, z.first});
372 storm::dd::Bdd<DdType> comparison_complex_xyz = (bddX0 && (bddY0 && bddZ1));
373 EXPECT_EQ(1ul, representative_complex_xyz.getNonZeroCount());
374 EXPECT_EQ(1ul, representative_complex_xyz.getLeafCount());
375 EXPECT_EQ(4ul, representative_complex_xyz.getNodeCount());
376 EXPECT_TRUE(representative_complex_xyz == comparison_complex_xyz);
377 });
378}
379
380TYPED_TEST(Dd, AddGetMetaVariableTest) {
381 const storm::dd::DdType DdType = TestFixture::DdType;
382 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
383
384 manager->execute([&]() {
385 ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
386 EXPECT_EQ(2ul, manager->getNumberOfMetaVariables());
387
388 STORM_SILENT_ASSERT_THROW(manager->addMetaVariable("x", 0, 3), storm::exceptions::InvalidArgumentException);
389
390 ASSERT_NO_THROW(manager->addMetaVariable("y", 0, 3));
391 EXPECT_EQ(4ul, manager->getNumberOfMetaVariables());
392
393 EXPECT_TRUE(manager->hasMetaVariable("x'"));
394 EXPECT_TRUE(manager->hasMetaVariable("y'"));
395
396 std::set<std::string> metaVariableSet = {"x", "x'", "y", "y'"};
397 EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames());
398 });
399}
400
401TYPED_TEST(Dd, EncodingTest) {
402 const storm::dd::DdType DdType = TestFixture::DdType;
403 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
404
405 manager->execute([&]() {
406 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
407
408 storm::dd::Bdd<DdType> encoding;
409 STORM_SILENT_ASSERT_THROW(encoding = manager->getEncoding(x.first, 0), storm::exceptions::InvalidArgumentException);
410 STORM_SILENT_ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException);
411 ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4));
412 EXPECT_EQ(1ul, encoding.getNonZeroCount());
413
414 // As a BDD, this DD has one only leaf, because there does not exist a 0-leaf, and (consequently) one node less
415 // than the MTBDD.
416 EXPECT_EQ(5ul, encoding.getNodeCount());
417 EXPECT_EQ(1ul, encoding.getLeafCount());
418
419 storm::dd::Add<DdType, double> add;
420 ASSERT_NO_THROW(add = encoding.template toAdd<double>());
421
422 // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6.
423 EXPECT_EQ(6ul, add.getNodeCount());
424 EXPECT_EQ(2ul, add.getLeafCount());
425 });
426}
427
428TYPED_TEST(Dd, RangeTest) {
429 const storm::dd::DdType DdType = TestFixture::DdType;
430 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
431 manager->execute([&]() {
432 std::pair<storm::expressions::Variable, storm::expressions::Variable> x;
433 ASSERT_NO_THROW(x = manager->addMetaVariable("x", 1, 9));
434
435 storm::dd::Bdd<DdType> range;
436 ASSERT_NO_THROW(range = manager->getRange(x.first));
437
438 EXPECT_EQ(9ul, range.getNonZeroCount());
439 EXPECT_EQ(1ul, range.getLeafCount());
440 EXPECT_EQ(5ul, range.getNodeCount());
441 });
442}
443
444TYPED_TEST(Dd, DoubleIdentityTest) {
445 const storm::dd::DdType DdType = TestFixture::DdType;
446 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
447 manager->execute([&]() {
448 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
449
450 storm::dd::Add<DdType, double> identity;
451 ASSERT_NO_THROW(identity = manager->template getIdentity<double>(x.first));
452
453 EXPECT_EQ(9ul, identity.getNonZeroCount());
454 EXPECT_EQ(10ul, identity.getLeafCount());
455 EXPECT_EQ(21ul, identity.getNodeCount());
456 });
457}
458
459TYPED_TEST(Dd, UintIdentityTest) {
460 const storm::dd::DdType DdType = TestFixture::DdType;
461 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
462 manager->execute([&]() {
463 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
464
465 storm::dd::Add<DdType, uint_fast64_t> identity;
466 ASSERT_NO_THROW(identity = manager->template getIdentity<uint_fast64_t>(x.first));
467
468 EXPECT_EQ(9ul, identity.getNonZeroCount());
469 EXPECT_EQ(10ul, identity.getLeafCount());
470 EXPECT_EQ(21ul, identity.getNodeCount());
471 });
472}
473
474TYPED_TEST(Dd, OperatorTest) {
475 const storm::dd::DdType DdType = TestFixture::DdType;
476 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
477 manager->execute([&]() {
478 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
479 EXPECT_TRUE(manager->template getAddZero<double>() == manager->template getAddZero<double>());
480 EXPECT_FALSE(manager->template getAddZero<double>() == manager->template getAddOne<double>());
481
482 EXPECT_FALSE(manager->template getAddZero<double>() != manager->template getAddZero<double>());
483 EXPECT_TRUE(manager->template getAddZero<double>() != manager->template getAddOne<double>());
484
485 storm::dd::Add<DdType, double> dd1 = manager->template getAddOne<double>();
486 storm::dd::Add<DdType, double> dd2 = manager->template getAddOne<double>();
487 storm::dd::Add<DdType, double> dd3 = dd1 + dd2;
488 storm::dd::Bdd<DdType> bdd;
489 EXPECT_TRUE(dd3 == manager->template getConstant<double>(2));
490
491 dd3 += manager->template getAddZero<double>();
492 EXPECT_TRUE(dd3 == manager->template getConstant<double>(2));
493
494 dd3 = dd1 * manager->template getConstant<double>(3);
495 EXPECT_TRUE(dd3 == manager->template getConstant<double>(3));
496
497 dd3 *= manager->template getConstant<double>(2);
498 EXPECT_TRUE(dd3 == manager->template getConstant<double>(6));
499
500 dd3 = dd1 - dd2;
501 EXPECT_TRUE(dd3.isZero());
502
503 dd3 -= manager->template getConstant<double>(-2);
504 EXPECT_TRUE(dd3 == manager->template getConstant<double>(2));
505
506 dd3 /= manager->template getConstant<double>(2);
507 EXPECT_TRUE(dd3.isOne());
508
509 bdd = !dd3.toBdd();
510 EXPECT_TRUE(bdd.isZero());
511
512 bdd = !bdd;
513 EXPECT_TRUE(bdd.isOne());
514
515 bdd = dd1.toBdd() || dd2.toBdd();
516 EXPECT_TRUE(bdd.isOne());
517
518 dd1 = manager->template getIdentity<double>(x.first);
519 dd2 = manager->template getConstant<double>(5);
520
521 bdd = dd1.equals(dd2);
522 EXPECT_EQ(1ul, bdd.getNonZeroCount());
523
524 storm::dd::Bdd<DdType> bdd2 = dd1.notEquals(dd2);
525 EXPECT_TRUE(bdd2 == !bdd);
526
527 bdd = dd1.less(dd2);
528 EXPECT_EQ(11ul, bdd.getNonZeroCount());
529
530 bdd = dd1.lessOrEqual(dd2);
531 EXPECT_EQ(12ul, bdd.getNonZeroCount());
532
533 bdd = dd1.greater(dd2);
534 EXPECT_EQ(4ul, bdd.getNonZeroCount());
535
536 bdd = dd1.greaterOrEqual(dd2);
537 EXPECT_EQ(5ul, bdd.getNonZeroCount());
538
539 dd3 = manager->getEncoding(x.first, 2).ite(dd2, dd1);
540 bdd = dd3.less(dd2);
541 EXPECT_EQ(10ul, bdd.getNonZeroCount());
542
543 storm::dd::Add<DdType, double> dd4 = dd3.minimum(dd1);
544 dd4 *= manager->getEncoding(x.first, 2).template toAdd<double>();
545 dd4 = dd4.sumAbstract({x.first});
546 EXPECT_EQ(2, dd4.getValue());
547
548 dd4 = dd3.maximum(dd1);
549 dd4 *= manager->getEncoding(x.first, 2).template toAdd<double>();
550 dd4 = dd4.sumAbstract({x.first});
551 EXPECT_EQ(5, dd4.getValue());
552
553 dd1 = manager->template getConstant<double>(0.01);
554 dd2 = manager->template getConstant<double>(0.01 + 1e-6);
555 EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false));
556 EXPECT_FALSE(dd1.equalModuloPrecision(dd2, 1e-6));
557 });
558}
559
560TYPED_TEST(Dd, AbstractionTest) {
561 const storm::dd::DdType DdType = TestFixture::DdType;
562 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
563 manager->execute([&]() {
564 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
565 storm::dd::Add<DdType, double> dd1;
566 storm::dd::Add<DdType, double> dd2;
567 storm::dd::Add<DdType, double> dd3;
568 storm::dd::Bdd<DdType> bdd;
569
570 dd1 = manager->template getIdentity<double>(x.first);
571 dd2 = manager->template getConstant<double>(5);
572 bdd = dd1.equals(dd2);
573 EXPECT_EQ(1ul, bdd.getNonZeroCount());
574 STORM_SILENT_ASSERT_THROW(bdd = bdd.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException);
575 ASSERT_NO_THROW(bdd = bdd.existsAbstract({x.first}));
576 EXPECT_EQ(0ul, bdd.getNonZeroCount());
577 EXPECT_EQ(1, bdd.template toAdd<double>().getMax());
578
579 dd3 = dd1.equals(dd2).template toAdd<double>();
580 dd3 *= manager->template getConstant<double>(3);
581 EXPECT_EQ(1ul, dd3.getNonZeroCount());
582 STORM_SILENT_ASSERT_THROW(bdd = dd3.toBdd().existsAbstract({x.second}), storm::exceptions::InvalidArgumentException);
583 ASSERT_NO_THROW(bdd = dd3.toBdd().existsAbstract({x.first}));
584 EXPECT_TRUE(bdd.isOne());
585
586 dd3 = dd1.equals(dd2).template toAdd<double>();
587 dd3 *= manager->template getConstant<double>(3);
588 STORM_SILENT_ASSERT_THROW(dd3 = dd3.sumAbstract({x.second}), storm::exceptions::InvalidArgumentException);
589 ASSERT_NO_THROW(dd3 = dd3.sumAbstract({x.first}));
590 EXPECT_EQ(0ul, dd3.getNonZeroCount());
591 EXPECT_EQ(3, dd3.getMax());
592
593 dd3 = dd1.equals(dd2).template toAdd<double>();
594 dd3 *= manager->template getConstant<double>(3);
595 STORM_SILENT_ASSERT_THROW(dd3 = dd3.minAbstract({x.second}), storm::exceptions::InvalidArgumentException);
596 ASSERT_NO_THROW(dd3 = dd3.minAbstract({x.first}));
597 EXPECT_EQ(0ul, dd3.getNonZeroCount());
598 EXPECT_EQ(0, dd3.getMax());
599
600 dd3 = dd1.equals(dd2).template toAdd<double>();
601 dd3 *= manager->template getConstant<double>(3);
602 STORM_SILENT_ASSERT_THROW(dd3 = dd3.maxAbstract({x.second}), storm::exceptions::InvalidArgumentException);
603 ASSERT_NO_THROW(dd3 = dd3.maxAbstract({x.first}));
604 EXPECT_EQ(0ul, dd3.getNonZeroCount());
605 EXPECT_EQ(3, dd3.getMax());
606 });
607}
608
609TYPED_TEST(Dd, SwapTest) {
610 const storm::dd::DdType DdType = TestFixture::DdType;
611 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
612
613 manager->execute([&]() {
614 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
615 std::pair<storm::expressions::Variable, storm::expressions::Variable> z = manager->addMetaVariable("z", 2, 8);
616 storm::dd::Add<DdType, double> dd1;
617 storm::dd::Add<DdType, double> dd2;
618
619 dd1 = manager->template getIdentity<double>(x.first);
620 STORM_SILENT_ASSERT_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, z.first)}), storm::exceptions::InvalidArgumentException);
621 ASSERT_NO_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, x.second)}));
622 EXPECT_TRUE(dd1 == manager->template getIdentity<double>(x.second));
623 });
624}
625
626TYPED_TEST(Dd, MultiplyMatrixTest) {
627 const storm::dd::DdType DdType = TestFixture::DdType;
628 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
629 manager->execute([&]() {
630 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
631
632 storm::dd::Add<DdType, double> dd1 =
633 manager->template getIdentity<double>(x.first).equals(manager->template getIdentity<double>(x.second)).template toAdd<double>();
634 storm::dd::Add<DdType, double> dd2 = manager->getRange(x.second).template toAdd<double>();
635 storm::dd::Add<DdType, double> dd3;
636 dd1 *= manager->template getConstant<double>(2);
637
638 ASSERT_NO_THROW(dd3 = dd1.multiplyMatrix(dd2, {x.second}));
639 ASSERT_NO_THROW(dd3 = dd3.swapVariables({std::make_pair(x.first, x.second)}));
640 EXPECT_TRUE(dd3 == dd2 * manager->template getConstant<double>(2));
641 });
642}
643
644TYPED_TEST(Dd, MultiplyMatrixTest2) {
645 const storm::dd::DdType DdType = TestFixture::DdType;
646 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
647 manager->execute([&]() {
648 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 0, 2);
649 std::pair<storm::expressions::Variable, storm::expressions::Variable> b = manager->addMetaVariable("b", 0, 2);
650
651 storm::dd::Add<DdType, double> p = manager->template getAddZero<double>();
652 p += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(b.first, 0, true)).template toAdd<double>();
653 p += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(b.first, 2, true)).template toAdd<double>();
654
655 storm::dd::Add<DdType, double> q = manager->template getAddZero<double>();
656 q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 0, true)).template toAdd<double>() *
657 manager->template getConstant<double>(0.3);
658 q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 0, true)).template toAdd<double>() *
659 manager->template getConstant<double>(0.3);
660 q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 2, true)).template toAdd<double>() *
661 manager->template getConstant<double>(0.7);
662 q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 2, true)).template toAdd<double>() *
663 manager->template getConstant<double>(0.7);
664 q += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(x.second, 0, true)).template toAdd<double>() *
665 manager->template getConstant<double>(1);
666
667 storm::dd::Add<DdType, double> r = q.multiplyMatrix(p, {x.first});
668
669 ASSERT_EQ(12ull, r.getNodeCount());
670 ASSERT_EQ(4ull, r.getLeafCount());
671 ASSERT_EQ(3ull, r.getNonZeroCount());
672 });
673}
674
675TYPED_TEST(Dd, GetSetValueTest) {
676 const storm::dd::DdType DdType = TestFixture::DdType;
677 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
678 manager->execute([&]() {
679 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
680
681 storm::dd::Add<DdType, double> dd1 = manager->template getAddOne<double>();
682 ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2));
683 EXPECT_EQ(2ul, dd1.getLeafCount());
684
685 std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
686 metaVariableToValueMap.emplace(x.first, 1);
687 EXPECT_EQ(1, dd1.getValue(metaVariableToValueMap));
688
689 metaVariableToValueMap.clear();
690 metaVariableToValueMap.emplace(x.first, 4);
691 EXPECT_EQ(2, dd1.getValue(metaVariableToValueMap));
692 });
693}
694
695TYPED_TEST(Dd, AddIteratorTest) {
696 const storm::dd::DdType DdType = TestFixture::DdType;
697 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
698 manager->execute([&]() {
699 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
700 std::pair<storm::expressions::Variable, storm::expressions::Variable> y = manager->addMetaVariable("y", 0, 3);
701
702 storm::dd::Add<DdType, double> dd;
703 ASSERT_NO_THROW(dd = manager->getRange(x.first).template toAdd<double>());
704
705 storm::dd::AddIterator<DdType, double> it, ite;
706 ASSERT_NO_THROW(it = dd.begin());
707 ASSERT_NO_THROW(ite = dd.end());
708 std::pair<storm::expressions::SimpleValuation, double> valuationValuePair;
709 uint_fast64_t numberOfValuations = 0;
710 while (it != ite) {
711 ASSERT_NO_THROW(valuationValuePair = *it);
712 ASSERT_NO_THROW(++it);
713 ++numberOfValuations;
714 }
715 EXPECT_EQ(9ul, numberOfValuations);
716
717 dd = manager->getRange(x.first).template toAdd<double>();
718 dd = dd.notZero().ite(manager->template getAddOne<double>(), manager->template getAddOne<double>());
719 ASSERT_NO_THROW(it = dd.begin());
720 ASSERT_NO_THROW(ite = dd.end());
721 numberOfValuations = 0;
722 while (it != ite) {
723 ASSERT_NO_THROW(valuationValuePair = *it);
724 ASSERT_NO_THROW(++it);
725 ++numberOfValuations;
726 }
727 EXPECT_EQ(16ul, numberOfValuations);
728
729 ASSERT_NO_THROW(it = dd.begin(false));
730 ASSERT_NO_THROW(ite = dd.end());
731 numberOfValuations = 0;
732 while (it != ite) {
733 ASSERT_NO_THROW(valuationValuePair = *it);
734 ASSERT_NO_THROW(++it);
735 ++numberOfValuations;
736 }
737 EXPECT_EQ(1ul, numberOfValuations);
738 });
739}
740
741TYPED_TEST(Dd, AddOddTest) {
742 const storm::dd::DdType DdType = TestFixture::DdType;
743 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
744 manager->execute([&]() {
745 std::pair<storm::expressions::Variable, storm::expressions::Variable> a = manager->addMetaVariable("a");
746 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
747
748 storm::dd::Add<DdType, double> dd = manager->template getIdentity<double>(x.first);
749 storm::dd::Odd odd;
750 ASSERT_NO_THROW(odd = dd.createOdd());
751 EXPECT_EQ(9ul, odd.getTotalOffset());
752 EXPECT_EQ(12ul, odd.getNodeCount());
753
754 std::vector<double> ddAsVector;
755 ASSERT_NO_THROW(ddAsVector = dd.toVector());
756 EXPECT_EQ(9ul, ddAsVector.size());
757 for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) {
758 EXPECT_TRUE(i + 1 == ddAsVector[i]);
759 }
760
761 // Create a non-trivial matrix.
762 dd = manager->template getIdentity<double>(x.first).equals(manager->template getIdentity<double>(x.second)).template toAdd<double>() *
763 manager->getRange(x.first).template toAdd<double>();
764 dd += manager->getEncoding(x.first, 1).template toAdd<double>() * manager->getRange(x.second).template toAdd<double>() +
765 manager->getEncoding(x.second, 1).template toAdd<double>() * manager->getRange(x.first).template toAdd<double>();
766
767 // Create the ODDs.
768 storm::dd::Odd rowOdd;
769 ASSERT_NO_THROW(rowOdd = manager->getRange(x.first).template toAdd<double>().createOdd());
770 storm::dd::Odd columnOdd;
771 ASSERT_NO_THROW(columnOdd = manager->getRange(x.second).template toAdd<double>().createOdd());
772
773 // Try to translate the matrix.
774 storm::storage::SparseMatrix<double> matrix;
775 ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd));
776
777 EXPECT_EQ(9ul, matrix.getRowCount());
778 EXPECT_EQ(9ul, matrix.getColumnCount());
779 EXPECT_EQ(25ul, matrix.getNonzeroEntryCount());
780
781 dd = manager->getRange(x.first).template toAdd<double>() * manager->getRange(x.second).template toAdd<double>() *
782 manager->getEncoding(a.first, 0).ite(dd, dd + manager->template getConstant<double>(1));
783 ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd));
784 EXPECT_EQ(18ul, matrix.getRowCount());
785 EXPECT_EQ(9ul, matrix.getRowGroupCount());
786 EXPECT_EQ(9ul, matrix.getColumnCount());
787 EXPECT_EQ(106ul, matrix.getNonzeroEntryCount());
788 });
789}
790
791TYPED_TEST(Dd, BddOddTest) {
792 const storm::dd::DdType DdType = TestFixture::DdType;
793 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
794 manager->execute([&]() {
795 std::pair<storm::expressions::Variable, storm::expressions::Variable> a = manager->addMetaVariable("a");
796 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
797
798 storm::dd::Add<DdType, double> dd = manager->template getIdentity<double>(x.first);
799 storm::dd::Bdd<DdType> bdd = dd.notZero();
800 storm::dd::Odd odd;
801 ASSERT_NO_THROW(odd = bdd.createOdd());
802 EXPECT_EQ(9ul, odd.getTotalOffset());
803 EXPECT_EQ(5ul, odd.getNodeCount());
804
805 std::vector<double> ddAsVector;
806 ASSERT_NO_THROW(ddAsVector = dd.toVector());
807 EXPECT_EQ(9ul, ddAsVector.size());
808 for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) {
809 EXPECT_EQ(i + 1, ddAsVector[i]);
810 }
811
812 storm::dd::Add<DdType, double> vectorAdd = storm::dd::Add<DdType, double>::fromVector(*manager, ddAsVector, odd, {x.first});
813
814 // Create a non-trivial matrix.
815 dd = manager->template getIdentity<double>(x.first).equals(manager->template getIdentity<double>(x.second)).template toAdd<double>() *
816 manager->getRange(x.first).template toAdd<double>();
817 dd += manager->getEncoding(x.first, 1).template toAdd<double>() * manager->getRange(x.second).template toAdd<double>() +
818 manager->getEncoding(x.second, 1).template toAdd<double>() * manager->getRange(x.first).template toAdd<double>();
819
820 // Create the ODDs.
821 storm::dd::Odd rowOdd;
822 ASSERT_NO_THROW(rowOdd = manager->getRange(x.first).createOdd());
823 storm::dd::Odd columnOdd;
824 ASSERT_NO_THROW(columnOdd = manager->getRange(x.second).createOdd());
825
826 // Try to translate the matrix.
827 storm::storage::SparseMatrix<double> matrix;
828 ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd));
829
830 EXPECT_EQ(9ul, matrix.getRowCount());
831 EXPECT_EQ(9ul, matrix.getColumnCount());
832 EXPECT_EQ(25ul, matrix.getNonzeroEntryCount());
833
834 dd = manager->getRange(x.first).template toAdd<double>() * manager->getRange(x.second).template toAdd<double>() *
835 manager->getEncoding(a.first, 0).ite(dd, dd + manager->template getConstant<double>(1));
836 ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd));
837 EXPECT_EQ(18ul, matrix.getRowCount());
838 EXPECT_EQ(9ul, matrix.getRowGroupCount());
839 EXPECT_EQ(9ul, matrix.getColumnCount());
840 EXPECT_EQ(106ul, matrix.getNonzeroEntryCount());
841 });
842}
843
844TYPED_TEST(Dd, BddToExpressionTest) {
845 const storm::dd::DdType DdType = TestFixture::DdType;
846 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
847 manager->execute([&]() {
848 std::pair<storm::expressions::Variable, storm::expressions::Variable> a = manager->addMetaVariable("a");
849 std::pair<storm::expressions::Variable, storm::expressions::Variable> b = manager->addMetaVariable("b");
850
851 storm::dd::Bdd<DdType> bdd = manager->getBddOne();
852 bdd &= manager->getEncoding(a.first, 1);
853 bdd |= manager->getEncoding(b.first, 0);
854
855 std::shared_ptr<storm::expressions::ExpressionManager> manager = std::make_shared<storm::expressions::ExpressionManager>();
856 storm::expressions::Variable c = manager->declareBooleanVariable("c");
857 storm::expressions::Variable d = manager->declareBooleanVariable("d");
858
859 auto result = bdd.toExpression(*manager);
860 });
861}
TYPED_TEST_SUITE
TYPED_TEST_SUITE(Dd, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition DdTest.cpp:30
TYPED_TEST
TYPED_TEST(Dd, AddConstants)
Definition DdTest.cpp:33
Cudd::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:25
Dd
Definition DdTest.cpp:25
Dd::DdType
static const storm::dd::DdType DdType
Definition DdTest.cpp:27
Sylvan::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:30
storm::dd::Add::swapVariables
Add< LibraryType, ValueType > swapVariables(std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &metaVariablePairs) const
Swaps the given pairs of meta variables in the ADD.
Definition Add.cpp:292
storm::dd::Add::equals
Bdd< LibraryType > equals(Add< LibraryType, ValueType > const &other) const
Retrieves the function that maps all evaluations to one that have identical function values.
Definition Add.cpp:96
storm::dd::Add::isOne
bool isOne() const
Retrieves whether this ADD represents the constant one function.
Definition Add.cpp:527
storm::dd::Add::getMax
ValueType getMax() const
Retrieves the highest function value of any encoding.
Definition Add.cpp:475
storm::dd::Add::lessOrEqual
Bdd< LibraryType > lessOrEqual(Add< LibraryType, ValueType > const &other) const
Retrieves the function that maps all evaluations to one whose function value in the first ADD are les...
Definition Add.cpp:111
storm::dd::Add::minimum
Add< LibraryType, ValueType > minimum(Add< LibraryType, ValueType > const &other) const
Retrieves the function that maps all evaluations to the minimum of the function values of the two ADD...
Definition Add.cpp:168
storm::dd::Add::toMatrix
storm::storage::SparseMatrix< ValueType > toMatrix() const
Converts the ADD to a (sparse) matrix.
Definition Add.cpp:634
storm::dd::Add::getMin
ValueType getMin() const
Retrieves the lowest function value of any encoding.
Definition Add.cpp:470
storm::dd::Add::greater
Bdd< LibraryType > greater(Add< LibraryType, ValueType > const &other) const
Retrieves the function that maps all evaluations to one whose function value in the first ADD are gre...
Definition Add.cpp:116
storm::dd::Add::maximum
Add< LibraryType, ValueType > maximum(Add< LibraryType, ValueType > const &other) const
Retrieves the function that maps all evaluations to the maximum of the function values of the two ADD...
Definition Add.cpp:173
storm::dd::Add::getValue
ValueType getValue(std::map< storm::expressions::Variable, int_fast64_t > const &metaVariableToValueMap=std::map< storm::expressions::Variable, int_fast64_t >()) const
Retrieves the value of the function when all meta variables are assigned the values of the given mapp...
Definition Add.cpp:508
storm::dd::Add::maxAbstract
Add< LibraryType, ValueType > maxAbstract(std::set< storm::expressions::Variable > const &metaVariables) const
Max-abstracts from the given meta variables.
Definition Add.cpp:198
storm::dd::Add::fromVector
static Add< LibraryType, ValueType > fromVector(DdManager< LibraryType > const &ddManager, std::vector< ValueType > const &values, Odd const &odd, std::set< storm::expressions::Variable > const &metaVariables)
Builds an ADD representing the given vector.
Definition Add.cpp:1178
storm::dd::Add::begin
AddIterator< LibraryType, ValueType > begin(bool enumerateDontCareMetaVariables=true) const
Retrieves an iterator that points to the first meta variable assignment with a non-zero function valu...
Definition Add.cpp:1149
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::Add::getNodeCount
virtual uint_fast64_t getNodeCount() const override
Retrieves the number of nodes necessary to represent the DD.
Definition Add.cpp:465
storm::dd::Add::minAbstractRepresentative
Bdd< LibraryType > minAbstractRepresentative(std::set< storm::expressions::Variable > const &metaVariables) const
Similar to minAbstract, but does not abstract from the variables but rather picks a valuation of each...
Definition Add.cpp:192
storm::dd::Add::greaterOrEqual
Bdd< LibraryType > greaterOrEqual(Add< LibraryType, ValueType > const &other) const
Retrieves the function that maps all evaluations to one whose function value in the first ADD are gre...
Definition Add.cpp:121
storm::dd::Add::minAbstract
Add< LibraryType, ValueType > minAbstract(std::set< storm::expressions::Variable > const &metaVariables) const
Min-abstracts from the given meta variables.
Definition Add.cpp:185
storm::dd::Add::createOdd
Odd createOdd() const
Creates an ODD based on the current ADD.
Definition Add.cpp:1192
storm::dd::Add::end
AddIterator< LibraryType, ValueType > end() const
Retrieves an iterator that points past the end of the container.
Definition Add.cpp:1161
storm::dd::Add::isZero
bool isZero() const
Retrieves whether this ADD represents the constant zero function.
Definition Add.cpp:532
storm::dd::Add::multiplyMatrix
Add< LibraryType, ValueType > multiplyMatrix(Add< LibraryType, ValueType > const &otherMatrix, std::set< storm::expressions::Variable > const &summationMetaVariables) const
Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given me...
Definition Add.cpp:372
storm::dd::Add::getLeafCount
virtual uint_fast64_t getLeafCount() const override
Retrieves the number of leaves of the ADD.
Definition Add.cpp:460
storm::dd::Add::toBdd
Bdd< LibraryType > toBdd() const
Converts the ADD to a BDD by mapping all values unequal to zero to 1.
Definition Add.cpp:1187
storm::dd::Add::equalModuloPrecision
bool equalModuloPrecision(Add< LibraryType, ValueType > const &other, ValueType const &precision, bool relative=true) const
Checks whether the current and the given ADD represent the same function modulo some given precision.
Definition Add.cpp:211
storm::dd::Add::notEquals
Bdd< LibraryType > notEquals(Add< LibraryType, ValueType > const &other) const
Retrieves the function that maps all evaluations to one that have distinct function values.
Definition Add.cpp:101
storm::dd::Add::setValue
void setValue(storm::expressions::Variable const &metaVariable, int_fast64_t variableValue, ValueType const &targetValue)
Sets the function values of all encodings that have the given value of the meta variable to the given...
Definition Add.cpp:480
storm::dd::Add::notZero
Bdd< LibraryType > notZero() const
Computes a BDD that represents the function in which all assignments with a function value unequal to...
Definition Add.cpp:431
storm::dd::Add::maxAbstractRepresentative
Bdd< LibraryType > maxAbstractRepresentative(std::set< storm::expressions::Variable > const &metaVariables) const
Similar to maxAbstract, but does not abstract from the variables but rather picks a valuation of each...
Definition Add.cpp:205
storm::dd::Add::toVector
std::vector< ValueType > toVector() const
Converts the ADD to a vector.
Definition Add.cpp:552
storm::dd::Add::less
Bdd< LibraryType > less(Add< LibraryType, ValueType > const &other) const
Retrieves the function that maps all evaluations to one whose function value in the first ADD are les...
Definition Add.cpp:106
storm::dd::Bdd::existsAbstract
Bdd< LibraryType > existsAbstract(std::set< storm::expressions::Variable > const &metaVariables) const
Existentially abstracts from the given meta variables.
Definition Bdd.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::dd::Bdd::toExpression
std::pair< std::vector< storm::expressions::Expression >, std::unordered_map< uint_fast64_t, storm::expressions::Variable > > toExpression(storm::expressions::ExpressionManager &manager) const
Translates the function the BDD is representing to a set of expressions that characterize the functio...
Definition Bdd.cpp:502
storm::dd::Bdd::getNodeCount
virtual uint_fast64_t getNodeCount() const override
Retrieves the number of nodes necessary to represent the DD.
Definition Bdd.cpp:527
storm::dd::Bdd::createOdd
Odd createOdd() const
Creates an ODD based on the current BDD.
Definition Bdd.cpp:571
storm::dd::Bdd::existsAbstractRepresentative
Bdd< LibraryType > existsAbstractRepresentative(std::set< storm::expressions::Variable > const &metaVariables) const
Similar to existsAbstract, but does not abstract from the variables but rather picks a valuation of e...
Definition Bdd.cpp:184
storm::dd::Bdd::isOne
bool isOne() const
Retrieves whether this DD represents the constant one function.
Definition Bdd.cpp:542
storm::dd::Bdd::getLeafCount
virtual uint_fast64_t getLeafCount() const override
Retrieves the number of leaves of the DD.
Definition Bdd.cpp:522
storm::dd::Odd::getNodeCount
uint_fast64_t getNodeCount() const
Retrieves the size of the ODD.
Definition Odd.cpp:51
storm::dd::Odd::getTotalOffset
uint_fast64_t getTotalOffset() const
Retrieves the total offset, i.e., the sum of the then- and else-offset.
Definition Odd.cpp:47
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:332
storm::storage::SparseMatrix::getRowGroupCount
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
Definition SparseMatrix.cpp:721
storm::storage::SparseMatrix::getColumnCount
index_type getColumnCount() const
Returns the number of columns of the matrix.
Definition SparseMatrix.cpp:666
storm::storage::SparseMatrix::getRowCount
index_type getRowCount() const
Returns the number of rows of the matrix.
Definition SparseMatrix.cpp:661
storm::storage::SparseMatrix::getNonzeroEntryCount
index_type getNonzeroEntryCount() const
Returns the cached number of nonzero entries in the matrix.
Definition SparseMatrix.cpp:689
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:99