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