Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SylvanDdTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include <carl/util/stringparser.h>
5
6#include "storm/adapters/RationalFunctionAdapter.h"
7#include "storm/exceptions/InvalidArgumentException.h"
8#include "storm/settings/SettingsManager.h"
9#include "storm/storage/SparseMatrix.h"
10#include "storm/storage/dd/Add.h"
11#include "storm/storage/dd/DdManager.h"
12#include "storm/storage/dd/DdMetaVariable.h"
13#include "storm/storage/dd/Odd.h"
14#include "storm/storage/expressions/Expression.h"
15#include "storm/storage/expressions/ExpressionManager.h"
16
17class Sylvan {
18 public:
19 static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan;
20};
21
22template<typename TestType>
23class SylvanDd : public ::testing::Test {
24 public:
25 static const storm::dd::DdType DdType = TestType::DdType;
26};
27
28typedef ::testing::Types<Sylvan> TestingTypes;
29TYPED_TEST_SUITE(SylvanDd, TestingTypes, );
30
31TYPED_TEST(SylvanDd, AddSharpenTest) {
32 const storm::dd::DdType DdType = TestFixture::DdType;
33 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
34 manager->execute([&]() {
35 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
36
37 storm::dd::Add<DdType, double> dd = manager->template getAddOne<double>();
38 ASSERT_NO_THROW(dd.setValue(x.first, 4, 1.89999999));
39 ASSERT_EQ(2ul, dd.getLeafCount());
40
41 storm::dd::Add<DdType, storm::RationalNumber> sharpened = dd.sharpenKwekMehlhorn(1);
42
43 std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
44 metaVariableToValueMap.emplace(x.first, 4);
45
46 sharpened = dd.sharpenKwekMehlhorn(1);
47 ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("9/5")), sharpened.getValue(metaVariableToValueMap));
48
49 sharpened = dd.sharpenKwekMehlhorn(2);
50 ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("19/10")), sharpened.getValue(metaVariableToValueMap));
51 });
52}
53
54TYPED_TEST(SylvanDd, AddRationalSharpenTest) {
55 const storm::dd::DdType DdType = TestFixture::DdType;
56 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
57 manager->execute([&]() {
58 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
59
60 storm::dd::Add<DdType, storm::RationalNumber> dd = manager->template getAddOne<storm::RationalNumber>();
61 ASSERT_NO_THROW(dd.setValue(x.first, 4, storm::utility::convertNumber<storm::RationalNumber>(1.89999999)));
62 ASSERT_EQ(2ul, dd.getLeafCount());
63
64 storm::dd::Add<DdType, storm::RationalNumber> sharpened = dd.sharpenKwekMehlhorn(1);
65
66 std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
67 metaVariableToValueMap.emplace(x.first, 4);
68
69 sharpened = dd.sharpenKwekMehlhorn(1);
70 ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("9/5")), sharpened.getValue(metaVariableToValueMap));
71
72 sharpened = dd.sharpenKwekMehlhorn(2);
73 ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("19/10")), sharpened.getValue(metaVariableToValueMap));
74 });
75}
76
77TYPED_TEST(SylvanDd, AddToRationalTest) {
78 const storm::dd::DdType DdType = TestFixture::DdType;
79 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
80 manager->execute([&]() {
81 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
82
83 storm::dd::Add<DdType, double> dd = manager->template getAddOne<double>();
84 ASSERT_NO_THROW(dd.setValue(x.first, 4, 0.4));
85 ASSERT_EQ(2ul, dd.getLeafCount());
86
87 storm::dd::Add<DdType, storm::RationalNumber> rationalDd = dd.template toValueType<storm::RationalNumber>();
88
89 std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
90 metaVariableToValueMap.emplace(x.first, 4);
91
92 ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("3602879701896397/9007199254740992")),
93 rationalDd.getValue(metaVariableToValueMap));
94 });
95}
96
97TYPED_TEST(SylvanDd, RationalFunctionConstants) {
98 const storm::dd::DdType DdType = TestFixture::DdType;
99 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
100 manager->execute([&]() {
101 storm::dd::Add<DdType, storm::RationalFunction> zero;
102 ASSERT_NO_THROW(zero = manager->template getAddZero<storm::RationalFunction>());
103
104 EXPECT_EQ(0ul, zero.getNonZeroCount());
105 EXPECT_EQ(1ul, zero.getLeafCount());
106 EXPECT_EQ(1ul, zero.getNodeCount());
107
108 storm::dd::Add<DdType, storm::RationalFunction> one;
109 ASSERT_NO_THROW(one = manager->template getAddOne<storm::RationalFunction>());
110
111 EXPECT_EQ(0ul, one.getNonZeroCount());
112 EXPECT_EQ(1ul, one.getLeafCount());
113 EXPECT_EQ(1ul, one.getNodeCount());
114
115 storm::dd::Add<DdType, storm::RationalFunction> two;
116 storm::RationalFunction constantTwo(2);
117
118 ASSERT_NO_THROW(two = manager->template getConstant<storm::RationalFunction>(constantTwo));
119
120 EXPECT_EQ(0ul, two.getNonZeroCount());
121 EXPECT_EQ(1ul, two.getLeafCount());
122 EXPECT_EQ(1ul, two.getNodeCount());
123
124 storm::dd::Add<DdType, storm::RationalFunction> function;
125 std::shared_ptr<storm::RawPolynomialCache> cache = std::make_shared<storm::RawPolynomialCache>();
126 carl::StringParser parser;
127 parser.setVariables({"x", "y", "z"});
128
129 storm::RationalFunction partA =
130 storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalFunctionCoefficient>("2*x+x*y"), cache));
131 storm::RationalFunction partB =
132 storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalFunctionCoefficient>("z"), cache),
133 storm::Polynomial(parser.template parseMultivariatePolynomial<storm::RationalFunctionCoefficient>("2*y"), cache));
134
135 storm::RationalFunction rationalFunction = storm::RationalFunction(partA + partB);
136
137 ASSERT_NO_THROW(function = manager->template getConstant<storm::RationalFunction>(rationalFunction));
138
139 EXPECT_EQ(0ul, function.getNonZeroCount());
140 EXPECT_EQ(1ul, function.getLeafCount());
141 EXPECT_EQ(1ul, function.getNodeCount());
142 });
143}
144
145TYPED_TEST(SylvanDd, RationalFunctionToDouble) {
146 const storm::dd::DdType DdType = TestFixture::DdType;
147 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
148
149 manager->execute([&]() {
150 std::pair<storm::expressions::Variable, storm::expressions::Variable> xExpr;
151 std::pair<storm::expressions::Variable, storm::expressions::Variable> yExpr;
152 std::pair<storm::expressions::Variable, storm::expressions::Variable> zExpr;
153 ASSERT_NO_THROW(xExpr = manager->addMetaVariable("x", 0, 1));
154 ASSERT_NO_THROW(yExpr = manager->addMetaVariable("y", 0, 1));
155 ASSERT_NO_THROW(zExpr = manager->addMetaVariable("z", 0, 1));
156
157 storm::dd::Bdd<DdType> bddX0 = manager->getEncoding(xExpr.first, 0);
158 storm::dd::Bdd<DdType> bddX1 = manager->getEncoding(xExpr.first, 1);
159 storm::dd::Bdd<DdType> bddY0 = manager->getEncoding(yExpr.first, 0);
160 storm::dd::Bdd<DdType> bddY1 = manager->getEncoding(yExpr.first, 1);
161 storm::dd::Bdd<DdType> bddZ0 = manager->getEncoding(zExpr.first, 0);
162 storm::dd::Bdd<DdType> bddZ1 = manager->getEncoding(zExpr.first, 1);
163
164 storm::dd::Add<DdType, storm::RationalFunction> complexAdd =
165 ((bddX0 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() *
166 manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(-1)))) +
167 ((bddX0 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() *
168 manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(0)))) +
169 ((bddX0 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() *
170 manager->template getConstant<storm::RationalFunction>(
171 storm::RationalFunction(storm::RationalFunctionCoefficient(1) / storm::RationalFunctionCoefficient(2)))) +
172 ((bddX0 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() *
173 manager->template getConstant<storm::RationalFunction>(
174 storm::RationalFunction(storm::RationalFunctionCoefficient(1) / storm::RationalFunctionCoefficient(3)))) +
175 ((bddX1 && (bddY0 && bddZ0)).template toAdd<storm::RationalFunction>() *
176 manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(100000)))) +
177 ((bddX1 && (bddY0 && bddZ1)).template toAdd<storm::RationalFunction>() *
178 manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(3)))) +
179 ((bddX1 && (bddY1 && bddZ0)).template toAdd<storm::RationalFunction>() *
180 manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(4)))) +
181 ((bddX1 && (bddY1 && bddZ1)).template toAdd<storm::RationalFunction>() *
182 manager->template getConstant<storm::RationalFunction>(storm::RationalFunction(storm::RationalFunctionCoefficient(0))));
183 EXPECT_EQ(6ul, complexAdd.getNonZeroCount());
184 EXPECT_EQ(7ul, complexAdd.getLeafCount());
185 EXPECT_EQ(14ul, complexAdd.getNodeCount());
186
187 storm::dd::Add<DdType, double> doubleAdd = complexAdd.template toValueType<double>();
188
189 EXPECT_EQ(6ul, doubleAdd.getNonZeroCount());
190 EXPECT_EQ(7ul, doubleAdd.getLeafCount());
191 EXPECT_EQ(14ul, doubleAdd.getNodeCount());
192
193 storm::dd::Add<DdType, double> comparisonAdd =
194 ((bddX0 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(-1.0)) +
195 ((bddX0 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.0)) +
196 ((bddX0 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(0.5)) +
197 ((bddX0 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.33333333333333333333)) +
198 ((bddX1 && (bddY0 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(100000.0)) +
199 ((bddX1 && (bddY0 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(3.0)) +
200 ((bddX1 && (bddY1 && bddZ0)).template toAdd<double>() * manager->template getConstant<double>(4.0)) +
201 ((bddX1 && (bddY1 && bddZ1)).template toAdd<double>() * manager->template getConstant<double>(0.0));
202
203 EXPECT_TRUE(comparisonAdd == doubleAdd);
204 });
205}
206
207TYPED_TEST(SylvanDd, RationalFunctionEncodingTest) {
208 const storm::dd::DdType DdType = TestFixture::DdType;
209 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
210 manager->execute([&]() {
211 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
212
213 storm::dd::Bdd<DdType> encoding;
214 STORM_SILENT_ASSERT_THROW(encoding = manager->getEncoding(x.first, 0), storm::exceptions::InvalidArgumentException);
215 STORM_SILENT_ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException);
216 ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4));
217 EXPECT_EQ(1ul, encoding.getNonZeroCount());
218
219 // As a BDD, this DD has one only leaf, because there does not exist a 0-leaf, and (consequently) one node less
220 // than the MTBDD.
221 EXPECT_EQ(5ul, encoding.getNodeCount());
222 EXPECT_EQ(1ul, encoding.getLeafCount());
223
224 storm::dd::Add<DdType, storm::RationalFunction> add;
225 ASSERT_NO_THROW(add = encoding.template toAdd<storm::RationalFunction>());
226
227 // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6.
228 EXPECT_EQ(6ul, add.getNodeCount());
229 EXPECT_EQ(2ul, add.getLeafCount());
230 });
231}
232
233TYPED_TEST(SylvanDd, RationalFunctionIdentityTest) {
234 const storm::dd::DdType DdType = TestFixture::DdType;
235 std::shared_ptr<storm::dd::DdManager<DdType>> manager(new storm::dd::DdManager<DdType>());
236 manager->execute([&]() {
237 std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
238
239 storm::dd::Add<DdType, storm::RationalFunction> identity;
240 ASSERT_NO_THROW(identity = manager->template getIdentity<storm::RationalFunction>(x.first));
241
242 EXPECT_EQ(9ul, identity.getNonZeroCount());
243 EXPECT_EQ(10ul, identity.getLeafCount());
244 EXPECT_EQ(21ul, identity.getNodeCount());
245 });
246}
TYPED_TEST_SUITE
TYPED_TEST_SUITE(SylvanDd, TestingTypes,)
TYPED_TEST
TYPED_TEST(SylvanDd, AddSharpenTest)
Definition SylvanDdTest.cpp:31
TestingTypes
::testing::Types< Sylvan > TestingTypes
Definition SylvanDdTest.cpp:28
SylvanDd::DdType
static const storm::dd::DdType DdType
Definition SylvanDdTest.cpp:25
Sylvan::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:30
storm::dd::Add::sharpenKwekMehlhorn
Add< LibraryType, storm::RationalNumber > sharpenKwekMehlhorn(uint64_t precision) const
Retrieves the function that sharpens all values in the current ADD with the Kwek-Mehlhorn algorithm.
Definition Add.cpp:151
storm::dd::Add::getValue
ValueType getValue(std::map< storm::expressions::Variable, int_fast64_t > const &metaVariableToValueMap=std::map< storm::expressions::Variable, int_fast64_t >()) const
Retrieves the value of the function when all meta variables are assigned the values of the given mapp...
Definition Add.cpp:508
storm::dd::Add::getNonZeroCount
virtual uint_fast64_t getNonZeroCount() const override
Retrieves the number of encodings that are mapped to a non-zero value.
Definition Add.cpp:451
storm::dd::Add::getNodeCount
virtual uint_fast64_t getNodeCount() const override
Retrieves the number of nodes necessary to represent the DD.
Definition Add.cpp:465
storm::dd::Add::getLeafCount
virtual uint_fast64_t getLeafCount() const override
Retrieves the number of leaves of the ADD.
Definition Add.cpp:460
storm::dd::Add::setValue
void setValue(storm::expressions::Variable const &metaVariable, int_fast64_t variableValue, ValueType const &targetValue)
Sets the function values of all encodings that have the given value of the meta variable to the given...
Definition Add.cpp:480
storm::dd::Bdd::getNonZeroCount
virtual uint_fast64_t getNonZeroCount() const override
Retrieves the number of encodings that are mapped to a non-zero value.
Definition Bdd.cpp:513
storm::dd::Bdd::getNodeCount
virtual uint_fast64_t getNodeCount() const override
Retrieves the number of nodes necessary to represent the DD.
Definition Bdd.cpp:527
storm::dd::Bdd::getLeafCount
virtual uint_fast64_t getLeafCount() const override
Retrieves the number of leaves of the DD.
Definition Bdd.cpp:522
storm::RationalFunction
carl::RationalFunction< Polynomial, true > RationalFunction
Definition RationalFunctionForward.h:55
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:99