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