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