sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge branch 'menu_games' into sylvanRationalFunctions 

# Conflicts:
#	test/functional/storage/CuddDdTest.cpp


Former-commit-id: b3d9341055
tempestpy_adaptions
PBerger 8 years ago
parent
23e67a26ad 3f15644e60
commit
e41ddfb762
2 changed files with 20 additions and 9 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
  2. 27
      test/functional/storage/CuddDdTest.cpp

2
resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
View File

@ -616,7 +616,7 @@ cuddBddExistAbstractRepresentativeRecur(
if (F->ref != 1) { if (F->ref != 1) {
cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, one); cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, one);
} }
return(cube);
return(Cudd_Not(cube));
} }
cuddRef(res1); cuddRef(res1);

27
test/functional/storage/CuddDdTest.cpp
View File

@ -68,28 +68,39 @@ TEST(CuddDd, BddExistAbstractRepresentative) {
ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1)); ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1));
storm::dd::Bdd<storm::dd::DdType::CUDD> bddX = manager->getEncoding(x.first, 1); storm::dd::Bdd<storm::dd::DdType::CUDD> bddX = manager->getEncoding(x.first, 1);
//bddX.exportToDot("/opt/masterThesis/storm/build/test_bdd_x.dot");
//bddX.template toAdd<double>().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_x.dot");
storm::dd::Bdd<storm::dd::DdType::CUDD> bddY = manager->getEncoding(y.first, 0); storm::dd::Bdd<storm::dd::DdType::CUDD> bddY = manager->getEncoding(y.first, 0);
//bddY.exportToDot("/opt/masterThesis/storm/build/test_bdd_y.dot");
//bddY.template toAdd<double>().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_y.dot");
storm::dd::Bdd<storm::dd::DdType::CUDD> bddZ = manager->getEncoding(z.first, 0); storm::dd::Bdd<storm::dd::DdType::CUDD> bddZ = manager->getEncoding(z.first, 0);
//bddZ.exportToDot("/opt/masterThesis/storm/build/test_bdd_z.dot");
//bddZ.template toAdd<double>().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_z.dot");
storm::dd::Bdd<storm::dd::DdType::CUDD> bddX1Y0Z0 = (bddX && bddY) && bddZ; storm::dd::Bdd<storm::dd::DdType::CUDD> bddX1Y0Z0 = (bddX && bddY) && bddZ;
//bddX1Y0Z0.exportToDot("/opt/masterThesis/storm/build/test_bddX1Y0Z0.dot");
//bddX1Y0Z0.template toAdd<double>().exportToDot("/opt/masterThesis/storm/build/test_cudd_bddX1Y0Z0.dot");
EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount());
EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount());
EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount());
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_x = bddX1Y0Z0.existsAbstractRepresentative({x.first}); storm::dd::Bdd<storm::dd::DdType::CUDD> representative_x = bddX1Y0Z0.existsAbstractRepresentative({x.first});
//representative_x.exportToDot("/opt/masterThesis/storm/build/test_representative_x.dot");
EXPECT_EQ(1ul, representative_x.getNonZeroCount());
EXPECT_EQ(1ul, representative_x.getLeafCount());
EXPECT_EQ(4ul, representative_x.getNodeCount());
EXPECT_TRUE(bddX1Y0Z0 == representative_x);
//representative_x.template toAdd<double>().exportToDot("/opt/masterThesis/storm/build/test_representativea_x.dot");
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_y = bddX1Y0Z0.existsAbstractRepresentative({y.first}); storm::dd::Bdd<storm::dd::DdType::CUDD> representative_y = bddX1Y0Z0.existsAbstractRepresentative({y.first});
//representative_y.exportToDot("/opt/masterThesis/storm/build/test_representative_y.dot");
EXPECT_EQ(1ul, representative_y.getNonZeroCount());
EXPECT_EQ(1ul, representative_y.getLeafCount());
EXPECT_EQ(4ul, representative_y.getNodeCount());
EXPECT_TRUE(bddX1Y0Z0 == representative_y);
//representative_y.template toAdd<double>().exportToDot("/opt/masterThesis/storm/build/test_representativea_y.dot");
storm::dd::Bdd<storm::dd::DdType::CUDD> representative_z = bddX1Y0Z0.existsAbstractRepresentative({z.first}); storm::dd::Bdd<storm::dd::DdType::CUDD> representative_z = bddX1Y0Z0.existsAbstractRepresentative({z.first});
//representative_z.exportToDot("/opt/masterThesis/storm/build/test_representative_z.dot");
EXPECT_EQ(1ul, representative_z.getNonZeroCount());
EXPECT_EQ(1ul, representative_z.getLeafCount());
EXPECT_EQ(4ul, representative_z.getNodeCount());
EXPECT_TRUE(bddX1Y0Z0 == representative_z);
//representative_z.template toAdd<double>().exportToDot("/opt/masterThesis/storm/build/test_representativea_z.dot");
} }
TEST(CuddDd, AddGetMetaVariableTest) { TEST(CuddDd, AddGetMetaVariableTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>()); std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));

Write Preview
Loading…
Cancel
Save