From 472851508c96308d7b6af20efb4dcf28dc210c2e Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 24 Nov 2015 22:06:25 +0100 Subject: [PATCH] changed return type of equal, notEqual, less, lessOrEqual, greater, greaterOrEqual to BDD since returning an ADD is logically not quite correct Former-commit-id: 64bf8b0704b6f46580c76bddc71a0cce1e6627c6 --- resources/3rdparty/sylvan/src/llmsset.h | 4 +- resources/3rdparty/sylvan/src/refs.h | 2 +- resources/3rdparty/sylvan/src/stats.h | 4 +- resources/3rdparty/sylvan/src/sylvan.h | 16 +-- resources/3rdparty/sylvan/src/sylvan_bdd.h | 2 +- resources/3rdparty/sylvan/src/sylvan_cache.h | 2 +- resources/3rdparty/sylvan/src/sylvan_common.h | 6 +- resources/3rdparty/sylvan/src/sylvan_gmp.h | 2 +- resources/3rdparty/sylvan/src/sylvan_mtbdd.c | 127 ++++++++++-------- resources/3rdparty/sylvan/src/sylvan_mtbdd.h | 10 +- resources/3rdparty/sylvan/src/sylvan_obj.cpp | 9 +- resources/3rdparty/sylvan/src/sylvan_obj.hpp | 6 +- src/adapters/AddExpressionAdapter.cpp | 36 +++-- src/builder/DdPrismModelBuilder.cpp | 26 ++-- src/models/symbolic/Model.cpp | 2 +- src/solver/SymbolicLinearEquationSolver.cpp | 2 +- src/storage/dd/Add.cpp | 29 ++-- src/storage/dd/Add.h | 12 +- src/storage/dd/Bdd.cpp | 1 - src/storage/dd/cudd/InternalCuddAdd.cpp | 31 ++--- src/storage/dd/cudd/InternalCuddAdd.h | 20 +-- src/storage/dd/sylvan/InternalSylvanAdd.cpp | 26 ++-- src/storage/dd/sylvan/InternalSylvanAdd.h | 22 +-- test/functional/storage/CuddDdTest.cpp | 30 ++--- test/functional/storage/SylvanDdTest.cpp | 2 +- 25 files changed, 222 insertions(+), 207 deletions(-) diff --git a/resources/3rdparty/sylvan/src/llmsset.h b/resources/3rdparty/sylvan/src/llmsset.h index 84c55e23b..0c3d5bc68 100644 --- a/resources/3rdparty/sylvan/src/llmsset.h +++ b/resources/3rdparty/sylvan/src/llmsset.h @@ -14,11 +14,11 @@ * limitations under the License. */ -#include +#include "sylvan_config.h" #include #include -#include +#include "lace.h" #ifndef LLMSSET_H #define LLMSSET_H diff --git a/resources/3rdparty/sylvan/src/refs.h b/resources/3rdparty/sylvan/src/refs.h index 697dcb980..aaf20bec0 100644 --- a/resources/3rdparty/sylvan/src/refs.h +++ b/resources/3rdparty/sylvan/src/refs.h @@ -15,7 +15,7 @@ */ #include // for uint32_t etc -#include +#include "sylvan_config.h" #ifndef REFS_INLINE_H #define REFS_INLINE_H diff --git a/resources/3rdparty/sylvan/src/stats.h b/resources/3rdparty/sylvan/src/stats.h index e06d6f4e3..b80c3eb76 100644 --- a/resources/3rdparty/sylvan/src/stats.h +++ b/resources/3rdparty/sylvan/src/stats.h @@ -14,8 +14,8 @@ * limitations under the License. */ -#include -#include +#include "lace.h" +#include "sylvan_config.h" #ifndef SYLVAN_STATS_H #define SYLVAN_STATS_H diff --git a/resources/3rdparty/sylvan/src/sylvan.h b/resources/3rdparty/sylvan/src/sylvan.h index 6fe09f9d6..3b490993a 100644 --- a/resources/3rdparty/sylvan/src/sylvan.h +++ b/resources/3rdparty/sylvan/src/sylvan.h @@ -35,16 +35,16 @@ * To temporarily disable garbage collection, use sylvan_gc_disable() and sylvan_gc_enable(). */ -#include +#include "sylvan_config.h" #include #include // for FILE #include -#include // for definitions +#include "lace.h" // for definitions -#include -#include -#include +#include "sylvan_cache.h" +#include "llmsset.h" +#include "stats.h" #ifndef SYLVAN_H #define SYLVAN_H @@ -175,8 +175,8 @@ extern llmsset_t nodes; } #endif /* __cplusplus */ -#include -#include -#include +#include "sylvan_bdd.h" +#include "sylvan_ldd.h" +#include "sylvan_mtbdd.h" #endif diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd.h b/resources/3rdparty/sylvan/src/sylvan_bdd.h index e4ca6627c..8ef6a27f0 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_bdd.h @@ -16,7 +16,7 @@ /* Do not include this file directly. Instead, include sylvan.h */ -#include +#include "tls.h" #ifndef SYLVAN_BDD_H #define SYLVAN_BDD_H diff --git a/resources/3rdparty/sylvan/src/sylvan_cache.h b/resources/3rdparty/sylvan/src/sylvan_cache.h index babc74f65..9555c3e58 100644 --- a/resources/3rdparty/sylvan/src/sylvan_cache.h +++ b/resources/3rdparty/sylvan/src/sylvan_cache.h @@ -1,6 +1,6 @@ #include // for uint32_t etc -#include +#include "sylvan_config.h" #ifndef CACHE_H #define CACHE_H diff --git a/resources/3rdparty/sylvan/src/sylvan_common.h b/resources/3rdparty/sylvan/src/sylvan_common.h index d26264e16..97bbf50c6 100644 --- a/resources/3rdparty/sylvan/src/sylvan_common.h +++ b/resources/3rdparty/sylvan/src/sylvan_common.h @@ -15,9 +15,9 @@ */ #include -#include -#include -#include +#include "sylvan.h" +#include "tls.h" +#include "sylvan_config.h" #ifndef SYLVAN_COMMON_H #define SYLVAN_COMMON_H diff --git a/resources/3rdparty/sylvan/src/sylvan_gmp.h b/resources/3rdparty/sylvan/src/sylvan_gmp.h index fbf6bc2ad..9650c56d3 100644 --- a/resources/3rdparty/sylvan/src/sylvan_gmp.h +++ b/resources/3rdparty/sylvan/src/sylvan_gmp.h @@ -21,7 +21,7 @@ #ifndef SYLVAN_GMP_H #define SYLVAN_GMP_H -#include +#include "sylvan.h" #include #ifdef __cplusplus diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index 9db5da54c..26de3cf1b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -14,7 +14,7 @@ * limitations under the License. */ -#include +#include "sylvan_config.h" #include #include @@ -25,11 +25,11 @@ #include #include -#include -#include -#include -#include -#include +#include "refs.h" +#include "sha2.h" +#include "sylvan.h" +#include "sylvan_common.h" +#include "sylvan_mtbdd_int.h" /* Primitives */ int @@ -1193,41 +1193,38 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb) /** * Binary operation Times (for MTBDDs of same type) - * Only for MTBDDs where either all leaves are Double. - * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), + * Only for MTBDDs where either all leaves are Integer or Double. + * If either operand is mtbdd_false (not defined), * then the result is mtbdd_false (i.e. not defined). */ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; -// if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; - // Handle Boolean MTBDDs: interpret as And -// if (a == mtbdd_true) return b; -// if (b == mtbdd_true) return a; + // Do not handle Boolean MTBDDs... mtbddnode_t na = GETNODE(a); mtbddnode_t nb = GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { -// uint64_t val_a = mtbddnode_getvalue(na); -// uint64_t val_b = mtbddnode_getvalue(nb); -// if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) { -// // both uint64_t -// if (val_a == 0) return a; -// else if (val_b == 0) return b; -// else { -// MTBDD result; -// if (val_a == 1) result = b; -// else if (val_b == 1) result = a; -// else result = mtbdd_uint64(val_a*val_b); -// int nega = mtbdd_isnegated(a); -// int negb = mtbdd_isnegated(b); -// if (nega ^ negb) return mtbdd_negate(result); -// else return result; -// } -// } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) { - if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) { + uint64_t val_a = mtbddnode_getvalue(na); + uint64_t val_b = mtbddnode_getvalue(nb); + if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) { + // both uint64_t + if (val_a == 0) return a; + else if (val_b == 0) return b; + else { + MTBDD result; + if (val_a == 1) result = b; + else if (val_b == 1) result = a; + else result = mtbdd_uint64(val_a*val_b); + int nega = mtbdd_isnegated(a); + int negb = mtbdd_isnegated(b); + if (nega ^ negb) return mtbdd_negate(result); + else return result; + } + } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) { // both double double vval_a = *(double*)&val_a; double vval_b = *(double*)&val_b; @@ -1244,32 +1241,32 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb) else return result; } } -// else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) { -// // both fraction -// uint64_t nom_a = val_a>>32; -// uint64_t nom_b = val_b>>32; -// uint64_t denom_a = val_a&0xffffffff; -// uint64_t denom_b = val_b&0xffffffff; -// // multiply! -// uint32_t c = gcd(nom_b, denom_a); -// uint32_t d = gcd(nom_a, denom_b); -// nom_a /= d; -// denom_a /= c; -// nom_a *= (nom_b/c); -// denom_a *= (denom_b/d); -// // compute result -// int nega = mtbdd_isnegated(a); -// int negb = mtbdd_isnegated(b); -// MTBDD result = mtbdd_fraction(nom_a, denom_a); -// if (nega ^ negb) return mtbdd_negate(result); -// else return result; -// } + else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) { + // both fraction + uint64_t nom_a = val_a>>32; + uint64_t nom_b = val_b>>32; + uint64_t denom_a = val_a&0xffffffff; + uint64_t denom_b = val_b&0xffffffff; + // multiply! + uint32_t c = gcd(denom_b, denom_a); + uint32_t d = gcd(nom_a, nom_b); + nom_a /= d; + denom_a /= c; + nom_a *= (denom_b/c); + denom_a *= (nom_b/d); + // compute result + int nega = mtbdd_isnegated(a); + int negb = mtbdd_isnegated(b); + MTBDD result = mtbdd_fraction(nom_a, denom_a); + if (nega ^ negb) return mtbdd_negate(result); + else return result; + } } -// if (a < b) { -// *pa = b; -// *pb = a; -// } + if (a < b) { + *pa = b; + *pb = a; + } return mtbdd_invalid; } @@ -1538,6 +1535,28 @@ TASK_IMPL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, a, size_t, svalue) return mtbdd_invalid; } +TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, a) +{ + /* We only expect "double" terminals, or false */ + if (a == mtbdd_false) return mtbdd_false; + if (a == mtbdd_true) return mtbdd_invalid; + + // a != constant + mtbddnode_t na = GETNODE(a); + + if (mtbddnode_isleaf(na)) { + if (mtbddnode_gettype(na) == 0) { + return mtbdd_getuint64(a) != 0 ? mtbdd_true : mtbdd_false; + } else if (mtbddnode_gettype(na) == 1) { + return mtbdd_getdouble(a) != 0.0 ? mtbdd_true : mtbdd_false; + } else if (mtbddnode_gettype(na) == 2) { + return mtbdd_getnumer(a) != 0 ? mtbdd_true : mtbdd_false; + } + } + + return mtbdd_invalid; +} + TASK_IMPL_2(MTBDD, mtbdd_threshold_double, MTBDD, dd, double, d) { return mtbdd_uapply(dd, TASK(mtbdd_op_threshold_double), *(size_t*)&d); diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h index c0b1a36a5..fb3ec24ac 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h @@ -226,7 +226,7 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_times, MTBDD, MTBDD, int); /** * Binary operation Divide (for MTBDDs of same type) - * Only for MTBDDs where all leaves are Double. + * Only for MTBDDs where all leaves are Integer or Double. * If either operand is mtbdd_false (not defined), * then the result is mtbdd_false (i.e. not defined). */ @@ -258,7 +258,7 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int); /** * Compute a - b */ -#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(minus)) +#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b)) /** * Compute a * b @@ -324,6 +324,12 @@ TASK_DECL_2(MTBDD, mtbdd_op_threshold_double, MTBDD, size_t) */ TASK_DECL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, size_t) +/** + * Monad that converts double to a Boolean MTBDD, translate terminals != 0 to 1 and to 0 otherwise; + */ +TASK_DECL_1(MTBDD, mtbdd_not_zero, MTBDD) +#define mtbdd_not_zero(dd) CALL(mtbdd_not_zero, dd) + /** * Convert double to a Boolean MTBDD, translate terminals >= value to 1 and to 0 otherwise; */ diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index 819882679..da6f7b66b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -14,7 +14,7 @@ * limitations under the License. */ -#include +#include "sylvan_obj.hpp" using namespace sylvan; @@ -899,6 +899,13 @@ Mtbdd::BddStrictThreshold(double value) const return mtbdd_strict_threshold_double(mtbdd, value); } +Bdd +Mtbdd::NotZero() const +{ + LACE_ME; + return mtbdd_not_zero(mtbdd); +} + Mtbdd Mtbdd::Support() const { diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index f0ee1add5..730e86261 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -20,8 +20,8 @@ #include #include -#include -#include +#include "lace.h" +#include "sylvan.h" namespace sylvan { @@ -587,6 +587,8 @@ public: * Same as MtbddStrictThreshold (Bdd = Boolean Mtbdd) */ Bdd BddStrictThreshold(double value) const; + + Bdd NotZero() const; /** * @brief Computes the support of a Mtbdd. diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp index baf1121e8..c86f9dca0 100644 --- a/src/adapters/AddExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -18,7 +18,11 @@ namespace storm { template storm::dd::Add AddExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { - return boost::any_cast>(expression.accept(*this)); + if (expression.hasBooleanType()) { + return boost::any_cast>(expression.accept(*this)).template toAdd(); + } else { + return boost::any_cast>(expression.accept(*this)); + } } template @@ -31,25 +35,25 @@ namespace storm { template boost::any AddExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) { - storm::dd::Bdd leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)).toBdd(); - storm::dd::Bdd rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)).toBdd(); + storm::dd::Bdd leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); + storm::dd::Bdd rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); - storm::dd::Add result; + storm::dd::Bdd result; switch (expression.getOperatorType()) { case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And: - result = (leftResult && rightResult).template toAdd(); + result = (leftResult && rightResult); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or: - result = (leftResult || rightResult).template toAdd(); + result = (leftResult || rightResult); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff: - result = (leftResult.iff(rightResult)).template toAdd(); + result = (leftResult.iff(rightResult)); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies: - result = (!leftResult || rightResult).template toAdd(); + result = (!leftResult || rightResult); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor: - result = (leftResult.exclusiveOr(rightResult)).template toAdd(); + result = (leftResult.exclusiveOr(rightResult)); break; } @@ -96,7 +100,7 @@ namespace storm { storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); - storm::dd::Add result; + storm::dd::Bdd result; switch (expression.getRelationType()) { case storm::expressions::BinaryRelationExpression::RelationType::Equal: result = leftResult.equals(rightResult); @@ -125,12 +129,16 @@ namespace storm { boost::any AddExpressionAdapter::visit(storm::expressions::VariableExpression const& expression) { auto const& variablePair = variableMapping.find(expression.getVariable()); STORM_LOG_THROW(variablePair != variableMapping.end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known."); - return ddManager->template getIdentity(variablePair->second); + if (expression.hasBooleanType()) { + return ddManager->template getIdentity(variablePair->second).toBdd(); + } else { + return ddManager->template getIdentity(variablePair->second); + } } template boost::any AddExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) { - storm::dd::Bdd result = boost::any_cast>(expression.getOperand()->accept(*this)).toBdd(); + storm::dd::Bdd result = boost::any_cast>(expression.getOperand()->accept(*this)); switch (expression.getOperatorType()) { case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: @@ -138,7 +146,7 @@ namespace storm { break; } - return result.template toAdd(); + return result; } template @@ -164,7 +172,7 @@ namespace storm { template boost::any AddExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression) { - return ddManager->getConstant(static_cast(expression.getValue())); + return expression.getValue() ? ddManager->getBddOne() : ddManager->getBddZero(); } template diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index fd6bbe3dd..2d4abe95f 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -118,7 +118,7 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); + storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd() * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); rowColumnMetaVariablePairs.push_back(variablePair); @@ -135,7 +135,7 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); - storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)); + storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd(); variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); rowColumnMetaVariablePairs.push_back(variablePair); @@ -159,7 +159,7 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); + storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd() * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); moduleIdentity *= variableIdentity; moduleRange *= manager->getRange(variablePair.first).template toAdd(); @@ -176,7 +176,7 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); - storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); + storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd() * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); moduleIdentity *= variableIdentity; moduleRange *= manager->getRange(variablePair.first).template toAdd(); @@ -334,7 +334,7 @@ namespace storm { storm::dd::Add result = updateExpression * guard; // Combine the variable and the assigned expression. - result = result.equals(writtenVariable); + result = result.equals(writtenVariable).template toAdd(); result *= guard; // Restrict the transitions to the range of the written variable. @@ -572,9 +572,9 @@ namespace storm { // Calculate number of required variables to encode the nondeterminism. uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); - storm::dd::Add equalsNumberOfChoicesDd = generationInfo.manager->template getAddZero(); + storm::dd::Bdd equalsNumberOfChoicesDd; std::vector> choiceDds(maxChoices, generationInfo.manager->template getAddZero()); - std::vector> remainingDds(maxChoices, generationInfo.manager->template getAddZero()); + std::vector> remainingDds(maxChoices, generationInfo.manager->getBddZero()); for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { // Determine the set of states with exactly currentChoices choices. @@ -594,7 +594,7 @@ namespace storm { for (std::size_t j = 0; j < commandDds.size(); ++j) { // Check if command guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices // choices such that one outgoing choice is given by the j-th command. - storm::dd::Add guardChoicesIntersection = commandDds[j].guardDd * equalsNumberOfChoicesDd; + storm::dd::Bdd guardChoicesIntersection = commandDds[j].guardDd.toBdd() && equalsNumberOfChoicesDd; // If there is no such state, continue with the next command. if (guardChoicesIntersection.isZero()) { @@ -604,19 +604,19 @@ namespace storm { // Split the currentChoices nondeterministic choices. for (uint_fast64_t k = 0; k < currentChoices; ++k) { // Calculate the overlapping part of command guard and the remaining DD. - storm::dd::Add remainingGuardChoicesIntersection = guardChoicesIntersection * remainingDds[k]; + storm::dd::Bdd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; // Check if we can add some overlapping parts to the current index. if (!remainingGuardChoicesIntersection.isZero()) { // Remove overlapping parts from the remaining DD. - remainingDds[k] = remainingDds[k] * !remainingGuardChoicesIntersection; + remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection; // Combine the overlapping part of the guard with command updates and add it to the resulting DD. - choiceDds[k] += remainingGuardChoicesIntersection * commandDds[j].transitionsDd; + choiceDds[k] += remainingGuardChoicesIntersection.template toAdd() * commandDds[j].transitionsDd; } // Remove overlapping parts from the command guard DD - guardChoicesIntersection = guardChoicesIntersection * !remainingGuardChoicesIntersection; + guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection; // If the guard DD has become equivalent to false, we can stop here. if (guardChoicesIntersection.isZero()) { @@ -631,7 +631,7 @@ namespace storm { } // Delete currentChoices out of overlapping DD - sumOfGuards = sumOfGuards * !equalsNumberOfChoicesDd; + sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); } return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables); diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index cfa44d86b..3d73aed35 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -123,7 +123,7 @@ namespace storm { storm::dd::Add Model::getRowColumnIdentity() const { storm::dd::Add result = this->getManager().template getAddOne(); for (auto const& pair : this->getRowColumnMetaVariablePairs()) { - result *= this->getManager().template getIdentity(pair.first).equals(this->getManager().template getIdentity(pair.second)); + result *= this->getManager().template getIdentity(pair.first).equals(this->getManager().template getIdentity(pair.second)).template toAdd(); result *= this->getManager().getRange(pair.first).template toAdd() * this->getManager().getRange(pair.second).template toAdd(); } return result; diff --git a/src/solver/SymbolicLinearEquationSolver.cpp b/src/solver/SymbolicLinearEquationSolver.cpp index 1638980d8..e9427f0a5 100644 --- a/src/solver/SymbolicLinearEquationSolver.cpp +++ b/src/solver/SymbolicLinearEquationSolver.cpp @@ -30,7 +30,7 @@ namespace storm { // Start by computing the Jacobi decomposition of the matrix A. storm::dd::Add diagonal = x.getDdManager()->template getAddOne(); for (auto const& pair : rowColumnMetaVariablePairs) { - diagonal *= x.getDdManager()->template getIdentity(pair.first).equals(x.getDdManager()->template getIdentity(pair.second)); + diagonal *= x.getDdManager()->template getIdentity(pair.first).equals(x.getDdManager()->template getIdentity(pair.second)).template toAdd(); diagonal *= x.getDdManager()->getRange(pair.first).template toAdd() * x.getDdManager()->getRange(pair.second).template toAdd(); } diagonal *= allRows.template toAdd(); diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 3f4841a99..1b48238e4 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -107,35 +107,35 @@ namespace storm { } template - Add Add::equals(Add const& other) const { - return Add(this->getDdManager(), internalAdd.equals(other), Dd::joinMetaVariables(*this, other)); + Bdd Add::equals(Add const& other) const { + return Bdd(this->getDdManager(), internalAdd.equals(other), Dd::joinMetaVariables(*this, other)); } template - Add Add::notEquals(Add const& other) const { - return Add(this->getDdManager(), internalAdd.notEquals(other), Dd::joinMetaVariables(*this, other)); + Bdd Add::notEquals(Add const& other) const { + return Bdd(this->getDdManager(), internalAdd.notEquals(other), Dd::joinMetaVariables(*this, other)); } template - Add Add::less(Add const& other) const { - return Add(this->getDdManager(), internalAdd.less(other), Dd::joinMetaVariables(*this, other)); + Bdd Add::less(Add const& other) const { + return Bdd(this->getDdManager(), internalAdd.less(other), Dd::joinMetaVariables(*this, other)); } template - Add Add::lessOrEqual(Add const& other) const { - return Add(this->getDdManager(), internalAdd.lessOrEqual(other), Dd::joinMetaVariables(*this, other)); + Bdd Add::lessOrEqual(Add const& other) const { + return Bdd(this->getDdManager(), internalAdd.lessOrEqual(other), Dd::joinMetaVariables(*this, other)); } template - Add Add::greater(Add const& other) const { - return Add(this->getDdManager(), internalAdd.greater(other), Dd::joinMetaVariables(*this, other)); + Bdd Add::greater(Add const& other) const { + return Bdd(this->getDdManager(), internalAdd.greater(other), Dd::joinMetaVariables(*this, other)); } template - Add Add::greaterOrEqual(Add const& other) const { - return Add(this->getDdManager(), internalAdd.greaterOrEqual(other), Dd::joinMetaVariables(*this, other)); + Bdd Add::greaterOrEqual(Add const& other) const { + return Bdd(this->getDdManager(), internalAdd.greaterOrEqual(other), Dd::joinMetaVariables(*this, other)); } @@ -266,7 +266,7 @@ namespace storm { template Bdd Add::notZero() const { - return this->toBdd(); + return Bdd(this->getDdManager(), internalAdd.notZero(), this->getContainedMetaVariables()); } template @@ -288,7 +288,6 @@ namespace storm { uint_fast64_t Add::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; if (LibraryType == DdType::CUDD) { - std::size_t numberOfDdVariables = 0; for (auto const& metaVariable : this->getContainedMetaVariables()) { numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); } @@ -775,7 +774,7 @@ namespace storm { template Bdd Add::toBdd() const { - return Bdd(this->getDdManager(), internalAdd.toBdd(), this->getContainedMetaVariables()); + return this->notZero(); } template diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index d4e3553b6..356336a1e 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -178,7 +178,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - Add equals(Add const& other) const; + Bdd equals(Add const& other) const; /*! * Retrieves the function that maps all evaluations to one that have distinct function values. @@ -186,7 +186,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - Add notEquals(Add const& other) const; + Bdd notEquals(Add const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less @@ -195,7 +195,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - Add less(Add const& other) const; + Bdd less(Add const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less or @@ -204,7 +204,7 @@ namespace storm { * @param other The DD with which to perform the operation. * @return The resulting function represented as an ADD. */ - Add lessOrEqual(Add const& other) const; + Bdd lessOrEqual(Add const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater @@ -213,7 +213,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - Add greater(Add const& other) const; + Bdd greater(Add const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater @@ -222,7 +222,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - Add greaterOrEqual(Add const& other) const; + Bdd greaterOrEqual(Add const& other) const; /*! * Retrieves the function that represents the current ADD to the power of the given ADD. diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 3a18d9b2f..7b344eae0 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -189,7 +189,6 @@ namespace storm { uint_fast64_t Bdd::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; if (LibraryType == DdType::CUDD) { - std::size_t numberOfDdVariables = 0; for (auto const& metaVariable : this->getContainedMetaVariables()) { numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); } diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 1a6a65ebc..83e317d97 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -93,33 +93,33 @@ namespace storm { } template - InternalAdd InternalAdd::equals(InternalAdd const& other) const { - return InternalAdd(ddManager, this->getCuddAdd().Equals(other.getCuddAdd())); + InternalBdd InternalAdd::equals(InternalAdd const& other) const { + return InternalBdd(ddManager, this->getCuddAdd().Equals(other.getCuddAdd()).BddPattern()); } template - InternalAdd InternalAdd::notEquals(InternalAdd const& other) const { - return InternalAdd(ddManager, this->getCuddAdd().NotEquals(other.getCuddAdd())); + InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { + return InternalBdd(ddManager, this->getCuddAdd().NotEquals(other.getCuddAdd()).BddPattern()); } template - InternalAdd InternalAdd::less(InternalAdd const& other) const { - return InternalAdd(ddManager, this->getCuddAdd().LessThan(other.getCuddAdd())); + InternalBdd InternalAdd::less(InternalAdd const& other) const { + return InternalBdd(ddManager, this->getCuddAdd().LessThan(other.getCuddAdd()).BddPattern()); } template - InternalAdd InternalAdd::lessOrEqual(InternalAdd const& other) const { - return InternalAdd(ddManager, this->getCuddAdd().LessThanOrEqual(other.getCuddAdd())); + InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + return InternalBdd(ddManager, this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()).BddPattern()); } template - InternalAdd InternalAdd::greater(InternalAdd const& other) const { - return InternalAdd(ddManager, this->getCuddAdd().GreaterThan(other.getCuddAdd())); + InternalBdd InternalAdd::greater(InternalAdd const& other) const { + return InternalBdd(ddManager, this->getCuddAdd().GreaterThan(other.getCuddAdd()).BddPattern()); } template - InternalAdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { - return InternalAdd(ddManager, this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd())); + InternalBdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { + return InternalBdd(ddManager, this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()).BddPattern()); } template @@ -226,7 +226,7 @@ namespace storm { template InternalBdd InternalAdd::notZero() const { - return this->toBdd(); + return InternalBdd(ddManager, this->getCuddAdd().BddPattern()); } template @@ -271,11 +271,6 @@ namespace storm { return static_cast(Cudd_V(constantMaxAdd.getNode())); } - template - InternalBdd InternalAdd::toBdd() const { - return InternalBdd(ddManager, this->getCuddAdd().BddPattern()); - } - template bool InternalAdd::isOne() const { return this->getCuddAdd().IsOne(); diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index 8cd8aa068..2d5b2110d 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -178,7 +178,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd equals(InternalAdd const& other) const; + InternalBdd equals(InternalAdd const& other) const; /*! * Retrieves the function that maps all evaluations to one that have distinct function values. @@ -186,7 +186,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd notEquals(InternalAdd const& other) const; + InternalBdd notEquals(InternalAdd const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less @@ -195,7 +195,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd less(InternalAdd const& other) const; + InternalBdd less(InternalAdd const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less or @@ -204,7 +204,7 @@ namespace storm { * @param other The DD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd lessOrEqual(InternalAdd const& other) const; + InternalBdd lessOrEqual(InternalAdd const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater @@ -213,7 +213,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd greater(InternalAdd const& other) const; + InternalBdd greater(InternalAdd const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater @@ -222,7 +222,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd greaterOrEqual(InternalAdd const& other) const; + InternalBdd greaterOrEqual(InternalAdd const& other) const; /*! * Retrieves the function that represents the current ADD to the power of the given ADD. @@ -439,14 +439,6 @@ namespace storm { */ ValueType getMax() const; - /*! - * Converts the ADD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as - * a call to notZero(). - * - * @return The corresponding BDD. - */ - InternalBdd toBdd() const; - /*! * Retrieves whether this ADD represents the constant one function. * diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index 0345be183..453445a5d 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -71,47 +71,48 @@ namespace storm { template InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { - this->sylvanMtbdd = this->sylvanMtbdd.Plus(other.sylvanMtbdd.Negate()); + this->sylvanMtbdd = this->sylvanMtbdd.Minus(other.sylvanMtbdd); return *this; } template InternalAdd InternalAdd::operator/(InternalAdd const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalAdd(ddManager, this->sylvanMtbdd.Divide(other.sylvanMtbdd)); } template InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + this->sylvanMtbdd = this->sylvanMtbdd.Divide(other.sylvanMtbdd); + return *this; } template - InternalAdd InternalAdd::equals(InternalAdd const& other) const { + InternalBdd InternalAdd::equals(InternalAdd const& other) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } template - InternalAdd InternalAdd::notEquals(InternalAdd const& other) const { + InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } template - InternalAdd InternalAdd::less(InternalAdd const& other) const { + InternalBdd InternalAdd::less(InternalAdd const& other) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } template - InternalAdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } template - InternalAdd InternalAdd::greater(InternalAdd const& other) const { + InternalBdd InternalAdd::greater(InternalAdd const& other) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } template - InternalAdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { + InternalBdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } @@ -206,7 +207,7 @@ namespace storm { template InternalBdd InternalAdd::notZero() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return InternalBdd(ddManager, this->sylvanMtbdd.NotZero()); } template @@ -249,11 +250,6 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } - template - InternalBdd InternalAdd::toBdd() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); - } - template bool InternalAdd::isOne() const { return *this == ddManager->getAddOne(); diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index 960ee1f01..39696ae9b 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -178,7 +178,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd equals(InternalAdd const& other) const; + InternalBdd equals(InternalAdd const& other) const; /*! * Retrieves the function that maps all evaluations to one that have distinct function values. @@ -186,7 +186,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd notEquals(InternalAdd const& other) const; + InternalBdd notEquals(InternalAdd const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less @@ -195,7 +195,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd less(InternalAdd const& other) const; + InternalBdd less(InternalAdd const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less or @@ -204,7 +204,7 @@ namespace storm { * @param other The DD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd lessOrEqual(InternalAdd const& other) const; + InternalBdd lessOrEqual(InternalAdd const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater @@ -213,7 +213,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd greater(InternalAdd const& other) const; + InternalBdd greater(InternalAdd const& other) const; /*! * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater @@ -222,7 +222,7 @@ namespace storm { * @param other The ADD with which to perform the operation. * @return The resulting function represented as an ADD. */ - InternalAdd greaterOrEqual(InternalAdd const& other) const; + InternalBdd greaterOrEqual(InternalAdd const& other) const; /*! * Retrieves the function that represents the current ADD to the power of the given ADD. @@ -438,15 +438,7 @@ namespace storm { * @return The highest function value of any encoding. */ ValueType getMax() const; - - /*! - * Converts the ADD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as - * a call to notZero(). - * - * @return The corresponding BDD. - */ - InternalBdd toBdd() const; - + /*! * Retrieves whether this ADD represents the constant one function. * diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 42326b0d0..106b52d43 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -145,26 +145,26 @@ TEST(CuddDd, OperatorTest) { dd1 = manager->template getIdentity(x.first); dd2 = manager->template getConstant(5); - dd3 = dd1.equals(dd2); + dd3 = dd1.equals(dd2).template toAdd(); EXPECT_EQ(1ul, dd3.getNonZeroCount()); - storm::dd::Add dd4 = dd1.notEquals(dd2); + storm::dd::Add dd4 = dd1.notEquals(dd2).template toAdd(); EXPECT_TRUE(dd4.toBdd() == !dd3.toBdd()); - dd3 = dd1.less(dd2); + dd3 = dd1.less(dd2).template toAdd(); EXPECT_EQ(11ul, dd3.getNonZeroCount()); - dd3 = dd1.lessOrEqual(dd2); + dd3 = dd1.lessOrEqual(dd2).template toAdd(); EXPECT_EQ(12ul, dd3.getNonZeroCount()); - dd3 = dd1.greater(dd2); + dd3 = dd1.greater(dd2).template toAdd(); EXPECT_EQ(4ul, dd3.getNonZeroCount()); - dd3 = dd1.greaterOrEqual(dd2); + dd3 = dd1.greaterOrEqual(dd2).template toAdd(); EXPECT_EQ(5ul, dd3.getNonZeroCount()); dd3 = (manager->getEncoding(x.first, 2).template toAdd()).ite(dd2, dd1); - dd4 = dd3.less(dd2); + dd4 = dd3.less(dd2).template toAdd(); EXPECT_EQ(10ul, dd4.getNonZeroCount()); dd4 = dd3.minimum(dd1); @@ -192,7 +192,7 @@ TEST(CuddDd, AbstractionTest) { dd1 = manager->template getIdentity(x.first); dd2 = manager->template getConstant(5); - dd3 = dd1.equals(dd2); + dd3 = dd1.equals(dd2).template toAdd(); storm::dd::Bdd dd3Bdd = dd3.toBdd(); EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount()); ASSERT_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); @@ -200,28 +200,28 @@ TEST(CuddDd, AbstractionTest) { EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount()); EXPECT_EQ(1, dd3Bdd.template toAdd().getMax()); - dd3 = dd1.equals(dd2); + dd3 = dd1.equals(dd2).template toAdd(); dd3 *= manager->template getConstant(3); EXPECT_EQ(1ul, dd3.getNonZeroCount()); ASSERT_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.first})); EXPECT_TRUE(dd3Bdd.isOne()); - dd3 = dd1.equals(dd2); + dd3 = dd1.equals(dd2).template toAdd(); dd3 *= manager->template getConstant(3); ASSERT_THROW(dd3 = dd3.sumAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3 = dd3.sumAbstract({x.first})); EXPECT_EQ(1ul, dd3.getNonZeroCount()); EXPECT_EQ(3, dd3.getMax()); - dd3 = dd1.equals(dd2); + dd3 = dd1.equals(dd2).template toAdd(); dd3 *= manager->template getConstant(3); ASSERT_THROW(dd3 = dd3.minAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3 = dd3.minAbstract({x.first})); EXPECT_EQ(0ul, dd3.getNonZeroCount()); EXPECT_EQ(0, dd3.getMax()); - dd3 = dd1.equals(dd2); + dd3 = dd1.equals(dd2).template toAdd(); dd3 *= manager->template getConstant(3); ASSERT_THROW(dd3 = dd3.maxAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3 = dd3.maxAbstract({x.first})); @@ -247,7 +247,7 @@ TEST(CuddDd, MultiplyMatrixTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Add dd1 = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)); + storm::dd::Add dd1 = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)).template toAdd(); storm::dd::Add dd2 = manager->getRange(x.second).template toAdd(); storm::dd::Add dd3; dd1 *= manager->template getConstant(2); @@ -336,7 +336,7 @@ TEST(CuddDd, AddOddTest) { } // Create a non-trivial matrix. - dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)) * manager->getRange(x.first).template toAdd(); + dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)).template toAdd() * manager->getRange(x.first).template toAdd(); dd += manager->getEncoding(x.first, 1).template toAdd() * manager->getRange(x.second).template toAdd() + manager->getEncoding(x.second, 1).template toAdd() * manager->getRange(x.first).template toAdd(); // Create the ODDs. @@ -382,7 +382,7 @@ TEST(CuddDd, BddOddTest) { storm::dd::Add vectorAdd = storm::dd::Add::fromVector(manager, ddAsVector, odd, {x.first}); // Create a non-trivial matrix. - dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)) * manager->getRange(x.first).template toAdd(); + dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)).template toAdd() * manager->getRange(x.first).template toAdd(); dd += manager->getEncoding(x.first, 1).template toAdd() * manager->getRange(x.second).template toAdd() + manager->getEncoding(x.second, 1).template toAdd() * manager->getRange(x.first).template toAdd(); // Create the ODDs. diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 4898dbc47..cd47c66a7 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -139,7 +139,7 @@ TEST(SylvanDd, OperatorTest) { // // dd1 = !dd3; // EXPECT_TRUE(dd1.isOne()); -// +// // dd3 = dd1 || dd2; // EXPECT_TRUE(dd3.isOne()); //