From 706ea569639713a11a3886ac6fb67c0d908f271d Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 19 Feb 2015 17:27:07 +0100 Subject: [PATCH] Now DDs are either MTBDDs or BDDs. This makes it possible to use BDDs where possible, which is faster. Former-commit-id: 07ffb5882d9603f8d4b93940f575cc62d8a968e3 --- src/adapters/DdExpressionAdapter.cpp | 4 +- src/builder/DdPrismModelBuilder.cpp | 87 ++-- src/builder/DdPrismModelBuilder.h | 19 +- src/settings/modules/GeneralSettings.cpp | 20 +- src/settings/modules/GeneralSettings.h | 12 + src/storage/dd/CuddDd.cpp | 589 +++++++++++++++++------ src/storage/dd/CuddDd.h | 116 ++++- src/storage/dd/CuddDdForwardIterator.cpp | 26 +- src/storage/dd/CuddDdForwardIterator.h | 4 +- src/storage/dd/CuddDdManager.cpp | 64 ++- src/storage/dd/CuddDdManager.h | 16 +- src/storage/dd/CuddDdMetaVariable.cpp | 15 +- src/storage/dd/CuddDdMetaVariable.h | 11 + src/storage/dd/CuddOdd.cpp | 12 +- src/storage/dd/CuddOdd.h | 7 +- src/utility/cli.h | 34 +- test/functional/storage/CuddDdTest.cpp | 50 +- 17 files changed, 777 insertions(+), 309 deletions(-) diff --git a/src/adapters/DdExpressionAdapter.cpp b/src/adapters/DdExpressionAdapter.cpp index 65e82f765..c3a63843c 100644 --- a/src/adapters/DdExpressionAdapter.cpp +++ b/src/adapters/DdExpressionAdapter.cpp @@ -40,13 +40,13 @@ namespace storm { result = leftResult || rightResult; break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff: - result = leftResult.equals(rightResult); + result = leftResult.iff(rightResult); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies: result = !leftResult || rightResult; break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor: - result = (leftResult && !rightResult) || (!leftResult && rightResult); + result = leftResult.exclusiveOr(rightResult); break; } diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index ef165a877..28a4a03df 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -50,7 +50,7 @@ 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(); + storm::dd::Dd updateDd = generationInfo.manager->getOne(true); STORM_LOG_TRACE("Translating update " << update); @@ -77,7 +77,7 @@ namespace storm { result *= guard; // Restrict the transitions to the range of the written variable. - result = result * generationInfo.manager->getRange(primedMetaVariable); + result = result * generationInfo.manager->getRange(primedMetaVariable, true); updateDd *= result; } @@ -130,7 +130,7 @@ namespace storm { STORM_LOG_WARN_COND(!guardDd.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable."); if (!guardDd.isZero()) { - storm::dd::Dd commandDd = generationInfo.manager->getZero(); + storm::dd::Dd commandDd = generationInfo.manager->getZero(true); for (storm::prism::Update const& update : command.getUpdates()) { storm::dd::Dd updateDd = createUpdateDecisionDiagram(generationInfo, module, guardDd, update); @@ -183,8 +183,8 @@ namespace storm { template typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionDTMC(GenerationInformation& generationInfo, std::vector const& commandDds) { - storm::dd::Dd allGuards = generationInfo.manager->getZero(); - storm::dd::Dd allCommands = generationInfo.manager->getZero(); + storm::dd::Dd allGuards = generationInfo.manager->getZero(true); + storm::dd::Dd allCommands = generationInfo.manager->getZero(true); storm::dd::Dd temporary; for (auto const& commandDd : commandDds) { @@ -201,7 +201,7 @@ 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(); + storm::dd::Dd result = generationInfo.manager->getZero(true); STORM_LOG_TRACE("Encoding " << value << " with " << numberOfBinaryVariables << " binary variable(s) starting from offset " << nondeterminismVariableOffset << "."); @@ -220,11 +220,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(); - storm::dd::Dd allCommands = generationInfo.manager->getZero(); + storm::dd::Dd allGuards = generationInfo.manager->getZero(true); + storm::dd::Dd allCommands = generationInfo.manager->getZero(true); // 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(); + storm::dd::Dd sumOfGuards = generationInfo.manager->getZero(true); for (auto const& commandDd : commandDds) { sumOfGuards += commandDd.guardDd; allGuards = allGuards || commandDd.guardDd; @@ -247,9 +247,9 @@ namespace storm { // Calculate number of required variables to encode the nondeterminism. uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); - storm::dd::Dd equalsNumberOfChoicesDd = generationInfo.manager->getZero(); - std::vector> choiceDds(maxChoices, generationInfo.manager->getZero()); - std::vector> remainingDds(maxChoices, generationInfo.manager->getZero()); + storm::dd::Dd equalsNumberOfChoicesDd = generationInfo.manager->getZero(true); + std::vector> choiceDds(maxChoices, generationInfo.manager->getZero(true)); + std::vector> remainingDds(maxChoices, generationInfo.manager->getZero(true)); for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { // Determine the set of states with exactly currentChoices choices. @@ -262,7 +262,7 @@ namespace storm { // Reset the previously used intermediate storage. for (uint_fast64_t j = 0; j < currentChoices; ++j) { - choiceDds[j] = generationInfo.manager->getZero(); + choiceDds[j] = generationInfo.manager->getZero(true); remainingDds[j] = equalsNumberOfChoicesDd; } @@ -335,23 +335,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(); + storm::dd::Dd nondeterminisimEncoding = generationInfo.manager->getOne(true); for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables; i < action1.numberOfUsedNondeterminismVariables; ++i) { - nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0); + nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true); } action2Extended *= nondeterminisimEncoding; } else if (action2.numberOfUsedNondeterminismVariables > action1.numberOfUsedNondeterminismVariables) { - storm::dd::Dd nondeterminisimEncoding = generationInfo.manager->getOne(); + storm::dd::Dd nondeterminisimEncoding = generationInfo.manager->getOne(true); for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables; i < action2.numberOfUsedNondeterminismVariables; ++i) { - nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0); + nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true); } action1Extended *= nondeterminisimEncoding; } // Add a new variable that resolves the nondeterminism between the two choices. - storm::dd::Dd combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2Extended, action1Extended); + storm::dd::Dd combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1, true).ite(action2Extended, action1Extended); return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, numberOfUsedNondeterminismVariables + 1); } else { @@ -381,44 +381,44 @@ namespace storm { storm::dd::Dd 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(); + storm::dd::Dd result = generationInfo.manager->getZero(true); // 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(); + storm::dd::Dd nondeterminismEncoding = generationInfo.manager->getOne(true); for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) { - nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0); + nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true); } result = module.independentAction.transitionsDd * nondeterminismEncoding; // Add variables to synchronized action DDs. std::map> synchronizingActionToDdMap; for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { - nondeterminismEncoding = generationInfo.manager->getOne(); + nondeterminismEncoding = generationInfo.manager->getOne(true); for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) { - nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0); + nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true); } synchronizingActionToDdMap.emplace(synchronizingAction.first, synchronizingAction.second.transitionsDd * nondeterminismEncoding); } // Add variables for synchronization. - storm::dd::Dd synchronization = generationInfo.manager->getOne(); + storm::dd::Dd synchronization = generationInfo.manager->getOne(true); for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { - synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0); + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0, true); } result *= synchronization; for (auto& synchronizingAction : synchronizingActionToDdMap) { - synchronization = generationInfo.manager->getOne(); + synchronization = generationInfo.manager->getOne(true); for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { if (i == synchronizingAction.first) { - synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1); + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1, true); } else { - synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0); + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0, true); } } @@ -549,14 +549,24 @@ namespace storm { // In particular, this creates the meta variables used to encode the model. GenerationInformation generationInfo(preparedProgram); - auto clock = std::chrono::high_resolution_clock::now(); + auto totalTimeStart = std::chrono::high_resolution_clock::now(); std::pair, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo); + auto totalTimeEnd = std::chrono::high_resolution_clock::now(); + std::cout << "building matrix took " << std::chrono::duration_cast(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl; + storm::dd::Dd transitionMatrix = transitionMatrixModulePair.first; ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second; // Cut the transition matrix to the reachable fragment of the state space. + totalTimeStart = std::chrono::high_resolution_clock::now(); storm::dd::Dd reachableStates = computeReachableStates(generationInfo, createInitialStatesDecisionDiagram(generationInfo), transitionMatrix); - transitionMatrix *= reachableStates; + totalTimeEnd = std::chrono::high_resolution_clock::now(); + std::cout << "reachability took " << std::chrono::duration_cast(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl; + + totalTimeStart = std::chrono::high_resolution_clock::now(); + transitionMatrix *= reachableStates.toMtbdd(); + totalTimeEnd = std::chrono::high_resolution_clock::now(); + std::cout << "cutting trans to reachable took " << std::chrono::duration_cast(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl; // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. storm::dd::Dd statesWithTransition = transitionMatrix.notZero(); @@ -564,7 +574,7 @@ namespace storm { statesWithTransition = statesWithTransition.existsAbstract(generationInfo.allNondeterminismVariables); } statesWithTransition = statesWithTransition.existsAbstract(generationInfo.columnMetaVariables); - storm::dd::Dd deadlockStates = reachableStates * !statesWithTransition; + storm::dd::Dd deadlockStates = (reachableStates && !statesWithTransition).toMtbdd(); if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. @@ -577,7 +587,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(); + storm::dd::Dd action = generationInfo.manager->getOne(true); 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; } @@ -592,10 +602,10 @@ namespace storm { template storm::dd::Dd DdPrismModelBuilder::createInitialStatesDecisionDiagram(GenerationInformation& generationInfo) { - storm::dd::Dd initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialConstruct().getInitialStatesExpression()); + storm::dd::Dd initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialConstruct().getInitialStatesExpression()).toBdd(); for (auto const& metaVariable : generationInfo.rowMetaVariables) { - initialStates *= generationInfo.manager->getRange(metaVariable); + initialStates &= generationInfo.manager->getRange(metaVariable); } return initialStates; @@ -603,7 +613,7 @@ 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.notZero(); + 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(); @@ -617,18 +627,17 @@ namespace storm { do { STORM_LOG_TRACE("Iteration " << iteration << " of computing reachable states."); changed = false; - storm::dd::Dd tmp = reachableStatesBdd * transitionBdd; - tmp = tmp.existsAbstract(generationInfo.rowMetaVariables); + storm::dd::Dd tmp = reachableStatesBdd.andExists(transitionBdd, generationInfo.rowMetaVariables); tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs); - storm::dd::Dd newReachableStates = tmp * (!reachableStatesBdd); + storm::dd::Dd newReachableStates = tmp && (!reachableStatesBdd); // Check whether new states were indeed discovered. if (!newReachableStates.isZero()) { changed = true; } - reachableStatesBdd += newReachableStates; + reachableStatesBdd |= newReachableStates; ++iteration; } while (changed); diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 20d94cf45..e8854939a 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -68,7 +68,7 @@ namespace storm { // Intentionally left empty. } - ActionDecisionDiagram(storm::dd::DdManager const& manager, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getZero()), transitionsDd(manager.getZero()), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { + ActionDecisionDiagram(storm::dd::DdManager const& manager, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getZero(true)), transitionsDd(manager.getZero(true)), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { // Intentionally left empty. } @@ -95,7 +95,7 @@ namespace storm { // Intentionally left empty. } - ModuleDecisionDiagram(storm::dd::DdManager const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero()), numberOfUsedNondeterminismVariables(0) { + ModuleDecisionDiagram(storm::dd::DdManager const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero(true)), numberOfUsedNondeterminismVariables(0) { // Intentionally left empty. } @@ -209,7 +209,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); + storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first, true); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); rowColumnMetaVariablePairs.push_back(variablePair); } @@ -230,8 +230,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(); - storm::dd::Dd moduleRange = manager->getOne(); + storm::dd::Dd moduleIdentity = manager->getOne(true); + storm::dd::Dd moduleRange = manager->getOne(true); for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); @@ -245,11 +245,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) * manager->getRange(variablePair.second); - variableIdentity.exportToDot(variablePair.first.getName() + "_ident.dot"); + storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first, true) * manager->getRange(variablePair.second, true); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); moduleIdentity *= variableIdentity; - moduleRange *= manager->getRange(variablePair.first); + moduleRange *= manager->getRange(variablePair.first, true); rowColumnMetaVariablePairs.push_back(variablePair); } @@ -263,10 +262,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) * manager->getRange(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); variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); moduleIdentity *= variableIdentity; - moduleRange *= manager->getRange(variablePair.first); + moduleRange *= manager->getRange(variablePair.first, true); rowColumnMetaVariablePairs.push_back(variablePair); } diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 05c03618a..9be7e66f0 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -20,7 +20,7 @@ namespace storm { const std::string GeneralSettings::configOptionName = "config"; const std::string GeneralSettings::configOptionShortName = "c"; const std::string GeneralSettings::explicitOptionName = "explicit"; - const std::string GeneralSettings::explicitOptionShortName = "e"; + const std::string GeneralSettings::explicitOptionShortName = "exp"; const std::string GeneralSettings::symbolicOptionName = "symbolic"; const std::string GeneralSettings::symbolicOptionShortName = "s"; const std::string GeneralSettings::propertyOptionName = "prop"; @@ -41,6 +41,8 @@ namespace storm { const std::string GeneralSettings::statisticsOptionShortName = "stats"; const std::string GeneralSettings::bisimulationOptionName = "bisimulation"; const std::string GeneralSettings::bisimulationOptionShortName = "bisim"; + const std::string GeneralSettings::engineOptionName = "engine"; + const std::string GeneralSettings::engineOptionShortName = "e"; #ifdef STORM_HAVE_CARL const std::string GeneralSettings::parametricOptionName = "parametric"; @@ -76,6 +78,10 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build()); + std::vector engines = {"sparse", "dd"}; + this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, dd}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build()); + std::vector linearEquationSolver = {"gmm++", "native"}; this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build()); @@ -251,6 +257,16 @@ namespace storm { return this->getOption(bisimulationOptionName).getHasOptionBeenSet(); } + GeneralSettings::Engine GeneralSettings::getEngine() const { + std::string engine = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString(); + if (engine == "sparse") { + return GeneralSettings::Engine::Sparse; + } else if (engine == "dd") { + return GeneralSettings::Engine::Dd; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engine << "'."); + } + #ifdef STORM_HAVE_CARL bool GeneralSettings::isParametricSet() const { return this->getOption(parametricOptionName).getHasOptionBeenSet(); @@ -265,6 +281,8 @@ namespace storm { uint_fast64_t propertySources = 0 + (isPropertySet() ? 1 : 0) + (isPropertyFileSet() ? 1 : 0); STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify either a file that contains the properties or a property on the command line, but not both."); + STORM_LOG_THROW(this->getEngine() != Engine::Dd || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "Decision-diagram engine can only be used with symbolic input models."); + return true; } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index db3810af5..1ca21175a 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -13,6 +13,9 @@ namespace storm { */ class GeneralSettings : public ModuleSettings { public: + // An enumeration of all engines. + enum class Engine { Sparse, Dd }; + // An enumeration of all available LP solvers. enum class LpSolver { Gurobi, glpk }; @@ -287,6 +290,13 @@ namespace storm { */ bool isBisimulationSet() const; + /*! + * Retrieves the selected engine. + * + * @return The selecte engine. + */ + Engine getEngine() const; + #ifdef STORM_HAVE_CARL /*! * Retrieves whether the option enabling parametric model checking is set. @@ -335,6 +345,8 @@ namespace storm { static const std::string statisticsOptionShortName; static const std::string bisimulationOptionName; static const std::string bisimulationOptionShortName; + static const std::string engineOptionName; + static const std::string engineOptionShortName; #ifdef STORM_HAVE_CARL static const std::string parametricOptionName; diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index fc1a40aa9..cea8e9dfd 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -7,29 +7,109 @@ #include "src/utility/vector.h" #include "src/utility/macros.h" +#include "src/exceptions/IllegalFunctionCallException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/NotImplementedException.h" namespace storm { namespace dd { - Dd::Dd(std::shared_ptr const> ddManager, ADD cuddAdd, std::set const& containedMetaVariables) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariables(containedMetaVariables) { + Dd::Dd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) { // 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; + } + + 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); + } + } + + Dd Dd::toMtbdd() const { + if (this->isMtbdd()) { + return *this; + } else { + return Dd(this->getDdManager(), this->getCuddBdd().Add(), this->containedMetaVariables); + } + } + + 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(); + } + } + + 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 { - return this->cuddAdd == other.getCuddAdd(); + 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 { - return this->cuddAdd != other.getCuddAdd(); + 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()); - - return Dd(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()), metaVariableNames); + + // 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); + } } Dd Dd::operator+(Dd const& other) const { @@ -39,11 +119,9 @@ namespace storm { } Dd& Dd::operator+=(Dd const& other) { - this->cuddAdd += other.getCuddAdd(); - - // Join the variable sets of the two participating DDs. + 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; } @@ -54,45 +132,48 @@ namespace storm { } Dd& Dd::operator*=(Dd const& other) { - this->cuddAdd *= other.getCuddAdd(); - - // Join the variable sets of the two participating DDs. 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(); + } 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; return result; } Dd Dd::operator-() const { - return this->getDdManager()->getZero() - *this; + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + return this->getDdManager()->getZero(true) - *this; } Dd& Dd::operator-=(Dd const& other) { - this->cuddAdd -= other.getCuddAdd(); - - // Join the variable sets of the two participating DDs. + 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()); - 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; return result; } Dd& Dd::operator/=(Dd const& other) { - this->cuddAdd = this->cuddAdd.Divide(other.getCuddAdd()); - - // Join the variable sets of the two participating DDs. + 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()); - return *this; } @@ -101,77 +182,155 @@ namespace storm { result.complement(); return result; } - + + Dd& Dd::complement() { + if (this->isBdd()) { + this->cuddDd = ~this->getCuddBdd(); + } else { + this->cuddDd = ~this->getCuddMtbdd(); + } + return *this; + } + Dd Dd::operator&&(Dd const& other) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - - // Rewrite a and b to not((not a) or (not b)). - return Dd(this->getDdManager(), ~(~this->getCuddAdd()).Or(~other.getCuddAdd()), metaVariables); + 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(); + } + return *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(); + } + 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()); + return *this; + } + + Dd Dd::iff(Dd const& other) const { std::set metaVariables(this->getContainedMetaVariables()); metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariables); + 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); + } + return *this; } - - Dd& Dd::complement() { - this->cuddAdd = ~this->cuddAdd; + + 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().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().Xor(other.getCuddBdd()), metaVariables); + } return *this; } 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->getCuddAdd().Equals(other.getCuddAdd()), metaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().Equals(other.getCuddMtbdd()), 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->getCuddAdd().NotEquals(other.getCuddAdd()), metaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().NotEquals(other.getCuddMtbdd()), 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->getCuddAdd().LessThan(other.getCuddAdd()), metaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().LessThan(other.getCuddMtbdd()), 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->getCuddAdd().LessThanOrEqual(other.getCuddAdd()), metaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().LessThanOrEqual(other.getCuddMtbdd()), 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->getCuddAdd().GreaterThan(other.getCuddAdd()), metaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().GreaterThan(other.getCuddMtbdd()), 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->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()), metaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().GreaterThanOrEqual(other.getCuddMtbdd()), 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->getCuddAdd().Minimum(other.getCuddAdd()), metaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().Minimum(other.getCuddMtbdd()), 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->getCuddAdd().Maximum(other.getCuddAdd()), metaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().Maximum(other.getCuddMtbdd()), metaVariables); } Dd Dd::existsAbstract(std::set const& metaVariables) const { - Dd cubeDd(this->getDdManager()->getOne()); + STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s)."); + Dd cubeDd(this->getDdManager()->getOne(false)); 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. @@ -179,15 +338,16 @@ namespace storm { newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd *= ddMetaVariable.getCube(); + cubeDd &= ddMetaVariable.getCube(); } - return Dd(this->getDdManager(), this->cuddAdd.OrAbstract(cubeDd.getCuddAdd()), newMetaVariables); + return Dd(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), 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()); - 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. @@ -195,15 +355,16 @@ namespace storm { newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd *= ddMetaVariable.getCube(); + cubeDd &= ddMetaVariable.getCube(); } - return Dd(this->getDdManager(), this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd()), newMetaVariables); + return Dd(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables); } Dd Dd::sumAbstract(std::set const& metaVariables) const { - Dd cubeDd(this->getDdManager()->getOne()); - + 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. @@ -211,15 +372,16 @@ namespace storm { newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd *= ddMetaVariable.getCube(); + cubeDd *= ddMetaVariable.getCubeAsMtbdd(); } - return Dd(this->getDdManager(), this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd()), newMetaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().ExistAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); } Dd Dd::minAbstract(std::set const& metaVariables) const { - Dd cubeDd(this->getDdManager()->getOne()); - + 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. @@ -227,15 +389,16 @@ namespace storm { newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd *= ddMetaVariable.getCube(); + cubeDd *= ddMetaVariable.getCubeAsMtbdd(); } - return Dd(this->getDdManager(), this->cuddAdd.MinAbstract(cubeDd.getCuddAdd()), newMetaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().MinAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); } Dd Dd::maxAbstract(std::set const& metaVariables) const { - Dd cubeDd(this->getDdManager()->getOne()); - + 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. @@ -243,63 +406,102 @@ namespace storm { newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd *= ddMetaVariable.getCube(); + cubeDd *= ddMetaVariable.getCubeAsMtbdd(); } - return Dd(this->getDdManager(), this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd()), newMetaVariables); + return Dd(this->getDdManager(), this->getCuddMtbdd().MaxAbstract(cubeDd.getCuddMtbdd()), newMetaVariables); } bool Dd::equalModuloPrecision(Dd const& other, double precision, bool relative) const { + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + if (relative) { - return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision); + return this->getCuddMtbdd().EqualSupNormRel(other.getCuddMtbdd(), precision); } else { - return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision); + return this->getCuddMtbdd().EqualSupNorm(other.getCuddMtbdd(), precision); } } void Dd::swapVariables(std::vector> const& metaVariablePairs) { - 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."; + 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. + 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. + bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first); + bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second); + if (containsVariable1 && !containsVariable2) { + this->removeContainedMetaVariable(metaVariablePair.first); + this->addContainedMetaVariable(metaVariablePair.second); + } else if (!containsVariable1 && containsVariable2) { + this->removeContainedMetaVariable(metaVariablePair.second); + this->addContainedMetaVariable(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()); + } } - // Keep track of the contained meta variables in the DD. - bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first); - bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second); - if (containsVariable1 && !containsVariable2) { - this->removeContainedMetaVariable(metaVariablePair.first); - this->addContainedMetaVariable(metaVariablePair.second); - } else if (!containsVariable1 && containsVariable2) { - this->removeContainedMetaVariable(metaVariablePair.second); - this->addContainedMetaVariable(metaVariablePair.first); + // Finally, call CUDD to swap the variables. + this->cuddDd = this->getCuddBdd().SwapVariables(from, to); + } 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. + bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first); + bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second); + if (containsVariable1 && !containsVariable2) { + this->removeContainedMetaVariable(metaVariablePair.first); + this->addContainedMetaVariable(metaVariablePair.second); + } else if (!containsVariable1 && containsVariable2) { + this->removeContainedMetaVariable(metaVariablePair.second); + this->addContainedMetaVariable(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()); + } } - // Add the variables to swap to the corresponding vectors. - for (auto const& ddVariable : variable1.getDdVariables()) { - from.push_back(ddVariable.getCuddAdd()); - } - for (auto const& ddVariable : variable2.getDdVariables()) { - to.push_back(ddVariable.getCuddAdd()); - } + // Finally, call CUDD to swap the variables. + this->cuddDd = this->getCuddMtbdd().SwapVariables(from, to); } - - // Finally, call CUDD to swap the variables. - this->cuddAdd = this->cuddAdd.SwapVariables(from, to); } Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariables) const { - std::vector summationDdVariables; - + STORM_LOG_WARN_COND(this->isMtbdd() && otherMatrix.isMtbdd(), "Performing arithmetical operation on BDD(s)."); + // 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.getCuddAdd()); + summationDdVariables.push_back(ddVariable.getCuddMtbdd()); } } @@ -308,37 +510,68 @@ 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->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariables); + 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); } Dd Dd::greater(double value) const { - return Dd(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(value).Add(), this->getContainedMetaVariables()); + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + return Dd(this->getDdManager(), this->getCuddMtbdd().BddStrictThreshold(value), this->getContainedMetaVariables()); } Dd Dd::greaterOrEqual(double value) const { - return Dd(this->getDdManager(), this->getCuddAdd().BddThreshold(value).Add(), this->getContainedMetaVariables()); + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + return Dd(this->getDdManager(), this->getCuddMtbdd().BddThreshold(value), this->getContainedMetaVariables()); } Dd Dd::notZero() const { - return Dd(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariables()); + return this->toBdd(); } Dd Dd::constrain(Dd const& constraint) const { std::set metaVariables(this->getContainedMetaVariables()); metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddAdd().Constrain(constraint.getCuddAdd()), metaVariables); + 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); + } } Dd Dd::restrict(Dd const& constraint) const { std::set metaVariables(this->getContainedMetaVariables()); metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end()); - return Dd(this->getDdManager(), this->getCuddAdd().Restrict(constraint.getCuddAdd()), metaVariables); + 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); + } } Dd Dd::getSupport() const { - return Dd(this->getDdManager(), this->getCuddAdd().Support().Add(), this->getContainedMetaVariables()); + if (this->isBdd()) { + return Dd(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables()); + } else { + return Dd(this->getDdManager(), this->getCuddMtbdd().Support(), this->getContainedMetaVariables()); + } } uint_fast64_t Dd::getNonZeroCount() const { @@ -346,24 +579,40 @@ namespace storm { for (auto const& metaVariable : this->getContainedMetaVariables()) { numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); } - return static_cast(this->cuddAdd.CountMinterm(static_cast(numberOfDdVariables))); + if (this->isBdd()) { + return static_cast(this->getCuddBdd().CountMinterm(static_cast(numberOfDdVariables))); + } else { + return static_cast(this->getCuddMtbdd().CountMinterm(static_cast(numberOfDdVariables))); + } } uint_fast64_t Dd::getLeafCount() const { - return static_cast(this->cuddAdd.CountLeaves()); + if (this->isBdd()) { + return static_cast(this->getCuddBdd().CountLeaves()); + } else { + return static_cast(this->getCuddMtbdd().CountLeaves()); + } } - + uint_fast64_t Dd::getNodeCount() const { - return static_cast(this->cuddAdd.nodeCount()); + if (this->isBdd()) { + return static_cast(this->getCuddBdd().nodeCount()); + } else { + return static_cast(this->getCuddMtbdd().nodeCount()); + } } double Dd::getMin() const { - ADD constantMinAdd = this->cuddAdd.FindMin(); + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + + ADD constantMinAdd = this->getCuddMtbdd().FindMin(); return static_cast(Cudd_V(constantMinAdd.getNode())); } double Dd::getMax() const { - ADD constantMaxAdd = this->cuddAdd.FindMax(); + STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s)."); + + ADD constantMaxAdd = this->getCuddMtbdd().FindMax(); return static_cast(Cudd_V(constantMaxAdd.getNode())); } @@ -381,65 +630,102 @@ namespace storm { } void Dd::setValue(std::map const& metaVariableToValueMap, double targetValue) { - 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 (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()); } - - this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd); } double Dd::getValue(std::map const& metaVariableToValueMap) const { std::set remainingMetaVariables(this->getContainedMetaVariables()); Dd valueEncoding(this->getDdManager()->getOne()); for (auto const& nameValuePair : metaVariableToValueMap) { - valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); if (this->containsMetaVariable(nameValuePair.first)) { remainingMetaVariables.erase(nameValuePair.first); } } - if (!remainingMetaVariables.empty()) { - throw storm::exceptions::InvalidArgumentException() << "Cannot evaluate function for which not all inputs were given."; - } + STORM_LOG_THROW(remainingMetaVariables.empty(), storm::exceptions::InvalidArgumentException, "Cannot evaluate function for which not all inputs were given."); - Dd value = *this * valueEncoding; - value = value.sumAbstract(this->getContainedMetaVariables()); - return static_cast(Cudd_V(value.getCuddAdd().getNode())); + if (this->isBdd()) { + Dd value = *this && valueEncoding; + return value.isZero() ? 0 : 1; + } else { + Dd value = *this * valueEncoding; + value = value.sumAbstract(this->getContainedMetaVariables()); + return static_cast(Cudd_V(value.getCuddMtbdd().getNode())); + } } bool Dd::isOne() const { - return *this == this->getDdManager()->getOne(); + if (this->isBdd()) { + return this->getCuddBdd().IsOne(); + } else { + return this->getCuddMtbdd().IsOne(); + } } bool Dd::isZero() const { - return *this == this->getDdManager()->getZero(); + if (this->isBdd()) { + return this->getCuddBdd().IsZero(); + } else { + return this->getCuddMtbdd().IsZero(); + } } bool Dd::isConstant() const { - return Cudd_IsConstant(this->cuddAdd.getNode()); + if (this->isBdd()) { + return Cudd_IsConstant(this->getCuddBdd().getNode()); + } else { + return Cudd_IsConstant(this->getCuddMtbdd().getNode()); + } } uint_fast64_t Dd::getIndex() const { - return static_cast(this->getCuddAdd().NodeReadIndex()); + if (this->isBdd()) { + return static_cast(this->getCuddBdd().NodeReadIndex()); + } else { + return static_cast(this->getCuddMtbdd().NodeReadIndex()); + } } template std::vector Dd::toVector() const { + STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD."); 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 result(rowOdd.getTotalOffset()); std::vector ddVariableIndices = this->getSortedVariableIndices(); - addToVectorRec(this->getCuddAdd().getNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result); + 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."); std::set rowVariables; std::set columnVariables; @@ -455,6 +741,7 @@ namespace storm { } 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."); std::set rowMetaVariables; std::set columnMetaVariables; @@ -470,6 +757,7 @@ namespace storm { } 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."); std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; @@ -500,7 +788,7 @@ namespace storm { // Use the toMatrixRec function to compute the number of elements in each row. Using the flag, we prevent // it from actually generating the entries in the entry vector. - toMatrixRec(this->getCuddAdd().getNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); + toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); // TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert // the resulting (DD) vector to an explicit vector. @@ -516,7 +804,7 @@ namespace storm { rowIndications[0] = 0; // Now actually fill the entry vector. - toMatrixRec(this->getCuddAdd().getNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); + toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { @@ -529,6 +817,7 @@ namespace storm { } 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."); std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; std::vector ddGroupVariableIndices; @@ -573,7 +862,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; - splitGroupsRec(this->getCuddAdd().getNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables); + splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables); // Create the actual storage for the non-zero entries. std::vector> columnsAndValues(this->getNonZeroCount()); @@ -584,10 +873,10 @@ namespace storm { for (uint_fast64_t i = 0; i < groups.size(); ++i) { auto const& dd = groups[i]; - toMatrixRec(dd.getCuddAdd().getNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); + 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); - addToVectorRec(statesWithGroupEnabled[i].getCuddAdd().getNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); + addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); } // Since we modified the rowGroupIndices, we need to restore the correct values. @@ -610,9 +899,9 @@ namespace storm { for (uint_fast64_t i = 0; i < groups.size(); ++i) { auto const& dd = groups[i]; - toMatrixRec(dd.getCuddAdd().getNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); + toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); - addToVectorRec(statesWithGroupEnabled[i].getCuddAdd().getNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); + addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); } // Since we modified the rowGroupIndices, we need to restore the correct values. @@ -632,7 +921,7 @@ namespace storm { 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 { // For the empty DD, we do not need to add any entries. - if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) { + if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { return; } @@ -684,7 +973,7 @@ 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 { // For the empty DD, we do not need to create a group. - if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) { + if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { return; } @@ -702,7 +991,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 { // For the empty DD, we do not need to add any entries. - if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) { + if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { return; } @@ -759,9 +1048,14 @@ namespace storm { } void Dd::exportToDot(std::string const& filename) const { - std::vector cuddAddVector = { this->cuddAdd }; if (filename.empty()) { - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); + if (this->isBdd()) { + std::vector cuddBddVector = { this->getCuddBdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddBddVector); + } else { + std::vector cuddAddVector = { this->getCuddMtbdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); + } } else { // Build the name input of the DD. std::vector ddNames; @@ -779,7 +1073,13 @@ namespace storm { // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); + 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); + } fclose(filePointer); // Finally, delete the names. @@ -792,14 +1092,6 @@ namespace storm { } } - ADD Dd::getCuddAdd() { - return this->cuddAdd; - } - - ADD const& Dd::getCuddAdd() const { - return this->cuddAdd; - } - void Dd::addContainedMetaVariable(storm::expressions::Variable const& metaVariable) { this->getContainedMetaVariables().insert(metaVariable); } @@ -815,7 +1107,7 @@ namespace storm { DdForwardIterator Dd::begin(bool enumerateDontCareMetaVariables) const { int* cube; double value; - DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); + DdGen* generator = this->getCuddDd().FirstCube(&cube, &value); return DdForwardIterator(this->getDdManager(), generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &this->getContainedMetaVariables(), enumerateDontCareMetaVariables); } @@ -824,14 +1116,13 @@ namespace storm { } storm::expressions::Expression Dd::toExpression() const { - return toExpressionRecur(this->getCuddAdd().getNode(), this->getDdManager()->getDdVariables()); + 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. - Dd tmp(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariables()); - return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->getCuddAdd().BddPattern().getNode(), this->getDdManager()->getDdVariables()); + return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->toBdd().getCuddDdNode(), this->getDdManager()->getDdVariables()); } storm::expressions::Expression Dd::toExpressionRecur(DdNode const* dd, std::vector const& variables) { @@ -869,7 +1160,7 @@ namespace storm { // } } - std::ostream & operator<<(std::ostream& out, const Dd& dd) { + std::ostream& operator<<(std::ostream& out, const Dd& dd) { dd.exportToDot(); return out; } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 0fa04f574..21038643a 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -5,6 +5,7 @@ #include #include #include +#include #include "src/storage/dd/Dd.h" #include "src/storage/dd/CuddDdForwardIterator.h" @@ -65,17 +66,51 @@ namespace storm { /*! * 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 + */ + Dd& operator&=(Dd const& other); + + /*! + * Performs a logical iff of the current and the given DD. + * + * @param other The second DD used for the operation. + * @return The logical iff of the operands. + */ + Dd iff(Dd const& other) const; + + /*! + * Performs a logical exclusive-or of the current and the given DD. + * + * @param other The second DD used for the operation. + * @return The logical exclusive-or of the operands. + */ + Dd exclusiveOr(Dd const& other) const; + /*! * Adds the two DDs. * @@ -296,6 +331,16 @@ namespace storm { */ 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. + */ + Dd andExists(Dd const& other, std::set const& existentialVariables) 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. @@ -605,20 +650,64 @@ namespace storm { friend std::ostream & operator<<(std::ostream& out, const Dd& dd); + /*! + * Converts an MTBDD 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; + private: /*! - * Retrieves a reference to the CUDD ADD object associated with this DD. + * Retrieves the CUDD BDD object associated with this DD. * - * @return The CUDD ADD object associated with this DD. + * @return The CUDD BDD object associated with this DD. */ - ADD getCuddAdd(); + BDD getCuddBdd() const; /*! - * Retrieves the CUDD ADD object associated with this DD. + * Retrieves the CUDD MTBDD object associated with this DD. * - * @return The CUDD ADD object assoicated with this DD. + * @return The CUDD MTBDD object associated with this DD. */ - ADD const& getCuddAdd() const; + ADD getCuddMtbdd() const; + + /*! + * Retrieves the CUDD object associated with this DD. + * + * @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. + */ + DdNode* getCuddDdNode() const; /*! * Adds the given meta variable to the set of meta variables that are contained in this DD. @@ -657,10 +746,19 @@ namespace storm { * Creates a DD that encapsulates the given CUDD ADD. * * @param ddManager The manager responsible for this DD. - * @param cuddAdd The CUDD ADD to store. + * @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. + * + * @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 cuddAdd, std::set const& containedMetaVariables = std::set()); + Dd(std::shared_ptr const> ddManager, BDD cuddDd, std::set const& containedMetaVariables = std::set()); /*! * Helper function to convert the DD into a (sparse) matrix. @@ -727,7 +825,7 @@ namespace storm { std::shared_ptr const> ddManager; // The ADD created by CUDD. - ADD cuddAdd; + boost::variant cuddDd; // The meta variables that appear in this DD. std::set containedMetaVariables; diff --git a/src/storage/dd/CuddDdForwardIterator.cpp b/src/storage/dd/CuddDdForwardIterator.cpp index 74f29d174..07b0a7e59 100644 --- a/src/storage/dd/CuddDdForwardIterator.cpp +++ b/src/storage/dd/CuddDdForwardIterator.cpp @@ -80,19 +80,19 @@ namespace storm { ++this->cubeCounter; for (uint_fast64_t index = 0; index < this->relevantDontCareDdVariables.size(); ++index) { - auto const& ddMetaVariable = this->ddManager->getMetaVariable(std::get<1>(this->relevantDontCareDdVariables[index])); + auto const& ddMetaVariable = this->ddManager->getMetaVariable(std::get<0>(this->relevantDontCareDdVariables[index])); if (ddMetaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { if ((this->cubeCounter & (1ull << index)) != 0) { - currentValuation.setBooleanValue(std::get<1>(this->relevantDontCareDdVariables[index]), true); + currentValuation.setBooleanValue(std::get<0>(this->relevantDontCareDdVariables[index]), true); } else { - currentValuation.setBooleanValue(std::get<1>(this->relevantDontCareDdVariables[index]), false); + currentValuation.setBooleanValue(std::get<0>(this->relevantDontCareDdVariables[index]), false); } } else { - storm::expressions::Variable const& metaVariable = std::get<1>(this->relevantDontCareDdVariables[index]); + storm::expressions::Variable const& metaVariable = std::get<0>(this->relevantDontCareDdVariables[index]); if ((this->cubeCounter & (1ull << index)) != 0) { - currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) | (1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); + currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) | (1ull << std::get<1>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); } else { - currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); + currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<1>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); } } } @@ -106,31 +106,31 @@ namespace storm { // valuations later. for (auto const& metaVariable : *this->metaVariables) { bool metaVariableAppearsInCube = false; - std::vector> localRelenvantDontCareDdVariables; + std::vector> localRelenvantDontCareDdVariables; auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable); if (ddMetaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { - if (this->cube[ddMetaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 0) { + if (this->cube[ddMetaVariable.getDdVariables().front().getIndex()] == 0) { metaVariableAppearsInCube = true; currentValuation.setBooleanValue(metaVariable, false); - } else if (this->cube[ddMetaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 1) { + } else if (this->cube[ddMetaVariable.getDdVariables().front().getIndex()] == 1) { metaVariableAppearsInCube = true; currentValuation.setBooleanValue(metaVariable, true); } else { - localRelenvantDontCareDdVariables.push_back(std::make_tuple(ddMetaVariable.getDdVariables()[0].getCuddAdd(), metaVariable, 0)); + localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, 0)); } } else { int_fast64_t intValue = 0; for (uint_fast64_t bitIndex = 0; bitIndex < ddMetaVariable.getNumberOfDdVariables(); ++bitIndex) { - if (cube[ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 0) { + if (cube[ddMetaVariable.getDdVariables()[bitIndex].getIndex()] == 0) { // Leave bit unset. metaVariableAppearsInCube = true; - } else if (cube[ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 1) { + } else if (cube[ddMetaVariable.getDdVariables()[bitIndex].getIndex()] == 1) { intValue |= 1ull << (ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1); metaVariableAppearsInCube = true; } else { // Temporarily leave bit unset so we can iterate trough the other option later. // Add the bit to the relevant don't care bits. - localRelenvantDontCareDdVariables.push_back(std::make_tuple(ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1)); + localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1)); } } if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) { diff --git a/src/storage/dd/CuddDdForwardIterator.h b/src/storage/dd/CuddDdForwardIterator.h index 4c7e97364..228c8e1b4 100644 --- a/src/storage/dd/CuddDdForwardIterator.h +++ b/src/storage/dd/CuddDdForwardIterator.h @@ -124,8 +124,8 @@ namespace storm { // This is needed, because cubes may represent many assignments (if they have don't care variables). uint_fast64_t cubeCounter; - // A vector of tuples of the form . - std::vector> relevantDontCareDdVariables; + // A vector of tuples of the form . + std::vector> relevantDontCareDdVariables; // The current valuation of meta variables. storm::expressions::SimpleValuation currentValuation; diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 5a7d21f05..a844075ce 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -37,19 +37,27 @@ namespace storm { } } - Dd DdManager::getOne() const { - return Dd(this->shared_from_this(), cuddManager.addOne()); + 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()); + } } - Dd DdManager::getZero() const { - return Dd(this->shared_from_this(), cuddManager.addZero()); + 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()); + } } Dd DdManager::getConstant(double value) const { return Dd(this->shared_from_this(), cuddManager.constant(value)); } - Dd DdManager::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const { + Dd DdManager::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value, bool asMtbdd) 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() << "'."); @@ -68,19 +76,23 @@ namespace storm { for (std::size_t i = 1; i < ddVariables.size(); ++i) { if (value & (1ull << (ddVariables.size() - i - 1))) { - result *= ddVariables[i]; + result &= ddVariables[i]; } else { - result *= !ddVariables[i]; + result &= !ddVariables[i]; } } - - return result; + + if (asMtbdd) { + return result.toMtbdd(); + } else { + return result; + } } - Dd DdManager::getRange(storm::expressions::Variable const& variable) const { + Dd DdManager::getRange(storm::expressions::Variable const& variable, bool asMtbdd) const { storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - Dd result = this->getZero(); + Dd result = this->getZero(asMtbdd); for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { result.setValue(variable, value, static_cast(1)); @@ -92,7 +104,7 @@ namespace storm { Dd DdManager::getIdentity(storm::expressions::Variable const& variable) const { storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - Dd result = this->getZero(); + Dd result = this->getZero(true); for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { result.setValue(variable, value, static_cast(value)); } @@ -117,13 +129,13 @@ namespace storm { std::vector> variables; std::vector> variablesPrime; for (std::size_t i = 0; i < numberOfBits; ++i) { - variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {unprimed})); - variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {primed})); + variables.emplace_back(Dd(this->shared_from_this(), cuddManager.bddVar(), {unprimed})); + variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.bddVar(), {primed})); } // Now group the non-primed and primed variable. for (uint_fast64_t i = 0; i < numberOfBits; ++i) { - this->getCuddManager().MakeTreeNode(variables[i].getCuddAdd().NodeReadIndex(), 2, MTR_FIXED); + this->getCuddManager().MakeTreeNode(variables[i].getIndex(), 2, MTR_FIXED); } metaVariableMap.emplace(unprimed, DdMetaVariable(name, low, high, variables, this->shared_from_this())); @@ -144,11 +156,11 @@ namespace storm { std::vector> variables; std::vector> variablesPrime; - variables.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {unprimed})); - variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.addVar(), {primed})); + variables.emplace_back(Dd(this->shared_from_this(), cuddManager.bddVar(), {unprimed})); + variablesPrime.emplace_back(Dd(this->shared_from_this(), cuddManager.bddVar(), {primed})); // Now group the non-primed and primed variable. - this->getCuddManager().MakeTreeNode(variables.front().getCuddAdd().NodeReadIndex(), 2, MTR_FIXED); + this->getCuddManager().MakeTreeNode(variables.front().getIndex(), 2, MTR_FIXED); metaVariableMap.emplace(unprimed, DdMetaVariable(name, variables, this->shared_from_this())); metaVariableMap.emplace(primed, DdMetaVariable(name + "'", variablesPrime, this->shared_from_this())); @@ -199,22 +211,22 @@ namespace storm { std::vector DdManager::getDdVariableNames() const { // First, we initialize a list DD variables and their names. - std::vector> variablePairs; + std::vector> variablePairs; for (auto const& variablePair : this->metaVariableMap) { DdMetaVariable const& metaVariable = variablePair.second; // If the meta variable is of type bool, we don't need to suffix it with the bit number. if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { - variablePairs.emplace_back(metaVariable.getDdVariables().front().getCuddAdd(), variablePair.first.getName()); + variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first.getName()); } else { // For integer-valued meta variables, we, however, have to add the suffix. for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) { - variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), variablePair.first.getName() + '.' + std::to_string(variableIndex)); + variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first.getName() + '.' + std::to_string(variableIndex)); } } } // Then, we sort this list according to the indices of the ADDs. - std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); }); + std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first < b.first; }); // Now, we project the sorted vector to its second component. std::vector result; @@ -227,22 +239,22 @@ namespace storm { std::vector DdManager::getDdVariables() const { // First, we initialize a list DD variables and their names. - std::vector> variablePairs; + std::vector> variablePairs; for (auto const& variablePair : this->metaVariableMap) { DdMetaVariable const& metaVariable = variablePair.second; // If the meta variable is of type bool, we don't need to suffix it with the bit number. if (metaVariable.getType() == DdMetaVariable::MetaVariableType::Bool) { - variablePairs.emplace_back(metaVariable.getDdVariables().front().getCuddAdd(), variablePair.first); + variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first); } else { // For integer-valued meta variables, we, however, have to add the suffix. for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) { - variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), variablePair.first); + variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first); } } } // Then, we sort this list according to the indices of the ADDs. - std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); }); + std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first < b.first; }); // Now, we project the sorted vector to its second component. std::vector result; diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 5aff80682..4926e792c 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -36,18 +36,20 @@ namespace storm { #endif /*! - * Retrieves a DD representing the constant one function. + * 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. * * @return A DD representing the constant one function. */ - Dd getOne() const; + Dd getOne(bool asMtbdd = false) const; /*! - * Retrieves a DD representing the constant zero function. + * 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. * * @return A DD representing the constant zero function. */ - Dd getZero() const; + Dd getZero(bool asMtbdd = false) const; /*! * Retrieves a DD representing the constant function with the given value. @@ -62,19 +64,21 @@ namespace storm { * * @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) const; + Dd getEncoding(storm::expressions::Variable const& variable, int_fast64_t value, bool asMtbdd = false) const; /*! * Retrieves the DD 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) const; + Dd getRange(storm::expressions::Variable const& variable, bool asMtbdd = false) const; /*! * Retrieves the DD representing the identity of the meta variable, i.e., a function that maps all legal diff --git a/src/storage/dd/CuddDdMetaVariable.cpp b/src/storage/dd/CuddDdMetaVariable.cpp index 13667bd99..a53465682 100644 --- a/src/storage/dd/CuddDdMetaVariable.cpp +++ b/src/storage/dd/CuddDdMetaVariable.cpp @@ -3,18 +3,20 @@ 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()), 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->getOne()), cubeAsMtbdd(manager->getOne(true)), manager(manager) { // Create the cube of all variables of this meta variable. for (auto const& ddVariable : this->ddVariables) { - this->cube *= ddVariable; + 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()), 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->getOne()), cubeAsMtbdd(manager->getOne(true)), manager(manager) { // Create the cube of all variables of this meta variable. for (auto const& ddVariable : this->ddVariables) { - this->cube *= ddVariable; + this->cube &= ddVariable; } + this->cubeAsMtbdd = this->cube.toMtbdd(); } std::string const& DdMetaVariable::getName() const { @@ -48,5 +50,10 @@ namespace storm { Dd 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 25375dc4d..aeea15389 100644 --- a/src/storage/dd/CuddDdMetaVariable.h +++ b/src/storage/dd/CuddDdMetaVariable.h @@ -113,6 +113,13 @@ namespace storm { */ 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; + // The name of the meta variable. std::string name; @@ -131,6 +138,10 @@ namespace storm { // 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; + // 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 bd06a8648..8e489ec03 100644 --- a/src/storage/dd/CuddOdd.cpp +++ b/src/storage/dd/CuddOdd.cpp @@ -17,17 +17,17 @@ namespace storm { std::vector>>> uniqueTableForLevels(ddVariableIndices.size() + 1); // Now construct the ODD structure. - std::shared_ptr> rootOdd = buildOddRec(dd.getCuddAdd().getNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); + // 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); // Finally, move the children of the root ODD into this ODD. - this->dd = rootOdd->dd; this->elseNode = std::move(rootOdd->elseNode); this->thenNode = std::move(rootOdd->thenNode); this->elseOffset = rootOdd->elseOffset; this->thenOffset = rootOdd->thenOffset; } - Odd::Odd(ADD dd, std::shared_ptr>&& elseNode, uint_fast64_t elseOffset, std::shared_ptr>&& thenNode, uint_fast64_t thenOffset) : dd(dd), elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) { + Odd::Odd(std::shared_ptr> elseNode, uint_fast64_t elseOffset, std::shared_ptr> thenNode, uint_fast64_t thenOffset) : elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) { // Intentionally left empty. } @@ -92,18 +92,18 @@ namespace storm { thenOffset = 1; } - return std::shared_ptr>(new Odd(ADD(manager, dd), nullptr, elseOffset, nullptr, thenOffset)); + return std::shared_ptr>(new Odd(nullptr, elseOffset, nullptr, thenOffset)); } else if (ddVariableIndices[currentLevel] < static_cast(dd->index)) { // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same // node for the then-successor as well. std::shared_ptr> elseNode = buildOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr> thenNode = elseNode; - return std::shared_ptr>(new Odd(ADD(manager, dd), std::move(elseNode), elseNode->getElseOffset() + elseNode->getThenOffset(), std::move(thenNode), thenNode->getElseOffset() + thenNode->getThenOffset())); + return std::shared_ptr>(new Odd(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset())); } else { // Otherwise, we compute the ODDs for both the then- and else successors. std::shared_ptr> elseNode = buildOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr> thenNode = buildOddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); - return std::shared_ptr>(new Odd(ADD(manager, dd), std::move(elseNode), elseNode->getElseOffset() + elseNode->getThenOffset(), std::move(thenNode), thenNode->getElseOffset() + thenNode->getThenOffset())); + return std::shared_ptr>(new Odd(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset())); } } } diff --git a/src/storage/dd/CuddOdd.h b/src/storage/dd/CuddOdd.h index 1d36613f0..c12dfb67c 100644 --- a/src/storage/dd/CuddOdd.h +++ b/src/storage/dd/CuddOdd.h @@ -92,13 +92,13 @@ namespace storm { /*! * Constructs an offset-labeled DD with the given topmost DD node, else- and then-successor. * - * @param dd The DD associated with this ODD node. + * @param dd The DD node associated with this ODD node. * @param elseNode The else-successor of thie ODD node. * @param elseOffset The offset of the else-successor. * @param thenNode The then-successor of thie ODD node. * @param thenOffset The offset of the then-successor. */ - Odd(ADD dd, std::shared_ptr>&& elseNode, uint_fast64_t elseOffset, std::shared_ptr>&& thenNode, uint_fast64_t thenOffset); + Odd(std::shared_ptr> elseNode, uint_fast64_t elseOffset, std::shared_ptr> thenNode, uint_fast64_t thenOffset); /*! * Recursively builds the ODD. @@ -114,9 +114,6 @@ namespace storm { */ static std::shared_ptr> buildOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels); - // The DD associated with this ODD node. - ADD dd; - // The then- and else-nodes. std::shared_ptr> elseNode; std::shared_ptr> thenNode; diff --git a/src/utility/cli.h b/src/utility/cli.h index 6cde40151..192c45b6f 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -70,6 +70,7 @@ log4cplus::Logger printer; #include "src/counterexamples/SMTMinimalCommandSetGenerator.h" // Headers related to exception handling. +#include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/InvalidTypeException.h" @@ -276,22 +277,25 @@ namespace storm { } // Customize model-building. -// typename storm::builder::ExplicitPrismModelBuilder::Options options; -// if (formula) { -// options = typename storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); -// } -// options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); -// -// // Then, build the model from the symbolic description. -// result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); - - typename storm::builder::DdPrismModelBuilder::Options options; - if (formula) { - options = typename storm::builder::DdPrismModelBuilder::Options(*formula.get()); + if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) { + typename storm::builder::ExplicitPrismModelBuilder::Options options; + if (formula) { + options = typename storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); + } + options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); + + // Then, build the model from the symbolic description. + result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); + } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd) { + typename storm::builder::DdPrismModelBuilder::Options options; + if (formula) { + options = typename storm::builder::DdPrismModelBuilder::Options(*formula.get()); + } + options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); + + storm::builder::DdPrismModelBuilder::translateProgram(program, options); } - options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); - storm::builder::DdPrismModelBuilder::translateProgram(program, options); return result; } @@ -425,6 +429,8 @@ namespace storm { STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed."); std::shared_ptr> model = buildSymbolicModel(program.get(), formula); + STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); + // Preprocess the model if needed. model = preprocessModel(model, formula); diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 52760783c..fdc283f5e 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -62,8 +62,15 @@ TEST(CuddDdManager, EncodingTest) { ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4)); EXPECT_EQ(1, encoding.getNonZeroCount()); - EXPECT_EQ(6, encoding.getNodeCount()); - EXPECT_EQ(2, encoding.getLeafCount()); + + // As a BDD, this DD has one only leaf, because there does not exist a 0-leaf, and (consequently) one node less + // than the MTBDD. + EXPECT_EQ(5, encoding.getNodeCount()); + 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()); } TEST(CuddDdManager, RangeTest) { @@ -75,8 +82,8 @@ TEST(CuddDdManager, RangeTest) { ASSERT_NO_THROW(range = manager->getRange(x.first)); EXPECT_EQ(9, range.getNonZeroCount()); - EXPECT_EQ(2, range.getLeafCount()); - EXPECT_EQ(6, range.getNodeCount()); + EXPECT_EQ(1, range.getLeafCount()); + EXPECT_EQ(5, range.getNodeCount()); } TEST(CuddDdManager, IdentityTest) { @@ -100,17 +107,14 @@ TEST(CuddDd, OperatorTest) { EXPECT_FALSE(manager->getZero() != manager->getZero()); EXPECT_TRUE(manager->getZero() != manager->getOne()); - storm::dd::Dd dd1 = manager->getOne(); - storm::dd::Dd dd2 = manager->getOne(); + storm::dd::Dd dd1 = manager->getOne(true); + storm::dd::Dd dd2 = manager->getOne(true); storm::dd::Dd dd3 = dd1 + dd2; EXPECT_TRUE(dd3 == manager->getConstant(2)); - dd3 += manager->getZero(); + dd3 += manager->getZero(true); EXPECT_TRUE(dd3 == manager->getConstant(2)); - dd3 = dd1 && manager->getConstant(3); - EXPECT_TRUE(dd1 == manager->getOne()); - dd3 = dd1 * manager->getConstant(3); EXPECT_TRUE(dd3 == manager->getConstant(3)); @@ -118,22 +122,22 @@ TEST(CuddDd, OperatorTest) { EXPECT_TRUE(dd3 == manager->getConstant(6)); dd3 = dd1 - dd2; - EXPECT_TRUE(dd3 == manager->getZero()); + EXPECT_TRUE(dd3.isZero()); dd3 -= manager->getConstant(-2); EXPECT_TRUE(dd3 == manager->getConstant(2)); dd3 /= manager->getConstant(2); - EXPECT_TRUE(dd3 == manager->getOne()); + EXPECT_TRUE(dd3.isOne()); - dd3.complement(); - EXPECT_TRUE(dd3 == manager->getZero()); + dd3 = dd3.toBdd().complement(); + EXPECT_TRUE(dd3.isZero()); dd1 = !dd3; - EXPECT_TRUE(dd1 == manager->getOne()); + EXPECT_TRUE(dd1.isOne()); - dd3 = dd1 || dd2; - EXPECT_TRUE(dd3 == manager->getOne()); + dd3 = dd1 || dd2.toBdd(); + EXPECT_TRUE(dd3.isOne()); dd1 = manager->getIdentity(x.first); dd2 = manager->getConstant(5); @@ -142,7 +146,7 @@ TEST(CuddDd, OperatorTest) { EXPECT_EQ(1, dd3.getNonZeroCount()); storm::dd::Dd dd4 = dd1.notEquals(dd2); - EXPECT_TRUE(dd4 == !dd3); + EXPECT_TRUE(dd4.toBdd() == !dd3.toBdd()); dd3 = dd1.less(dd2); EXPECT_EQ(11, dd3.getNonZeroCount()); @@ -161,12 +165,12 @@ TEST(CuddDd, OperatorTest) { EXPECT_EQ(10, dd4.getNonZeroCount()); dd4 = dd3.minimum(dd1); - dd4 *= manager->getEncoding(x.first, 2); + dd4 *= manager->getEncoding(x.first, 2, true); dd4 = dd4.sumAbstract({x.first}); EXPECT_EQ(2, dd4.getValue()); dd4 = dd3.maximum(dd1); - dd4 *= manager->getEncoding(x.first, 2); + dd4 *= manager->getEncoding(x.first, 2, true); dd4 = dd4.sumAbstract({x.first}); EXPECT_EQ(5, dd4.getValue()); @@ -197,7 +201,7 @@ TEST(CuddDd, AbstractionTest) { 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 == manager->getZero()); + EXPECT_TRUE(dd3.isOne()); dd3 = dd1.equals(dd2); dd3 *= manager->getConstant(3); @@ -253,7 +257,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(); + storm::dd::Dd dd1 = manager->getOne(true); ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2)); EXPECT_EQ(2, dd1.getLeafCount()); @@ -397,7 +401,7 @@ TEST(CuddDd, OddTest) { } // Create a non-trivial matrix. - dd = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)) * manager->getRange(x.first); + 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); // Create the ODDs.