diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index d17bbd3d4..c2452ed3b 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -359,6 +359,46 @@ namespace storm { } } + template + Bdd Bdd::renameVariablesConcretize(std::set const& from, std::set const& to) const { + std::vector> fromBdds; + std::vector> toBdds; + + for (auto const& metaVariable : from) { + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present."); + DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); + for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { + fromBdds.push_back(ddVariable.getInternalBdd()); + } + } + std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); + for (auto const& metaVariable : to) { + STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present."); + DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); + for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { + toBdds.push_back(ddVariable.getInternalBdd()); + } + } + std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); + + std::set newContainedMetaVariables = to; + std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin())); + + STORM_LOG_ASSERT(toBdds.size() >= fromBdds.size(), "Unable to perform rename-concretize with mismatching sizes."); + + if (fromBdds.size() == toBdds.size()) { + return Bdd(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); + } else { + InternalBdd negatedCube = this->getDdManager().getBddOne().getInternalBdd(); + for (uint64_t index = fromBdds.size(); index < toBdds.size(); ++index) { + negatedCube &= !toBdds[index]; + } + toBdds.resize(fromBdds.size()); + + return Bdd(this->getDdManager(), (internalBdd && negatedCube).swapVariables(fromBdds, toBdds), newContainedMetaVariables); + } + } + template template Add Bdd::toAdd() const { diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index c80e6a43b..bfb845c70 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -298,6 +298,19 @@ namespace storm { */ Bdd renameVariablesAbstract(std::set const& from, std::set const& to) const; + /*! + * Renames the given meta variables in the BDD. The number of the underlying DD variables of the from meta + * variable set needs to be at most as large as the to meta variable set. If the amount of variables coincide, + * this operation coincides with renameVariables. Otherwise, it first adds a unique encoding in terms of the + * superfluous variables and then performs the renaming. + * + * @param from The meta variables to be renamed. The current ADD needs to contain all these meta variables. + * @param to The meta variables that are the target of the renaming process. The current ADD must not contain + * any of these meta variables. + * @return The resulting ADD. + */ + Bdd renameVariablesConcretize(std::set const& from, std::set const& to) const; + /*! * Retrieves whether this DD represents the constant one function. * diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 593f1491a..108164a2a 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -936,10 +936,6 @@ namespace storm { bool useRepresentativesForThisExtraction = this->useRepresentatives; if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::MarkovAutomaton) { - if (modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::MarkovAutomaton) { - STORM_LOG_WARN_COND(!useRepresentativesForThisExtraction, "Using representatives is unsupported for MDPs, falling back to regular extraction."); - useRepresentativesForThisExtraction = false; - } // Sanity checks. STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size."); @@ -948,16 +944,20 @@ namespace storm { std::set blockVariableSet = {partition.getBlockVariable()}; std::set blockPrimeVariableSet = {partition.getPrimedBlockVariable()}; std::vector> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())}; + + auto start = std::chrono::high_resolution_clock::now(); + // Compute representatives. storm::dd::Bdd partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero(); + partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); + auto representatives = InternalRepresentativeComputer(partitionAsBdd, model.getRowVariables()).getRepresentatives(); + if (useRepresentativesForThisExtraction) { - storm::dd::Bdd partitionAsBddOverPrimedBlockVariable = partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet); - storm::dd::Bdd representativePartition = partitionAsBddOverPrimedBlockVariable.existsAbstractRepresentative(model.getColumnVariables()).renameVariables(model.getColumnVariables(), blockVariableSet); - partitionAsBdd = (representativePartition && partitionAsBddOverPrimedBlockVariable).existsAbstract(blockPrimeVariableSet); + storm::dd::Bdd partitionAsBddOverPrimedBlockVariables = partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet); + storm::dd::Bdd tmp = (representatives && partitionAsBddOverPrimedBlockVariables).renameVariablesConcretize(model.getRowVariables(), blockVariableSet); + partitionAsBdd = (tmp && partitionAsBddOverPrimedBlockVariables).existsAbstract(blockPrimeVariableSet); } - auto start = std::chrono::high_resolution_clock::now(); - partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); storm::dd::Bdd reachableStates = partitionAsBdd.existsAbstract(model.getRowVariables()); storm::dd::Bdd initialStates = (model.getInitialStates() && partitionAsBdd).existsAbstract(model.getRowVariables()); @@ -989,7 +989,6 @@ namespace storm { storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()); // Pick a representative from each block. - auto representatives = InternalRepresentativeComputer(partitionAsBdd, model.getRowVariables()).getRepresentatives(); partitionAsBdd &= representatives; partitionAsAdd *= partitionAsBdd.template toAdd(); @@ -1047,6 +1046,7 @@ namespace storm { std::shared_ptr> QuotientExtractor::extractQuotientUsingOriginalVariables(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation) { auto modelType = model.getType(); + bool useRepresentativesForThisExtraction = this->useRepresentatives; if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::MarkovAutomaton) { STORM_LOG_WARN_COND(!this->useRepresentatives, "Using representatives is unsupported for this extraction, falling back to regular extraction."); @@ -1058,10 +1058,19 @@ namespace storm { std::set blockPrimeVariableSet = {partition.getPrimedBlockVariable()}; std::vector> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())}; - storm::dd::Bdd partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero(); - auto start = std::chrono::high_resolution_clock::now(); + + // Compute representatives. + storm::dd::Bdd partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero(); partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); + auto representatives = InternalRepresentativeComputer(partitionAsBdd, model.getRowVariables()).getRepresentatives(); + + if (useRepresentativesForThisExtraction) { + storm::dd::Bdd partitionAsBddOverPrimedBlockVariables = partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet); + storm::dd::Bdd tmp = (representatives && partitionAsBddOverPrimedBlockVariables).renameVariablesConcretize(model.getRowVariables(), blockVariableSet); + partitionAsBdd = (tmp && partitionAsBddOverPrimedBlockVariables).existsAbstract(blockPrimeVariableSet); + } + storm::dd::Bdd reachableStates = partitionAsBdd.existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); storm::dd::Bdd initialStates = (model.getInitialStates() && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); @@ -1093,7 +1102,6 @@ namespace storm { storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(model.getRowVariables(), model.getColumnVariables()), model.getColumnVariables()).renameVariablesAbstract(blockVariableSet, model.getColumnVariables()); // Pick a representative from each block. - auto representatives = InternalRepresentativeComputer(partitionAsBdd, model.getRowVariables()).getRepresentatives(); partitionAsBdd &= representatives; partitionAsAdd = partitionAsBdd.template toAdd();