From 907e3512c05bd5afa588fa9bac318a01f3225c3a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 1 Apr 2015 20:15:01 +0200
Subject: [PATCH] Fixed a potential bug in the ODD generation and it now uses
hash maps instead of regular maps.
Former-commit-id: f8e5fb3018fed7c49ed011eb17d390f71781efea
---
src/storage/dd/CuddOdd.cpp | 17 ++++++++++++-----
src/storage/dd/CuddOdd.h | 11 +++++++++--
2 files changed, 21 insertions(+), 7 deletions(-)
diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp
index e459406aa..40805d9e9 100644
--- a/src/storage/dd/CuddOdd.cpp
+++ b/src/storage/dd/CuddOdd.cpp
@@ -14,7 +14,7 @@ namespace storm {
std::vector<uint_fast64_t> ddVariableIndices = add.getSortedVariableIndices();
// Prepare a unique table for each level that keeps the constructed ODD nodes unique.
- std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>> uniqueTableForLevels(ddVariableIndices.size() + 1);
+ std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>> uniqueTableForLevels(ddVariableIndices.size() + 1);
// Now construct the ODD structure from the ADD.
std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddFromAddRec(add.getCuddDdNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
@@ -33,7 +33,7 @@ namespace storm {
std::vector<uint_fast64_t> ddVariableIndices = bdd.getSortedVariableIndices();
// Prepare a unique table for each level that keeps the constructed ODD nodes unique.
- std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>> uniqueTableForLevels(ddVariableIndices.size() + 1);
+ std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd<DdType::CUDD>>, HashFunctor>> uniqueTableForLevels(ddVariableIndices.size() + 1);
// Now construct the ODD structure from the BDD.
std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddFromBddRec(Cudd_Regular(bdd.getCuddDdNode()), manager->getCuddManager(), 0, Cudd_IsComplement(bdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
@@ -91,7 +91,7 @@ namespace storm {
}
}
- std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels) {
+ std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels) {
// Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
auto const& iterator = uniqueTableForLevels[currentLevel].find(dd);
if (iterator != uniqueTableForLevels[currentLevel].end()) {
@@ -130,9 +130,16 @@ namespace storm {
}
}
- std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels) {
+ std::size_t Odd<DdType::CUDD>::HashFunctor::operator()(std::pair<DdNode*, bool> const& key) const {
+ std::size_t result = 0;
+ boost::hash_combine(result, key.first);
+ boost::hash_combine(result, key.second);
+ return result;
+ }
+
+ std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd<DdType::CUDD>>, HashFunctor>>& uniqueTableForLevels) {
// Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
- auto const& iterator = uniqueTableForLevels[currentLevel].find(dd);
+ auto const& iterator = uniqueTableForLevels[currentLevel].find(std::make_pair(dd, complement));
if (iterator != uniqueTableForLevels[currentLevel].end()) {
return iterator->second;
} else {
diff --git a/src/storage/dd/CuddOdd.h b/src/storage/dd/CuddOdd.h
index 0c4c1793f..2d64275a3 100644
--- a/src/storage/dd/CuddOdd.h
+++ b/src/storage/dd/CuddOdd.h
@@ -2,6 +2,7 @@
#define STORM_STORAGE_DD_CUDDODD_H_
#include <memory>
+#include <unordered_map>
#include "src/storage/dd/Odd.h"
#include "src/storage/dd/CuddAdd.h"
@@ -96,6 +97,12 @@ namespace storm {
uint_fast64_t getNodeCount() const;
private:
+ // Declare a hash functor that is used for the unique tables in the construction process.
+ class HashFunctor {
+ public:
+ std::size_t operator()(std::pair<DdNode*, bool> const& key) const;
+ };
+
/*!
* Constructs an offset-labeled DD with the given topmost DD node, else- and then-successor.
*
@@ -119,7 +126,7 @@ namespace storm {
* ODD nodes for the same DD and level unique.
* @return A pointer to the constructed ODD for the given arguments.
*/
- static std::shared_ptr<Odd<DdType::CUDD>> buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels);
+ static std::shared_ptr<Odd<DdType::CUDD>> buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels);
/*!
* Recursively builds the ODD from a BDD (that potentially has complement edges).
@@ -134,7 +141,7 @@ namespace storm {
* ODD nodes for the same DD and level unique.
* @return A pointer to the constructed ODD for the given arguments.
*/
- static std::shared_ptr<Odd<DdType::CUDD>> buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels);
+ static std::shared_ptr<Odd<DdType::CUDD>> buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd<DdType::CUDD>>, HashFunctor>>& uniqueTableForLevels);
// The then- and else-nodes.
std::shared_ptr<Odd<DdType::CUDD>> elseNode;