From 60701cebdb7eed4dca4889218347faa2bc486a1b Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 27 Mar 2015 22:48:04 +0100 Subject: [PATCH] ADDs and BDDs are no longer mixed in the abstraction layer. Former-commit-id: 3c31063ea631f496eae7112d2a442d049a86d2c1 --- ...onAdapter.cpp => AddExpressionAdapter.cpp} | 70 +- ...essionAdapter.h => AddExpressionAdapter.h} | 8 +- src/builder/DdPrismModelBuilder.cpp | 179 ++-- src/builder/DdPrismModelBuilder.h | 64 +- .../SymbolicPropositionalModelChecker.cpp | 2 +- .../SymbolicQualitativeCheckResult.cpp | 2 +- .../results/SymbolicQualitativeCheckResult.h | 8 +- .../SymbolicQuantitativeCheckResult.cpp | 2 +- .../results/SymbolicQuantitativeCheckResult.h | 8 +- src/models/symbolic/DeterministicModel.cpp | 14 +- src/models/symbolic/DeterministicModel.h | 14 +- src/models/symbolic/Dtmc.cpp | 14 +- src/models/symbolic/Dtmc.h | 14 +- src/models/symbolic/Mdp.cpp | 14 +- src/models/symbolic/Mdp.h | 14 +- src/models/symbolic/Model.cpp | 34 +- src/models/symbolic/Model.h | 50 +- src/models/symbolic/NondeterministicModel.cpp | 18 +- src/models/symbolic/NondeterministicModel.h | 18 +- src/storage/dd/CuddAdd.cpp | 852 +++++------------- src/storage/dd/CuddAdd.h | 556 ++++-------- src/storage/dd/CuddBdd.cpp | 140 +-- src/storage/dd/CuddBdd.h | 12 +- src/storage/dd/CuddDd.cpp | 14 + src/storage/dd/CuddDd.h | 9 +- src/storage/dd/CuddDdForwardIterator.h | 4 +- src/storage/dd/CuddDdManager.cpp | 69 +- src/storage/dd/CuddDdManager.h | 51 +- src/storage/dd/CuddDdMetaVariable.cpp | 15 +- src/storage/dd/CuddDdMetaVariable.h | 29 +- src/storage/dd/CuddOdd.cpp | 8 +- src/storage/dd/CuddOdd.h | 6 +- src/utility/graph.h | 155 ++-- test/functional/storage/CuddDdTest.cpp | 182 ++-- test/functional/utility/GraphTest.cpp | 4 +- 35 files changed, 941 insertions(+), 1712 deletions(-) rename src/adapters/{DdExpressionAdapter.cpp => AddExpressionAdapter.cpp} (60%) rename src/adapters/{DdExpressionAdapter.h => AddExpressionAdapter.h} (83%) diff --git a/src/adapters/DdExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp similarity index 60% rename from src/adapters/DdExpressionAdapter.cpp rename to src/adapters/AddExpressionAdapter.cpp index e33fb40b9..12677b85e 100644 --- a/src/adapters/DdExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -1,4 +1,4 @@ -#include "src/adapters/DdExpressionAdapter.h" +#include "src/adapters/AddExpressionAdapter.h" #include "src/utility/macros.h" #include "src/exceptions/ExpressionEvaluationException.h" @@ -9,44 +9,44 @@ namespace storm { namespace adapters { template - DdExpressionAdapter::DdExpressionAdapter(std::shared_ptr> ddManager, std::map const& variableMapping) : ddManager(ddManager), variableMapping(variableMapping) { + AddExpressionAdapter::AddExpressionAdapter(std::shared_ptr> ddManager, std::map const& variableMapping) : ddManager(ddManager), variableMapping(variableMapping) { // Intentionally left empty. } template - storm::dd::Dd DdExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { - return boost::any_cast>(expression.accept(*this)); + storm::dd::Add AddExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { + return boost::any_cast>(expression.accept(*this)); } template - boost::any DdExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression) { - storm::dd::Dd elseDd = boost::any_cast>(expression.getElseExpression()->accept(*this)); - storm::dd::Dd thenDd = boost::any_cast>(expression.getThenExpression()->accept(*this)); - storm::dd::Dd conditionDd = boost::any_cast>(expression.getCondition()->accept(*this)); + boost::any AddExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression) { + storm::dd::Add elseDd = boost::any_cast>(expression.getElseExpression()->accept(*this)); + storm::dd::Add thenDd = boost::any_cast>(expression.getThenExpression()->accept(*this)); + storm::dd::Add conditionDd = boost::any_cast>(expression.getCondition()->accept(*this)); return conditionDd.ite(thenDd, elseDd); } template - boost::any DdExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) { - storm::dd::Dd leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - storm::dd::Dd rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); + 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::Dd result; + storm::dd::Add result; switch (expression.getOperatorType()) { case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And: - result = leftResult && rightResult; + result = (leftResult && rightResult).toAdd(); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or: - result = leftResult || rightResult; + result = (leftResult || rightResult).toAdd(); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff: - result = leftResult.iff(rightResult); + result = (leftResult.iff(rightResult)).toAdd(); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies: - result = !leftResult || rightResult; + result = (!leftResult || rightResult).toAdd(); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor: - result = leftResult.exclusiveOr(rightResult); + result = (leftResult.exclusiveOr(rightResult)).toAdd(); break; } @@ -54,11 +54,11 @@ namespace storm { } template - boost::any DdExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) { - storm::dd::Dd leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - storm::dd::Dd rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); + boost::any AddExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) { + storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); + storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); - storm::dd::Dd result; + storm::dd::Add result; switch (expression.getOperatorType()) { case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus: result = leftResult + rightResult; @@ -86,11 +86,11 @@ namespace storm { } template - boost::any DdExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression) { - storm::dd::Dd leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - storm::dd::Dd rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); + boost::any AddExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression) { + storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); + storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); - storm::dd::Dd result; + storm::dd::Add result; switch (expression.getRelationType()) { case storm::expressions::BinaryRelationExpression::RelationType::Equal: result = leftResult.equals(rightResult); @@ -116,15 +116,15 @@ namespace storm { } template - boost::any DdExpressionAdapter::visit(storm::expressions::VariableExpression const& expression) { + 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->getIdentity(variablePair->second); } template - boost::any DdExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) { - storm::dd::Dd result = boost::any_cast>(expression.getOperand()->accept(*this)); + boost::any AddExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) { + storm::dd::Bdd result = boost::any_cast>(expression.getOperand()->accept(*this)).toBdd(); switch (expression.getOperatorType()) { case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: @@ -132,12 +132,12 @@ namespace storm { break; } - return result; + return result.toAdd(); } template - boost::any DdExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) { - storm::dd::Dd result = boost::any_cast>(expression.getOperand()->accept(*this)); + boost::any AddExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) { + storm::dd::Add result = boost::any_cast>(expression.getOperand()->accept(*this)); switch (expression.getOperatorType()) { case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: @@ -151,22 +151,22 @@ namespace storm { } template - boost::any DdExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression) { + boost::any AddExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression) { return ddManager->getConstant(expression.getValue()); } template - boost::any DdExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression) { + boost::any AddExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression) { return ddManager->getConstant(expression.getValue()); } template - boost::any DdExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { + boost::any AddExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { return ddManager->getConstant(expression.getValue()); } // Explicitly instantiate the symbolic expression adapter - template class DdExpressionAdapter; + template class AddExpressionAdapter; } // namespace adapters } // namespace storm diff --git a/src/adapters/DdExpressionAdapter.h b/src/adapters/AddExpressionAdapter.h similarity index 83% rename from src/adapters/DdExpressionAdapter.h rename to src/adapters/AddExpressionAdapter.h index cba1c422b..8225556f1 100644 --- a/src/adapters/DdExpressionAdapter.h +++ b/src/adapters/AddExpressionAdapter.h @@ -5,18 +5,18 @@ #include "src/storage/expressions/Expressions.h" #include "storage/expressions/ExpressionVisitor.h" -#include "src/storage/dd/Dd.h" +#include "src/storage/dd/Add.h" #include "src/storage/dd/DdManager.h" namespace storm { namespace adapters { template - class DdExpressionAdapter : public storm::expressions::ExpressionVisitor { + class AddExpressionAdapter : public storm::expressions::ExpressionVisitor { public: - DdExpressionAdapter(std::shared_ptr> ddManager, std::map const& variableMapping); + AddExpressionAdapter(std::shared_ptr> ddManager, std::map const& variableMapping); - storm::dd::Dd translateExpression(storm::expressions::Expression const& expression); + storm::dd::Add translateExpression(storm::expressions::Expression const& expression); virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression) override; virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) override; diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 74508e763..ec80e6dd6 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -52,8 +52,8 @@ namespace storm { } template - storm::dd::Dd DdPrismModelBuilder::createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Dd const& guard, storm::prism::Update const& update) { - storm::dd::Dd updateDd = generationInfo.manager->getOne(true); + storm::dd::Add DdPrismModelBuilder::createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Add const& guard, storm::prism::Update const& update) { + storm::dd::Add updateDd = generationInfo.manager->getAddOne(); STORM_LOG_TRACE("Translating update " << update); @@ -67,20 +67,20 @@ namespace storm { // Translate the written variable. auto const& primedMetaVariable = generationInfo.variableToColumnMetaVariableMap.at(assignment.getVariable()); - storm::dd::Dd writtenVariable = generationInfo.manager->getIdentity(primedMetaVariable); + storm::dd::Add writtenVariable = generationInfo.manager->getIdentity(primedMetaVariable); // Translate the expression that is being assigned. - storm::dd::Dd updateExpression = generationInfo.rowExpressionAdapter->translateExpression(assignment.getExpression()); + storm::dd::Add updateExpression = generationInfo.rowExpressionAdapter->translateExpression(assignment.getExpression()); // Combine the update expression with the guard. - storm::dd::Dd result = updateExpression * guard; + storm::dd::Add result = updateExpression * guard; // Combine the variable and the assigned expression. result = result.equals(writtenVariable); result *= guard; // Restrict the transitions to the range of the written variable. - result = result * generationInfo.manager->getRange(primedMetaVariable, true); + result = result * generationInfo.manager->getRange(primedMetaVariable).toAdd(); updateDd *= result; } @@ -129,17 +129,17 @@ namespace storm { template typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command) { STORM_LOG_TRACE("Translating guard " << command.getGuardExpression()); - storm::dd::Dd guardDd = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()) * generationInfo.moduleToRangeMap[module.getName()]; + storm::dd::Add guardDd = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()) * generationInfo.moduleToRangeMap[module.getName()]; STORM_LOG_WARN_COND(!guardDd.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable."); if (!guardDd.isZero()) { - storm::dd::Dd commandDd = generationInfo.manager->getZero(true); + storm::dd::Add commandDd = generationInfo.manager->getAddZero(); for (storm::prism::Update const& update : command.getUpdates()) { - storm::dd::Dd updateDd = createUpdateDecisionDiagram(generationInfo, module, guardDd, update); + storm::dd::Add updateDd = createUpdateDecisionDiagram(generationInfo, module, guardDd, update); STORM_LOG_WARN_COND(!updateDd.isZero(), "Update '" << update << "' does not have any effect."); - storm::dd::Dd probabilityDd = generationInfo.rowExpressionAdapter->translateExpression(update.getLikelihoodExpression()); + storm::dd::Add probabilityDd = generationInfo.rowExpressionAdapter->translateExpression(update.getLikelihoodExpression()); updateDd *= probabilityDd; commandDd += updateDd; @@ -186,9 +186,9 @@ namespace storm { template typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionDTMC(GenerationInformation& generationInfo, std::vector const& commandDds) { - storm::dd::Dd allGuards = generationInfo.manager->getZero(true); - storm::dd::Dd allCommands = generationInfo.manager->getZero(true); - storm::dd::Dd temporary; + storm::dd::Add allGuards = generationInfo.manager->getAddZero(); + storm::dd::Add allCommands = generationInfo.manager->getAddZero(); + storm::dd::Add temporary; for (auto const& commandDd : commandDds) { // Check for overlapping guards. @@ -203,8 +203,8 @@ namespace storm { } template - storm::dd::Dd DdPrismModelBuilder::encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value) { - storm::dd::Dd result = generationInfo.manager->getZero(true); + storm::dd::Add DdPrismModelBuilder::encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value) { + storm::dd::Add result = generationInfo.manager->getAddZero(); STORM_LOG_TRACE("Encoding " << value << " with " << numberOfBinaryVariables << " binary variable(s) starting from offset " << nondeterminismVariableOffset << "."); @@ -223,11 +223,11 @@ namespace storm { template typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector const& commandDds, uint_fast64_t nondeterminismVariableOffset) { - storm::dd::Dd allGuards = generationInfo.manager->getZero(true); - storm::dd::Dd allCommands = generationInfo.manager->getZero(true); + storm::dd::Add allGuards = generationInfo.manager->getAddZero(); + storm::dd::Add allCommands = generationInfo.manager->getAddZero(); // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. - storm::dd::Dd sumOfGuards = generationInfo.manager->getZero(true); + storm::dd::Add sumOfGuards = generationInfo.manager->getAddZero(); for (auto const& commandDd : commandDds) { sumOfGuards += commandDd.guardDd; allGuards = allGuards || commandDd.guardDd; @@ -242,17 +242,16 @@ namespace storm { } else if (maxChoices == 1) { // Sum up all commands. for (auto const& commandDd : commandDds) { - // FIXME: necessary to multiply with guard again? - allCommands += commandDd.guardDd * commandDd.transitionsDd; + allCommands += commandDd.transitionsDd; } return ActionDecisionDiagram(sumOfGuards, allCommands); } else { // Calculate number of required variables to encode the nondeterminism. uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); - storm::dd::Dd equalsNumberOfChoicesDd = generationInfo.manager->getZero(true); - std::vector> choiceDds(maxChoices, generationInfo.manager->getZero(true)); - std::vector> remainingDds(maxChoices, generationInfo.manager->getZero(true)); + storm::dd::Add equalsNumberOfChoicesDd = generationInfo.manager->getAddZero(); + std::vector> choiceDds(maxChoices, generationInfo.manager->getAddZero()); + std::vector> remainingDds(maxChoices, generationInfo.manager->getAddZero()); for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { // Determine the set of states with exactly currentChoices choices. @@ -265,14 +264,14 @@ namespace storm { // Reset the previously used intermediate storage. for (uint_fast64_t j = 0; j < currentChoices; ++j) { - choiceDds[j] = generationInfo.manager->getZero(true); + choiceDds[j] = generationInfo.manager->getAddZero(); remainingDds[j] = equalsNumberOfChoicesDd; } 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::Dd guardChoicesIntersection = commandDds[j].guardDd && equalsNumberOfChoicesDd; + storm::dd::Add guardChoicesIntersection = commandDds[j].guardDd * equalsNumberOfChoicesDd; // If there is no such state, continue with the next command. if (guardChoicesIntersection.isZero()) { @@ -282,19 +281,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::Dd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; + storm::dd::Add 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; } // 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()) { @@ -309,7 +308,7 @@ namespace storm { } // Delete currentChoices out of overlapping DD - sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd); + sumOfGuards = sumOfGuards * !equalsNumberOfChoicesDd; } return ActionDecisionDiagram(allGuards, allCommands, nondeterminismVariableOffset + numberOfBinaryVariables); @@ -322,9 +321,9 @@ namespace storm { } template - typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2, storm::dd::Dd const& identityDd1, storm::dd::Dd const& identityDd2) { - storm::dd::Dd action1Extended = action1.transitionsDd * identityDd2; - storm::dd::Dd action2Extended = action2.transitionsDd * identityDd1; + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2) { + storm::dd::Add action1Extended = action1.transitionsDd * identityDd2; + storm::dd::Add action2Extended = action2.transitionsDd * identityDd1; if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1Extended + action2Extended, 0); @@ -338,23 +337,23 @@ namespace storm { // Bring both choices to the same number of variables that encode the nondeterminism. uint_fast64_t numberOfUsedNondeterminismVariables = std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables); if (action1.numberOfUsedNondeterminismVariables > action2.numberOfUsedNondeterminismVariables) { - storm::dd::Dd nondeterminisimEncoding = generationInfo.manager->getOne(true); + storm::dd::Add nondeterminismEncoding = generationInfo.manager->getAddOne(); for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables; i < action1.numberOfUsedNondeterminismVariables; ++i) { - nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true); + nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).toAdd(); } - action2Extended *= nondeterminisimEncoding; + action2Extended *= nondeterminismEncoding; } else if (action2.numberOfUsedNondeterminismVariables > action1.numberOfUsedNondeterminismVariables) { - storm::dd::Dd nondeterminisimEncoding = generationInfo.manager->getOne(true); + storm::dd::Add nondeterminismEncoding = generationInfo.manager->getAddOne(); for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables; i < action2.numberOfUsedNondeterminismVariables; ++i) { - nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true); + nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).toAdd(); } - action1Extended *= nondeterminisimEncoding; + action1Extended *= nondeterminismEncoding; } // Add a new variable that resolves the nondeterminism between the two choices. - storm::dd::Dd combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1, true).ite(action2Extended, action1Extended); + storm::dd::Add combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).toAdd().ite(action2Extended, action1Extended); return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, numberOfUsedNondeterminismVariables + 1); } else { @@ -381,41 +380,41 @@ namespace storm { } template - storm::dd::Dd DdPrismModelBuilder::getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional const& synchronizationAction) { - storm::dd::Dd synchronization = generationInfo.manager->getOne(true); + storm::dd::Add DdPrismModelBuilder::getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional const& synchronizationAction) { + storm::dd::Add synchronization = generationInfo.manager->getAddOne(); for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { if (synchronizationAction && synchronizationAction.get() == i) { - synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1, true); + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1).toAdd(); } else { - synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0, true); + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0).toAdd(); } } return synchronization; } template - storm::dd::Dd DdPrismModelBuilder::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module) { + storm::dd::Add DdPrismModelBuilder::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module) { // If the model is an MDP, we need to encode the nondeterminism using additional variables. if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - storm::dd::Dd result = generationInfo.manager->getZero(true); + storm::dd::Add result = generationInfo.manager->getAddZero(); // First, determine the highest number of nondeterminism variables that is used in any action and make // all actions use the same amout of nondeterminism variables. uint_fast64_t numberOfUsedNondeterminismVariables = module.numberOfUsedNondeterminismVariables; // Add variables to independent action DD. - storm::dd::Dd nondeterminismEncoding = generationInfo.manager->getOne(true); + storm::dd::Add nondeterminismEncoding = generationInfo.manager->getAddOne(); for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) { - nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true); + nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).toAdd(); } result = module.independentAction.transitionsDd * nondeterminismEncoding; // Add variables to synchronized action DDs. - std::map> synchronizingActionToDdMap; + std::map> synchronizingActionToDdMap; for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { - nondeterminismEncoding = generationInfo.manager->getOne(true); + nondeterminismEncoding = generationInfo.manager->getAddOne(); for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) { - nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true); + nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).toAdd(); } synchronizingActionToDdMap.emplace(synchronizingAction.first, synchronizingAction.second.transitionsDd * nondeterminismEncoding); } @@ -435,7 +434,7 @@ namespace storm { return result; } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { // Simply add all actions. - storm::dd::Dd result = module.independentAction.transitionsDd; + storm::dd::Add result = module.independentAction.transitionsDd; for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { result += synchronizingAction.second.transitionsDd; } @@ -446,7 +445,7 @@ namespace storm { } template - std::pair, typename DdPrismModelBuilder::ModuleDecisionDiagram> DdPrismModelBuilder::createSystemDecisionDiagram(GenerationInformation& generationInfo) { + std::pair, typename DdPrismModelBuilder::ModuleDecisionDiagram> DdPrismModelBuilder::createSystemDecisionDiagram(GenerationInformation& generationInfo) { // Create the initial offset mapping. std::map synchronizingActionToOffsetMap; for (auto const& actionIndex : generationInfo.program.getActionIndices()) { @@ -501,7 +500,7 @@ namespace storm { system.numberOfUsedNondeterminismVariables = std::max(system.numberOfUsedNondeterminismVariables, numberOfUsedNondeterminismVariables); } - storm::dd::Dd result = createSystemFromModule(generationInfo, system); + storm::dd::Add result = createSystemFromModule(generationInfo, system); // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { @@ -519,12 +518,12 @@ namespace storm { } template - std::pair, storm::dd::Dd> DdPrismModelBuilder::createRewardDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Dd const& fullTransitionMatrix) { + std::pair, storm::dd::Add> DdPrismModelBuilder::createRewardDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& fullTransitionMatrix) { // Start by creating the state reward vector. - storm::dd::Dd stateRewards = generationInfo.manager->getZero(); + storm::dd::Add stateRewards = generationInfo.manager->getAddZero(); for (auto const& stateReward : rewardModel.getStateRewards()) { - storm::dd::Dd states = generationInfo.rowExpressionAdapter->translateExpression(stateReward.getStatePredicateExpression()); - storm::dd::Dd rewards = generationInfo.rowExpressionAdapter->translateExpression(stateReward.getRewardValueExpression()); + storm::dd::Add states = generationInfo.rowExpressionAdapter->translateExpression(stateReward.getStatePredicateExpression()); + storm::dd::Add rewards = generationInfo.rowExpressionAdapter->translateExpression(stateReward.getRewardValueExpression()); // Restrict the rewards to those states that satisfy the condition. rewards = states * rewards; @@ -538,13 +537,13 @@ namespace storm { } // Then build the transition reward matrix. - storm::dd::Dd transitionRewards = generationInfo.manager->getZero(); + storm::dd::Add transitionRewards = generationInfo.manager->getAddZero(); for (auto const& transitionReward : rewardModel.getTransitionRewards()) { - storm::dd::Dd states = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getStatePredicateExpression()); - storm::dd::Dd rewards = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getRewardValueExpression()); + storm::dd::Add states = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getStatePredicateExpression()); + storm::dd::Add rewards = generationInfo.rowExpressionAdapter->translateExpression(transitionReward.getRewardValueExpression()); - storm::dd::Dd synchronization; - storm::dd::Dd transitions; + storm::dd::Add synchronization; + storm::dd::Add transitions; if (transitionReward.isLabeled()) { synchronization = getSynchronizationDecisionDiagram(generationInfo, transitionReward.getActionIndex()); transitions = globalModule.synchronizingActionToDecisionDiagramMap.at(transitionReward.getActionIndex()).transitionsDd; @@ -553,9 +552,9 @@ namespace storm { transitions = globalModule.independentAction.transitionsDd; } - storm::dd::Dd transitionRewardDd = synchronization * states * rewards; + storm::dd::Add transitionRewardDd = synchronization * states * rewards; if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - transitionRewardDd += transitions.notZero() * transitionRewardDd; + transitionRewardDd += transitions.notZero().toAdd() * transitionRewardDd; } else { transitionRewardDd += transitions * transitionRewardDd; } @@ -608,15 +607,15 @@ namespace storm { // In particular, this creates the meta variables used to encode the model. GenerationInformation generationInfo(preparedProgram); - std::pair, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo); - storm::dd::Dd transitionMatrix = transitionMatrixModulePair.first; + std::pair, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo); + storm::dd::Add transitionMatrix = transitionMatrixModulePair.first; ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second; // Finally, we build the DDs for a reward structure, if requested. It is important to do this now, because // we still have the uncut transition matrix, which is needed for the reward computation. This is because // the reward computation might divide by the transition probabilities, which must therefore never be 0. // However, cutting it to the reachable fragment, there might be zero probability transitions. - boost::optional, storm::dd::Dd>> stateAndTransitionRewards; + boost::optional, storm::dd::Add>> stateAndTransitionRewards; if (options.buildRewards) { // If a specific reward model was selected or one with the empty name exists, select it. storm::prism::RewardModel rewardModel = storm::prism::RewardModel(); @@ -634,17 +633,17 @@ namespace storm { } // Cut the transition matrix to the reachable fragment of the state space. - storm::dd::Dd initialStates = createInitialStatesDecisionDiagram(generationInfo); - storm::dd::Dd reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrix); - transitionMatrix *= reachableStates.toMtbdd(); - - // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. - storm::dd::Dd statesWithTransition = transitionMatrix.notZero(); + storm::dd::Bdd initialStates = createInitialStatesDecisionDiagram(generationInfo); + storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); if (program.getModelType() == storm::prism::Program::ModelType::MDP) { - statesWithTransition = statesWithTransition.existsAbstract(generationInfo.allNondeterminismVariables); + transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables); } - statesWithTransition = statesWithTransition.existsAbstract(generationInfo.columnMetaVariables); - storm::dd::Dd deadlockStates = (reachableStates && !statesWithTransition).toMtbdd(); + storm::dd::Bdd reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd); + transitionMatrix *= reachableStates.toAdd(); + + // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. + storm::dd::Bdd statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables); + storm::dd::Add deadlockStates = (reachableStates && !statesWithTransition).toAdd(); if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. @@ -657,7 +656,7 @@ namespace storm { } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { // For MDPs, however, we need to select an action associated with the self-loop, if we do not // want to attach a lot of self-loops to the deadlock states. - storm::dd::Dd action = generationInfo.manager->getOne(true); + storm::dd::Add action = generationInfo.manager->getAddOne(); std::for_each(generationInfo.allNondeterminismVariables.begin(), generationInfo.allNondeterminismVariables.end(), [&action,&generationInfo] (storm::expressions::Variable const& metaVariable) { action *= !generationInfo.manager->getIdentity(metaVariable); } ); transitionMatrix += deadlockStates * globalModule.identity * action; } @@ -673,17 +672,17 @@ namespace storm { } if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { - return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, stateAndTransitionRewards ? stateAndTransitionRewards.get().first : boost::optional>(), stateAndTransitionRewards ? stateAndTransitionRewards.get().second : boost::optional>())); + return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, stateAndTransitionRewards ? stateAndTransitionRewards.get().first : boost::optional>(), stateAndTransitionRewards ? stateAndTransitionRewards.get().second : boost::optional>())); } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, stateAndTransitionRewards ? stateAndTransitionRewards.get().first : boost::optional>(), stateAndTransitionRewards ? stateAndTransitionRewards.get().second : boost::optional>())); + return std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, stateAndTransitionRewards ? stateAndTransitionRewards.get().first : boost::optional>(), stateAndTransitionRewards ? stateAndTransitionRewards.get().second : boost::optional>())); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); } } template - storm::dd::Dd DdPrismModelBuilder::createInitialStatesDecisionDiagram(GenerationInformation& generationInfo) { - storm::dd::Dd initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialConstruct().getInitialStatesExpression()).toBdd(); + storm::dd::Bdd DdPrismModelBuilder::createInitialStatesDecisionDiagram(GenerationInformation& generationInfo) { + storm::dd::Bdd initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialConstruct().getInitialStatesExpression()).toBdd(); for (auto const& metaVariable : generationInfo.rowMetaVariables) { initialStates &= generationInfo.manager->getRange(metaVariable); @@ -693,14 +692,8 @@ namespace storm { } template - storm::dd::Dd DdPrismModelBuilder::computeReachableStates(GenerationInformation& generationInfo, storm::dd::Dd const& initialStates, storm::dd::Dd const& transitions) { - storm::dd::Dd reachableStatesBdd = initialStates.toBdd(); - - // If the model is an MDP, we can abstract from the variables encoding the nondeterminism in the model. - storm::dd::Dd transitionBdd = transitions.notZero(); - if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { - transitionBdd = transitionBdd.existsAbstract(generationInfo.allNondeterminismVariables); - } + storm::dd::Bdd DdPrismModelBuilder::computeReachableStates(GenerationInformation& generationInfo, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionBdd) { + storm::dd::Bdd reachableStates = initialStates; // Perform the BFS to discover all reachable states. bool changed = true; @@ -708,21 +701,21 @@ namespace storm { do { STORM_LOG_TRACE("Iteration " << iteration << " of computing reachable states."); changed = false; - storm::dd::Dd tmp = reachableStatesBdd.andExists(transitionBdd, generationInfo.rowMetaVariables); + storm::dd::Bdd tmp = reachableStates.andExists(transitionBdd, generationInfo.rowMetaVariables); tmp = tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs); - storm::dd::Dd newReachableStates = tmp && (!reachableStatesBdd); + storm::dd::Bdd newReachableStates = tmp && (!reachableStates); // Check whether new states were indeed discovered. if (!newReachableStates.isZero()) { changed = true; } - reachableStatesBdd |= newReachableStates; + reachableStates |= newReachableStates; ++iteration; } while (changed); - return reachableStatesBdd; + return reachableStates; } // Explicitly instantiate the symbolic expression adapter diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index fb6e8c7ff..4f6d8f580 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -7,7 +7,7 @@ #include "src/models/symbolic/Model.h" #include "src/logic/Formulas.h" #include "src/storage/prism/Program.h" -#include "src/adapters/DdExpressionAdapter.h" +#include "src/adapters/AddExpressionAdapter.h" #include "src/utility/macros.h" namespace storm { @@ -71,11 +71,11 @@ namespace storm { // Intentionally left empty. } - ActionDecisionDiagram(storm::dd::DdManager const& manager, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getZero(true)), transitionsDd(manager.getZero(true)), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { + ActionDecisionDiagram(storm::dd::DdManager const& manager, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getAddZero()), transitionsDd(manager.getAddZero()), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { // Intentionally left empty. } - ActionDecisionDiagram(storm::dd::Dd guardDd, storm::dd::Dd transitionsDd, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(guardDd), transitionsDd(transitionsDd), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { + ActionDecisionDiagram(storm::dd::Add guardDd, storm::dd::Add transitionsDd, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(guardDd), transitionsDd(transitionsDd), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { // Intentionally left empty. } @@ -83,10 +83,10 @@ namespace storm { ActionDecisionDiagram& operator=(ActionDecisionDiagram const& other) = default; // The guard of the action. - storm::dd::Dd guardDd; + storm::dd::Add guardDd; // The actual transitions (source and target states). - storm::dd::Dd transitionsDd; + storm::dd::Add transitionsDd; // The number of variables that are used to encode the nondeterminism. uint_fast64_t numberOfUsedNondeterminismVariables; @@ -98,11 +98,11 @@ namespace storm { // Intentionally left empty. } - ModuleDecisionDiagram(storm::dd::DdManager const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero(true)), numberOfUsedNondeterminismVariables(0) { + ModuleDecisionDiagram(storm::dd::DdManager const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getAddZero()), numberOfUsedNondeterminismVariables(0) { // Intentionally left empty. } - ModuleDecisionDiagram(ActionDecisionDiagram const& independentAction, std::map const& synchronizingActionToDecisionDiagramMap, storm::dd::Dd const& identity, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : independentAction(independentAction), synchronizingActionToDecisionDiagramMap(synchronizingActionToDecisionDiagramMap), identity(identity), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { + ModuleDecisionDiagram(ActionDecisionDiagram const& independentAction, std::map const& synchronizingActionToDecisionDiagramMap, storm::dd::Add const& identity, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : independentAction(independentAction), synchronizingActionToDecisionDiagramMap(synchronizingActionToDecisionDiagramMap), identity(identity), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { // Intentionally left empty. } @@ -120,7 +120,7 @@ namespace storm { std::map synchronizingActionToDecisionDiagramMap; // A decision diagram that represents the identity of this module. - storm::dd::Dd identity; + storm::dd::Add identity; // The number of variables encoding the nondeterminism that were actually used. uint_fast64_t numberOfUsedNondeterminismVariables; @@ -135,8 +135,8 @@ namespace storm { // Initializes variables and identity DDs. createMetaVariablesAndIdentities(); - rowExpressionAdapter = std::shared_ptr>(new storm::adapters::DdExpressionAdapter(manager, variableToRowMetaVariableMap)); - columnExpressionAdapter = std::shared_ptr>(new storm::adapters::DdExpressionAdapter(manager, variableToColumnMetaVariableMap)); + rowExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToRowMetaVariableMap)); + columnExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToColumnMetaVariableMap)); } // The program that is currently translated. @@ -148,12 +148,12 @@ namespace storm { // The meta variables for the row encoding. std::set rowMetaVariables; std::map variableToRowMetaVariableMap; - std::shared_ptr> rowExpressionAdapter; + std::shared_ptr> rowExpressionAdapter; // The meta variables for the column encoding. std::set columnMetaVariables; std::map variableToColumnMetaVariableMap; - std::shared_ptr> columnExpressionAdapter; + std::shared_ptr> columnExpressionAdapter; // All pairs of row/column meta variables. std::vector> rowColumnMetaVariablePairs; @@ -169,13 +169,13 @@ namespace storm { std::set allNondeterminismVariables; // DDs representing the identity for each variable. - std::map> variableToIdentityMap; + std::map> variableToIdentityMap; // DDs representing the identity for each module. - std::map> moduleToIdentityMap; + std::map> moduleToIdentityMap; // DDs representing the valid ranges of the variables of each module. - std::map> moduleToRangeMap; + std::map> moduleToRangeMap; private: /*! @@ -212,7 +212,7 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first, true); + storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd(); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); rowColumnMetaVariablePairs.push_back(variablePair); } @@ -225,7 +225,7 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); - storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)); + storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)); variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); rowColumnMetaVariablePairs.push_back(variablePair); @@ -233,8 +233,8 @@ namespace storm { // Create meta variables for each of the modules' variables. for (storm::prism::Module const& module : program.getModules()) { - storm::dd::Dd moduleIdentity = manager->getOne(true); - storm::dd::Dd moduleRange = manager->getOne(true); + storm::dd::Add moduleIdentity = manager->getAddOne(); + storm::dd::Add moduleRange = manager->getAddOne(); for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); @@ -248,10 +248,10 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first, true) * manager->getRange(variablePair.second, true); + storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd() * manager->getRange(variablePair.second).toAdd(); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); moduleIdentity *= variableIdentity; - moduleRange *= manager->getRange(variablePair.first, true); + moduleRange *= manager->getRange(variablePair.first).toAdd(); rowColumnMetaVariablePairs.push_back(variablePair); } @@ -265,10 +265,10 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); - storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first, true) * manager->getRange(variablePair.second, true); + storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd() * manager->getRange(variablePair.second).toAdd(); variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); moduleIdentity *= variableIdentity; - moduleRange *= manager->getRange(variablePair.first, true); + moduleRange *= manager->getRange(variablePair.first).toAdd(); rowColumnMetaVariablePairs.push_back(variablePair); } @@ -280,9 +280,9 @@ namespace storm { private: - static storm::dd::Dd encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value); + static storm::dd::Add encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value); - static storm::dd::Dd createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Dd const& guard, storm::prism::Update const& update); + static storm::dd::Add createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Add const& guard, storm::prism::Update const& update); static ActionDecisionDiagram createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command); @@ -294,21 +294,21 @@ namespace storm { static ActionDecisionDiagram combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2); - static ActionDecisionDiagram combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2, storm::dd::Dd const& identityDd1, storm::dd::Dd const& identityDd2); + static ActionDecisionDiagram combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2, storm::dd::Add const& identityDd1, storm::dd::Add const& identityDd2); static ModuleDecisionDiagram createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map const& synchronizingActionToOffsetMap); - static storm::dd::Dd getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional const& synchronizationAction = boost::optional()); + static storm::dd::Add getSynchronizationDecisionDiagram(GenerationInformation& generationInfo, boost::optional const& synchronizationAction = boost::optional()); - static storm::dd::Dd createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); + static storm::dd::Add createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); - static std::pair, storm::dd::Dd> createRewardDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Dd const& fullTransitionMatrix); + static std::pair, storm::dd::Add> createRewardDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& fullTransitionMatrix); - static std::pair, ModuleDecisionDiagram> createSystemDecisionDiagram(GenerationInformation& generationInfo); + static std::pair, ModuleDecisionDiagram> createSystemDecisionDiagram(GenerationInformation& generationInfo); - static storm::dd::Dd createInitialStatesDecisionDiagram(GenerationInformation& generationInfo); + static storm::dd::Bdd createInitialStatesDecisionDiagram(GenerationInformation& generationInfo); - static storm::dd::Dd computeReachableStates(GenerationInformation& generationInfo, storm::dd::Dd const& initialStates, storm::dd::Dd const& transitions); + static storm::dd::Bdd computeReachableStates(GenerationInformation& generationInfo, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions); }; diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index 137c292b5..1552235d9 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -25,7 +25,7 @@ namespace storm { if (stateFormula.isTrueFormula()) { return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getReachableStates())); } else { - return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getManager().getZero())); + return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero())); } } diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp index 290da6884..766e2674f 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -6,7 +6,7 @@ namespace storm { namespace modelchecker { template - SymbolicQualitativeCheckResult::SymbolicQualitativeCheckResult(storm::dd::Dd const& allStates, storm::dd::Dd const& truthValues) : allStates(allStates), truthValues(truthValues) { + SymbolicQualitativeCheckResult::SymbolicQualitativeCheckResult(storm::dd::Bdd const& allStates, storm::dd::Bdd const& truthValues) : allStates(allStates), truthValues(truthValues) { // Intentionally left empty. } diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/modelchecker/results/SymbolicQualitativeCheckResult.h index 83c49ab98..e0c70ead3 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -2,7 +2,7 @@ #define STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ #include "src/storage/dd/DdType.h" -#include "src/storage/dd/Dd.h" +#include "src/storage/dd/CuddBdd.h" #include "src/modelchecker/results/QualitativeCheckResult.h" #include "src/utility/OsDetection.h" @@ -12,7 +12,7 @@ namespace storm { class SymbolicQualitativeCheckResult : public QualitativeCheckResult { public: SymbolicQualitativeCheckResult() = default; - SymbolicQualitativeCheckResult(storm::dd::Dd const& allStates, storm::dd::Dd const& truthValues); + SymbolicQualitativeCheckResult(storm::dd::Bdd const& allStates, storm::dd::Bdd const& truthValues); SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult const& other) = default; SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult const& other) = default; @@ -38,10 +38,10 @@ namespace storm { private: // The set of all states. - storm::dd::Dd allStates; + storm::dd::Bdd allStates; // The values of the qualitative check result. - storm::dd::Dd truthValues; + storm::dd::Bdd truthValues; }; } } diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index b78df481d..50d7d0ac7 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -7,7 +7,7 @@ namespace storm { namespace modelchecker { template - SymbolicQuantitativeCheckResult::SymbolicQuantitativeCheckResult(storm::dd::Dd const& allStates, storm::dd::Dd const& values) : allStates(allStates), values(values) { + SymbolicQuantitativeCheckResult::SymbolicQuantitativeCheckResult(storm::dd::Add const& allStates, storm::dd::Add const& values) : allStates(allStates), values(values) { // Intentionally left empty. } diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h index 0b1e331f4..28490aed2 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -2,7 +2,7 @@ #define STORM_MODELCHECKER_SYMBOLICQUANTITATIVECHECKRESULT_H_ #include "src/storage/dd/DdType.h" -#include "src/storage/dd/Dd.h" +#include "src/storage/dd/CuddAdd.h" #include "src/modelchecker/results/QuantitativeCheckResult.h" #include "src/utility/OsDetection.h" @@ -12,7 +12,7 @@ namespace storm { class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult { public: SymbolicQuantitativeCheckResult() = default; - SymbolicQuantitativeCheckResult(storm::dd::Dd const& allStates, storm::dd::Dd const& values); + SymbolicQuantitativeCheckResult(storm::dd::Add const& allStates, storm::dd::Add const& values); SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult const& other) = default; SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult const& other) = default; @@ -36,10 +36,10 @@ namespace storm { private: // The set of all states. - storm::dd::Dd allStates; + storm::dd::Add allStates; // The values of the quantitative check result. - storm::dd::Dd values; + storm::dd::Add values; }; } } diff --git a/src/models/symbolic/DeterministicModel.cpp b/src/models/symbolic/DeterministicModel.cpp index 64aca24ab..57cf7af60 100644 --- a/src/models/symbolic/DeterministicModel.cpp +++ b/src/models/symbolic/DeterministicModel.cpp @@ -7,17 +7,17 @@ namespace storm { template DeterministicModel::DeterministicModel(storm::models::ModelType const& modelType, std::shared_ptr> manager, - storm::dd::Dd reachableStates, - storm::dd::Dd initialStates, - storm::dd::Dd transitionMatrix, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, - boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix) + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) : Model(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix) { // Intentionally left empty. } diff --git a/src/models/symbolic/DeterministicModel.h b/src/models/symbolic/DeterministicModel.h index 274d2818a..84d6116c8 100644 --- a/src/models/symbolic/DeterministicModel.h +++ b/src/models/symbolic/DeterministicModel.h @@ -43,17 +43,17 @@ namespace storm { */ DeterministicModel(storm::models::ModelType const& modelType, std::shared_ptr> manager, - storm::dd::Dd reachableStates, - storm::dd::Dd initialStates, - storm::dd::Dd transitionMatrix, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), - boost::optional> const& optionalStateRewardVector = boost::optional>(), - boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); }; } // namespace symbolic diff --git a/src/models/symbolic/Dtmc.cpp b/src/models/symbolic/Dtmc.cpp index 5c28f063f..c11b94850 100644 --- a/src/models/symbolic/Dtmc.cpp +++ b/src/models/symbolic/Dtmc.cpp @@ -6,17 +6,17 @@ namespace storm { template Dtmc::Dtmc(std::shared_ptr> manager, - storm::dd::Dd reachableStates, - storm::dd::Dd initialStates, - storm::dd::Dd transitionMatrix, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, - boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix) + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) : DeterministicModel(storm::models::ModelType::Dtmc, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix) { // Intentionally left empty. } diff --git a/src/models/symbolic/Dtmc.h b/src/models/symbolic/Dtmc.h index b9c12e86e..47f7a9db4 100644 --- a/src/models/symbolic/Dtmc.h +++ b/src/models/symbolic/Dtmc.h @@ -41,17 +41,17 @@ namespace storm { * @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. */ Dtmc(std::shared_ptr> manager, - storm::dd::Dd reachableStates, - storm::dd::Dd initialStates, - storm::dd::Dd transitionMatrix, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), - boost::optional> const& optionalStateRewardVector = boost::optional>(), - boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); }; } // namespace symbolic diff --git a/src/models/symbolic/Mdp.cpp b/src/models/symbolic/Mdp.cpp index 36462c072..6084e2965 100644 --- a/src/models/symbolic/Mdp.cpp +++ b/src/models/symbolic/Mdp.cpp @@ -6,18 +6,18 @@ namespace storm { template Mdp::Mdp(std::shared_ptr> manager, - storm::dd::Dd reachableStates, - storm::dd::Dd initialStates, - storm::dd::Dd transitionMatrix, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::set const& nondeterminismVariables, std::map labelToExpressionMap, - boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix) + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) : NondeterministicModel(storm::models::ModelType::Mdp, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix) { // Intentionally left empty. } diff --git a/src/models/symbolic/Mdp.h b/src/models/symbolic/Mdp.h index 587bdfac7..e8c0aead2 100644 --- a/src/models/symbolic/Mdp.h +++ b/src/models/symbolic/Mdp.h @@ -43,18 +43,18 @@ namespace storm { * @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model. */ Mdp(std::shared_ptr> manager, - storm::dd::Dd reachableStates, - storm::dd::Dd initialStates, - storm::dd::Dd transitionMatrix, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::set const& nondeterminismVariables, std::map labelToExpressionMap = std::map(), - boost::optional> const& optionalStateRewardVector = boost::optional>(), - boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); }; diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 6778d8eb0..fc7f1aad6 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -6,17 +6,17 @@ namespace storm { template Model::Model(storm::models::ModelType const& modelType, std::shared_ptr> manager, - storm::dd::Dd reachableStates, - storm::dd::Dd initialStates, - storm::dd::Dd transitionMatrix, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, - boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix) + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) : ModelBase(modelType), manager(manager), reachableStates(reachableStates), initialStates(initialStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(rowExpressionAdapter), columnVariables(columnVariables), columnExpressionAdapter(columnExpressionAdapter), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToExpressionMap(labelToExpressionMap), stateRewardVector(optionalStateRewardVector), transitionRewardMatrix(optionalTransitionRewardMatrix) { // Intentionally left empty. } @@ -42,23 +42,23 @@ namespace storm { } template - storm::dd::Dd const& Model::getReachableStates() const { + storm::dd::Bdd const& Model::getReachableStates() const { return reachableStates; } template - storm::dd::Dd const& Model::getInitialStates() const { + storm::dd::Bdd const& Model::getInitialStates() const { return initialStates; } template - storm::dd::Dd Model::getStates(std::string const& label) const { + storm::dd::Bdd Model::getStates(std::string const& label) const { STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model."); return rowExpressionAdapter->translateExpression(labelToExpressionMap.at(label)).toBdd() && this->reachableStates; } template - storm::dd::Dd Model::getStates(storm::expressions::Expression const& expression) const { + storm::dd::Bdd Model::getStates(storm::expressions::Expression const& expression) const { return rowExpressionAdapter->translateExpression(expression).toBdd() && this->reachableStates; } @@ -68,27 +68,27 @@ namespace storm { } template - storm::dd::Dd const& Model::getTransitionMatrix() const { + storm::dd::Add const& Model::getTransitionMatrix() const { return transitionMatrix; } template - storm::dd::Dd& Model::getTransitionMatrix() { + storm::dd::Add& Model::getTransitionMatrix() { return transitionMatrix; } template - storm::dd::Dd const& Model::getTransitionRewardMatrix() const { + storm::dd::Add const& Model::getTransitionRewardMatrix() const { return transitionRewardMatrix.get(); } template - storm::dd::Dd& Model::getTransitionRewardMatrix() { + storm::dd::Add& Model::getTransitionRewardMatrix() { return transitionRewardMatrix.get(); } template - storm::dd::Dd const& Model::getStateRewardVector() const { + storm::dd::Add const& Model::getStateRewardVector() const { return stateRewardVector.get(); } @@ -123,7 +123,7 @@ namespace storm { } template - void Model::setTransitionMatrix(storm::dd::Dd const& transitionMatrix) { + void Model::setTransitionMatrix(storm::dd::Add const& transitionMatrix) { this->transitionMatrix = transitionMatrix; } diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index 52dee50cb..d9bf5eb02 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -7,7 +7,7 @@ #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Variable.h" -#include "src/adapters/DdExpressionAdapter.h" +#include "src/adapters/AddExpressionAdapter.h" #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdManager.h" #include "src/models/ModelBase.h" @@ -52,17 +52,17 @@ namespace storm { */ Model(storm::models::ModelType const& modelType, std::shared_ptr> manager, - storm::dd::Dd reachableStates, - storm::dd::Dd initialStates, - storm::dd::Dd transitionMatrix, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), - boost::optional> const& optionalStateRewardVector = boost::optional>(), - boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); virtual uint_fast64_t getNumberOfStates() const override; @@ -87,14 +87,14 @@ namespace storm { * * @return The reachble states of the model. */ - storm::dd::Dd const& getReachableStates() const; + storm::dd::Bdd const& getReachableStates() const; /*! * Retrieves the initial states of the model. * * @return The initial states of the model. */ - storm::dd::Dd const& getInitialStates() const; + storm::dd::Bdd const& getInitialStates() const; /*! * Returns the sets of states labeled with the given label. @@ -102,7 +102,7 @@ namespace storm { * @param label The label for which to get the labeled states. * @return The set of states labeled with the requested label in the form of a bit vector. */ - storm::dd::Dd getStates(std::string const& label) const; + storm::dd::Bdd getStates(std::string const& label) const; /*! * Returns the set of states labeled satisfying the given expression (that must be of boolean type). @@ -110,7 +110,7 @@ namespace storm { * @param expression The expression that needs to hold in the states. * @return The set of states labeled satisfying the given expression. */ - storm::dd::Dd getStates(storm::expressions::Expression const& expression) const; + storm::dd::Bdd getStates(storm::expressions::Expression const& expression) const; /*! * Retrieves whether the given label is a valid label in this model. @@ -125,14 +125,14 @@ namespace storm { * * @return A matrix representing the transitions of the model. */ - storm::dd::Dd const& getTransitionMatrix() const; + storm::dd::Add const& getTransitionMatrix() const; /*! * Retrieves the matrix representing the transitions of the model. * * @return A matrix representing the transitions of the model. */ - storm::dd::Dd& getTransitionMatrix(); + storm::dd::Add& getTransitionMatrix(); /*! * Retrieves the matrix representing the transition rewards of the model. Note that calling this method @@ -140,7 +140,7 @@ namespace storm { * * @return The matrix representing the transition rewards of the model. */ - storm::dd::Dd const& getTransitionRewardMatrix() const; + storm::dd::Add const& getTransitionRewardMatrix() const; /*! * Retrieves the matrix representing the transition rewards of the model. Note that calling this method @@ -148,7 +148,7 @@ namespace storm { * * @return The matrix representing the transition rewards of the model. */ - storm::dd::Dd& getTransitionRewardMatrix(); + storm::dd::Add& getTransitionRewardMatrix(); /*! * Retrieves a vector representing the state rewards of the model. Note that calling this method is only @@ -156,7 +156,7 @@ namespace storm { * * @return A vector representing the state rewards of the model. */ - storm::dd::Dd const& getStateRewardVector() const; + storm::dd::Add const& getStateRewardVector() const; /*! * Retrieves whether this model has state rewards. @@ -206,7 +206,7 @@ namespace storm { * * @param transitionMatrix The new transition matrix of the model. */ - void setTransitionMatrix(storm::dd::Dd const& transitionMatrix); + void setTransitionMatrix(storm::dd::Add const& transitionMatrix); /*! * Retrieves the mapping of labels to their defining expressions. @@ -220,25 +220,25 @@ namespace storm { std::shared_ptr> manager; // A vector representing the reachable states of the model. - storm::dd::Dd reachableStates; + storm::dd::Bdd reachableStates; // A vector representing the initial states of the model. - storm::dd::Dd initialStates; + storm::dd::Bdd initialStates; // A matrix representing transition relation. - storm::dd::Dd transitionMatrix; + storm::dd::Add transitionMatrix; // The meta variables used to encode the rows of the transition matrix. std::set rowVariables; // An adapter that can translate expressions to DDs over the row meta variables. - std::shared_ptr> rowExpressionAdapter; + std::shared_ptr> rowExpressionAdapter; // The meta variables used to encode the columns of the transition matrix. std::set columnVariables; // An adapter that can translate expressions to DDs over the column meta variables. - std::shared_ptr> columnExpressionAdapter; + std::shared_ptr> columnExpressionAdapter; // A vector holding all pairs of row and column meta variable pairs. This is used to swap the variables // in the DDs from row to column variables and vice versa. @@ -248,10 +248,10 @@ namespace storm { std::map labelToExpressionMap; // If set, a vector representing the rewards of the states. - boost::optional> stateRewardVector; + boost::optional> stateRewardVector; // If set, a matrix representing the rewards of transitions. - boost::optional> transitionRewardMatrix; + boost::optional> transitionRewardMatrix; }; } // namespace symbolic diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp index 59a8381e5..5572c3fe2 100644 --- a/src/models/symbolic/NondeterministicModel.cpp +++ b/src/models/symbolic/NondeterministicModel.cpp @@ -7,18 +7,18 @@ namespace storm { template NondeterministicModel::NondeterministicModel(storm::models::ModelType const& modelType, std::shared_ptr> manager, - storm::dd::Dd reachableStates, - storm::dd::Dd initialStates, - storm::dd::Dd transitionMatrix, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::set const& nondeterminismVariables, std::map labelToExpressionMap, - boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix) + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) : Model(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix), nondeterminismVariables(nondeterminismVariables) { // Prepare the mask of illegal nondeterministic choices. @@ -31,7 +31,7 @@ namespace storm { std::set rowAndNondeterminsmVariables; std::set_union(this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), this->getRowVariables().begin(), this->getRowVariables().end(), std::inserter(rowAndNondeterminsmVariables, rowAndNondeterminsmVariables.begin())); - storm::dd::Dd tmp = this->getTransitionMatrix().notZero().existsAbstract(this->getColumnVariables()).toMtbdd().sumAbstract(rowAndNondeterminsmVariables); + storm::dd::Add tmp = this->getTransitionMatrix().notZero().existsAbstract(this->getColumnVariables()).toAdd().sumAbstract(rowAndNondeterminsmVariables); return static_cast(tmp.getValue()); } @@ -41,7 +41,7 @@ namespace storm { } template - storm::dd::Dd const& NondeterministicModel::getIllegalMask() const { + storm::dd::Bdd const& NondeterministicModel::getIllegalMask() const { return illegalMask; } diff --git a/src/models/symbolic/NondeterministicModel.h b/src/models/symbolic/NondeterministicModel.h index 1e6d36cd6..16be5ce99 100644 --- a/src/models/symbolic/NondeterministicModel.h +++ b/src/models/symbolic/NondeterministicModel.h @@ -44,18 +44,18 @@ namespace storm { */ NondeterministicModel(storm::models::ModelType const& modelType, std::shared_ptr> manager, - storm::dd::Dd reachableStates, - storm::dd::Dd initialStates, - storm::dd::Dd transitionMatrix, + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::set const& nondeterminismVariables, std::map labelToExpressionMap = std::map(), - boost::optional> const& optionalStateRewardVector = boost::optional>(), - boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); + boost::optional> const& optionalStateRewardVector = boost::optional>(), + boost::optional> const& optionalTransitionRewardMatrix = boost::optional>()); /*! * Retrieves the number of nondeterministic choices in the model. @@ -76,7 +76,7 @@ namespace storm { * * @return A BDD characterizing all illegal nondeterminism encodings in the model. */ - storm::dd::Dd const& getIllegalMask() const; + storm::dd::Bdd const& getIllegalMask() const; virtual void printModelInformationToStream(std::ostream& out) const override; @@ -86,7 +86,7 @@ namespace storm { std::set nondeterminismVariables; // A mask that characterizes all legal nondeterministic choices. - storm::dd::Dd illegalMask; + storm::dd::Bdd illegalMask; }; } // namespace symbolic diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp index 31476bc8e..cc04c5f76 100644 --- a/src/storage/dd/CuddAdd.cpp +++ b/src/storage/dd/CuddAdd.cpp @@ -1,7 +1,8 @@ #include #include -#include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" #include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/CuddDdManager.h" #include "src/utility/vector.h" @@ -13,329 +14,156 @@ namespace storm { namespace dd { - Dd::Dd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) { + Add::Add(std::shared_ptr const> ddManager, ADD cuddAdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), cuddAdd(cuddAdd) { // Intentionally left empty. } - Dd::Dd(std::shared_ptr const> ddManager, ADD cuddDd, std::set const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) { - // Intentionally left empty. - } - - bool Dd::isBdd() const { - return this->cuddDd.which() == 0; + Bdd Add::toBdd() const { + return Bdd(this->getDdManager(), this->getCuddAdd().BddPattern(), this->getContainedMetaVariables()); } - bool Dd::isMtbdd() const { - return this->cuddDd.which() == 1; - } - - Dd Dd::toBdd() const { - if (this->isBdd()) { - return *this; - } else { - return Dd(this->getDdManager(), this->getCuddMtbdd().BddPattern(), this->containedMetaVariables); - } + ADD Add::getCuddAdd() const { + return this->cuddAdd; } - Dd Dd::toMtbdd() const { - if (this->isMtbdd()) { - return *this; - } else { - return Dd(this->getDdManager(), this->getCuddBdd().Add(), this->containedMetaVariables); - } + DdNode* Add::getCuddDdNode() const { + return this->getCuddAdd().getNode(); } - BDD Dd::getCuddBdd() const { - if (this->isBdd()) { - return boost::get(this->cuddDd); - } else { - STORM_LOG_WARN_COND(false, "Implicitly converting MTBDD to BDD."); - return this->getCuddMtbdd().BddPattern(); - } + bool Add::operator==(Add const& other) const { + return this->getCuddAdd() == other.getCuddAdd(); } - ADD Dd::getCuddMtbdd() const { - if (this->isMtbdd()) { - return boost::get(this->cuddDd); - } else { - STORM_LOG_WARN_COND(false, "Implicitly converting BDD to MTBDD."); - return this->getCuddBdd().Add(); - } - } - - ABDD const& Dd::getCuddDd() const { - if (this->isBdd()) { - return static_cast(boost::get(this->cuddDd)); - } else { - return static_cast(boost::get(this->cuddDd)); - } - } - - DdNode* Dd::getCuddDdNode() const { - if (this->isBdd()) { - return this->getCuddBdd().getNode(); - } else { - return this->getCuddMtbdd().getNode(); - } - } - - bool Dd::operator==(Dd const& other) const { - if (this->isBdd()) { - if (other.isBdd()) { - return this->getCuddBdd() == other.getCuddBdd(); - } else { - return false; - } - } else { - if (other.isMtbdd()) { - return this->getCuddMtbdd() == other.getCuddMtbdd(); - } else { - return false; - } - } - } - - bool Dd::operator!=(Dd const& other) const { + bool Add::operator!=(Add const& other) const { return !(*this == other); } - Dd Dd::ite(Dd const& thenDd, Dd const& elseDd) const { - std::set metaVariableNames(this->getContainedMetaVariables()); - metaVariableNames.insert(thenDd.getContainedMetaVariables().begin(), thenDd.getContainedMetaVariables().end()); - metaVariableNames.insert(elseDd.getContainedMetaVariables().begin(), elseDd.getContainedMetaVariables().end()); + Add Add::ite(Add const& thenDd, Add const& elseDd) const { + std::set metaVariableNames; + std::set_union(thenDd.getContainedMetaVariables().begin(), thenDd.getContainedMetaVariables().end(), elseDd.getContainedMetaVariables().begin(), elseDd.getContainedMetaVariables().end(), std::inserter(metaVariableNames, metaVariableNames.begin())); + metaVariableNames.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end()); - // If all involved DDs are BDDs, the result is also going to be a BDD. - if (this->isBdd() && thenDd.isBdd() && elseDd.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames); - } else { - return Dd(this->getDdManager(), this->toMtbdd().getCuddMtbdd().Ite(thenDd.toMtbdd().getCuddMtbdd(), elseDd.toMtbdd().getCuddMtbdd()), metaVariableNames); - } + return Add(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()), metaVariableNames); } - Dd Dd::operator+(Dd const& other) const { - Dd result(*this); - result += other; - return result; - } - - Dd& Dd::operator+=(Dd const& other) { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing addition on BDDs."); - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - this->cuddDd = this->getCuddMtbdd() + other.getCuddMtbdd(); - return *this; + Add Add::operator!() const { + return Add(this->getDdManager(), ~this->getCuddAdd(), this->getContainedMetaVariables()); } - Dd Dd::operator*(Dd const& other) const { - Dd result(*this); - result *= other; + Add Add::operator||(Add const& other) const { + Add result(*this); + result |= other; return result; } - Dd& Dd::operator*=(Dd const& other) { - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - if (this->isMtbdd() && other.isMtbdd()) { - this->cuddDd = this->getCuddMtbdd() * other.getCuddMtbdd(); - } else if (this->isBdd() && other.isBdd()) { - this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); - } else { - STORM_LOG_WARN_COND(false, "Performing multiplication on two DDs of different type."); - this->cuddDd = this->getCuddMtbdd() * other.getCuddMtbdd(); - } + Add& Add::operator|=(Add const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + this->cuddAdd = this->getCuddAdd() | other.getCuddAdd(); return *this; } - Dd Dd::operator-(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - Dd result(*this); - result -= other; + Add Add::operator+(Add const& other) const { + Add result(*this); + result += other; return result; } - Dd Dd::operator-() const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - return this->getDdManager()->getZero(true) - *this; - } - - Dd& Dd::operator-=(Dd const& other) { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - this->cuddDd = this->getCuddMtbdd() - other.getCuddMtbdd(); - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + Add& Add::operator+=(Add const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + this->cuddAdd = this->getCuddAdd() + other.getCuddAdd(); return *this; } - Dd Dd::operator/(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - Dd result(*this); - result /= other; + Add Add::operator*(Add const& other) const { + Add result(*this); + result *= other; return result; } - Dd& Dd::operator/=(Dd const& other) { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - this->cuddDd = this->getCuddMtbdd().Divide(other.getCuddMtbdd()); - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + Add& Add::operator*=(Add const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + this->cuddAdd = this->getCuddAdd() * other.getCuddAdd(); return *this; } - Dd Dd::operator!() const { - Dd result(*this); - result.complement(); + Add Add::operator-(Add const& other) const { + Add result(*this); + result -= other; return result; } - Dd& Dd::complement() { - if (this->isBdd()) { - this->cuddDd = ~this->getCuddBdd(); - } else { - this->cuddDd = ~this->getCuddMtbdd(); - } - return *this; + Add Add::operator-() const { + return this->getDdManager()->getAddZero() - *this; } - Dd Dd::operator&&(Dd const& other) const { - Dd result(*this); - result &= other; - return result; - } - - Dd& Dd::operator&=(Dd const& other) { - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - if (this->isBdd() && other.isBdd()) { - this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); - } else if (this->isMtbdd() && other.isMtbdd()) { - // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that - // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. - this->cuddDd = this->getCuddMtbdd() & other.getCuddMtbdd(); - } else { - STORM_LOG_WARN_COND(false, "Performing logical and on two DDs of different type."); - this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); - } + Add& Add::operator-=(Add const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + this->cuddAdd = this->getCuddAdd() - other.getCuddAdd(); return *this; } - Dd Dd::operator||(Dd const& other) const { - Dd result(*this); - result |= other; + Add Add::operator/(Add const& other) const { + Add result(*this); + result /= other; return result; } - Dd& Dd::operator|=(Dd const& other) { - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - if (this->isBdd() && other.isBdd()) { - this->cuddDd = this->getCuddBdd() | other.getCuddBdd(); - } else if (this->isMtbdd() && other.isMtbdd()) { - // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that - // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. - this->cuddDd = this->getCuddMtbdd() | other.getCuddMtbdd(); - } else { - STORM_LOG_WARN_COND(false, "Performing logical and on two DDs of different type."); - this->cuddDd = this->getCuddBdd() & other.getCuddBdd(); - } - return *this; - - STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s)."); - this->cuddDd = this->getCuddBdd() | other.getCuddBdd(); - this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); + Add& Add::operator/=(Add const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + this->cuddAdd = this->getCuddAdd().Divide(other.getCuddAdd()); return *this; } - Dd Dd::iff(Dd const& other) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - if (this->isBdd() && other.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables); - } else if (this->isMtbdd() && other.isMtbdd()) { - // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that - // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. - return Dd(this->getDdManager(), this->getCuddMtbdd().Xnor(other.getCuddMtbdd()), metaVariables); - } else { - STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type."); - return Dd(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables); - } - } - - Dd Dd::exclusiveOr(Dd const& other) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - if (this->isBdd() && other.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables); - } else if (this->isMtbdd() && other.isMtbdd()) { - // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that - // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise. - return Dd(this->getDdManager(), this->getCuddMtbdd().Xor(other.getCuddMtbdd()), metaVariables); - } else { - STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type."); - return Dd(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables); - } - } - - Dd Dd::implies(Dd const& other) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operatiorn on MTBDDs."); - return Dd(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getOne().getCuddBdd()), metaVariables); - } - - Dd Dd::equals(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().Equals(other.getCuddMtbdd()), metaVariables); + Add Add::equals(Add const& other) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Add(this->getDdManager(), this->getCuddAdd().Equals(other.getCuddAdd()), metaVariables); } - Dd Dd::notEquals(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().NotEquals(other.getCuddMtbdd()), metaVariables); + Add Add::notEquals(Add const& other) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Add(this->getDdManager(), this->getCuddAdd().NotEquals(other.getCuddAdd()), metaVariables); } - Dd Dd::less(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().LessThan(other.getCuddMtbdd()), metaVariables); + Add Add::less(Add const& other) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Add(this->getDdManager(), this->getCuddAdd().LessThan(other.getCuddAdd()), metaVariables); } - Dd Dd::lessOrEqual(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().LessThanOrEqual(other.getCuddMtbdd()), metaVariables); + Add Add::lessOrEqual(Add const& other) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Add(this->getDdManager(), this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()), metaVariables); } - Dd Dd::greater(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().GreaterThan(other.getCuddMtbdd()), metaVariables); + Add Add::greater(Add const& other) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Add(this->getDdManager(), this->getCuddAdd().GreaterThan(other.getCuddAdd()), metaVariables); } - Dd Dd::greaterOrEqual(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().GreaterThanOrEqual(other.getCuddMtbdd()), metaVariables); + Add Add::greaterOrEqual(Add const& other) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Add(this->getDdManager(), this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()), metaVariables); } - Dd Dd::minimum(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().Minimum(other.getCuddMtbdd()), metaVariables); + Add Add::minimum(Add const& other) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Add(this->getDdManager(), this->getCuddAdd().Minimum(other.getCuddAdd()), metaVariables); } - Dd Dd::maximum(Dd const& other) const { - STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddMtbdd().Maximum(other.getCuddMtbdd()), metaVariables); + Add Add::maximum(Add const& other) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Add(this->getDdManager(), this->getCuddAdd().Maximum(other.getCuddAdd()), metaVariables); } - Dd Dd::existsAbstract(std::set const& metaVariables) const { - STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne(false)); + Add Add::sumAbstract(std::set const& metaVariables) const { + Bdd cubeDd = this->getDdManager()->getBddOne(); std::set newMetaVariables = this->getContainedMetaVariables(); for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. @@ -346,13 +174,11 @@ namespace storm { cubeDd &= ddMetaVariable.getCube(); } - return Dd(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), newMetaVariables); + return Add(this->getDdManager(), this->getCuddAdd().ExistAbstract(cubeDd.toAdd().getCuddAdd()), newMetaVariables); } - Dd Dd::universalAbstract(std::set const& metaVariables) const { - STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne()); + Add Add::minAbstract(std::set const& metaVariables) const { + Bdd cubeDd = this->getDdManager()->getBddOne(); std::set newMetaVariables = this->getContainedMetaVariables(); for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. @@ -363,47 +189,11 @@ namespace storm { cubeDd &= ddMetaVariable.getCube(); } - return Dd(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables); - } - - Dd Dd::sumAbstract(std::set const& metaVariables) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne(true)); - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd *= ddMetaVariable.getCubeAsMtbdd(); - } - - return Dd(this->getDdManager(), this->getCuddMtbdd().ExistAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); - } - - Dd Dd::minAbstract(std::set const& metaVariables) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne(true)); - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd *= ddMetaVariable.getCubeAsMtbdd(); - } - - return Dd(this->getDdManager(), this->getCuddMtbdd().MinAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); + return Add(this->getDdManager(), this->getCuddAdd().MinAbstract(cubeDd.toAdd().getCuddAdd()), newMetaVariables); } - Dd Dd::maxAbstract(std::set const& metaVariables) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne(true)); + Add Add::maxAbstract(std::set const& metaVariables) const { + Bdd cubeDd = this->getDdManager()->getBddOne(); std::set newMetaVariables = this->getContainedMetaVariables(); for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. @@ -411,95 +201,60 @@ namespace storm { newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd *= ddMetaVariable.getCubeAsMtbdd(); + cubeDd &= ddMetaVariable.getCube(); } - return Dd(this->getDdManager(), this->getCuddMtbdd().MaxAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); + return Add(this->getDdManager(), this->getCuddAdd().MaxAbstract(cubeDd.toAdd().getCuddAdd()), newMetaVariables); } - bool Dd::equalModuloPrecision(Dd const& other, double precision, bool relative) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - + bool Add::equalModuloPrecision(Add const& other, double precision, bool relative) const { if (relative) { - return this->getCuddMtbdd().EqualSupNormRel(other.getCuddMtbdd(), precision); + return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision); } else { - return this->getCuddMtbdd().EqualSupNorm(other.getCuddMtbdd(), precision); + return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision); } } - Dd Dd::swapVariables(std::vector> const& metaVariablePairs) { + Add Add::swapVariables(std::vector> const& metaVariablePairs) { std::set newContainedMetaVariables; - if (this->isBdd()) { - std::vector from; - std::vector to; - for (auto const& metaVariablePair : metaVariablePairs) { - DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); - DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); - - // Check if it's legal so swap the meta variables. - STORM_LOG_THROW(variable1.getNumberOfDdVariables() == variable2.getNumberOfDdVariables(), storm::exceptions::InvalidArgumentException, "Unable to swap meta variables with different size."); - - // Keep track of the contained meta variables in the DD. - if (this->containsMetaVariable(metaVariablePair.first)) { - newContainedMetaVariables.insert(metaVariablePair.second); - } - if (this->containsMetaVariable(metaVariablePair.second)) { - newContainedMetaVariables.insert(metaVariablePair.first); - } - - // Add the variables to swap to the corresponding vectors. - for (auto const& ddVariable : variable1.getDdVariables()) { - from.push_back(ddVariable.getCuddBdd()); - } - for (auto const& ddVariable : variable2.getDdVariables()) { - to.push_back(ddVariable.getCuddBdd()); - } + std::vector from; + std::vector to; + for (auto const& metaVariablePair : metaVariablePairs) { + DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); + DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); + + // Check if it's legal so swap the meta variables. + if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) { + throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size."; } - // Finally, call CUDD to swap the variables. - return Dd(this->getDdManager(), this->getCuddBdd().SwapVariables(from, to), newContainedMetaVariables); - } else { - std::vector from; - std::vector to; - for (auto const& metaVariablePair : metaVariablePairs) { - DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); - DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); - - // Check if it's legal so swap the meta variables. - if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) { - throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size."; - } - - // Keep track of the contained meta variables in the DD. - if (this->containsMetaVariable(metaVariablePair.first)) { - newContainedMetaVariables.insert(metaVariablePair.second); - } - if (this->containsMetaVariable(metaVariablePair.second)) { - newContainedMetaVariables.insert(metaVariablePair.first); - } - - // Add the variables to swap to the corresponding vectors. - for (auto const& ddVariable : variable1.getDdVariables()) { - from.push_back(ddVariable.getCuddMtbdd()); - } - for (auto const& ddVariable : variable2.getDdVariables()) { - to.push_back(ddVariable.getCuddMtbdd()); - } + // Keep track of the contained meta variables in the DD. + if (this->containsMetaVariable(metaVariablePair.first)) { + newContainedMetaVariables.insert(metaVariablePair.second); + } + if (this->containsMetaVariable(metaVariablePair.second)) { + newContainedMetaVariables.insert(metaVariablePair.first); } - // Finally, call CUDD to swap the variables. - return Dd(this->getDdManager(), this->getCuddMtbdd().SwapVariables(from, to), newContainedMetaVariables); + // Add the variables to swap to the corresponding vectors. + for (auto const& ddVariable : variable1.getDdVariables()) { + from.push_back(ddVariable.toAdd().getCuddAdd()); + } + for (auto const& ddVariable : variable2.getDdVariables()) { + to.push_back(ddVariable.toAdd().getCuddAdd()); + } } + + // Finally, call CUDD to swap the variables. + return Add(this->getDdManager(), this->getCuddAdd().SwapVariables(from, to), newContainedMetaVariables); } - Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariables) const { - STORM_LOG_WARN_COND(this->isMtbdd() && otherMatrix.isMtbdd(), "Performing arithmetical operation on BDD(s)."); - + Add Add::multiplyMatrix(Add const& otherMatrix, std::set const& summationMetaVariables) const { // Create the CUDD summation variables. std::vector summationDdVariables; for (auto const& metaVariable : summationMetaVariables) { for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) { - summationDdVariables.push_back(ddVariable.getCuddMtbdd()); + summationDdVariables.push_back(ddVariable.toAdd().getCuddAdd()); } } @@ -508,154 +263,90 @@ namespace storm { std::set containedMetaVariables; std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); - return Dd(this->getDdManager(), this->getCuddMtbdd().MatrixMultiply(otherMatrix.getCuddMtbdd(), summationDdVariables), containedMetaVariables); - } - - Dd Dd::andExists(Dd const& other, std::set const& existentialVariables) const { - STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne()); - for (auto const& metaVariable : existentialVariables) { - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd &= ddMetaVariable.getCube(); - } - - std::set unionOfMetaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); - std::set containedMetaVariables; - std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); - - return Dd(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeDd.getCuddBdd()), containedMetaVariables); + return Add(this->getDdManager(), this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariables); } - Dd Dd::greater(double value) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - return Dd(this->getDdManager(), this->getCuddMtbdd().BddStrictThreshold(value), this->getContainedMetaVariables()); + Bdd Add::greater(double value) const { + return Bdd(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(value), this->getContainedMetaVariables()); } - Dd Dd::greaterOrEqual(double value) const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - return Dd(this->getDdManager(), this->getCuddMtbdd().BddThreshold(value), this->getContainedMetaVariables()); + Bdd Add::greaterOrEqual(double value) const { + return Bdd(this->getDdManager(), this->getCuddAdd().BddThreshold(value), this->getContainedMetaVariables()); } - Dd Dd::notZero() const { + Bdd Add::notZero() const { return this->toBdd(); } - Dd Dd::constrain(Dd const& constraint) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); - - if (this->isBdd() && constraint.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables); - } else { - return Dd(this->getDdManager(), this->getCuddMtbdd().Constrain(constraint.getCuddMtbdd()), metaVariables); - } + Add Add::constrain(Add const& constraint) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Add(this->getDdManager(), this->getCuddAdd().Constrain(constraint.getCuddAdd()), metaVariables); } - Dd Dd::restrict(Dd const& constraint) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); - - if (this->isBdd() && constraint.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables); - } else { - return Dd(this->getDdManager(), this->getCuddMtbdd().Restrict(constraint.getCuddMtbdd()), metaVariables); - } + Add Add::restrict(Add const& constraint) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Add(this->getDdManager(), this->getCuddAdd().Restrict(constraint.getCuddAdd()), metaVariables); } - Dd Dd::getSupport() const { - if (this->isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables()); - } else { - return Dd(this->getDdManager(), this->getCuddMtbdd().Support(), this->getContainedMetaVariables()); - } + Bdd Add::getSupport() const { + return Bdd(this->getDdManager(), this->getCuddAdd().Support(), this->getContainedMetaVariables()); } - uint_fast64_t Dd::getNonZeroCount() const { + uint_fast64_t Add::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; for (auto const& metaVariable : this->getContainedMetaVariables()) { numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); } - if (this->isBdd()) { - return static_cast(this->getCuddBdd().CountMinterm(static_cast(numberOfDdVariables))); - } else { - return static_cast(this->getCuddMtbdd().CountMinterm(static_cast(numberOfDdVariables))); - } + return static_cast(this->getCuddAdd().CountMinterm(static_cast(numberOfDdVariables))); } - uint_fast64_t Dd::getLeafCount() const { - if (this->isBdd()) { - return static_cast(this->getCuddBdd().CountLeaves()); - } else { - return static_cast(this->getCuddMtbdd().CountLeaves()); - } + uint_fast64_t Add::getLeafCount() const { + return static_cast(this->getCuddAdd().CountLeaves()); } - uint_fast64_t Dd::getNodeCount() const { - if (this->isBdd()) { - return static_cast(this->getCuddBdd().nodeCount()); - } else { - return static_cast(this->getCuddMtbdd().nodeCount()); - } + uint_fast64_t Add::getNodeCount() const { + return static_cast(this->getCuddAdd().nodeCount()); } - double Dd::getMin() const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - ADD constantMinAdd = this->getCuddMtbdd().FindMin(); + double Add::getMin() const { + ADD constantMinAdd = this->getCuddAdd().FindMin(); return static_cast(Cudd_V(constantMinAdd.getNode())); } - double Dd::getMax() const { - STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); - - ADD constantMaxAdd = this->getCuddMtbdd().FindMax(); + double Add::getMax() const { + ADD constantMaxAdd = this->getCuddAdd().FindMax(); return static_cast(Cudd_V(constantMaxAdd.getNode())); } - void Dd::setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue) { + void Add::setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue) { std::map metaVariableToValueMap; metaVariableToValueMap.emplace(metaVariable, variableValue); this->setValue(metaVariableToValueMap, targetValue); } - void Dd::setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue) { + void Add::setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue) { std::map metaVariableToValueMap; metaVariableToValueMap.emplace(metaVariable1, variableValue1); metaVariableToValueMap.emplace(metaVariable2, variableValue2); this->setValue(metaVariableToValueMap, targetValue); } - void Dd::setValue(std::map const& metaVariableToValueMap, double targetValue) { - if (this->isBdd()) { - STORM_LOG_THROW(targetValue == storm::utility::zero() || targetValue == storm::utility::one(), storm::exceptions::InvalidArgumentException, "Cannot set encoding to non-0, non-1 value " << targetValue << " in BDD."); - Dd valueEncoding(this->getDdManager()->getOne()); - for (auto const& nameValuePair : metaVariableToValueMap) { - valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); - // Also record that the DD now contains the meta variable. - this->addContainedMetaVariable(nameValuePair.first); - } - if (targetValue == storm::utility::one()) { - this->cuddDd = valueEncoding.getCuddBdd().Ite(this->getDdManager()->getOne().getCuddBdd(), this->getCuddBdd()); - } else { - this->cuddDd = valueEncoding.getCuddBdd().Ite(this->getDdManager()->getZero().getCuddBdd(), this->getCuddBdd()); - } - } else { - Dd valueEncoding(this->getDdManager()->getOne()); - for (auto const& nameValuePair : metaVariableToValueMap) { - valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); - // Also record that the DD now contains the meta variable. - this->addContainedMetaVariable(nameValuePair.first); - } - - this->cuddDd = valueEncoding.toMtbdd().getCuddMtbdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddMtbdd(), this->getCuddMtbdd()); + void Add::setValue(std::map const& metaVariableToValueMap, double targetValue) { + Bdd valueEncoding = this->getDdManager()->getBddOne(); + for (auto const& nameValuePair : metaVariableToValueMap) { + valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + // Also record that the DD now contains the meta variable. + this->addMetaVariable(nameValuePair.first); } + + this->cuddAdd = valueEncoding.toAdd().getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->getCuddAdd()); } - double Dd::getValue(std::map const& metaVariableToValueMap) const { + double Add::getValue(std::map const& metaVariableToValueMap) const { std::set remainingMetaVariables(this->getContainedMetaVariables()); - Dd valueEncoding(this->getDdManager()->getOne()); + Bdd valueEncoding = this->getDdManager()->getBddOne(); for (auto const& nameValuePair : metaVariableToValueMap) { valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); if (this->containsMetaVariable(nameValuePair.first)) { @@ -665,65 +356,41 @@ namespace storm { STORM_LOG_THROW(remainingMetaVariables.empty(), storm::exceptions::InvalidArgumentException, "Cannot evaluate function for which not all inputs were given."); - if (this->isBdd()) { - Dd value = *this && valueEncoding; - return value.isZero() ? 0 : 1; - } else { - Dd value = *this * valueEncoding.toMtbdd(); - value = value.sumAbstract(this->getContainedMetaVariables()); - return static_cast(Cudd_V(value.getCuddMtbdd().getNode())); - } + Add value = *this * valueEncoding.toAdd(); + value = value.sumAbstract(this->getContainedMetaVariables()); + return static_cast(Cudd_V(value.getCuddAdd().getNode())); } - bool Dd::isOne() const { - if (this->isBdd()) { - return this->getCuddBdd().IsOne(); - } else { - return this->getCuddMtbdd().IsOne(); - } + bool Add::isOne() const { + return this->getCuddAdd().IsOne(); } - bool Dd::isZero() const { - if (this->isBdd()) { - return this->getCuddBdd().IsZero(); - } else { - return this->getCuddMtbdd().IsZero(); - } + bool Add::isZero() const { + return this->getCuddAdd().IsZero(); } - bool Dd::isConstant() const { - if (this->isBdd()) { - return Cudd_IsConstant(this->getCuddBdd().getNode()); - } else { - return Cudd_IsConstant(this->getCuddMtbdd().getNode()); - } + bool Add::isConstant() const { + return Cudd_IsConstant(this->getCuddAdd().getNode()); } - uint_fast64_t Dd::getIndex() const { - if (this->isBdd()) { - return static_cast(this->getCuddBdd().NodeReadIndex()); - } else { - return static_cast(this->getCuddMtbdd().NodeReadIndex()); - } + uint_fast64_t Add::getIndex() const { + return static_cast(this->getCuddAdd().NodeReadIndex()); } template - std::vector Dd::toVector() const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD."); + std::vector Add::toVector() const { return this->toVector(Odd(*this)); } template - std::vector Dd::toVector(Odd const& rowOdd) const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD."); + std::vector Add::toVector(Odd const& rowOdd) const { std::vector result(rowOdd.getTotalOffset()); std::vector ddVariableIndices = this->getSortedVariableIndices(); addToVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result); return result; } - storm::storage::SparseMatrix Dd::toMatrix() const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); + storm::storage::SparseMatrix Add::toMatrix() const { std::set rowVariables; std::set columnVariables; @@ -735,11 +402,10 @@ namespace storm { } } - return toMatrix(rowVariables, columnVariables, Odd(this->existsAbstract(rowVariables)), Odd(this->existsAbstract(columnVariables))); + return toMatrix(rowVariables, columnVariables, Odd(this->sumAbstract(rowVariables)), Odd(this->sumAbstract(columnVariables))); } - storm::storage::SparseMatrix Dd::toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); + storm::storage::SparseMatrix Add::toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { std::set rowMetaVariables; std::set columnMetaVariables; @@ -754,8 +420,7 @@ namespace storm { return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd); } - storm::storage::SparseMatrix Dd::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); + storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; @@ -814,8 +479,7 @@ namespace storm { return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices)); } - storm::storage::SparseMatrix Dd::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD."); + storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; std::vector ddGroupVariableIndices; @@ -845,7 +509,7 @@ namespace storm { // TODO: assert that the group variables are at the very top of the variable ordering? // Start by computing the offsets (in terms of rows) for each row group. - Dd stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).sumAbstract(groupMetaVariables); + Add stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).toAdd().sumAbstract(groupMetaVariables); std::vector rowGroupIndices = stateToNumberOfChoices.toVector(rowOdd); rowGroupIndices.resize(rowGroupIndices.size() + 1); uint_fast64_t tmp = 0; @@ -859,7 +523,7 @@ namespace storm { // Next, we split the matrix into one for each group. This only works if the group variables are at the very // top. - std::vector> groups; + std::vector> groups; splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables); // Create the actual storage for the non-zero entries. @@ -867,13 +531,13 @@ namespace storm { // Now compute the indices at which the individual rows start. std::vector rowIndications(rowGroupIndices.back() + 1); - std::vector> statesWithGroupEnabled(groups.size()); + std::vector> statesWithGroupEnabled(groups.size()); for (uint_fast64_t i = 0; i < groups.size(); ++i) { auto const& dd = groups[i]; toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); - statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnMetaVariables); + statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnMetaVariables).toAdd(); addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); } @@ -917,7 +581,7 @@ namespace storm { return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); } - void Dd::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { + void Add::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { // For the empty DD, we do not need to add any entries. if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { return; @@ -969,14 +633,14 @@ namespace storm { } } - void Dd::splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const { + void Add::splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const { // For the empty DD, we do not need to create a group. if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { return; } if (currentLevel == maxLevel) { - groups.push_back(Dd(this->getDdManager(), ADD(this->getDdManager()->getCuddManager(), dd), remainingMetaVariables)); + groups.push_back(Add(this->getDdManager(), ADD(this->getDdManager()->getCuddManager(), dd), remainingMetaVariables)); } else if (ddGroupVariableIndices[currentLevel] < dd->index) { splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); @@ -987,7 +651,7 @@ namespace storm { } template - void Dd::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { + void Add::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { // For the empty DD, we do not need to add any entries. if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { return; @@ -1007,53 +671,11 @@ namespace storm { addToVectorRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector); } } - - std::vector Dd::getSortedVariableIndices() const { - std::vector ddVariableIndices; - for (auto const& metaVariableName : this->getContainedMetaVariables()) { - auto const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddVariableIndices.push_back(ddVariable.getIndex()); - } - } - - // Next, we need to sort them, since they may be arbitrarily ordered otherwise. - std::sort(ddVariableIndices.begin(), ddVariableIndices.end()); - return ddVariableIndices; - } - - bool Dd::containsMetaVariable(storm::expressions::Variable const& metaVariable) const { - return containedMetaVariables.find(metaVariable) != containedMetaVariables.end(); - } - - bool Dd::containsMetaVariables(std::set const& metaVariables) const { - for (auto const& metaVariable : metaVariables) { - auto const& ddMetaVariable = containedMetaVariables.find(metaVariable); - - if (ddMetaVariable == containedMetaVariables.end()) { - return false; - } - } - return true; - } - - std::set const& Dd::getContainedMetaVariables() const { - return this->containedMetaVariables; - } - - std::set& Dd::getContainedMetaVariables() { - return this->containedMetaVariables; - } - - void Dd::exportToDot(std::string const& filename) const { + + void Add::exportToDot(std::string const& filename) const { if (filename.empty()) { - if (this->isBdd()) { - std::vector cuddBddVector = { this->getCuddBdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddBddVector); - } else { - std::vector cuddAddVector = { this->getCuddMtbdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); - } + std::vector cuddAddVector = { this->getCuddAdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); } else { // Build the name input of the DD. std::vector ddNames; @@ -1071,13 +693,8 @@ namespace storm { // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); - if (this->isBdd()) { - std::vector cuddBddVector = { this->getCuddBdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); - } else { - std::vector cuddAddVector = { this->getCuddMtbdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); - } + std::vector cuddAddVector = { this->getCuddAdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); fclose(filePointer); // Finally, delete the names. @@ -1090,85 +707,28 @@ namespace storm { } } - void Dd::addContainedMetaVariable(storm::expressions::Variable const& metaVariable) { - this->getContainedMetaVariables().insert(metaVariable); - } - - void Dd::removeContainedMetaVariable(storm::expressions::Variable const& metaVariable) { - this->getContainedMetaVariables().erase(metaVariable); - } - - std::shared_ptr const> Dd::getDdManager() const { - return this->ddManager; - } - - DdForwardIterator Dd::begin(bool enumerateDontCareMetaVariables) const { + DdForwardIterator Add::begin(bool enumerateDontCareMetaVariables) const { int* cube; double value; - DdGen* generator = this->getCuddDd().FirstCube(&cube, &value); + DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); return DdForwardIterator(this->getDdManager(), generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &this->getContainedMetaVariables(), enumerateDontCareMetaVariables); } - DdForwardIterator Dd::end(bool enumerateDontCareMetaVariables) const { + DdForwardIterator Add::end(bool enumerateDontCareMetaVariables) const { return DdForwardIterator(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); } - - storm::expressions::Expression Dd::toExpression() const { - return toExpressionRecur(this->getCuddDdNode(), this->getDdManager()->getDdVariables()); - } - - storm::expressions::Expression Dd::getMintermExpression() const { - // Note that we first transform the ADD into a BDD to convert all non-zero terminals to ones and therefore - // make the DD more compact. - return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->toBdd().getCuddDdNode(), this->getDdManager()->getDdVariables()); - } - - storm::expressions::Expression Dd::toExpressionRecur(DdNode const* dd, std::vector const& variables) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This feature is currently unavailable."); - // If the DD is a terminal node, we can simply return a constant expression. - // if (Cudd_IsConstant(dd)) { - // return storm::expressions::Expression::createDoubleLiteral(static_cast(Cudd_V(dd))); - // } else { - // return storm::expressions::Expression::createBooleanVariable(variableNames[dd->index]).ite(toExpressionRecur(Cudd_T(dd), variableNames), toExpressionRecur(Cudd_E(dd), variableNames)); - // } - } - - storm::expressions::Expression Dd::getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector const& variables) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This feature is currently unavailable."); - // If the DD is a terminal node, we can simply return a constant expression. - // if (Cudd_IsConstant(dd)) { - // if (Cudd_IsComplement(dd)) { - // return storm::expressions::Expression::createBooleanLiteral(false); - // } else { - // return storm::expressions::Expression::createBooleanLiteral((dd == Cudd_ReadOne(manager)) ? true : false); - // } - // } else { - // // Get regular versions of the pointers. - // DdNode* regularDd = Cudd_Regular(dd); - // DdNode* thenDd = Cudd_T(regularDd); - // DdNode* elseDd = Cudd_E(regularDd); - // - // // Compute expression recursively. - // storm::expressions::Expression result = storm::expressions::Expression::createBooleanVariable(variableNames[dd->index]).ite(getMintermExpressionRecur(manager, thenDd, variableNames), getMintermExpressionRecur(manager, elseDd, variableNames)); - // if (Cudd_IsComplement(dd)) { - // result = !result; - // } - // - // return result; - // } - } - - std::ostream& operator<<(std::ostream& out, const Dd& dd) { - dd.exportToDot(); + + std::ostream& operator<<(std::ostream& out, const Add& add) { + add.exportToDot(); return out; } // Explicitly instantiate some templated functions. - template std::vector Dd::toVector() const; - template std::vector Dd::toVector(Odd const& rowOdd) const; - template void Dd::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; - template std::vector Dd::toVector() const; - template std::vector Dd::toVector(Odd const& rowOdd) const; - template void Dd::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + template std::vector Add::toVector() const; + template std::vector Add::toVector(Odd const& rowOdd) const; + template void Add::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + template std::vector Add::toVector() const; + template std::vector Add::toVector(Odd const& rowOdd) const; + template void Add::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; } } \ No newline at end of file diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h index f860e79bf..a43738d85 100644 --- a/src/storage/dd/CuddAdd.h +++ b/src/storage/dd/CuddAdd.h @@ -1,16 +1,10 @@ -#ifndef STORM_STORAGE_DD_CUDDDD_H_ -#define STORM_STORAGE_DD_CUDDDD_H_ +#ifndef STORM_STORAGE_DD_CUDDADD_H_ +#define STORM_STORAGE_DD_CUDDADD_H_ -#include -#include -#include -#include -#include - -#include "src/storage/dd/Dd.h" +#include "src/storage/dd/Add.h" +#include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdForwardIterator.h" #include "src/storage/SparseMatrix.h" -#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Variable.h" #include "src/utility/OsDetection.h" @@ -22,22 +16,24 @@ namespace storm { // Forward-declare some classes. template class DdManager; template class Odd; + template class Bdd; template<> - class Dd { + class Add : public Dd { public: // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. friend class DdManager; friend class DdForwardIterator; + friend class Bdd; friend class Odd; // Instantiate all copy/move constructors/assignments with the default implementation. - Dd() = default; - Dd(Dd const& other) = default; - Dd& operator=(Dd const& other) = default; + Add() = default; + Add(Add const& other) = default; + Add& operator=(Add const& other) = default; #ifndef WINDOWS - Dd(Dd&& other) = default; - Dd& operator=(Dd&& other) = default; + Add(Add&& other) = default; + Add& operator=(Add&& other) = default; #endif /*! @@ -46,7 +42,7 @@ namespace storm { * @param other The DD that is to be compared with the current one. * @return True if the DDs represent the same function. */ - bool operator==(Dd const& other) const; + bool operator==(Add const& other) const; /*! * Retrieves whether the two DDs represent different functions. @@ -54,375 +50,309 @@ namespace storm { * @param other The DD that is to be compared with the current one. * @return True if the DDs represent the different functions. */ - bool operator!=(Dd const& other) const; + bool operator!=(Add const& other) const; /*! * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero * function value to the function values specified by the first DD and all others to the function values * specified by the second DD. - */ - Dd ite(Dd const& thenDd, Dd const& elseDd) const; - - /*! - * Performs a logical or of the current and the given DD. - * - * @param other The second DD used for the operation. - * @return The logical or of the operands. - */ - Dd operator||(Dd const& other) const; - - /*! - * Performs a logical or of the current and the given DD and assigns it to the current DD. - * - * @param other The second DD used for the operation. - * @return A reference to the current DD after the operation - */ - Dd& operator|=(Dd const& other); - - /*! - * Performs a logical and of the current and the given DD. - * - * @param other The second DD used for the operation. - * @return The logical and of the operands. - */ - Dd operator&&(Dd const& other) const; - - /*! - * Performs a logical and of the current and the given DD and assigns it to the current DD. * - * @param other The second DD used for the operation. - * @return A reference to the current DD after the operation + * @param thenDd The ADD specifying the 'then' part. + * @param elseDd The ADD specifying the 'else' part. + * @return The ADD corresponding to the if-then-else of the operands. */ - Dd& operator&=(Dd const& other); + Add ite(Add const& thenDd, Add const& elseDd) const; /*! - * Performs a logical iff of the current and the given DD. + * Logically inverts the current ADD. That is, all inputs yielding non-zero values will be mapped to zero in + * the result and vice versa. * - * @param other The second DD used for the operation. - * @return The logical iff of the operands. + * @return The resulting ADD. */ - Dd iff(Dd const& other) const; + Add operator!() const; /*! - * Performs a logical exclusive-or of the current and the given DD. + * Performs a logical or of the current anBd the given ADD. As a prerequisite, the operand ADDs need to be + * 0/1 ADDs. * - * @param other The second DD used for the operation. - * @return The logical exclusive-or of the operands. + * @param other The second ADD used for the operation. + * @return The logical or of the operands. */ - Dd exclusiveOr(Dd const& other) const; + Add operator||(Add const& other) const; /*! - * Performs a logical implication of the current and the given DD. + * Performs a logical or of the current and the given ADD and assigns it to the current ADD. As a + * prerequisite, the operand ADDs need to be 0/1 ADDs. * - * @param other The second DD used for the operation. - * @return The logical implication of the operands. + * @param other The second ADD used for the operation. + * @return A reference to the current ADD after the operation */ - Dd implies(Dd const& other) const; + Add& operator|=(Add const& other); /*! - * Adds the two DDs. + * Adds the two ADDs. * - * @param other The DD to add to the current one. + * @param other The ADD to add to the current one. * @return The result of the addition. */ - Dd operator+(Dd const& other) const; + Add operator+(Add const& other) const; /*! - * Adds the given DD to the current one. + * Adds the given ADD to the current one. * - * @param other The DD to add to the current one. - * @return A reference to the current DD after the operation. + * @param other The ADD to add to the current one. + * @return A reference to the current ADD after the operation. */ - Dd& operator+=(Dd const& other); + Add& operator+=(Add const& other); /*! - * Multiplies the two DDs. + * Multiplies the two ADDs. * - * @param other The DD to multiply with the current one. + * @param other The ADD to multiply with the current one. * @return The result of the multiplication. */ - Dd operator*(Dd const& other) const; + Add operator*(Add const& other) const; /*! - * Multiplies the given DD with the current one and assigns the result to the current DD. + * Multiplies the given ADD with the current one and assigns the result to the current ADD. * - * @param other The DD to multiply with the current one. - * @return A reference to the current DD after the operation. + * @param other The ADD to multiply with the current one. + * @return A reference to the current ADD after the operation. */ - Dd& operator*=(Dd const& other); + Add& operator*=(Add const& other); /*! - * Subtracts the given DD from the current one. + * Subtracts the given ADD from the current one. * - * @param other The DD to subtract from the current one. + * @param other The ADD to subtract from the current one. * @return The result of the subtraction. */ - Dd operator-(Dd const& other) const; + Add operator-(Add const& other) const; /*! - * Subtracts the DD from the constant zero function. + * Subtracts the ADD from the constant zero function. * - * @return The resulting function represented as a DD. + * @return The resulting function represented as a ADD. */ - Dd operator-() const; + Add operator-() const; /*! - * Subtracts the given DD from the current one and assigns the result to the current DD. + * Subtracts the given ADD from the current one and assigns the result to the current ADD. * - * @param other The DD to subtract from the current one. - * @return A reference to the current DD after the operation. + * @param other The ADD to subtract from the current one. + * @return A reference to the current ADD after the operation. */ - Dd& operator-=(Dd const& other); + Add& operator-=(Add const& other); /*! - * Divides the current DD by the given one. + * Divides the current ADD by the given one. * - * @param other The DD by which to divide the current one. + * @param other The ADD by which to divide the current one. * @return The result of the division. */ - Dd operator/(Dd const& other) const; - - /*! - * Divides the current DD by the given one and assigns the result to the current DD. - * - * @param other The DD by which to divide the current one. - * @return A reference to the current DD after the operation. - */ - Dd& operator/=(Dd const& other); - - /*! - * Retrieves the logical complement of the current DD. The result will map all encodings with a value - * unequal to zero to false and all others to true. - * - * @return The logical complement of the current DD. - */ - Dd operator!() const; + Add operator/(Add const& other) const; /*! - * Logically complements the current DD. The result will map all encodings with a value - * unequal to zero to false and all others to true. + * Divides the current ADD by the given one and assigns the result to the current ADD. * - * @return A reference to the current DD after the operation. + * @param other The ADD by which to divide the current one. + * @return A reference to the current ADD after the operation. */ - Dd& complement(); + Add& operator/=(Add const& other); /*! - * Retrieves the function that maps all evaluations to one that have an identical function values. + * Retrieves the function that maps all evaluations to one that have identical function values. * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. */ - Dd equals(Dd const& other) const; + Add equals(Add const& other) const; /*! * Retrieves the function that maps all evaluations to one that have distinct function values. * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. - */ - Dd notEquals(Dd const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one whose function value in the first DD are less - * than the one in the given DD. - * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. - */ - Dd less(Dd const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one whose function value in the first DD are less or - * equal than the one in the given DD. - * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. */ - Dd lessOrEqual(Dd const& other) const; + Add notEquals(Add const& other) const; /*! - * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater - * than the one in the given DD. + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less + * than the one in the given ADD. * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. */ - Dd greater(Dd const& other) const; + Add less(Add const& other) const; /*! - * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater - * or equal than the one in the given DD. + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less or + * equal than the one in the given ADD. * * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. + * @return The resulting function represented as an ADD. */ - Dd greaterOrEqual(Dd const& other) const; + Add lessOrEqual(Add const& other) const; /*! - * Retrieves the function that maps all evaluations to the minimum of the function values of the two DDs. + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater + * than the one in the given ADD. * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. */ - Dd minimum(Dd const& other) const; + Add greater(Add const& other) const; /*! - * Retrieves the function that maps all evaluations to the maximum of the function values of the two DDs. + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater + * or equal than the one in the given ADD. * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as a DD. + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. */ - Dd maximum(Dd const& other) const; + Add greaterOrEqual(Add const& other) const; /*! - * Existentially abstracts from the given meta variables. + * Retrieves the function that maps all evaluations to the minimum of the function values of the two ADDs. * - * @param metaVariables The meta variables from which to abstract. + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. */ - Dd existsAbstract(std::set const& metaVariables) const; + Add minimum(Add const& other) const; /*! - * Universally abstracts from the given meta variables. + * Retrieves the function that maps all evaluations to the maximum of the function values of the two ADDs. * - * @param metaVariables The meta variables from which to abstract. + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. */ - Dd universalAbstract(std::set const& metaVariables) const; + Add maximum(Add const& other) const; /*! * Sum-abstracts from the given meta variables. * * @param metaVariables The meta variables from which to abstract. */ - Dd sumAbstract(std::set const& metaVariables) const; + Add sumAbstract(std::set const& metaVariables) const; /*! * Min-abstracts from the given meta variables. * * @param metaVariables The meta variables from which to abstract. */ - Dd minAbstract(std::set const& metaVariables) const; + Add minAbstract(std::set const& metaVariables) const; /*! * Max-abstracts from the given meta variables. * * @param metaVariables The meta variables from which to abstract. */ - Dd maxAbstract(std::set const& metaVariables) const; + Add maxAbstract(std::set const& metaVariables) const; /*! - * Checks whether the current and the given DD represent the same function modulo some given precision. + * Checks whether the current and the given ADD represent the same function modulo some given precision. * - * @param other The DD with which to compare. + * @param other The ADD with which to compare. * @param precision An upper bound on the maximal difference between any two function values that is to be * tolerated. * @param relative If set to true, not the absolute values have to be within the precision, but the relative * values. */ - bool equalModuloPrecision(Dd const& other, double precision, bool relative = true) const; + bool equalModuloPrecision(Add const& other, double precision, bool relative = true) const; /*! - * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have - * the same number of underlying DD variables. + * Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have + * the same number of underlying ADD variables. * * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. - * @return The resulting DD. + * @return The resulting ADD. */ - Dd swapVariables(std::vector> const& metaVariablePairs); + Add swapVariables(std::vector> const& metaVariablePairs); /*! - * Multiplies the current DD (representing a matrix) with the given matrix by summing over the given meta + * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta * variables. * * @param otherMatrix The matrix with which to multiply. * @param summationMetaVariables The names of the meta variables over which to sum during the matrix- * matrix multiplication. - * @return A DD representing the result of the matrix-matrix multiplication. - */ - Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariables) const; - - /*! - * Computes the logical and of the current and the given DD and existentially abstracts from the given set - * of variables. - * - * @param other The second DD for the logical and. - * @param existentialVariables The variables from which to existentially abstract. - * @return A DD representing the result. + * @return An ADD representing the result of the matrix-matrix multiplication. */ - Dd andExists(Dd const& other, std::set const& existentialVariables) const; + Add multiplyMatrix(Add const& otherMatrix, std::set const& summationMetaVariables) const; /*! - * Computes a DD that represents the function in which all assignments with a function value strictly larger - * than the given value are mapped to one and all others to zero. + * Computes a BDD that represents the function in which all assignments with a function value strictly + * larger than the given value are mapped to one and all others to zero. * * @param value The value used for the comparison. - * @return The resulting DD. + * @return The resulting BDD. */ - Dd greater(double value) const; + Bdd greater(double value) const; /*! - * Computes a DD that represents the function in which all assignments with a function value larger or equal + * Computes a BDD that represents the function in which all assignments with a function value larger or equal * to the given value are mapped to one and all others to zero. * * @param value The value used for the comparison. - * @return The resulting DD. + * @return The resulting BDD. */ - Dd greaterOrEqual(double value) const; + Bdd greaterOrEqual(double value) const; /*! - * Computes a DD that represents the function in which all assignments with a function value unequal to zero - * are mapped to one and all others to zero. + * Computes a BDD that represents the function in which all assignments with a function value unequal to + * zero are mapped to one and all others to zero. * * @return The resulting DD. */ - Dd notZero() const; + Bdd notZero() const; /*! - * Computes the constraint of the current DD with the given constraint. That is, the function value of the - * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint + * Computes the constraint of the current ADD with the given constraint. That is, the function value of the + * resulting ADD will be the same as the current ones for all assignments mapping to one in the constraint * and may be different otherwise. * * @param constraint The constraint to use for the operation. - * @return The resulting DD. + * @return The resulting ADD. */ - Dd constrain(Dd const& constraint) const; + Add constrain(Add const& constraint) const; /*! - * Computes the restriction of the current DD with the given constraint. That is, the function value of the + * Computes the restriction of the current ADD with the given constraint. That is, the function value of the * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint * and may be different otherwise. * * @param constraint The constraint to use for the operation. - * @return The resulting DD. + * @return The resulting ADD. */ - Dd restrict(Dd const& constraint) const; + Add restrict(Add const& constraint) const; /*! - * Retrieves the support of the current DD. + * Retrieves the support of the current ADD. * - * @return The support represented as a DD. + * @return The support represented as a BDD. */ - Dd getSupport() const; + Bdd getSupport() const; /*! * Retrieves the number of encodings that are mapped to a non-zero value. * * @return The number of encodings that are mapped to a non-zero value. */ - uint_fast64_t getNonZeroCount() const; + virtual uint_fast64_t getNonZeroCount() const override; /*! - * Retrieves the number of leaves of the DD. + * Retrieves the number of leaves of the ADD. * - * @return The number of leaves of the DD. + * @return The number of leaves of the ADD. */ - uint_fast64_t getLeafCount() const; + virtual uint_fast64_t getLeafCount() const override; /*! * Retrieves the number of nodes necessary to represent the DD. * * @return The number of nodes in this DD. */ - uint_fast64_t getNodeCount() const; + virtual uint_fast64_t getNodeCount() const override; /*! * Retrieves the lowest function value of any encoding. @@ -485,23 +415,23 @@ namespace storm { double getValue(std::map const& metaVariableToValueMap = std::map()) const; /*! - * Retrieves whether this DD represents the constant one function. + * Retrieves whether this ADD represents the constant one function. * - * @return True if this DD represents the constant one function. + * @return True if this ADD represents the constant one function. */ bool isOne() const; /*! - * Retrieves whether this DD represents the constant zero function. + * Retrieves whether this ADD represents the constant zero function. * - * @return True if this DD represents the constant zero function. + * @return True if this ADD represents the constant zero function. */ bool isZero() const; /*! - * Retrieves whether this DD represents a constant function. + * Retrieves whether this ADD represents a constant function. * - * @return True if this DD represents a constants function. + * @return True if this ADD represents a constants function. */ bool isConstant() const; @@ -510,101 +440,71 @@ namespace storm { * * @return The index of the topmost variable in DD. */ - uint_fast64_t getIndex() const; + virtual uint_fast64_t getIndex() const override; /*! - * Converts the DD to a vector. + * Converts the ADD to a vector. * - * @return The double vector that is represented by this DD. + * @return The double vector that is represented by this ADD. */ template std::vector toVector() const; /*! - * Converts the DD to a vector. The given offset-labeled DD is used to determine the correct row of + * Converts the ADD to a vector. The given offset-labeled DD is used to determine the correct row of * each entry. * * @param rowOdd The ODD used for determining the correct row. - * @return The double vector that is represented by this DD. + * @return The double vector that is represented by this ADD. */ template std::vector toVector(storm::dd::Odd const& rowOdd) const; /*! - * Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the + * Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the * row, whereas all primed variables are assumed to encode the column. * - * @return The matrix that is represented by this DD. + * @return The matrix that is represented by this ADD. */ storm::storage::SparseMatrix toMatrix() const; /*! - * Converts the DD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the + * Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the * row, whereas all primed variables are assumed to encode the column. The given offset-labeled DDs are used * to determine the correct row and column, respectively, for each entry. * * @param rowOdd The ODD used for determining the correct row. * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this DD. + * @return The matrix that is represented by this ADD. */ storm::storage::SparseMatrix toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; /*! - * Converts the DD to a (sparse) double matrix. The given offset-labeled DDs are used to determine the + * Converts the ADD to a (sparse) double matrix. The given offset-labeled DDs are used to determine the * correct row and column, respectively, for each entry. * * @param rowMetaVariables The meta variables that encode the rows of the matrix. * @param columnMetaVariables The meta variables that encode the columns of the matrix. * @param rowOdd The ODD used for determining the correct row. * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this DD. + * @return The matrix that is represented by this ADD. */ storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; /*! - * Converts the DD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to + * Converts the ADD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to * determine the correct row and column, respectively, for each entry. Note: this function assumes that - * the meta variables used to distinguish different row groups are at the very top of the DD. + * the meta variables used to distinguish different row groups are at the very top of the ADD. * * @param rowMetaVariables The meta variables that encode the rows of the matrix. * @param columnMetaVariables The meta variables that encode the columns of the matrix. * @param groupMetaVariables The meta variables that are used to distinguish different row groups. * @param rowOdd The ODD used for determining the correct row. * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this DD. + * @return The matrix that is represented by this ADD. */ storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - /*! - * Retrieves whether the given meta variable is contained in the DD. - * - * @param metaVariable The meta variable for which to query membership. - * @return True iff the meta variable is contained in the DD. - */ - bool containsMetaVariable(storm::expressions::Variable const& metaVariable) const; - - /*! - * Retrieves whether the given meta variables are all contained in the DD. - * - * @param metaVariables The meta variables for which to query membership. - * @return True iff all meta variables are contained in the DD. - */ - bool containsMetaVariables(std::set const& metaVariables) const; - - /*! - * Retrieves the set of all meta variables contained in the DD. - * - * @return The set of all meta variables contained in the DD. - */ - std::set const& getContainedMetaVariables() const; - - /*! - * Retrieves the set of all meta variables contained in the DD. - * - * @return The set of all meta variables contained in the DD. - */ - std::set& getContainedMetaVariables(); - /*! * Exports the DD to the given file in the dot format. * @@ -612,13 +512,6 @@ namespace storm { */ void exportToDot(std::string const& filename = "") const; - /*! - * Retrieves the manager that is responsible for this DD. - * - * A pointer to the manager that is responsible for this DD. - */ - std::shared_ptr const> getDdManager() const; - /*! * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. * @@ -637,137 +530,40 @@ namespace storm { */ DdForwardIterator end(bool enumerateDontCareMetaVariables = true) const; - /*! - * Converts the DD into a (heavily nested) if-then-else expression that represents the very same function. - * The variable names used in the expression are derived from the meta variable name and are extended with a - * suffix ".i" if the meta variable is integer-valued, expressing that the variable is the i-th bit of the - * meta variable. - * - * @return The resulting expression. - */ - storm::expressions::Expression toExpression() const; - - /*! - * Converts the DD into a (heavily nested) if-then-else (with negations) expression that evaluates to true - * if and only if the assignment is minterm of the DD. The variable names used in the expression are derived - * from the meta variable name and are extended with a suffix ".i" if the meta variable is integer-valued, - * expressing that the variable is the i-th bit of the meta variable. - * - * @return The resulting expression. - */ - storm::expressions::Expression getMintermExpression() const; - - friend std::ostream & operator<<(std::ostream& out, const Dd& dd); + friend std::ostream & operator<<(std::ostream& out, const Add& add); /*! - * Converts an MTBDD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as + * 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. */ - Dd toBdd() const; - - /*! - * Converts a BDD to an equivalent MTBDD. - * - * @return The corresponding MTBDD. - */ - Dd toMtbdd() const; - - /*! - * Retrieves whether this DD is a BDD. - * - * @return True iff this DD is a BDD. - */ - bool isBdd() const; - - /*! - * Retrieves whether this DD is an MTBDD. Even though MTBDDs technicall subsume BDDs, this will return false - * if the DD is actually a BDD. - * - * @return True iff this DD is an MTBDD. - */ - bool isMtbdd() const; + Bdd toBdd() const; private: - /*! - * Retrieves the CUDD BDD object associated with this DD. - * - * @return The CUDD BDD object associated with this DD. - */ - BDD getCuddBdd() const; /*! - * Retrieves the CUDD MTBDD object associated with this DD. + * Retrieves the CUDD ADD object associated with this ADD. * - * @return The CUDD MTBDD object associated with this DD. + * @return The CUDD ADD object associated with this ADD. */ - ADD getCuddMtbdd() const; + ADD getCuddAdd() const; /*! - * Retrieves the CUDD object associated with this DD. + * Retrieves the raw DD node of CUDD associated with this ADD. * - * @return The CUDD object associated with this DD. - */ - ABDD const& getCuddDd() const; - - /*! - * Retrieves the raw DD node of CUDD associated with this DD. - * - * @return The DD node of CUDD associated with this DD. + * @return The DD node of CUDD associated with this ADD. */ DdNode* getCuddDdNode() const; /*! - * Adds the given meta variable to the set of meta variables that are contained in this DD. - * - * @param metaVariable The name of the meta variable to add. - */ - void addContainedMetaVariable(storm::expressions::Variable const& metaVariable); - - /*! - * Removes the given meta variable to the set of meta variables that are contained in this DD. - * - * @param metaVariable The name of the meta variable to remove. - */ - void removeContainedMetaVariable(storm::expressions::Variable const& metaVariable); - - /*! - * Performs the recursive step of toExpression on the given DD. - * - * @param dd The dd to translate into an expression. - * @param variables The variables to use in the expression. - * @return The resulting expression. - */ - static storm::expressions::Expression toExpressionRecur(DdNode const* dd, std::vector const& variables); - - /*! - * Performs the recursive step of getMintermExpression on the given DD. - * - * @param manager The manager of the DD. - * @param dd The dd whose minterms to translate into an expression. - * @param variables The variables to use in the expression. - * @return The resulting expression. - */ - static storm::expressions::Expression getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector const& variables); - - /*! - * Creates a DD that encapsulates the given CUDD ADD. - * - * @param ddManager The manager responsible for this DD. - * @param cuddDd The CUDD ADD to store. - * @param containedMetaVariables The meta variables that appear in the DD. - */ - Dd(std::shared_ptr const> ddManager, ADD cuddDd, std::set const& containedMetaVariables = std::set()); - - /*! - * Creates a DD that encapsulates the given CUDD ADD. + * Creates an ADD that encapsulates the given CUDD ADD. * * @param ddManager The manager responsible for this DD. - * @param cuddDd The CUDD ADD to store. + * @param cuddAdd The CUDD ADD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ - Dd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables = std::set()); + Add(std::shared_ptr const> ddManager, ADD cuddAdd, std::set const& containedMetaVariables = std::set()); /*! * Helper function to convert the DD into a (sparse) matrix. @@ -806,7 +602,7 @@ namespace storm { * @param maxLevel The number of levels that need to be considered. * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. */ - void splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const; + void splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const; /*! * Performs a recursive step to add the given DD-based vector to the given explicit vector. @@ -822,24 +618,10 @@ namespace storm { template void addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; - /*! - * Retrieves the indices of all DD variables that are contained in this DD (not necessarily in the support, - * because they could be "don't cares"). Additionally, the indices are sorted to allow for easy access. - * - * @return The (sorted) indices of all DD variables that are contained in this DD. - */ - std::vector getSortedVariableIndices() const; - - // A pointer to the manager responsible for this DD. - std::shared_ptr const> ddManager; - // The ADD created by CUDD. - boost::variant cuddDd; - - // The meta variables that appear in this DD. - std::set containedMetaVariables; + ADD cuddAdd; }; } } -#endif /* STORM_STORAGE_DD_CUDDDD_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DD_CUDDADD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/CuddBdd.cpp b/src/storage/dd/CuddBdd.cpp index dd095af21..b311682f8 100644 --- a/src/storage/dd/CuddBdd.cpp +++ b/src/storage/dd/CuddBdd.cpp @@ -5,9 +5,12 @@ #include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/CuddDdManager.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + namespace storm { namespace dd { - Bdd::Bdd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables) { + Bdd::Bdd(std::shared_ptr const> ddManager, BDD cuddBdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), cuddBdd(cuddBdd) { // Intentionally left empty. } @@ -47,10 +50,11 @@ namespace storm { Bdd& Bdd::complement() { this->cuddBdd = ~this->getCuddBdd(); + return *this; } Bdd Bdd::operator&&(Bdd const& other) const { - Dd result(*this); + Bdd result(*this); result &= other; return result; } @@ -92,7 +96,7 @@ namespace storm { } Bdd Bdd::existsAbstract(std::set const& metaVariables) const { - Dd cubeDd(this->getDdManager()->getBddOne()); + Bdd cubeBdd = this->getDdManager()->getBddOne(); std::set newMetaVariables = this->getContainedMetaVariables(); for (auto const& metaVariable : metaVariables) { @@ -101,14 +105,14 @@ namespace storm { newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd &= ddMetaVariable.getCube(); + cubeBdd &= ddMetaVariable.getCube(); } - return Bdd(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), newMetaVariables); + return Bdd(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeBdd.getCuddBdd()), newMetaVariables); } - Dd Bdd::universalAbstract(std::set const& metaVariables) const { - Dd cubeDd(this->getDdManager()->getBddOne()); + Bdd Bdd::universalAbstract(std::set const& metaVariables) const { + Bdd cubeBdd = this->getDdManager()->getBddOne(); std::set newMetaVariables = this->getContainedMetaVariables(); for (auto const& metaVariable : metaVariables) { @@ -117,13 +121,13 @@ namespace storm { newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd &= ddMetaVariable.getCube(); + cubeBdd &= ddMetaVariable.getCube(); } - return Bdd(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables); + return Bdd(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeBdd.getCuddBdd()), newMetaVariables); } - Dd Bdd::swapVariables(std::vector> const& metaVariablePairs) { + Bdd Bdd::swapVariables(std::vector> const& metaVariablePairs) { std::set newContainedMetaVariables; std::vector from; std::vector to; @@ -156,12 +160,10 @@ namespace storm { } Bdd Bdd::andExists(Bdd const& other, std::set const& existentialVariables) const { - STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s)."); - - Dd cubeDd(this->getDdManager()->getOne()); + Bdd cubeBdd(this->getDdManager()->getBddOne()); for (auto const& metaVariable : existentialVariables) { DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd &= ddMetaVariable.getCube(); + cubeBdd &= ddMetaVariable.getCube(); } std::set unionOfMetaVariables; @@ -169,37 +171,23 @@ namespace storm { std::set containedMetaVariables; std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); - return Dd(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeDd.getCuddBdd()), containedMetaVariables); + return Bdd(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeBdd.getCuddBdd()), containedMetaVariables); } - Dd Bdd::constrain(Dd const& constraint) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); - - if (this->isBdd() && constraint.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables); - } else { - return Dd(this->getDdManager(), this->getCuddMtbdd().Constrain(constraint.getCuddMtbdd()), metaVariables); - } + Bdd Bdd::constrain(Bdd const& constraint) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Bdd(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables); } - Dd Bdd::restrict(Dd const& constraint) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); - - if (this->isBdd() && constraint.isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables); - } else { - return Dd(this->getDdManager(), this->getCuddMtbdd().Restrict(constraint.getCuddMtbdd()), metaVariables); - } + Bdd Bdd::restrict(Bdd const& constraint) const { + std::set metaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return Bdd(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables); } - Dd Bdd::getSupport() const { - if (this->isBdd()) { - return Dd(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables()); - } else { - return Dd(this->getDdManager(), this->getCuddMtbdd().Support(), this->getContainedMetaVariables()); - } + Bdd Bdd::getSupport() const { + return Bdd(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables()); } uint_fast64_t Bdd::getNonZeroCount() const { @@ -207,76 +195,33 @@ namespace storm { for (auto const& metaVariable : this->getContainedMetaVariables()) { numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); } - if (this->isBdd()) { - return static_cast(this->getCuddBdd().CountMinterm(static_cast(numberOfDdVariables))); - } else { - return static_cast(this->getCuddMtbdd().CountMinterm(static_cast(numberOfDdVariables))); - } + return static_cast(this->getCuddBdd().CountMinterm(static_cast(numberOfDdVariables))); } - + uint_fast64_t Bdd::getLeafCount() const { - if (this->isBdd()) { - return static_cast(this->getCuddBdd().CountLeaves()); - } else { - return static_cast(this->getCuddMtbdd().CountLeaves()); - } + return static_cast(this->getCuddBdd().CountLeaves()); } uint_fast64_t Bdd::getNodeCount() const { - if (this->isBdd()) { - return static_cast(this->getCuddBdd().nodeCount()); - } else { - return static_cast(this->getCuddMtbdd().nodeCount()); - } + return static_cast(this->getCuddBdd().nodeCount()); } bool Bdd::isOne() const { - if (this->isBdd()) { - return this->getCuddBdd().IsOne(); - } else { - return this->getCuddMtbdd().IsOne(); - } + return this->getCuddBdd().IsOne(); } bool Bdd::isZero() const { - if (this->isBdd()) { - return this->getCuddBdd().IsZero(); - } else { - return this->getCuddMtbdd().IsZero(); - } + return this->getCuddBdd().IsZero(); } uint_fast64_t Bdd::getIndex() const { - if (this->isBdd()) { - return static_cast(this->getCuddBdd().NodeReadIndex()); - } else { - return static_cast(this->getCuddMtbdd().NodeReadIndex()); - } - } - - std::vector Bdd::getSortedVariableIndices() const { - std::vector ddVariableIndices; - for (auto const& metaVariableName : this->getContainedMetaVariables()) { - auto const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddVariableIndices.push_back(ddVariable.getIndex()); - } - } - - // Next, we need to sort them, since they may be arbitrarily ordered otherwise. - std::sort(ddVariableIndices.begin(), ddVariableIndices.end()); - return ddVariableIndices; + return static_cast(this->getCuddBdd().NodeReadIndex()); } void Bdd::exportToDot(std::string const& filename) const { if (filename.empty()) { - if (this->isBdd()) { - std::vector cuddBddVector = { this->getCuddBdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddBddVector); - } else { - std::vector cuddAddVector = { this->getCuddMtbdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); - } + std::vector cuddBddVector = { this->getCuddBdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddBddVector); } else { // Build the name input of the DD. std::vector ddNames; @@ -294,13 +239,8 @@ namespace storm { // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); - if (this->isBdd()) { - std::vector cuddBddVector = { this->getCuddBdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); - } else { - std::vector cuddAddVector = { this->getCuddMtbdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); - } + std::vector cuddBddVector = { this->getCuddBdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); fclose(filePointer); // Finally, delete the names. @@ -313,8 +253,8 @@ namespace storm { } } - std::ostream& operator<<(std::ostream& out, const Dd& dd) { - dd.exportToDot(); + std::ostream& operator<<(std::ostream& out, const Bdd& bdd) { + bdd.exportToDot(); return out; } } diff --git a/src/storage/dd/CuddBdd.h b/src/storage/dd/CuddBdd.h index 19335a3f4..7ba62cceb 100644 --- a/src/storage/dd/CuddBdd.h +++ b/src/storage/dd/CuddBdd.h @@ -23,6 +23,7 @@ namespace storm { // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. friend class DdManager; friend class DdForwardIterator; + friend class Add; friend class Odd; // Instantiate all copy/move constructors/assignments with the default implementation. @@ -198,6 +199,13 @@ namespace storm { */ virtual uint_fast64_t getNonZeroCount() const override; + /*! + * Retrieves the number of leaves of the DD. + * + * @return The number of leaves of the DD. + */ + virtual uint_fast64_t getLeafCount() const override; + /*! * Retrieves the number of nodes necessary to represent the DD. * @@ -261,10 +269,10 @@ namespace storm { * Creates a DD that encapsulates the given CUDD ADD. * * @param ddManager The manager responsible for this DD. - * @param cuddDd The CUDD ADD to store. + * @param cuddBdd The CUDD BDD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ - Bdd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables = std::set()); + Bdd(std::shared_ptr const> ddManager, BDD cuddBdd, std::set const& containedMetaVariables = std::set()); // The BDD created by CUDD. BDD cuddBdd; diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 3ec7328f4..43e2afd3f 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -48,5 +48,19 @@ namespace storm { std::set_difference(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin())); containedMetaVariables = std::move(result); } + + std::vector Dd::getSortedVariableIndices() const { + std::vector ddVariableIndices; + for (auto const& metaVariableName : this->getContainedMetaVariables()) { + auto const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddVariableIndices.push_back(ddVariable.getIndex()); + } + } + + // Next, we need to sort them, since they may be arbitrarily ordered otherwise. + std::sort(ddVariableIndices.begin(), ddVariableIndices.end()); + return ddVariableIndices; + } } } \ No newline at end of file diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 197d2454c..fdeb085ef 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -104,7 +104,14 @@ namespace storm { * A pointer to the manager that is responsible for this DD. */ std::shared_ptr const> getDdManager() const; - + + /*! + * Retrieves the (sorted) list of the variable indices of DD variables contained in this DD. + * + * @return The sorted list of variable indices. + */ + std::vector getSortedVariableIndices() const; + protected: /*! diff --git a/src/storage/dd/CuddDdForwardIterator.h b/src/storage/dd/CuddDdForwardIterator.h index 228c8e1b4..e6498458d 100644 --- a/src/storage/dd/CuddDdForwardIterator.h +++ b/src/storage/dd/CuddDdForwardIterator.h @@ -17,12 +17,12 @@ namespace storm { namespace dd { // Forward-declare the DdManager class. template class DdManager; - template class Dd; + template class Add; template<> class DdForwardIterator { public: - friend class Dd; + friend class Add; // Default-instantiate the constructor. DdForwardIterator(); diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index a844075ce..63a84a58b 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -37,27 +37,28 @@ namespace storm { } } - Dd DdManager::getOne(bool asMtbdd) const { - if (asMtbdd) { - return Dd(this->shared_from_this(), cuddManager.addOne()); - } else { - return Dd(this->shared_from_this(), cuddManager.bddOne()); - } + Bdd DdManager::getBddOne() const { + return Bdd(this->shared_from_this(), cuddManager.bddOne()); + } + + Add DdManager::getAddOne() const { + return Add(this->shared_from_this(), cuddManager.addOne()); } - Dd DdManager::getZero(bool asMtbdd) const { - if (asMtbdd) { - return Dd(this->shared_from_this(), cuddManager.addZero()); - } else { - return Dd(this->shared_from_this(), cuddManager.bddZero()); - } + Bdd DdManager::getBddZero() const { + return Bdd(this->shared_from_this(), cuddManager.bddZero()); } - Dd DdManager::getConstant(double value) const { - return Dd(this->shared_from_this(), cuddManager.constant(value)); + Add DdManager::getAddZero() const { + return Add(this->shared_from_this(), cuddManager.addZero()); } - Dd DdManager::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value, bool asMtbdd) const { + + Add DdManager::getConstant(double value) const { + return Add(this->shared_from_this(), cuddManager.constant(value)); + } + + Bdd DdManager::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const { DdMetaVariable const& metaVariable = this->getMetaVariable(variable); STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'."); @@ -65,9 +66,9 @@ namespace storm { // Now compute the encoding relative to the low value of the meta variable. value -= metaVariable.getLow(); - std::vector> const& ddVariables = metaVariable.getDdVariables(); + std::vector> const& ddVariables = metaVariable.getDdVariables(); - Dd result; + Bdd result; if (value & (1ull << (ddVariables.size() - 1))) { result = ddVariables[0]; } else { @@ -82,31 +83,27 @@ namespace storm { } } - if (asMtbdd) { - return result.toMtbdd(); - } else { - return result; - } + return result; } - Dd DdManager::getRange(storm::expressions::Variable const& variable, bool asMtbdd) const { + Bdd DdManager::getRange(storm::expressions::Variable const& variable) const { storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - Dd result = this->getZero(asMtbdd); + Bdd result = this->getBddZero(); for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { - result.setValue(variable, value, static_cast(1)); + result |= this->getEncoding(variable, value); } return result; } - Dd DdManager::getIdentity(storm::expressions::Variable const& variable) const { + Add DdManager::getIdentity(storm::expressions::Variable const& variable) const { storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - Dd result = this->getZero(true); + Add result = this->getAddZero(); for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { - result.setValue(variable, value, static_cast(value)); + result += this->getEncoding(variable, value).toAdd() * this->getConstant(value); } return result; } @@ -126,11 +123,11 @@ namespace storm { storm::expressions::Variable unprimed = manager->declareBitVectorVariable(name, numberOfBits); storm::expressions::Variable primed = manager->declareBitVectorVariable(name + "'", numberOfBits); - std::vector> variables; - std::vector> variablesPrime; + std::vector> variables; + std::vector> variablesPrime; for (std::size_t i = 0; i < numberOfBits; ++i) { - variables.emplace_back(Dd(this->shared_from_this(), cuddManager.bddVar(), {unprimed})); - variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.bddVar(), {primed})); + variables.emplace_back(Bdd(this->shared_from_this(), cuddManager.bddVar(), {unprimed})); + variablesPrime.emplace_back(Bdd(this->shared_from_this(), cuddManager.bddVar(), {primed})); } // Now group the non-primed and primed variable. @@ -154,10 +151,10 @@ namespace storm { storm::expressions::Variable unprimed = manager->declareBooleanVariable(name); storm::expressions::Variable primed = manager->declareBooleanVariable(name + "'"); - std::vector> variables; - std::vector> variablesPrime; - variables.emplace_back(Dd(this->shared_from_this(), cuddManager.bddVar(), {unprimed})); - variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.bddVar(), {primed})); + std::vector> variables; + std::vector> variablesPrime; + variables.emplace_back(Bdd(this->shared_from_this(), cuddManager.bddVar(), {unprimed})); + variablesPrime.emplace_back(Bdd(this->shared_from_this(), cuddManager.bddVar(), {primed})); // Now group the non-primed and primed variable. this->getCuddManager().MakeTreeNode(variables.front().getIndex(), 2, MTR_FIXED); diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 4926e792c..07c11eb19 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -18,7 +18,8 @@ namespace storm { template<> class DdManager : public std::enable_shared_from_this> { public: - friend class Dd; + friend class Bdd; + friend class Add; friend class Odd; friend class DdForwardIterator; @@ -36,58 +37,68 @@ namespace storm { #endif /*! - * Retrieves a DD representing the constant one function. If the flag is set, the result will be given in - * terms of an MTBDD rather than a BDD. + * Retrieves a BDD representing the constant one function. * - * @return A DD representing the constant one function. + * @return A BDD representing the constant one function. */ - Dd getOne(bool asMtbdd = false) const; + Bdd getBddOne() const; /*! - * Retrieves a DD representing the constant zero function. If the flag is set, the result will be given in - * terms of an MTBDD rather than a BDD. + * Retrieves an ADD representing the constant one function. * - * @return A DD representing the constant zero function. + * @return An ADD representing the constant one function. */ - Dd getZero(bool asMtbdd = false) const; + Add getAddOne() const; /*! - * Retrieves a DD representing the constant function with the given value. + * Retrieves a BDD representing the constant zero function. * - * @return A DD representing the constant function with the given value. + * @return A BDD representing the constant zero function. */ - Dd getConstant(double value) const; + Bdd getBddZero() const; /*! - * Retrieves the DD representing the function that maps all inputs which have the given meta variable equal + * Retrieves an ADD representing the constant zero function. + * + * @return An ADD representing the constant zero function. + */ + Add getAddZero() const; + + /*! + * Retrieves an ADD representing the constant function with the given value. + * + * @return An ADD representing the constant function with the given value. + */ + Add getConstant(double value) const; + + /*! + * Retrieves the BDD representing the function that maps all inputs which have the given meta variable equal * to the given value one. * * @param variable The expression variable associated with the meta variable. * @param value The value the meta variable is supposed to have. - * @param asMtbdd If set to true, the result will be given in terms of an MTBDD. * @return The DD representing the function that maps all inputs which have the given meta variable equal * to the given value one. */ - Dd getEncoding(storm::expressions::Variable const& variable, int_fast64_t value, bool asMtbdd = false) const; + Bdd getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const; /*! - * Retrieves the DD representing the range of the meta variable, i.e., a function that maps all legal values + * Retrieves the BDD representing the range of the meta variable, i.e., a function that maps all legal values * of the range of the meta variable to one. * * @param variable The expression variable associated with the meta variable. - * @param asMtbdd If set to true, the result will be given in terms of an MTBDD. * @return The range of the meta variable. */ - Dd getRange(storm::expressions::Variable const& variable, bool asMtbdd = false) const; + Bdd getRange(storm::expressions::Variable const& variable) const; /*! - * Retrieves the DD representing the identity of the meta variable, i.e., a function that maps all legal + * Retrieves the ADD representing the identity of the meta variable, i.e., a function that maps all legal * values of the range of the meta variable to themselves. * * @param variable The expression variable associated with the meta variable. * @return The identity of the meta variable. */ - Dd getIdentity(storm::expressions::Variable const& variable) const; + Add getIdentity(storm::expressions::Variable const& variable) const; /*! * Adds an integer meta variable with the given range. diff --git a/src/storage/dd/CuddDdMetaVariable.cpp b/src/storage/dd/CuddDdMetaVariable.cpp index a53465682..4784f7235 100644 --- a/src/storage/dd/CuddDdMetaVariable.cpp +++ b/src/storage/dd/CuddDdMetaVariable.cpp @@ -3,20 +3,18 @@ namespace storm { namespace dd { - DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), cubeAsMtbdd(manager->getOne(true)), manager(manager) { + DdMetaVariable::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getBddOne()), manager(manager) { // Create the cube of all variables of this meta variable. for (auto const& ddVariable : this->ddVariables) { this->cube &= ddVariable; } - this->cubeAsMtbdd = this->cube.toMtbdd(); } - DdMetaVariable::DdMetaVariable(std::string const& name, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables), cube(manager->getOne()), cubeAsMtbdd(manager->getOne(true)), manager(manager) { + DdMetaVariable::DdMetaVariable(std::string const& name, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables), cube(manager->getBddOne()), manager(manager) { // Create the cube of all variables of this meta variable. for (auto const& ddVariable : this->ddVariables) { this->cube &= ddVariable; } - this->cubeAsMtbdd = this->cube.toMtbdd(); } std::string const& DdMetaVariable::getName() const { @@ -43,17 +41,12 @@ namespace storm { return this->manager; } - std::vector> const& DdMetaVariable::getDdVariables() const { + std::vector> const& DdMetaVariable::getDdVariables() const { return this->ddVariables; } - Dd const& DdMetaVariable::getCube() const { + Bdd const& DdMetaVariable::getCube() const { return this->cube; } - - Dd const& DdMetaVariable::getCubeAsMtbdd() const { - return this->cubeAsMtbdd; - } - } } \ No newline at end of file diff --git a/src/storage/dd/CuddDdMetaVariable.h b/src/storage/dd/CuddDdMetaVariable.h index aeea15389..4f016a6ce 100644 --- a/src/storage/dd/CuddDdMetaVariable.h +++ b/src/storage/dd/CuddDdMetaVariable.h @@ -7,8 +7,10 @@ #include #include "utility/OsDetection.h" -#include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/DdMetaVariable.h" +#include "src/storage/dd/CuddDdForwardIterator.h" #include "src/storage/expressions/Expression.h" namespace storm { @@ -23,6 +25,8 @@ namespace storm { // Declare the DdManager class as friend so it can access the internals of a meta variable. friend class DdManager; friend class Dd; + friend class Bdd; + friend class Add; friend class Odd; friend class DdForwardIterator; @@ -38,7 +42,7 @@ namespace storm { * @param ddVariables The vector of variables used to encode this variable. * @param manager A pointer to the manager that is responsible for this meta variable. */ - DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager); + DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector> const& ddVariables, std::shared_ptr> manager); /*! * Creates a boolean meta variable with the given name. @@ -46,7 +50,7 @@ namespace storm { * @param ddVariables The vector of variables used to encode this variable. * @param manager A pointer to the manager that is responsible for this meta variable. */ - DdMetaVariable(std::string const& name, std::vector> const& ddVariables, std::shared_ptr> manager); + DdMetaVariable(std::string const& name, std::vector> const& ddVariables, std::shared_ptr> manager); // Explictly generate all default versions of copy/move constructors/assignments. DdMetaVariable(DdMetaVariable const& other) = default; @@ -104,21 +108,14 @@ namespace storm { * * @return A vector of variables used to encode the meta variable. */ - std::vector> const& getDdVariables() const; + std::vector> const& getDdVariables() const; /*! * Retrieves the cube of all variables that encode this meta variable. * * @return The cube of all variables that encode this meta variable. */ - Dd const& getCube() const; - - /*! - * Retrieves the cube of all variables that encode this meta variable represented as an MTBDD. - * - * @return The cube of all variables that encode this meta variable. - */ - Dd const& getCubeAsMtbdd() const; + Bdd const& getCube() const; // The name of the meta variable. std::string name; @@ -133,14 +130,10 @@ namespace storm { int_fast64_t high; // The vector of variables that are used to encode the meta variable. - std::vector> ddVariables; + std::vector> ddVariables; // The cube consisting of all variables that encode the meta variable. - Dd cube; - - // The cube consisting of all variables that encode the meta variable represented by an MTBDD. This is - // used as a shortcut mainly for the abstraction methods. - Dd cubeAsMtbdd; + Bdd cube; // A pointer to the manager responsible for this meta variable. std::shared_ptr> manager; diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp index 8e489ec03..342f7458a 100644 --- a/src/storage/dd/CuddOdd.cpp +++ b/src/storage/dd/CuddOdd.cpp @@ -7,18 +7,18 @@ namespace storm { namespace dd { - Odd::Odd(Dd const& dd) { - std::shared_ptr const> manager = dd.getDdManager(); + Odd::Odd(Add const& add) { + std::shared_ptr const> manager = add.getDdManager(); // First, we need to determine the involved DD variables indices. - std::vector ddVariableIndices = dd.getSortedVariableIndices(); + std::vector ddVariableIndices = add.getSortedVariableIndices(); // Prepare a unique table for each level that keeps the constructed ODD nodes unique. std::vector>>> uniqueTableForLevels(ddVariableIndices.size() + 1); // Now construct the ODD structure. // Currently, the DD needs to be an MTBDD, because complement edges are not supported. - std::shared_ptr> rootOdd = buildOddRec(dd.toMtbdd().getCuddDdNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); + std::shared_ptr> rootOdd = buildOddRec(add.getCuddDdNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); // Finally, move the children of the root ODD into this ODD. this->elseNode = std::move(rootOdd->elseNode); diff --git a/src/storage/dd/CuddOdd.h b/src/storage/dd/CuddOdd.h index c12dfb67c..9d93d6e47 100644 --- a/src/storage/dd/CuddOdd.h +++ b/src/storage/dd/CuddOdd.h @@ -4,7 +4,7 @@ #include #include "src/storage/dd/Odd.h" -#include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddAdd.h" #include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. @@ -18,9 +18,9 @@ namespace storm { /*! * Constructs an offset-labeled DD from the given DD. * - * @param dd The DD for which to build the offset-labeled DD. + * @param add The ADD for which to build the offset-labeled DD. */ - Odd(Dd const& dd); + Odd(Add const& add); // Instantiate all copy/move constructors/assignments with the default implementation. Odd() = default; diff --git a/src/utility/graph.h b/src/utility/graph.h index 8eff8179d..13d30f34f 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -259,24 +259,24 @@ namespace storm { * * @param model The (symbolic) model for which to compute the set of states. * @param transitionMatrixBdd The transition matrix of the model as a BDD. - * @param phiStatesBdd The BDD containing all phi states of the model. - * @param psiStatesBdd The BDD containing all psi states of the model. + * @param phiStates The BDD containing all phi states of the model. + * @param psiStates The BDD containing all psi states of the model. * @return All states with positive probability. */ template - storm::dd::Dd performProbGreater0(storm::models::symbolic::DeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { + storm::dd::Bdd performProbGreater0(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); - storm::dd::Dd lastIterationStates = manager.getZero(); - storm::dd::Dd statesWithProbabilityGreater0 = psiStatesBdd; + storm::dd::Bdd lastIterationStates = manager.getBddZero(); + storm::dd::Bdd statesWithProbabilityGreater0 = psiStates; uint_fast64_t iterations = 0; while (lastIterationStates != statesWithProbabilityGreater0) { lastIterationStates = statesWithProbabilityGreater0; statesWithProbabilityGreater0 = statesWithProbabilityGreater0.swapVariables(model.getRowColumnMetaVariablePairs()); - statesWithProbabilityGreater0 &= transitionMatrixBdd; + statesWithProbabilityGreater0 &= transitionMatrix; statesWithProbabilityGreater0 = statesWithProbabilityGreater0.existsAbstract(model.getColumnVariables()); - statesWithProbabilityGreater0 &= phiStatesBdd; + statesWithProbabilityGreater0 &= phiStates; statesWithProbabilityGreater0 |= lastIterationStates; ++iterations; } @@ -289,17 +289,16 @@ namespace storm { * deterministic model. * * @param model The (symbolic) model for which to compute the set of states. - * @param transitionMatrixBdd The transition matrix of the model as a BDD. - * @param phiStatesBdd The BDD containing all phi states of the model. - * @param psiStatesBdd The BDD containing all psi states of the model. - * @return A pair of DDs that represent all states with probability 0 and 1, respectively. + * @param phiStates The BDD containing all phi states of the model. + * @param psiStates The BDD containing all psi states of the model. + * @return A pair of BDDs that represent all states with probability 0 and 1, respectively. */ template - static std::pair, storm::dd::Dd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { - std::pair, storm::dd::Dd> result; - storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); - result.first = performProbGreater0(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd); - result.second = !performProbGreater0(model, transitionMatrixBdd, !psiStatesBdd && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates(); + static std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + std::pair, storm::dd::Bdd> result; + storm::dd::Bdd transitionMatrix = model.getTransitionMatrix().notZero(); + result.first = performProbGreater0(model, transitionMatrix, phiStates, psiStates); + result.second = !performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates(); result.first = !result.first && model.getReachableStates(); return result; } @@ -706,25 +705,25 @@ namespace storm { * zero of satisfying phi until psi. * * @param model The (symbolic) model for which to compute the set of states. - * @param transitionMatrixBdd The transition matrix of the model as a BDD. - * @param phiStatesBdd The BDD containing all phi states of the model. - * @param psiStatesBdd The BDD containing all psi states of the model. - * @return A DD representing all such states. + * @param transitionMatrix The transition matrix of the model as a BDD. + * @param phiStates The BDD containing all phi states of the model. + * @param psiStates The BDD containing all psi states of the model. + * @return A BDD representing all such states. */ template - storm::dd::Dd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { + storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); - storm::dd::Dd lastIterationStates = manager.getZero(); - storm::dd::Dd statesWithProbabilityGreater0E = psiStatesBdd; + storm::dd::Bdd lastIterationStates = manager.getBddZero(); + storm::dd::Bdd statesWithProbabilityGreater0E = psiStates; uint_fast64_t iterations = 0; - storm::dd::Dd abstractedTransitionMatrixBdd = transitionMatrixBdd.existsAbstract(model.getNondeterminismVariables()); + storm::dd::Bdd abstractedTransitionMatrix = transitionMatrix.existsAbstract(model.getNondeterminismVariables()); while (lastIterationStates != statesWithProbabilityGreater0E) { lastIterationStates = statesWithProbabilityGreater0E; statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.swapVariables(model.getRowColumnMetaVariablePairs()); - statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.andExists(abstractedTransitionMatrixBdd, model.getColumnVariables()); - statesWithProbabilityGreater0E &= phiStatesBdd; + statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.andExists(abstractedTransitionMatrix, model.getColumnVariables()); + statesWithProbabilityGreater0E &= phiStates; statesWithProbabilityGreater0E |= lastIterationStates; ++iterations; } @@ -737,14 +736,14 @@ namespace storm { * than zero of satisfying phi until psi. * * @param model The (symbolic) model for which to compute the set of states. - * @param transitionMatrixBdd The transition matrix of the model as a BDD. + * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The phi states of the model. * @param psiStates The psi states of the model. - * @return A DD representing all such states. + * @return A BDD representing all such states. */ template - storm::dd::Dd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { - return !performProbGreater0E(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd) && model.getReachableStates(); + storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + return !performProbGreater0E(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates(); } /*! @@ -752,27 +751,27 @@ namespace storm { * phi until psi. * * @param model The (symbolic) model for which to compute the set of states. - * @param transitionMatrixBdd The transition matrix of the model as a BDD. - * @param phiStatesBdd The BDD containing all phi states of the model. - * @param psiStatesBdd The BDD containing all psi states of the model. - * @return A DD representing all such states. + * @param transitionMatrix The transition matrix of the model as a BDD. + * @param phiStates The BDD containing all phi states of the model. + * @param psiStates The BDD containing all psi states of the model. + * @return A BDD representing all such states. */ template - storm::dd::Dd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { + storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); - storm::dd::Dd lastIterationStates = manager.getZero(); - storm::dd::Dd statesWithProbabilityGreater0A = psiStatesBdd; + storm::dd::Bdd lastIterationStates = manager.getBddZero(); + storm::dd::Bdd statesWithProbabilityGreater0A = psiStates; uint_fast64_t iterations = 0; while (lastIterationStates != statesWithProbabilityGreater0A) { lastIterationStates = statesWithProbabilityGreater0A; statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.swapVariables(model.getRowColumnMetaVariablePairs()); - statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.andExists(transitionMatrixBdd, model.getColumnVariables()); + statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.andExists(transitionMatrix, model.getColumnVariables()); statesWithProbabilityGreater0A |= model.getIllegalMask(); statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.universalAbstract(model.getNondeterminismVariables()); - statesWithProbabilityGreater0A &= phiStatesBdd; - statesWithProbabilityGreater0A |= psiStatesBdd; + statesWithProbabilityGreater0A &= phiStates; + statesWithProbabilityGreater0A |= psiStates; ++iterations; } @@ -784,43 +783,43 @@ namespace storm { * phi until psi. * * @param model The (symbolic) model for which to compute the set of states. - * @param transitionMatrixBdd The transition matrix of the model as a BDD. - * @param phiStatesBdd The BDD containing all phi states of the model. - * @param psiStatesBdd The BDD containing all psi states of the model. - * @return A DD representing all such states. + * @param transitionMatrix The transition matrix of the model as a BDD. + * @param phiStates The BDD containing all phi states of the model. + * @param psiStates The BDD containing all psi states of the model. + * @return A BDD representing all such states. */ template - storm::dd::Dd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { - return !performProbGreater0A(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd) && model.getReachableStates(); + storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + return !performProbGreater0A(model, transitionMatrix, phiStates, psiStates) && model.getReachableStates(); } /*! * Computes the set of states for which all schedulers achieve probability one of satisfying phi until psi. * * @param model The (symbolic) model for which to compute the set of states. - * @param transitionMatrixBdd The transition matrix of the model as a BDD. - * @param phiStatesBdd The BDD containing all phi states of the model. - * @param psiStatesBdd The BDD containing all psi states of the model. + * @param transitionMatrix The transition matrix of the model as a BDD. + * @param phiStates The BDD containing all phi states of the model. + * @param psiStates The BDD containing all psi states of the model. * @param statesWithProbabilityGreater0A The states of the model that have a probability greater zero under * all schedulers. - * @return A DD representing all such states. + * @return A BDD representing all such states. */ template - storm::dd::Dd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd, storm::dd::Dd const& statesWithProbabilityGreater0A) { + storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); - storm::dd::Dd lastIterationStates = manager.getZero(); - storm::dd::Dd statesWithProbability1A = psiStatesBdd || statesWithProbabilityGreater0A; + storm::dd::Bdd lastIterationStates = manager.getBddZero(); + storm::dd::Bdd statesWithProbability1A = psiStates || statesWithProbabilityGreater0A; uint_fast64_t iterations = 0; while (lastIterationStates != statesWithProbability1A) { lastIterationStates = statesWithProbability1A; statesWithProbability1A = statesWithProbability1A.swapVariables(model.getRowColumnMetaVariablePairs()); - statesWithProbability1A = transitionMatrixBdd.implies(statesWithProbability1A).universalAbstract(model.getColumnVariables()); + statesWithProbability1A = transitionMatrix.implies(statesWithProbability1A).universalAbstract(model.getColumnVariables()); statesWithProbability1A |= model.getIllegalMask(); statesWithProbability1A = statesWithProbability1A.universalAbstract(model.getNondeterminismVariables()); statesWithProbability1A &= statesWithProbabilityGreater0A; - statesWithProbability1A |= psiStatesBdd; + statesWithProbability1A |= psiStates; ++iterations; } @@ -832,35 +831,35 @@ namespace storm { * phi until psi. * * @param model The (symbolic) model for which to compute the set of states. - * @param transitionMatrixBdd The transition matrix of the model as a BDD. - * @param phiStatesBdd The BDD containing all phi states of the model. - * @param psiStatesBdd The BDD containing all psi states of the model. + * @param transitionMatrix The transition matrix of the model as a BDD. + * @param phiStates The BDD containing all phi states of the model. + * @param psiStates The BDD containing all psi states of the model. * @param statesWithProbabilityGreater0E The states of the model that have a scheduler that achieves a value * greater than zero. - * @return A DD representing all such states. + * @return A BDD representing all such states. */ template - storm::dd::Dd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& transitionMatrixBdd, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd, storm::dd::Dd const& statesWithProbabilityGreater0E) { + storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); - storm::dd::Dd statesWithProbability1E = statesWithProbabilityGreater0E; + storm::dd::Bdd statesWithProbability1E = statesWithProbabilityGreater0E; uint_fast64_t iterations = 0; bool outerLoopDone = false; while (!outerLoopDone) { - storm::dd::Dd innerStates = manager.getZero(); + storm::dd::Bdd innerStates = manager.getBddZero(); bool innerLoopDone = false; while (!innerLoopDone) { - storm::dd::Dd temporary = statesWithProbability1E.swapVariables(model.getRowColumnMetaVariablePairs()); - temporary = transitionMatrixBdd.implies(temporary).universalAbstract(model.getColumnVariables()); + storm::dd::Bdd temporary = statesWithProbability1E.swapVariables(model.getRowColumnMetaVariablePairs()); + temporary = transitionMatrix.implies(temporary).universalAbstract(model.getColumnVariables()); - storm::dd::Dd temporary2 = innerStates.swapVariables(model.getRowColumnMetaVariablePairs()); - temporary2 = transitionMatrixBdd.andExists(temporary2, model.getColumnVariables()); + storm::dd::Bdd temporary2 = innerStates.swapVariables(model.getRowColumnMetaVariablePairs()); + temporary2 = transitionMatrix.andExists(temporary2, model.getColumnVariables()); temporary = temporary.andExists(temporary2, model.getNondeterminismVariables()); - temporary &= phiStatesBdd; - temporary |= psiStatesBdd; + temporary &= phiStates; + temporary |= psiStates; if (innerStates == temporary) { innerLoopDone = true; @@ -881,20 +880,20 @@ namespace storm { } template - std::pair, storm::dd::Dd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { - std::pair, storm::dd::Dd> result; - storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); - result.first = performProb0A(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd); - result.second = performProb1E(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd, !result.first && model.getReachableStates()); + std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + std::pair, storm::dd::Bdd> result; + storm::dd::Bdd transitionMatrix = model.getTransitionMatrix().notZero(); + result.first = performProb0A(model, transitionMatrix, phiStates, psiStates); + result.second = performProb1E(model, transitionMatrix, phiStates, psiStates, !result.first && model.getReachableStates()); return result; } template - std::pair, storm::dd::Dd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Dd const& phiStatesBdd, storm::dd::Dd const& psiStatesBdd) { - std::pair, storm::dd::Dd> result; - storm::dd::Dd transitionMatrixBdd = model.getTransitionMatrix().notZero(); - result.first = performProb0E(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd); - result.second = performProb1A(model, transitionMatrixBdd, phiStatesBdd, psiStatesBdd, !result.first && model.getReachableStates()); + std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + std::pair, storm::dd::Bdd> result; + storm::dd::Bdd transitionMatrix = model.getTransitionMatrix().notZero(); + result.first = performProb0E(model, transitionMatrix, phiStates, psiStates); + result.second = performProb1A(model, transitionMatrix, phiStates, psiStates, !result.first && model.getReachableStates()); return result; } diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 773334797..654283a90 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -2,14 +2,14 @@ #include "storm-config.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/storage/dd/CuddDdManager.h" -#include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/DdMetaVariable.h" TEST(CuddDdManager, Constants) { std::shared_ptr> manager(new storm::dd::DdManager()); - storm::dd::Dd zero; - ASSERT_NO_THROW(zero = manager->getZero()); + storm::dd::Add zero; + ASSERT_NO_THROW(zero = manager->getAddZero()); EXPECT_EQ(0, zero.getNonZeroCount()); EXPECT_EQ(1, zero.getLeafCount()); @@ -17,8 +17,8 @@ TEST(CuddDdManager, Constants) { EXPECT_EQ(0, zero.getMin()); EXPECT_EQ(0, zero.getMax()); - storm::dd::Dd one; - ASSERT_NO_THROW(one = manager->getOne()); + storm::dd::Add one; + ASSERT_NO_THROW(one = manager->getAddOne()); EXPECT_EQ(1, one.getNonZeroCount()); EXPECT_EQ(1, one.getLeafCount()); @@ -26,7 +26,7 @@ TEST(CuddDdManager, Constants) { EXPECT_EQ(1, one.getMin()); EXPECT_EQ(1, one.getMax()); - storm::dd::Dd two; + storm::dd::Add two; ASSERT_NO_THROW(two = manager->getConstant(2)); EXPECT_EQ(1, two.getNonZeroCount()); @@ -57,7 +57,7 @@ TEST(CuddDdManager, EncodingTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Dd encoding; + storm::dd::Bdd encoding; ASSERT_THROW(encoding = manager->getEncoding(x.first, 0), storm::exceptions::InvalidArgumentException); ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4)); @@ -69,8 +69,8 @@ TEST(CuddDdManager, EncodingTest) { EXPECT_EQ(1, encoding.getLeafCount()); // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6. - EXPECT_EQ(6, encoding.toMtbdd().getNodeCount()); - EXPECT_EQ(2, encoding.toMtbdd().getLeafCount()); + EXPECT_EQ(6, encoding.toAdd().getNodeCount()); + EXPECT_EQ(2, encoding.toAdd().getLeafCount()); } TEST(CuddDdManager, RangeTest) { @@ -78,7 +78,7 @@ TEST(CuddDdManager, RangeTest) { std::pair x; ASSERT_NO_THROW(x = manager->addMetaVariable("x", 1, 9)); - storm::dd::Dd range; + storm::dd::Bdd range; ASSERT_NO_THROW(range = manager->getRange(x.first)); EXPECT_EQ(9, range.getNonZeroCount()); @@ -90,29 +90,29 @@ TEST(CuddDdManager, IdentityTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Dd range; - ASSERT_NO_THROW(range = manager->getIdentity(x.first)); + storm::dd::Add identity; + ASSERT_NO_THROW(identity = manager->getIdentity(x.first)); - EXPECT_EQ(9, range.getNonZeroCount()); - EXPECT_EQ(10, range.getLeafCount()); - EXPECT_EQ(21, range.getNodeCount()); + EXPECT_EQ(9, identity.getNonZeroCount()); + EXPECT_EQ(10, identity.getLeafCount()); + EXPECT_EQ(21, identity.getNodeCount()); } TEST(CuddDd, OperatorTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - EXPECT_TRUE(manager->getZero() == manager->getZero()); - EXPECT_FALSE(manager->getZero() == manager->getOne()); + EXPECT_TRUE(manager->getAddZero() == manager->getAddZero()); + EXPECT_FALSE(manager->getAddZero() == manager->getAddOne()); - EXPECT_FALSE(manager->getZero() != manager->getZero()); - EXPECT_TRUE(manager->getZero() != manager->getOne()); + EXPECT_FALSE(manager->getAddZero() != manager->getAddZero()); + EXPECT_TRUE(manager->getAddZero() != manager->getAddOne()); - storm::dd::Dd dd1 = manager->getOne(true); - storm::dd::Dd dd2 = manager->getOne(true); - storm::dd::Dd dd3 = dd1 + dd2; + storm::dd::Add dd1 = manager->getAddOne(); + storm::dd::Add dd2 = manager->getAddOne(); + storm::dd::Add dd3 = dd1 + dd2; EXPECT_TRUE(dd3 == manager->getConstant(2)); - dd3 += manager->getZero(true); + dd3 += manager->getAddZero(); EXPECT_TRUE(dd3 == manager->getConstant(2)); dd3 = dd1 * manager->getConstant(3); @@ -130,13 +130,13 @@ TEST(CuddDd, OperatorTest) { dd3 /= manager->getConstant(2); EXPECT_TRUE(dd3.isOne()); - dd3 = dd3.toBdd().complement(); + dd3 = !dd3; EXPECT_TRUE(dd3.isZero()); dd1 = !dd3; EXPECT_TRUE(dd1.isOne()); - dd3 = dd1 || dd2.toBdd(); + dd3 = dd1 || dd2; EXPECT_TRUE(dd3.isOne()); dd1 = manager->getIdentity(x.first); @@ -145,7 +145,7 @@ TEST(CuddDd, OperatorTest) { dd3 = dd1.equals(dd2); EXPECT_EQ(1, dd3.getNonZeroCount()); - storm::dd::Dd dd4 = dd1.notEquals(dd2); + storm::dd::Add dd4 = dd1.notEquals(dd2); EXPECT_TRUE(dd4.toBdd() == !dd3.toBdd()); dd3 = dd1.less(dd2); @@ -160,17 +160,17 @@ TEST(CuddDd, OperatorTest) { dd3 = dd1.greaterOrEqual(dd2); EXPECT_EQ(5, dd3.getNonZeroCount()); - dd3 = (manager->getEncoding(x.first, 2)).ite(dd2, dd1); + dd3 = (manager->getEncoding(x.first, 2).toAdd()).ite(dd2, dd1); dd4 = dd3.less(dd2); EXPECT_EQ(10, dd4.getNonZeroCount()); dd4 = dd3.minimum(dd1); - dd4 *= manager->getEncoding(x.first, 2, true); + dd4 *= manager->getEncoding(x.first, 2).toAdd(); dd4 = dd4.sumAbstract({x.first}); EXPECT_EQ(2, dd4.getValue()); dd4 = dd3.maximum(dd1); - dd4 *= manager->getEncoding(x.first, 2, true); + dd4 *= manager->getEncoding(x.first, 2).toAdd(); dd4 = dd4.sumAbstract({x.first}); EXPECT_EQ(5, dd4.getValue()); @@ -183,25 +183,26 @@ TEST(CuddDd, OperatorTest) { TEST(CuddDd, AbstractionTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Dd dd1; - storm::dd::Dd dd2; - storm::dd::Dd dd3; + storm::dd::Add dd1; + storm::dd::Add dd2; + storm::dd::Add dd3; dd1 = manager->getIdentity(x.first); dd2 = manager->getConstant(5); dd3 = dd1.equals(dd2); - EXPECT_EQ(1, dd3.getNonZeroCount()); - ASSERT_THROW(dd3 = dd3.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(dd3 = dd3.existsAbstract({x.first})); - EXPECT_EQ(1, dd3.getNonZeroCount()); - EXPECT_EQ(1, dd3.getMax()); + storm::dd::Bdd dd3Bdd = dd3.toBdd(); + EXPECT_EQ(1, dd3Bdd.getNonZeroCount()); + ASSERT_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.first})); + EXPECT_EQ(1, dd3Bdd.getNonZeroCount()); + EXPECT_EQ(1, dd3Bdd.toAdd().getMax()); dd3 = dd1.equals(dd2); dd3 *= manager->getConstant(3); EXPECT_EQ(1, dd3.getNonZeroCount()); - ASSERT_THROW(dd3 = dd3.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); - ASSERT_NO_THROW(dd3 = dd3.existsAbstract({x.first})); - EXPECT_TRUE(dd3.isOne()); + 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 *= manager->getConstant(3); @@ -230,8 +231,8 @@ TEST(CuddDd, SwapTest) { std::pair x = manager->addMetaVariable("x", 1, 9); std::pair z = manager->addMetaVariable("z", 2, 8); - storm::dd::Dd dd1; - storm::dd::Dd dd2; + storm::dd::Add dd1; + storm::dd::Add dd2; dd1 = manager->getIdentity(x.first); ASSERT_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, z.first)}), storm::exceptions::InvalidArgumentException); @@ -243,9 +244,9 @@ TEST(CuddDd, MultiplyMatrixTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Dd dd1 = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)); - storm::dd::Dd dd2 = manager->getRange(x.second); - storm::dd::Dd dd3; + storm::dd::Add dd1 = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)); + storm::dd::Add dd2 = manager->getRange(x.second).toAdd(); + storm::dd::Add dd3; dd1 *= manager->getConstant(2); ASSERT_NO_THROW(dd3 = dd1.multiplyMatrix(dd2, {x.second})); @@ -257,7 +258,7 @@ TEST(CuddDd, GetSetValueTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Dd dd1 = manager->getOne(true); + storm::dd::Add dd1 = manager->getAddOne(); ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2)); EXPECT_EQ(2, dd1.getLeafCount()); @@ -275,8 +276,8 @@ TEST(CuddDd, ForwardIteratorTest) { std::pair x = manager->addMetaVariable("x", 1, 9); std::pair y = manager->addMetaVariable("y", 0, 3); - storm::dd::Dd dd; - ASSERT_NO_THROW(dd = manager->getRange(x.first)); + storm::dd::Add dd; + ASSERT_NO_THROW(dd = manager->getRange(x.first).toAdd()); storm::dd::DdForwardIterator it, ite; ASSERT_NO_THROW(it = dd.begin()); @@ -290,8 +291,8 @@ TEST(CuddDd, ForwardIteratorTest) { } EXPECT_EQ(9, numberOfValuations); - dd = manager->getRange(x.first); - dd = dd.ite(manager->getOne(), manager->getOne()); + dd = manager->getRange(x.first).toAdd(); + dd = dd.ite(manager->getAddOne(), manager->getAddOne()); ASSERT_NO_THROW(it = dd.begin()); ASSERT_NO_THROW(ite = dd.end()); numberOfValuations = 0; @@ -313,81 +314,12 @@ TEST(CuddDd, ForwardIteratorTest) { EXPECT_EQ(1, numberOfValuations); } -// FIXME: make toExpression work again and then fix this test. -//TEST(CuddDd, ToExpressionTest) { -// std::shared_ptr> manager(new storm::dd::DdManager()); -// std::pair x = manager->addMetaVariable("x", 1, 9); -// -// storm::dd::Dd dd; -// ASSERT_NO_THROW(dd = manager->getIdentity(x.first)); -// -// storm::expressions::Expression ddAsExpression; -// ASSERT_NO_THROW(ddAsExpression = dd.toExpression()); -// -// storm::expressions::SimpleValuation valuation; -// for (std::size_t bit = 0; bit < manager->getMetaVariable(x.first).getNumberOfDdVariables(); ++bit) { -// valuation.addBooleanIdentifier("x." + std::to_string(bit)); -// } -// -// storm::dd::DdMetaVariable const& metaVariable = manager->getMetaVariable("x"); -// -// for (auto valuationValuePair : dd) { -// for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) { -// // Check if the i-th bit is set or not and modify the valuation accordingly. -// if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1ull << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) { -// valuation.setBooleanValue("x." + std::to_string(i), true); -// } else { -// valuation.setBooleanValue("x." + std::to_string(i), false); -// } -// } -// -// // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very -// // same value as the current value obtained from the DD. -// EXPECT_EQ(valuationValuePair.second, ddAsExpression.evaluateAsDouble(&valuation)); -// } -// -// storm::expressions::Expression mintermExpression = dd.getMintermExpression(); -// -// // Check whether all minterms are covered. -// for (auto valuationValuePair : dd) { -// for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) { -// // Check if the i-th bit is set or not and modify the valuation accordingly. -// if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1ull << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) { -// valuation.setBooleanValue("x." + std::to_string(i), true); -// } else { -// valuation.setBooleanValue("x." + std::to_string(i), false); -// } -// } -// -// // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very -// // same value as the current value obtained from the DD. -// EXPECT_TRUE(mintermExpression.evaluateAsBool(&valuation)); -// } -// -// // Now check no additional minterms are covered. -// dd = !dd; -// for (auto valuationValuePair : dd) { -// for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) { -// // Check if the i-th bit is set or not and modify the valuation accordingly. -// if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1ull << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) { -// valuation.setBooleanValue("x." + std::to_string(i), true); -// } else { -// valuation.setBooleanValue("x." + std::to_string(i), false); -// } -// } -// -// // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very -// // same value as the current value obtained from the DD. -// EXPECT_FALSE(mintermExpression.evaluateAsBool(&valuation)); -// } -//} - TEST(CuddDd, OddTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair a = manager->addMetaVariable("a"); std::pair x = manager->addMetaVariable("x", 1, 9); - storm::dd::Dd dd = manager->getIdentity(x.first); + storm::dd::Add dd = manager->getIdentity(x.first); storm::dd::Odd odd; ASSERT_NO_THROW(odd = storm::dd::Odd(dd)); EXPECT_EQ(9, odd.getTotalOffset()); @@ -401,14 +333,14 @@ TEST(CuddDd, OddTest) { } // Create a non-trivial matrix. - dd = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)) * manager->getRange(x.first); - dd += manager->getEncoding(x.first, 1) * manager->getRange(x.second) + manager->getEncoding(x.second, 1) * manager->getRange(x.first); + dd = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)) * manager->getRange(x.first).toAdd(); + dd += manager->getEncoding(x.first, 1).toAdd() * manager->getRange(x.second).toAdd() + manager->getEncoding(x.second, 1).toAdd() * manager->getRange(x.first).toAdd(); // Create the ODDs. storm::dd::Odd rowOdd; - ASSERT_NO_THROW(rowOdd = storm::dd::Odd(manager->getRange(x.first))); + ASSERT_NO_THROW(rowOdd = storm::dd::Odd(manager->getRange(x.first).toAdd())); storm::dd::Odd columnOdd; - ASSERT_NO_THROW(columnOdd = storm::dd::Odd(manager->getRange(x.second))); + ASSERT_NO_THROW(columnOdd = storm::dd::Odd(manager->getRange(x.second).toAdd())); // Try to translate the matrix. storm::storage::SparseMatrix matrix; @@ -418,7 +350,7 @@ TEST(CuddDd, OddTest) { EXPECT_EQ(9, matrix.getColumnCount()); EXPECT_EQ(25, matrix.getNonzeroEntryCount()); - dd = manager->getRange(x.first) * manager->getRange(x.second) * manager->getEncoding(a.first, 0).ite(dd, dd + manager->getConstant(1)); + dd = manager->getRange(x.first).toAdd() * manager->getRange(x.second).toAdd() * manager->getEncoding(a.first, 0).toAdd().ite(dd, dd + manager->getConstant(1)); ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, {a.first}, rowOdd, columnOdd)); EXPECT_EQ(18, matrix.getRowCount()); EXPECT_EQ(9, matrix.getRowGroupCount()); diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 68c62182a..bbb927001 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -17,7 +17,7 @@ TEST(GraphTest, SymbolicProb01) { ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); - std::pair, storm::dd::Dd> statesWithProbability01; + std::pair, storm::dd::Bdd> statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), model->getReachableStates(), model->getStates("observe0Greater1"))); EXPECT_EQ(4409, statesWithProbability01.first.getNonZeroCount()); @@ -38,7 +38,7 @@ TEST(GraphTest, SymbolicProb01MinMax) { ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); - std::pair, storm::dd::Dd> statesWithProbability01; + std::pair, storm::dd::Bdd> statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("elected"))); EXPECT_EQ(0, statesWithProbability01.first.getNonZeroCount());