diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 75a2c8947..ad5566050 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -41,6 +41,46 @@ TEST(SylvanDd, Constants) { EXPECT_EQ(2, two.getMax()); } +TEST(SylvanDd, AddGetMetaVariableTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); + EXPECT_EQ(2ul, manager->getNumberOfMetaVariables()); + + ASSERT_THROW(manager->addMetaVariable("x", 0, 3), storm::exceptions::InvalidArgumentException); + + ASSERT_NO_THROW(manager->addMetaVariable("y", 0, 3)); + EXPECT_EQ(4ul, manager->getNumberOfMetaVariables()); + + EXPECT_TRUE(manager->hasMetaVariable("x'")); + EXPECT_TRUE(manager->hasMetaVariable("y'")); + + std::set metaVariableSet = {"x", "x'", "y", "y'"}; + EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames()); +} + +TEST(SylvanDd, EncodingTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + + storm::dd::Bdd encoding; + ASSERT_THROW(encoding = manager->getEncoding(x.first, 0), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4)); + EXPECT_EQ(1ul, encoding.getNonZeroCount()); + + // As a BDD, this DD has one only leaf, because there does not exist a 0-leaf, and (consequently) one node less + // than the MTBDD. + EXPECT_EQ(5ul, encoding.getNodeCount()); + EXPECT_EQ(1ul, encoding.getLeafCount()); + + storm::dd::Add add; + ASSERT_NO_THROW(add = encoding.template toAdd()); + + // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6. + EXPECT_EQ(6ul, add.getNodeCount()); + EXPECT_EQ(2ul, add.getLeafCount()); +} + #ifdef STORM_HAVE_CARL TEST(SylvanDd, RationalFunctionConstants) { std::shared_ptr> manager(new storm::dd::DdManager()); @@ -67,26 +107,8 @@ TEST(SylvanDd, RationalFunctionConstants) { EXPECT_EQ(1ul, two.getLeafCount()); EXPECT_EQ(1ul, two.getNodeCount()); } -#endif - -TEST(SylvanDd, AddGetMetaVariableTest) { - std::shared_ptr> manager(new storm::dd::DdManager()); - ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); - EXPECT_EQ(2ul, manager->getNumberOfMetaVariables()); - - ASSERT_THROW(manager->addMetaVariable("x", 0, 3), storm::exceptions::InvalidArgumentException); - - ASSERT_NO_THROW(manager->addMetaVariable("y", 0, 3)); - EXPECT_EQ(4ul, manager->getNumberOfMetaVariables()); - - EXPECT_TRUE(manager->hasMetaVariable("x'")); - EXPECT_TRUE(manager->hasMetaVariable("y'")); - - std::set metaVariableSet = {"x", "x'", "y", "y'"}; - EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames()); -} -TEST(SylvanDd, EncodingTest) { +TEST(SylvanDd, RationalFunctionEncodingTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); @@ -101,14 +123,28 @@ TEST(SylvanDd, EncodingTest) { EXPECT_EQ(5ul, encoding.getNodeCount()); EXPECT_EQ(1ul, encoding.getLeafCount()); - storm::dd::Add add; - ASSERT_NO_THROW(add = encoding.template toAdd()); + storm::dd::Add add; + ASSERT_NO_THROW(add = encoding.template toAdd()); // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6. EXPECT_EQ(6ul, add.getNodeCount()); EXPECT_EQ(2ul, add.getLeafCount()); } +TEST(SylvanDd, RationalFunctionIdentityTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + + storm::dd::Add identity; + ASSERT_NO_THROW(identity = manager->getIdentity(x.first)); + + EXPECT_EQ(9ul, identity.getNonZeroCount()); + EXPECT_EQ(10ul, identity.getLeafCount()); + EXPECT_EQ(21ul, identity.getNodeCount()); +} + +#endif + TEST(SylvanDd, RangeTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x; @@ -440,4 +476,4 @@ TEST(SylvanDd, BddOddTest) { EXPECT_EQ(9ul, matrix.getRowGroupCount()); EXPECT_EQ(9ul, matrix.getColumnCount()); EXPECT_EQ(106ul, matrix.getNonzeroEntryCount()); -} \ No newline at end of file +}