From da69e8d9b70e03962c6f0e305ca4440cf157e112 Mon Sep 17 00:00:00 2001 From: Philipp Berger Date: Wed, 7 Dec 2016 16:26:02 +0100 Subject: [PATCH 1/2] Cherry-picked changes. --- .../sylvan/src/storm_function_wrapper.cpp | 333 ++++++++++-------- .../sylvan/src/storm_function_wrapper.h | 2 + .../sylvan/src/sylvan_obj_mtbdd_storm.hpp | 2 + .../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 6 + .../src/sylvan_storm_rational_function.h | 24 +- src/storm/storage/dd/Add.cpp | 25 +- src/storm/storage/dd/Add.h | 7 + src/storm/storage/dd/DdManager.cpp | 8 + src/storm/storage/dd/DdManager.h | 8 + .../storage/dd/sylvan/InternalSylvanAdd.cpp | 15 +- .../storage/dd/sylvan/InternalSylvanAdd.h | 9 +- src/test/storage/SylvanDdTest.cpp | 59 +++- 12 files changed, 339 insertions(+), 159 deletions(-) diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp index a3fb9dce6..b5132f984 100644 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp @@ -5,6 +5,8 @@ #include #include #include +#include + #include "storm/adapters/CarlAdapter.h" #include "sylvan_storm_rational_function.h" @@ -13,224 +15,267 @@ #include #include -#undef DEBUG_STORM_FUNCTION_WRAPPER - -#ifdef DEBUG_STORM_FUNCTION_WRAPPER -#define LOG_I(funcName) std::cout << "Entering function " << funcName << std::endl; -#define LOG_O(funcName) std::cout << "Leaving function " << funcName << std::endl; -#else -#define LOG_I(funcName) -#define LOG_O(funcName) -#endif +std::mutex carlMutex; void storm_rational_function_init(storm_rational_function_ptr* a) { - LOG_I("init") -#ifdef DEBUG_STORM_FUNCTION_WRAPPER - std::cout << "storm_rational_function_init - ptr of old = " << *a << ", value = " << *((storm::RationalFunction*)(*a)) << std::endl; -#endif - storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); + std::lock_guard lock(carlMutex); + { + storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); + + if (srf_ptr == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_init()!" << std::endl; + return; + } - if (srf_ptr == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_init()!" << std::endl; - return; + *a = srf_ptr; } - - *a = srf_ptr; -#ifdef DEBUG_STORM_FUNCTION_WRAPPER - std::cout << "storm_rational_function_init - ptr of new = " << *a << ", value = " << *((storm::RationalFunction*)(*a)) << std::endl; -#endif - LOG_O("init") } void storm_rational_function_destroy(storm_rational_function_ptr a) { - LOG_I("destroy") - delete (storm::RationalFunction*)a; - LOG_O("destroy") + std::lock_guard lock(carlMutex); + { + storm::RationalFunction* srf = (storm::RationalFunction*)a; + delete srf; + } } int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) { - LOG_I("equals") - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - - LOG_O("equals") - + std::lock_guard lock(carlMutex); int result = 0; - if (srf_a == srf_b) { - result = 1; - } + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; -#ifdef DEBUG_STORM_FUNCTION_WRAPPER - std::cout << "storm_rational_function_equals called with ptr = " << a << " value a = " << srf_a << " and ptr = " << b << " value b = " << srf_b << " result = " << result << "." << std::endl; -#endif + if (srf_a == srf_b) { + result = 1; + } + } return result; } storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) { - LOG_I("plus") - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_plus()!" << std::endl; - return (storm_rational_function_ptr)nullptr; - } + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - *result_srf += srf_b; - - storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_plus()!" << std::endl; + return result; + } + + *result_srf += srf_b; + result = (storm_rational_function_ptr)result_srf; + } - LOG_O("plus") return result; } storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { - LOG_I("minus") - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_minus()!" << std::endl; - return (storm_rational_function_ptr)nullptr; - } + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - *result_srf -= srf_b; - - storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; - - LOG_O("minus") + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_minus()!" << std::endl; + return result; + } + + *result_srf -= srf_b; + result = (storm_rational_function_ptr)result_srf; + } return result; } storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { - LOG_I("times") - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_times()!" << std::endl; - return (storm_rational_function_ptr)nullptr; - } + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - *result_srf *= srf_b; - - storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; - - LOG_O("times") + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_times()!" << std::endl; + return result; + } + + *result_srf *= srf_b; + result = (storm_rational_function_ptr)result_srf; + } return result; } storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { - LOG_I("divide") - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_divide()!" << std::endl; - return (storm_rational_function_ptr)nullptr; - } + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; - *result_srf /= srf_b; - - storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; - - LOG_O("divide") + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_divide()!" << std::endl; + return result; + } + + *result_srf /= srf_b; + result = (storm_rational_function_ptr)result_srf; + } return result; } uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { - LOG_I("hash") - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - - size_t hash = carl::hash_value(srf_a); - -#ifdef DEBUG_STORM_FUNCTION_WRAPPER - std::cout << "storm_rational_function_hash of value " << srf_a << " is " << hash << std::endl; -#endif - - uint64_t result = hash ^ seed; - - LOG_O("hash") + std::lock_guard lock(carlMutex); + + uint64_t result = 0; + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + size_t hash = carl::hash_value(srf_a); + + result = hash ^ seed; + } return result; } storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) { - LOG_I("negate") - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - if (result_srf == nullptr) { - std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl; - return (storm_rational_function_ptr)nullptr; - } + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - *result_srf = -srf_a; - - storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; - - LOG_O("negate") + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl; + return result; + } + + *result_srf = -srf_a; + result = (storm_rational_function_ptr)result_srf; + } return result; } int storm_rational_function_is_zero(storm_rational_function_ptr a) { - LOG_I("isZero") - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + std::lock_guard lock(carlMutex); - if (srf_a.isZero()) { + bool resultIsZero = false; + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + resultIsZero = srf_a.isZero(); + } + + if (resultIsZero) { return 1; } else { return 0; } } +double storm_rational_function_get_constant(storm_rational_function_ptr a) { + std::lock_guard lock(carlMutex); + + double result = -1.0; + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + + if (srf_a.isConstant()) { + result = carl::toDouble(storm::RationalNumber(srf_a.nominatorAsNumber() / srf_a.denominatorAsNumber())); + } else { + std::cout << "Defaulting to -1.0 since this is not a constant: " << srf_a << std::endl; + } + } + return result; +} + storm_rational_function_ptr storm_rational_function_get_zero() { - static storm::RationalFunction zeroFunction(0); - LOG_I("getZero") - return (storm_rational_function_ptr)(&zeroFunction); + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; + + { + storm::RationalFunction* result_srf = new storm::RationalFunction(0); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_get_zero()!" << std::endl; + return result; + } + result = (storm_rational_function_ptr)result_srf; + } + + return result; } storm_rational_function_ptr storm_rational_function_get_one() { - static storm::RationalFunction oneFunction(1); - LOG_I("getOne") - return (storm_rational_function_ptr)(&oneFunction); + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; + + { + storm::RationalFunction* result_srf = new storm::RationalFunction(1); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_get_one()!" << std::endl; + return result; + } + result = (storm_rational_function_ptr)result_srf; + } + + return result; } void print_storm_rational_function(storm_rational_function_ptr a) { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - std::cout << srf_a << std::flush; + std::lock_guard lock(carlMutex); + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + std::cout << srf_a << std::flush; + } } void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out) { - std::stringstream ss; - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - ss << srf_a; - std::string s = ss.str(); - fprintf(out, "%s", s.c_str()); + std::lock_guard lock(carlMutex); + { + std::stringstream ss; + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + ss << srf_a; + std::string s = ss.str(); + fprintf(out, "%s", s.c_str()); + } } -MTBDD testiTest(storm::RationalFunction const& currentFunction, std::map>> const& replacements) { +MTBDD testiTest(storm::RationalFunction const& currentFunction, std::map>> const& replacements) { if (currentFunction.isConstant()) { return mtbdd_storm_rational_function((storm_rational_function_ptr)¤tFunction); } std::set variablesInFunction = currentFunction.gatherVariables(); - std::map>>::const_iterator it = replacements.cbegin(); - std::map>>::const_iterator end = replacements.cend(); + std::map>>::const_iterator it = replacements.cbegin(); + std::map>>::const_iterator end = replacements.cend(); // Walking the (ordered) map enforces an ordering on the MTBDD for (; it != end; ++it) { - if (variablesInFunction.find(it->first) != variablesInFunction.cend()) { - std::map highReplacement = {{it->first, it->second.second.first}}; - std::map lowReplacement = {{it->first, it->second.second.second}}; - MTBDD high = testiTest(currentFunction.substitute(highReplacement), replacements); - MTBDD low = testiTest(currentFunction.substitute(lowReplacement), replacements); + if (variablesInFunction.find(it->second.first) != variablesInFunction.cend()) { + std::map highReplacement = {{it->second.first, it->second.second.first}}; + std::map lowReplacement = {{it->second.first, it->second.second.second}}; + + std::lock_guard* lock = new std::lock_guard(carlMutex); + storm::RationalFunction const highSrf = currentFunction.substitute(highReplacement); + storm::RationalFunction const lowSrf = currentFunction.substitute(lowReplacement); + delete lock; + + MTBDD high = testiTest(highSrf, replacements); + MTBDD low = testiTest(lowSrf, replacements); LACE_ME - return mtbdd_ite(mtbdd_ithvar(it->second.first), high, low); + return mtbdd_ite(mtbdd_ithvar(it->first), high, low); + } else { + //std::cout << "No match for variable " << it->second.first << std::endl; } } @@ -238,12 +283,16 @@ MTBDD testiTest(storm::RationalFunction const& currentFunction, std::map lock(carlMutex); + if (srf_a.isConstant()) { + return dd; + } } - std::map>>* replacements = (std::map>>*)context; + std::map>>* replacements = (std::map>>*)context; return testiTest(srf_a, *replacements); } diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.h b/resources/3rdparty/sylvan/src/storm_function_wrapper.h index 40c31dd0f..104842972 100644 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.h +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.h @@ -33,6 +33,8 @@ int storm_rational_function_is_zero(storm_rational_function_ptr a); MTBDD storm_rational_function_leaf_parameter_replacement(MTBDD dd, storm_rational_function_ptr a, void* context); +double storm_rational_function_get_constant(storm_rational_function_ptr a); + #ifdef __cplusplus } #endif diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index 26d79732f..cb272dbbb 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -32,6 +32,8 @@ Mtbdd AbstractPlusRF(const BddSet &variables) const; Mtbdd ReplaceLeavesRF(void* context) const; + + Mtbdd ToDoubleRF() const; #endif /** diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index 008114e20..bead06e8a 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -23,6 +23,12 @@ Bdd::toStormRationalFunctionMtbdd() const { return mtbdd_bool_to_storm_rational_function(bdd); } +Mtbdd +Mtbdd::ToDoubleRF() const { + LACE_ME; + return sylvan_storm_rational_function_to_double(mtbdd); +} + Mtbdd Mtbdd::PlusRF(const Mtbdd &other) const { diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h index 458bc5002..0b06cdf0f 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -104,14 +104,16 @@ TASK_DECL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, MTBDD, MTBD */ #define sylvan_storm_rational_function_abstract_plus(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_plus)) +/** + * Apply a unary operation to
. + * Callback is consulted after the cache, thus the application to a terminal is cached. + */ +TASK_DECL_3(MTBDD, mtbdd_uapply_nocache, MTBDD, mtbdd_uapply_op, size_t); +#define mtbdd_uapply_nocache(dd, op, param) CALL(mtbdd_uapply_nocache, dd, op, param) + /** * Functionality regarding the replacement of leaves in MTBDDs. - * - * uint64_t mtbdd_getvalue - * uint32_t mtbdd_gettype - * void* custom context ptr */ -typedef MTBDD (*mtbddLeaveReplacementFunction)(uint64_t, uint32_t, void*); /** * Operation "replace" for one storm::RationalFunction MTBDD @@ -121,7 +123,17 @@ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_replace_leaves, MTBDD, size /** * Compute the MTBDD that arises from a after calling the mtbddLeaveReplacementFunction on each leaf. */ -#define sylvan_storm_rational_function_replace_leaves(a, ctx) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_replace_leaves), ctx) +#define sylvan_storm_rational_function_replace_leaves(a, ctx) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_function_op_replace_leaves), ctx) + +/** + * Takes a storm::RationalFunction MTBDD and transforms it into a double MTBDD + */ +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, size_t) + +/** + * Compute the MTBDD that arises from a after calling the mtbddLeaveReplacementFunction on each leaf. + */ +#define sylvan_storm_rational_function_to_double(a) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_function_op_to_double), 0) #ifdef __cplusplus } diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 748729907..8bf7a41a4 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -791,10 +791,18 @@ namespace storm { } template<> - Add Add::replaceLeaves(std::map>> const& replacementMap) const { - std::map>> internalReplacementMap; + Add Add::replaceLeaves(std::map>> const& replacementMap) const { + std::map>> internalReplacementMap; std::set containedMetaVariables = this->getContainedMetaVariables(); + uint32_t highestIndex = 0; + for (storm::expressions::Variable const& var: containedMetaVariables) { + uint32_t index = this->getDdManager().getMetaVariable(var).getDdVariables().at(0).getIndex(); + if (index > highestIndex) { + highestIndex = index; + } + } + std::map>>::const_iterator it = replacementMap.cbegin(); std::map>>::const_iterator end = replacementMap.cend(); @@ -803,13 +811,24 @@ namespace storm { STORM_LOG_THROW(metaVariable.getNumberOfDdVariables() == 1, storm::exceptions::InvalidArgumentException, "Cannot use MetaVariable with more then one internal DD variable."); auto const& ddVariable = metaVariable.getDdVariables().at(0); + STORM_LOG_ASSERT(ddVariable.getIndex() > highestIndex, "Can not replace leaves with DD variable that would not be at the bottom!"); - internalReplacementMap.insert(std::make_pair(it->first, std::make_pair(ddVariable.getIndex(), it->second.second))); + internalReplacementMap.insert(std::make_pair(ddVariable.getIndex(), std::make_pair(it->first, it->second.second))); containedMetaVariables.insert(it->second.first); } return Add(this->getDdManager(), internalAdd.replaceLeaves(internalReplacementMap), containedMetaVariables); } + + template + Add Add::toDouble() const { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Not yet implemented: replaceLeaves"); + } + + template<> + Add Add::toDouble() const { + return Add(this->getDdManager(), internalAdd.toDouble(), this->getContainedMetaVariables()); + } #endif template class Add; diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 05a4261d6..2654a8c91 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -254,6 +254,13 @@ namespace storm { * @return The resulting function represented as an ADD. */ Add replaceLeaves(std::map>> const& replacementMap) const; + + /*! + * Replaces the leaves in this MTBDD, converting them to double if possible, and -1.0 else. + * + * @return The resulting function represented as an ADD. + */ + Add toDouble() const; #endif /*! diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp index e5b802464..3cd2539dd 100644 --- a/src/storm/storage/dd/DdManager.cpp +++ b/src/storm/storage/dd/DdManager.cpp @@ -234,6 +234,14 @@ namespace storm { bool DdManager::hasMetaVariable(std::string const& metaVariableName) const { return manager->hasVariable(metaVariableName); } + + template + storm::expressions::Variable DdManager::getMetaVariable(std::string const& metaVariableName) const { + // Check whether the meta variable exists. + STORM_LOG_THROW(hasMetaVariable(metaVariableName), storm::exceptions::InvalidArgumentException, "Unknown meta variable name '" << metaVariableName << "'."); + + return manager->getVariable(metaVariableName); + } template bool DdManager::supportsOrderedInsertion() const { diff --git a/src/storm/storage/dd/DdManager.h b/src/storm/storage/dd/DdManager.h index 00ce35e26..0ab1ed1c9 100644 --- a/src/storm/storage/dd/DdManager.h +++ b/src/storm/storage/dd/DdManager.h @@ -163,6 +163,14 @@ namespace storm { * @return True if the given meta variable name is managed by this manager. */ bool hasMetaVariable(std::string const& variableName) const; + + /*! + * Retrieves the given meta variable by name. + * + * @param variableName The name of the variable. + * @return The meta variable. + */ + storm::expressions::Variable getMetaVariable(std::string const& variableName) const; /*! * Checks whether this manager supports the ordered insertion of variables, i.e. inserting variables at diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 8bc217e44..391f26be9 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -290,17 +290,28 @@ namespace storm { #endif template - InternalAdd InternalAdd::replaceLeaves(std::map>> const& replacementMap) const { + InternalAdd InternalAdd::replaceLeaves(std::map>> const& replacementMap) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: replaceLeaves"); } #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::replaceLeaves(std::map>> const& replacementMap) const { + InternalAdd InternalAdd::replaceLeaves(std::map>> const& replacementMap) const { return InternalAdd(ddManager, this->sylvanMtbdd.ReplaceLeavesRF((void*)&replacementMap)); } #endif + template + InternalAdd InternalAdd::toDouble() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: toDouble"); + } + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::toDouble() const { + return InternalAdd(ddManager, this->sylvanMtbdd.ToDoubleRF()); + } +#endif template InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index ea0707380..17fd8eca2 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -255,7 +255,14 @@ namespace storm { * @param replacementMap The variable replacement map. * @return The resulting function represented as an ADD. */ - InternalAdd replaceLeaves(std::map>> const& replacementMap) const; + InternalAdd replaceLeaves(std::map>> const& replacementMap) const; + + /*! + * Replaces the leaves in this MTBDD, converting them to double if possible, and -1.0 else. + * + * @return The resulting function represented as an ADD. + */ + InternalAdd toDouble() const; #endif /*! diff --git a/src/test/storage/SylvanDdTest.cpp b/src/test/storage/SylvanDdTest.cpp index f32f3be1a..fc27dcc03 100644 --- a/src/test/storage/SylvanDdTest.cpp +++ b/src/test/storage/SylvanDdTest.cpp @@ -136,7 +136,6 @@ TEST(SylvanDd, BddExistAbstractRepresentative) { storm::dd::Bdd bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1; storm::dd::Bdd bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1; - //bddAllTrueOrAllFalse.template toAdd().exportToDot("test_Sylvan_addAllTrueOrAllFalse.dot"); representative_x = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first}); EXPECT_EQ(2ul, representative_x.getNonZeroCount()); @@ -464,6 +463,11 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementSimpleVariable) { EXPECT_EQ(2ul, replacedAddSimpleX.getLeafCount()); EXPECT_EQ(3ul, replacedAddSimpleX.getNodeCount()); EXPECT_TRUE(replacedAddSimpleX == complexAdd); + + storm::dd::Add abstractedAddMax = replacedAddSimpleX.toDouble().maxAbstract({xExpr.first}); + storm::dd::Add abstractedAddMin = replacedAddSimpleX.toDouble().minAbstract({xExpr.first}); + EXPECT_TRUE(abstractedAddMax == manager->template getConstant(0.66666666666666666666)); + EXPECT_TRUE(abstractedAddMin == manager->template getConstant(0.33333333333333333333)); } TEST(SylvanDd, RationalFunctionLeaveReplacementTwoVariables) { @@ -537,7 +541,6 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementComplexFunction) { parser.setVariables({"x", "y", "z"}); storm::RationalFunction zDivTwoY = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial("2*y"), cache)); - //storm::RationalFunction rationalFunction(two * x + x*y + constantOneDivTwo * z / y); storm::RationalFunction rationalFunction = storm::RationalFunction(storm::Polynomial(parser.parseMultivariatePolynomial("2*x+x*y"), cache), storm::Polynomial(parser.parseMultivariatePolynomial("1"), cache)) + zDivTwoY; ASSERT_NO_THROW(function = manager->template getConstant(rationalFunction)); @@ -617,9 +620,6 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementComplexFunction) { EXPECT_EQ(8ul, replacedAdd.getLeafCount()); EXPECT_EQ(15ul, replacedAdd.getNodeCount()); EXPECT_TRUE(replacedAdd == complexAdd); - - replacedAdd.exportToDot("sylvan_replacedAddC.dot"); - complexAdd.exportToDot("sylvan_complexAddC.dot"); } TEST(SylvanDd, RationalFunctionConstants) { @@ -664,6 +664,55 @@ TEST(SylvanDd, RationalFunctionConstants) { EXPECT_EQ(1ul, function.getNodeCount()); } +TEST(SylvanDd, RationalFunctionToDouble) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + std::pair xExpr; + std::pair yExpr; + std::pair zExpr; + ASSERT_NO_THROW(xExpr = manager->addMetaVariable("x", 0, 1)); + ASSERT_NO_THROW(yExpr = manager->addMetaVariable("y", 0, 1)); + ASSERT_NO_THROW(zExpr = manager->addMetaVariable("z", 0, 1)); + + storm::dd::Bdd bddX0 = manager->getEncoding(xExpr.first, 0); + storm::dd::Bdd bddX1 = manager->getEncoding(xExpr.first, 1); + storm::dd::Bdd bddY0 = manager->getEncoding(yExpr.first, 0); + storm::dd::Bdd bddY1 = manager->getEncoding(yExpr.first, 1); + storm::dd::Bdd bddZ0 = manager->getEncoding(zExpr.first, 0); + storm::dd::Bdd bddZ1 = manager->getEncoding(zExpr.first, 1); + + storm::dd::Add complexAdd = + ((bddX0 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(-1)))) + + ((bddX0 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(0)))) + + ((bddX0 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(1) / storm::RationalNumber(2)))) + + ((bddX0 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(1) / storm::RationalNumber(3)))) + + ((bddX1 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(100000)))) + + ((bddX1 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(3)))) + + ((bddX1 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(4)))) + + ((bddX1 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(storm::RationalNumber(0)))); + EXPECT_EQ(6ul, complexAdd.getNonZeroCount()); + EXPECT_EQ(7ul, complexAdd.getLeafCount()); + EXPECT_EQ(14ul, complexAdd.getNodeCount()); + + storm::dd::Add doubleAdd = complexAdd.toDouble(); + + EXPECT_EQ(6ul, doubleAdd.getNonZeroCount()); + EXPECT_EQ(7ul, doubleAdd.getLeafCount()); + EXPECT_EQ(14ul, doubleAdd.getNodeCount()); + + storm::dd::Add comparisonAdd = + ((bddX0 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(-1.0)) + + ((bddX0 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(0.0)) + + ((bddX0 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(0.5)) + + ((bddX0 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(0.33333333333333333333)) + + ((bddX1 && (bddY0 && bddZ0)).template toAdd() * manager->template getConstant(100000.0)) + + ((bddX1 && (bddY0 && bddZ1)).template toAdd() * manager->template getConstant(3.0)) + + ((bddX1 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(4.0)) + + ((bddX1 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(0.0)); + + EXPECT_TRUE(comparisonAdd == doubleAdd); +} + TEST(SylvanDd, RationalFunctionEncodingTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); From 822ae6be402d0ce9d0ccbd54394ab9a4ab517b84 Mon Sep 17 00:00:00 2001 From: Philipp Berger Date: Tue, 20 Dec 2016 13:44:05 +0100 Subject: [PATCH 2/2] Fixes --- .../src/sylvan_storm_rational_function.c | 72 +++++++++++++++++-- 1 file changed, 67 insertions(+), 5 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c index ae08ee588..1453449d9 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -205,7 +205,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, p storm_rational_function_ptr mres = storm_rational_function_plus(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); - // TODO: Delete mres? + storm_rational_function_destroy(mres); return res; } @@ -240,7 +240,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*, storm_rational_function_ptr mres = storm_rational_function_minus(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); - // TODO: Delete mres? + storm_rational_function_destroy(mres); return res; } @@ -273,7 +273,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*, storm_rational_function_ptr mres = storm_rational_function_times(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); - // TODO: Delete mres? + storm_rational_function_destroy(mres); return res; } @@ -307,7 +307,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, storm_rational_function_ptr mres = storm_rational_function_divide(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); - // TODO: Delete mres? + storm_rational_function_destroy(mres); return res; } @@ -369,7 +369,8 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p) storm_rational_function_ptr mres = storm_rational_function_negate(mdd); MTBDD res = mtbdd_storm_rational_function(mres); - // TODO: Delete mres? + storm_rational_function_destroy(mres); + return res; } @@ -398,6 +399,30 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_replace_leaves, MTBDD, dd, return mtbdd_invalid; } +/** + * Operation to double for one storm::RationalFunction MTBDD + */ +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, dd, size_t, p) +{ + LOG_I("task_impl_2 op_toDouble") + /* Handle partial functions */ + if (dd == mtbdd_false) return mtbdd_false; + + /* Compute result for leaf */ + if (mtbdd_isleaf(dd)) { + if (mtbdd_gettype(dd) != sylvan_storm_rational_function_type) { + printf("Can not convert to double, this has type %u!\n", mtbdd_gettype(dd)); + assert(0); + } + + storm_rational_function_ptr mdd = (storm_rational_function_ptr)mtbdd_getvalue(dd); + MTBDD result = mtbdd_double(storm_rational_function_get_constant(mdd)); + return result; + } + + return mtbdd_invalid; + (void)p; +} /** * Multiply and , and abstract variables using summation. @@ -477,3 +502,40 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b cache_put3(CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS, a, b, v, result); return result; } + +/** + * Apply a unary operation to
. + */ +TASK_IMPL_3(MTBDD, mtbdd_uapply_nocache, MTBDD, dd, mtbdd_uapply_op, op, size_t, param) +{ + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Check cache */ + MTBDD result; + //if (cache_get3(CACHE_MTBDD_UAPPLY, dd, (size_t)op, param, &result)) return result; + + /* Check terminal case */ + result = WRAP(op, dd, param); + if (result != mtbdd_invalid) { + /* Store in cache */ + //cache_put3(CACHE_MTBDD_UAPPLY, dd, (size_t)op, param, result); + return result; + } + + /* Get cofactors */ + mtbddnode_t ndd = MTBDD_GETNODE(dd); + MTBDD ddlow = node_getlow(dd, ndd); + MTBDD ddhigh = node_gethigh(dd, ndd); + + /* Recursive */ + mtbdd_refs_spawn(SPAWN(mtbdd_uapply_nocache, ddhigh, op, param)); + MTBDD low = mtbdd_refs_push(CALL(mtbdd_uapply_nocache, ddlow, op, param)); + MTBDD high = mtbdd_refs_sync(SYNC(mtbdd_uapply_nocache)); + mtbdd_refs_pop(1); + result = mtbdd_makenode(mtbddnode_getvariable(ndd), low, high); + + /* Store in cache */ + //cache_put3(CACHE_MTBDD_UAPPLY, dd, (size_t)op, param, result); + return result; +}