From 10f8ddc343076e0a99d79874b61a978ebcd702bb Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 27 Feb 2018 22:58:21 +0100 Subject: [PATCH 1/5] started on quotient extraction using the original variables, debugging CUDD... --- .../settings/modules/BisimulationSettings.cpp | 6 + .../settings/modules/BisimulationSettings.h | 8 ++ src/storm/storage/dd/Add.cpp | 40 ++++++ src/storm/storage/dd/Add.h | 14 ++ src/storm/storage/dd/Bdd.cpp | 38 +++++ src/storm/storage/dd/Bdd.h | 13 ++ .../dd/bisimulation/QuotientExtractor.cpp | 136 +++++++++++++++++- .../dd/bisimulation/QuotientExtractor.h | 4 +- src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 1 + .../storage/dd/sylvan/InternalSylvanAdd.h | 2 +- 10 files changed, 259 insertions(+), 3 deletions(-) diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index 8ed66dbdf..491958105 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -15,6 +15,7 @@ namespace storm { const std::string BisimulationSettings::moduleName = "bisimulation"; const std::string BisimulationSettings::typeOptionName = "type"; const std::string BisimulationSettings::representativeOptionName = "repr"; + const std::string BisimulationSettings::originalVariablesOptionName = "origvar"; const std::string BisimulationSettings::quotientFormatOptionName = "quot"; const std::string BisimulationSettings::signatureModeOptionName = "sigmode"; const std::string BisimulationSettings::reuseOptionName = "reuse"; @@ -29,6 +30,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, quotientFormatOptionName, true, "Sets the format in which the quotient is extracted (only applies to DD-based bisimulation).").addArgument(storm::settings::ArgumentBuilder::createStringArgument("format", "The format of the quotient.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(quotTypes)).setDefaultValueString("dd").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, representativeOptionName, false, "Sets whether to use representatives in the quotient rather than block numbers.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, originalVariablesOptionName, false, "Sets whether to use the original variables in the quotient rather than the block variables.").build()); std::vector signatureModes = { "eager", "lazy" }; this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build()); @@ -78,6 +80,10 @@ namespace storm { return this->getOption(representativeOptionName).getHasOptionBeenSet(); } + bool BisimulationSettings::isUseOriginalVariablesSet() const { + return this->getOption(originalVariablesOptionName).getHasOptionBeenSet(); + } + storm::dd::bisimulation::SignatureMode BisimulationSettings::getSignatureMode() const { std::string modeAsString = this->getOption(signatureModeOptionName).getArgumentByName("mode").getValueAsString(); if (modeAsString == "eager") { diff --git a/src/storm/settings/modules/BisimulationSettings.h b/src/storm/settings/modules/BisimulationSettings.h index a482263bc..eb9627f68 100644 --- a/src/storm/settings/modules/BisimulationSettings.h +++ b/src/storm/settings/modules/BisimulationSettings.h @@ -56,6 +56,13 @@ namespace storm { */ bool isUseRepresentativesSet() const; + /*! + * Retrieves whether the extracted quotient model is supposed to use the same variables as the original + * model. + * NOTE: only applies to DD-based bisimulation. + */ + bool isUseOriginalVariablesSet() const; + /*! * Retrieves the mode to compute signatures. */ @@ -85,6 +92,7 @@ namespace storm { // Define the string names of the options as constants. static const std::string typeOptionName; static const std::string representativeOptionName; + static const std::string originalVariablesOptionName; static const std::string quotientFormatOptionName; static const std::string signatureModeOptionName; static const std::string reuseOptionName; diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 635d16aed..91a00a497 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -231,6 +231,46 @@ namespace storm { return Add(this->getDdManager(), internalAdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); } + template + Add Add::renameVariablesAbstract(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::cout << "from - idx " << ddVariable.getInternalBdd().getIndex() << ", lvl " << ddVariable.getInternalBdd().getLevel() << std::endl; + } + } +// 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::cout << "to - idx " << ddVariable.getInternalBdd().getIndex() << ", lvl " << ddVariable.getInternalBdd().getLevel() << std::endl; + } + } +// 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())); + + if (fromBdds.size() == toBdds.size()) { + return Add(this->getDdManager(), internalAdd.permuteVariables(fromBdds, toBdds), newContainedMetaVariables); + } else { + InternalBdd cube = this->getDdManager().getBddOne().getInternalBdd(); + for (uint64_t index = fromBdds.size(); index < fromBdds.size(); ++index) { + cube &= fromBdds[index]; + } + fromBdds.resize(toBdds.size()); + + return Add(this->getDdManager(), internalAdd.sumAbstract(cube).permuteVariables(fromBdds, toBdds), newContainedMetaVariables); + } + } + template Add Add::swapVariables(std::vector> const& metaVariablePairs) const { std::set newContainedMetaVariables; diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index c25b5a8c4..1a4a811d5 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -331,6 +331,20 @@ namespace storm { */ Add renameVariables(std::set const& from, std::set const& to) const; + /*! + * Renames the given meta variables in the ADD. The number of the underlying DD variables of the from meta + * variable set needs to be at least as large as the to meta variable set. If the amount of variables coincide, + * this operation coincides with renameVariables. Otherwise, it first abstracts from 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. + */ + Add renameVariablesAbstract(std::set const& from, std::set const& to) const; + + /*! * Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have * the same number of underlying ADD variables. diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index 66c6d69a7..f1fee9ab6 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -319,6 +319,44 @@ namespace storm { return Bdd(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); } + template + Bdd Bdd::renameVariablesAbstract(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())); + + if (fromBdds.size() == toBdds.size()) { + return Bdd(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); + } else { + InternalBdd cube = this->getDdManager().getBddOne().getInternalBdd(); + for (uint64_t index = fromBdds.size(); index < fromBdds.size(); ++index) { + cube &= fromBdds[index]; + } + fromBdds.resize(toBdds.size()); + + return Bdd(this->getDdManager(), internalBdd.existsAbstract(cube).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 41d6b2b86..c80e6a43b 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -285,6 +285,19 @@ namespace storm { */ Bdd renameVariables(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 least as large as the to meta variable set. If the amount of variables coincide, + * this operation coincides with renameVariables. Otherwise, it first abstracts from 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 renameVariablesAbstract(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 340b191fe..dd1ce6d6b 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -821,6 +821,7 @@ namespace storm { QuotientExtractor::QuotientExtractor() : useRepresentatives(false) { auto const& settings = storm::settings::getModule(); this->useRepresentatives = settings.isUseRepresentativesSet(); + this->useOriginalVariables = settings.isUseOriginalVariablesSet(); this->quotientFormat = settings.getQuotientFormat(); } @@ -921,7 +922,12 @@ namespace storm { template std::shared_ptr> QuotientExtractor::extractDdQuotient(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation) { - return extractQuotientUsingBlockVariables(model, partition, preservationInformation); + + if (this->useOriginalVariables) { + return extractQuotientUsingOriginalVariables(model, partition, preservationInformation); + } else { + return extractQuotientUsingBlockVariables(model, partition, preservationInformation); + } } template @@ -1036,6 +1042,134 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type."); } } + + template + std::shared_ptr> QuotientExtractor::extractQuotientUsingOriginalVariables(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation) { + auto modelType = model.getType(); + + 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."); + + // Sanity checks. + STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size."); + STORM_LOG_ASSERT(partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()) == model.getReachableStates(), "Mismatching partition."); + + std::set blockVariableSet = {partition.getBlockVariable()}; + 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(); + partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); + 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()); + + std::map> preservedLabelBdds; + for (auto const& label : preservationInformation.getLabels()) { + preservedLabelBdds.emplace(label, (model.getStates(label) && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables())); + } + for (auto const& expression : preservationInformation.getExpressions()) { + std::stringstream stream; + stream << expression; + std::string expressionAsString = stream.str(); + + auto it = preservedLabelBdds.find(expressionAsString); + if (it != preservedLabelBdds.end()) { + STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition."); + } else { + preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables())); + } + } + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + + start = std::chrono::high_resolution_clock::now(); + std::set blockAndRowVariables; + std::set_union(blockVariableSet.begin(), blockVariableSet.end(), model.getRowVariables().begin(), model.getRowVariables().end(), std::inserter(blockAndRowVariables, blockAndRowVariables.end())); + std::set blockPrimeAndColumnVariables; + std::set_union(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end(), model.getColumnVariables().begin(), model.getColumnVariables().end(), std::inserter(blockPrimeAndColumnVariables, blockPrimeAndColumnVariables.end())); + storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); + storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()).renameVariablesAbstract(blockPrimeVariableSet, model.getColumnVariables()); + (model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()).renameVariablesAbstract(blockPrimeVariableSet, model.getColumnVariables())).exportToDot("tmp0.dot"); + quotientTransitionMatrix.exportToDot("tmp1.dot"); + std::cout << "q1 size: " << quotientTransitionMatrix.getNodeCount() << ", " << quotientTransitionMatrix.getNonZeroCount() << std::endl; + quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).exportToDot("tmp1_1.dot"); +// quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).exportToDot("tmp1_1.dot"); + + // Pick a representative from each block. + auto representatives = InternalRepresentativeComputer(partitionAsBdd, model.getRowVariables()).getRepresentatives(); + partitionAsBdd &= representatives; + partitionAsAdd *= partitionAsBdd.template toAdd(); + partitionAsAdd.exportToDot("partrepr.dot"); + partitionAsAdd.sumAbstract(model.getRowVariables()).exportToDot("part2.dot"); + std::cout << "part size " << partitionAsAdd.getNodeCount() << ", " << partitionAsAdd.getNonZeroCount() << std::endl; + + auto tmp1 = partitionAsAdd.multiplyMatrix(quotientTransitionMatri, model.getRowVariables()); + auto tmp2 = (quotientTransitionMatrix * partitionAsAdd).sumAbstract(model.getRowVariables()); + std::cout << "size1: " << tmp1.getNodeCount() << ", " << tmp1.getNonZeroCount() << std::endl; + std::cout << "size2: " << tmp2.getNodeCount() << ", " << tmp2.getNonZeroCount() << std::endl; + if (tmp1 != tmp2) { + tmp1.exportToDot("tmp1__.dot"); + tmp2.exportToDot("tmp2__.dot"); + (tmp2-tmp1).exportToDot("diff.dot"); + STORM_LOG_ASSERT(false, "error"); + } + quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).exportToDot("tmp2.dot"); + quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).sumAbstract(model.getColumnVariables()).exportToDot("tmp2_2.dot"); +// quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).sumAbstract(blockPrimeVariableSet).exportToDot("tmp2_2.dot"); + quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); + end = std::chrono::high_resolution_clock::now(); + + // Check quotient matrix for sanity. + if (std::is_same::value) { + STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one()).isZero(), "Illegal entries in quotient matrix."); + } else { + STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one() + storm::utility::convertNumber(1e-6)).isZero(), "Illegal entries in quotient matrix."); + } + quotientTransitionMatrix.exportToDot("trans.dot"); + quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).exportToDot("trans1.dot"); + quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd().exportToDot("trans2.dot"); + STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd(), storm::utility::convertNumber(1e-6)), "Illegal probabilistic matrix."); + + STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + + storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); + storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(model.getColumnVariables()) && reachableStates; + + start = std::chrono::high_resolution_clock::now(); + std::unordered_map> quotientRewardModels; + for (auto const& rewardModelName : preservationInformation.getRewardModelNames()) { + auto const& rewardModel = model.getRewardModel(rewardModelName); + + boost::optional> quotientStateRewards; + if (rewardModel.hasStateRewards()) { + quotientStateRewards = rewardModel.getStateRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); + } + + boost::optional> quotientStateActionRewards; + if (rewardModel.hasStateActionRewards()) { + quotientStateActionRewards = rewardModel.getStateActionRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); + } + + quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel(quotientStateRewards, quotientStateActionRewards, boost::none)); + } + end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + + if (modelType == storm::models::ModelType::Dtmc) { + return std::shared_ptr>(new storm::models::symbolic::Dtmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels)); + } else if (modelType == storm::models::ModelType::Ctmc) { + return std::shared_ptr>(new storm::models::symbolic::Ctmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels)); + } else if (modelType == storm::models::ModelType::Mdp) { + return std::shared_ptr>(new storm::models::symbolic::Mdp(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); + } else { + return std::shared_ptr>(new storm::models::symbolic::MarkovAutomaton(model.getManager().asSharedPointer(), model. template as>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type."); + } + } template class QuotientExtractor; diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.h b/src/storm/storage/dd/bisimulation/QuotientExtractor.h index dcce31659..b75b27b08 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.h +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.h @@ -28,8 +28,10 @@ namespace storm { std::shared_ptr> extractDdQuotient(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation); std::shared_ptr> extractQuotientUsingBlockVariables(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation); - + std::shared_ptr> extractQuotientUsingOriginalVariables(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation); + bool useRepresentatives; + bool useOriginalVariables; storm::settings::modules::BisimulationSettings::QuotientFormat quotientFormat; }; diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 11c6b12ca..158060519 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -202,6 +202,7 @@ namespace storm { for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { fromAdd.push_back(it1->getCuddBdd().Add()); toAdd.push_back(it2->getCuddBdd().Add()); + std::cout << fromAdd.back().NodeReadIndex() << " <-> " << toAdd.back().NodeReadIndex() << std::endl; } return InternalAdd(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd)); } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index dc65e240a..5137caf15 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -319,7 +319,7 @@ namespace storm { * @return The resulting ADD. */ InternalAdd swapVariables(std::vector> const& from, std::vector> const& to) const; - + /*! * Permutes the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by * ADDs must have equal length. From 27d6e48dad29607e62f01a40d9fe6beac0644901 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 28 Feb 2018 14:48:08 +0100 Subject: [PATCH 2/5] workaround for quotient extraction using the original variables --- src/storm/storage/dd/Add.cpp | 10 ++--- src/storm/storage/dd/Bdd.cpp | 4 +- .../dd/bisimulation/QuotientExtractor.cpp | 41 +++++-------------- src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 1 - src/test/storm/storage/CuddDdTest.cpp | 23 +++++++++++ 5 files changed, 42 insertions(+), 37 deletions(-) diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 91a00a497..9e91b2123 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -241,28 +241,28 @@ namespace storm { DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { fromBdds.push_back(ddVariable.getInternalBdd()); - std::cout << "from - idx " << ddVariable.getInternalBdd().getIndex() << ", lvl " << ddVariable.getInternalBdd().getLevel() << std::endl; } } -// std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); + 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::cout << "to - idx " << ddVariable.getInternalBdd().getIndex() << ", lvl " << ddVariable.getInternalBdd().getLevel() << std::endl; } } -// std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); + 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(fromBdds.size() >= toBdds.size(), "Unable to perform rename-abstract with mismatching sizes."); + if (fromBdds.size() == toBdds.size()) { return Add(this->getDdManager(), internalAdd.permuteVariables(fromBdds, toBdds), newContainedMetaVariables); } else { InternalBdd cube = this->getDdManager().getBddOne().getInternalBdd(); - for (uint64_t index = fromBdds.size(); index < fromBdds.size(); ++index) { + for (uint64_t index = toBdds.size(); index < fromBdds.size(); ++index) { cube &= fromBdds[index]; } fromBdds.resize(toBdds.size()); diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index f1fee9ab6..d17bbd3d4 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -344,11 +344,13 @@ namespace storm { 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(fromBdds.size() >= toBdds.size(), "Unable to perform rename-abstract with mismatching sizes."); + if (fromBdds.size() == toBdds.size()) { return Bdd(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); } else { InternalBdd cube = this->getDdManager().getBddOne().getInternalBdd(); - for (uint64_t index = fromBdds.size(); index < fromBdds.size(); ++index) { + for (uint64_t index = toBdds.size(); index < fromBdds.size(); ++index) { cube &= fromBdds[index]; } fromBdds.resize(toBdds.size()); diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index dd1ce6d6b..e28c80aaa 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -1090,35 +1090,19 @@ namespace storm { std::set blockPrimeAndColumnVariables; std::set_union(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end(), model.getColumnVariables().begin(), model.getColumnVariables().end(), std::inserter(blockPrimeAndColumnVariables, blockPrimeAndColumnVariables.end())); storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); - storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()).renameVariablesAbstract(blockPrimeVariableSet, model.getColumnVariables()); - (model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()).renameVariablesAbstract(blockPrimeVariableSet, model.getColumnVariables())).exportToDot("tmp0.dot"); - quotientTransitionMatrix.exportToDot("tmp1.dot"); - std::cout << "q1 size: " << quotientTransitionMatrix.getNodeCount() << ", " << quotientTransitionMatrix.getNonZeroCount() << std::endl; - quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).exportToDot("tmp1_1.dot"); -// quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).exportToDot("tmp1_1.dot"); + 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(); - partitionAsAdd.exportToDot("partrepr.dot"); - partitionAsAdd.sumAbstract(model.getRowVariables()).exportToDot("part2.dot"); - std::cout << "part size " << partitionAsAdd.getNodeCount() << ", " << partitionAsAdd.getNonZeroCount() << std::endl; - - auto tmp1 = partitionAsAdd.multiplyMatrix(quotientTransitionMatri, model.getRowVariables()); - auto tmp2 = (quotientTransitionMatrix * partitionAsAdd).sumAbstract(model.getRowVariables()); - std::cout << "size1: " << tmp1.getNodeCount() << ", " << tmp1.getNonZeroCount() << std::endl; - std::cout << "size2: " << tmp2.getNodeCount() << ", " << tmp2.getNonZeroCount() << std::endl; - if (tmp1 != tmp2) { - tmp1.exportToDot("tmp1__.dot"); - tmp2.exportToDot("tmp2__.dot"); - (tmp2-tmp1).exportToDot("diff.dot"); - STORM_LOG_ASSERT(false, "error"); + partitionAsAdd = partitionAsBdd.template toAdd(); + + // Workaround for problem with CUDD. Matrix-Matrix multiplication yields other result than multiplication+sum-abstract... + if (DdType == storm::dd::DdType::CUDD) { + quotientTransitionMatrix = (quotientTransitionMatrix * partitionAsAdd).sumAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); + } else { + quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); } - quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).exportToDot("tmp2.dot"); - quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).sumAbstract(model.getColumnVariables()).exportToDot("tmp2_2.dot"); -// quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).sumAbstract(blockPrimeVariableSet).exportToDot("tmp2_2.dot"); - quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); end = std::chrono::high_resolution_clock::now(); // Check quotient matrix for sanity. @@ -1127,9 +1111,6 @@ namespace storm { } else { STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one() + storm::utility::convertNumber(1e-6)).isZero(), "Illegal entries in quotient matrix."); } - quotientTransitionMatrix.exportToDot("trans.dot"); - quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).exportToDot("trans1.dot"); - quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd().exportToDot("trans2.dot"); STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd(), storm::utility::convertNumber(1e-6)), "Illegal probabilistic matrix."); STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); @@ -1160,11 +1141,11 @@ namespace storm { if (modelType == storm::models::ModelType::Dtmc) { return std::shared_ptr>(new storm::models::symbolic::Dtmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels)); } else if (modelType == storm::models::ModelType::Ctmc) { - return std::shared_ptr>(new storm::models::symbolic::Ctmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Ctmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels)); } else if (modelType == storm::models::ModelType::Mdp) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Mdp(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); } else { - return std::shared_ptr>(new storm::models::symbolic::MarkovAutomaton(model.getManager().asSharedPointer(), model. template as>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); + return std::shared_ptr>(new storm::models::symbolic::MarkovAutomaton(model.getManager().asSharedPointer(), model. template as>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); } } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type."); diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 158060519..11c6b12ca 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -202,7 +202,6 @@ namespace storm { for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { fromAdd.push_back(it1->getCuddBdd().Add()); toAdd.push_back(it2->getCuddBdd().Add()); - std::cout << fromAdd.back().NodeReadIndex() << " <-> " << toAdd.back().NodeReadIndex() << std::endl; } return InternalAdd(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd)); } diff --git a/src/test/storm/storage/CuddDdTest.cpp b/src/test/storm/storage/CuddDdTest.cpp index 499be2a12..bc6ffab10 100644 --- a/src/test/storm/storage/CuddDdTest.cpp +++ b/src/test/storm/storage/CuddDdTest.cpp @@ -589,6 +589,29 @@ TEST(CuddDd, MultiplyMatrixTest) { EXPECT_TRUE(dd3 == dd2 * manager->template getConstant(2)); } +TEST(CuddDd, MultiplyMatrixTest2) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 0, 2); + std::pair b = manager->addMetaVariable("b", 0, 2); + + storm::dd::Add p = manager->getAddZero(); + p += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(b.first, 0, true)).template toAdd(); + p += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(b.first, 2, true)).template toAdd(); + + storm::dd::Add q = manager->getAddZero(); + q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 0, true)).template toAdd() * manager->template getConstant(0.3); + q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 0, true)).template toAdd() * manager->template getConstant(0.3); + q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 2, true)).template toAdd() * manager->template getConstant(0.7); + q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 2, true)).template toAdd() * manager->template getConstant(0.7); + q += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(x.second, 0, true)).template toAdd() * manager->template getConstant(1); + + storm::dd::Add r = q.multiplyMatrix(p, {x.first}); + + ASSERT_EQ(12, r.getNodeCount()); + ASSERT_EQ(4, r.getLeafCount()); + ASSERT_EQ(3, r.getNonZeroCount()); +} + TEST(CuddDd, GetSetValueTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); From 24cca08ccf5cb1285b5381d50e330920b4940376 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 1 Mar 2018 09:28:18 +0100 Subject: [PATCH 3/5] disabling LTO for gcc >= 7 --- CMakeLists.txt | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index e78152e06..f284dae11 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -181,9 +181,15 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang") set(STORM_COMPILER_ID "AppleClang") set(CMAKE_MACOSX_RPATH ON) elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU") + set(GCC ON) # using GCC if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 5.0) message(FATAL_ERROR "gcc version must be at least 5.0.") + elseif (CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 7.0 OR CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 7.0) + if (STORM_USE_LTO) + set(STORM_USE_LTO OFF) + message(WARNING "Disabling link-time optimization, because of known incompatibility of LTO with gcc >= 7.") + endif() endif() set(STORM_COMPILER_GCC ON) From 34b6593ed86f241466f0758ea07e484f6a033488 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 1 Mar 2018 22:09:06 +0100 Subject: [PATCH 4/5] overhauled output of dd-based bisimulation for benchmarking --- .../settings/modules/BisimulationSettings.cpp | 2 +- .../SymbolicNativeLinearEquationSolver.cpp | 2 +- .../storage/dd/BisimulationDecomposition.cpp | 47 +++++++++---------- .../storage/dd/BisimulationDecomposition.h | 2 +- .../NondeterministicModelPartitionRefiner.cpp | 11 ++++- .../storage/dd/bisimulation/Partition.cpp | 10 +++- .../dd/bisimulation/PartitionRefiner.cpp | 5 +- .../dd/bisimulation/QuotientExtractor.cpp | 20 ++++---- src/storm/utility/dd.cpp | 2 +- src/test/storm/storage/CuddDdTest.cpp | 6 +-- 10 files changed, 59 insertions(+), 48 deletions(-) diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index 491958105..56b3419e9 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -15,7 +15,7 @@ namespace storm { const std::string BisimulationSettings::moduleName = "bisimulation"; const std::string BisimulationSettings::typeOptionName = "type"; const std::string BisimulationSettings::representativeOptionName = "repr"; - const std::string BisimulationSettings::originalVariablesOptionName = "origvar"; + const std::string BisimulationSettings::originalVariablesOptionName = "origvars"; const std::string BisimulationSettings::quotientFormatOptionName = "quot"; const std::string BisimulationSettings::signatureModeOptionName = "sigmode"; const std::string BisimulationSettings::reuseOptionName = "reuse"; diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index 4252b1483..7c25f0e35 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -88,7 +88,7 @@ namespace storm { storm::dd::Add lu = diagonal.ite(manager.template getAddZero(), this->A); storm::dd::Add diagonalAdd = diagonal.template toAdd(); storm::dd::Add diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables); - + storm::dd::Add scaledLu = lu / diag; storm::dd::Add scaledB = b / diag; diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index 386653329..b19142b1d 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -57,14 +57,16 @@ namespace storm { template void BisimulationDecomposition::initialize() { auto const& generalSettings = storm::settings::getModule(); - showProgress = generalSettings.isVerboseSet(); + verboseProgress = generalSettings.isVerboseSet(); showProgressDelay = generalSettings.getShowProgressDelay(); + + auto start = std::chrono::high_resolution_clock::now(); this->refineWrtRewardModels(); + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_INFO("Refining with respect to reward models took " << std::chrono::duration_cast(end - start).count() << "ms."); - STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); -#ifndef NDEBUG + STORM_LOG_INFO("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes."); -#endif } template @@ -80,21 +82,18 @@ namespace storm { refined = refiner->refine(mode); ++iterations; - STORM_LOG_TRACE("After iteration " << iterations << " partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); - if (showProgress) { - auto now = std::chrono::high_resolution_clock::now(); - auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); - if (static_cast(durationSinceLastMessage) >= showProgressDelay) { - auto durationSinceStart = std::chrono::duration_cast(now - start).count(); - STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "s) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); - timeOfLastMessage = std::chrono::high_resolution_clock::now(); - } + auto now = std::chrono::high_resolution_clock::now(); + auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); + if (static_cast(durationSinceLastMessage) >= showProgressDelay * 1000 || verboseProgress) { + auto durationSinceStart = std::chrono::duration_cast(now - start).count(); + STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); + timeOfLastMessage = std::chrono::high_resolution_clock::now(); } } auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Partition refinement completed in " << std::chrono::duration_cast(end - start).count() << "ms (" << iterations << " iterations)."); + STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast(end - start).count() << "ms (" << iterations << " iterations)."); } template @@ -112,14 +111,12 @@ namespace storm { ++iterations; - if (showProgress) { - auto now = std::chrono::high_resolution_clock::now(); - auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); - if (static_cast(durationSinceLastMessage) >= showProgressDelay) { - auto durationSinceStart = std::chrono::duration_cast(now - start).count(); - STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); - timeOfLastMessage = std::chrono::high_resolution_clock::now(); - } + auto now = std::chrono::high_resolution_clock::now(); + auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); + if (static_cast(durationSinceLastMessage) >= showProgressDelay || verboseProgress) { + auto durationSinceStart = std::chrono::duration_cast(now - start).count(); + STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); + timeOfLastMessage = std::chrono::high_resolution_clock::now(); } } @@ -135,13 +132,13 @@ namespace storm { std::shared_ptr> BisimulationDecomposition::getQuotient() const { std::shared_ptr> quotient; if (this->refiner->getStatus() == Status::FixedPoint) { - STORM_LOG_TRACE("Starting full quotient extraction."); + STORM_LOG_INFO("Starting full quotient extraction."); QuotientExtractor extractor; quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation); } else { STORM_LOG_THROW(model.getType() == storm::models::ModelType::Dtmc || model.getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidOperationException, "Can only extract partial quotient for discrete-time models."); - STORM_LOG_TRACE("Starting partial quotient extraction."); + STORM_LOG_INFO("Starting partial quotient extraction."); if (!partialQuotientExtractor) { partialQuotientExtractor = std::make_unique>(model); } @@ -149,7 +146,7 @@ namespace storm { quotient = partialQuotientExtractor->extract(refiner->getStatePartition(), preservationInformation); } - STORM_LOG_TRACE("Quotient extraction done."); + STORM_LOG_INFO("Quotient extraction done."); return quotient; } diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h index 21ff7de2a..b5a088ca2 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.h +++ b/src/storm/storage/dd/BisimulationDecomposition.h @@ -83,7 +83,7 @@ namespace storm { mutable std::unique_ptr> partialQuotientExtractor; // A flag indicating whether progress is reported. - bool showProgress; + bool verboseProgress; // The delay between progress reports. uint64_t showProgressDelay; diff --git a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp index 67fd21e8c..1bf58a5ad 100644 --- a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp @@ -42,12 +42,21 @@ namespace storm { } else { choicePartitionAsBdd = this->choicePartition.asAdd().notZero(); } - Signature stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd()); + auto signatureStart = std::chrono::high_resolution_clock::now(); + Signature stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd()); + auto signatureEnd = std::chrono::high_resolution_clock::now(); + // If the choice partition changed, refine the state partition. STORM_LOG_TRACE("Refining state partition."); + auto refinementStart = std::chrono::high_resolution_clock::now(); Partition newStatePartition = this->internalRefine(stateSignature, this->stateSignatureRefiner, this->statePartition); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + auto signatureTime = std::chrono::duration_cast(signatureEnd - signatureStart).count(); + auto refinementTime = std::chrono::duration_cast(refinementEnd - refinementStart).count(); + STORM_LOG_INFO("Refinement " << (this->refinements-1) << " produced " << newStatePartition.getNumberOfBlocks() << " blocks and was completed in " << (signatureTime + refinementTime) << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms)."); + if (newStatePartition == this->statePartition) { this->status = Status::FixedPoint; return false; diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index d3708c6a5..6ada72f6b 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -130,6 +130,8 @@ namespace storm { std::pair blockVariables = createBlockVariables(model); + auto start = std::chrono::high_resolution_clock::now(); + // Set up the construction. storm::dd::DdManager& manager = model.getManager(); storm::dd::Bdd partitionBdd = manager.getBddZero(); @@ -153,6 +155,9 @@ namespace storm { // Move the partition over to the primed variables. partitionBdd = partitionBdd.swapVariables(model.getRowColumnMetaVariablePairs()); + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_INFO("Created distance and label-based initial partition in " << std::chrono::duration_cast(end - start).count() << "ms."); + // Store the partition as an ADD only in the case of CUDD. if (DdType == storm::dd::DdType::CUDD) { return Partition(partitionBdd.template toAdd(), blockVariables, blockCount, blockCount); @@ -191,8 +196,11 @@ namespace storm { for (auto const& expression : expressions) { stateSets.emplace_back(model.getStates(expression)); } + auto start = std::chrono::high_resolution_clock::now(); std::pair, uint64_t> partitionBddAndBlockCount = createPartitionBdd(model.getManager(), model, stateSets, blockVariables.first); - + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_INFO("Created label-based initial partition in " << std::chrono::duration_cast(end - start).count() << "ms."); + // Store the partition as an ADD only in the case of CUDD. if (DdType == storm::dd::DdType::CUDD) { return Partition(partitionBddAndBlockCount.first.template toAdd(), blockVariables, partitionBddAndBlockCount.second, partitionBddAndBlockCount.second); diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index 476bd5285..94a6d3666 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -66,7 +66,7 @@ namespace storm { } auto totalTimeInRefinement = std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - start).count(); - STORM_LOG_TRACE("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms)."); + STORM_LOG_INFO("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms)."); ++refinements; return newPartition; } else { @@ -78,10 +78,7 @@ namespace storm { Partition PartitionRefiner::internalRefine(Signature const& signature, SignatureRefiner& signatureRefiner, Partition const& oldPartition) { STORM_LOG_TRACE("Signature " << refinements << " DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); - auto start = std::chrono::high_resolution_clock::now(); auto newPartition = signatureRefiner.refine(oldPartition, signature); - auto totalTimeInRefinement = std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - start).count(); - STORM_LOG_TRACE("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms."); ++refinements; return newPartition; diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index e28c80aaa..593f1491a 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -835,7 +835,7 @@ namespace storm { result = extractDdQuotient(model, partition, preservationInformation); } auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Quotient extraction completed in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient extraction completed in " << std::chrono::duration_cast(end - start).count() << "ms."); STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "Quotient could not be extracted."); @@ -856,7 +856,7 @@ namespace storm { InternalSparseQuotientExtractor sparseExtractor(model, partitionAsBdd, partition.getBlockVariable(), partition.getNumberOfBlocks(), representatives); storm::storage::SparseMatrix quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix()); auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); start = std::chrono::high_resolution_clock::now(); storm::models::sparse::StateLabeling quotientStateLabeling(partition.getNumberOfBlocks()); @@ -878,7 +878,7 @@ namespace storm { } } end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); start = std::chrono::high_resolution_clock::now(); std::unordered_map> quotientRewardModels; @@ -898,7 +898,7 @@ namespace storm { quotientRewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel(std::move(quotientStateRewards), std::move(quotientStateActionRewards), boost::none)); } end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); std::shared_ptr> result; if (model.getType() == storm::models::ModelType::Dtmc) { @@ -978,7 +978,7 @@ namespace storm { } } auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); start = std::chrono::high_resolution_clock::now(); std::set blockAndRowVariables; @@ -1004,7 +1004,7 @@ namespace storm { } STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd(), storm::utility::convertNumber(1e-6)), "Illegal non-probabilistic matrix."); - STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates; @@ -1027,7 +1027,7 @@ namespace storm { quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel(quotientStateRewards, quotientStateActionRewards, boost::none)); } end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); if (modelType == storm::models::ModelType::Dtmc) { return std::shared_ptr>(new storm::models::symbolic::Dtmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels)); @@ -1082,7 +1082,7 @@ namespace storm { } } auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); start = std::chrono::high_resolution_clock::now(); std::set blockAndRowVariables; @@ -1113,7 +1113,7 @@ namespace storm { } STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd(), storm::utility::convertNumber(1e-6)), "Illegal probabilistic matrix."); - STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(model.getColumnVariables()) && reachableStates; @@ -1136,7 +1136,7 @@ namespace storm { quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel(quotientStateRewards, quotientStateActionRewards, boost::none)); } end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); if (modelType == storm::models::ModelType::Dtmc) { return std::shared_ptr>(new storm::models::symbolic::Dtmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels)); diff --git a/src/storm/utility/dd.cpp b/src/storm/utility/dd.cpp index 47d15347e..626dc845f 100644 --- a/src/storm/utility/dd.cpp +++ b/src/storm/utility/dd.cpp @@ -47,7 +47,7 @@ namespace storm { template storm::dd::Bdd getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs) { - return ddManager.getIdentity(rowColumnMetaVariablePairs); + return ddManager.getIdentity(rowColumnMetaVariablePairs, false); } template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); diff --git a/src/test/storm/storage/CuddDdTest.cpp b/src/test/storm/storage/CuddDdTest.cpp index bc6ffab10..c1ae09561 100644 --- a/src/test/storm/storage/CuddDdTest.cpp +++ b/src/test/storm/storage/CuddDdTest.cpp @@ -607,9 +607,9 @@ TEST(CuddDd, MultiplyMatrixTest2) { storm::dd::Add r = q.multiplyMatrix(p, {x.first}); - ASSERT_EQ(12, r.getNodeCount()); - ASSERT_EQ(4, r.getLeafCount()); - ASSERT_EQ(3, r.getNonZeroCount()); + ASSERT_EQ(12ull, r.getNodeCount()); + ASSERT_EQ(4ull, r.getLeafCount()); + ASSERT_EQ(3ull, r.getNonZeroCount()); } TEST(CuddDd, GetSetValueTest) { From 66e08f9cd77a007113a2bc295fda4df9b96b35bf Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 2 Mar 2018 09:05:01 +0100 Subject: [PATCH 5/5] more time output in dd-based bisimulation --- .../storage/dd/BisimulationDecomposition.cpp | 2 +- .../NondeterministicModelPartitionRefiner.cpp | 3 ++- .../dd/bisimulation/PartitionRefiner.cpp | 19 ++++++++++++++++--- .../dd/bisimulation/PartitionRefiner.h | 3 +++ 4 files changed, 22 insertions(+), 5 deletions(-) diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index b19142b1d..682f5602d 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -93,7 +93,7 @@ namespace storm { } auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast(end - start).count() << "ms (" << iterations << " iterations)."); + STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast(end - start).count() << "ms (" << iterations << " iterations, signature: " << std::chrono::duration_cast(refiner->getTotalSignatureTime()).count() << "ms, refinement: " << std::chrono::duration_cast(refiner->getTotalRefinementTime()).count() << "ms)."); } template diff --git a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp index 1bf58a5ad..129c426c7 100644 --- a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp @@ -46,7 +46,8 @@ namespace storm { auto signatureStart = std::chrono::high_resolution_clock::now(); Signature stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd()); auto signatureEnd = std::chrono::high_resolution_clock::now(); - + this->totalSignatureTime += (signatureEnd - signatureStart); + // If the choice partition changed, refine the state partition. STORM_LOG_TRACE("Refining state partition."); auto refinementStart = std::chrono::high_resolution_clock::now(); diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index 94a6d3666..87af0987b 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -12,7 +12,7 @@ namespace storm { namespace bisimulation { template - PartitionRefiner::PartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getColumnVariables(), !model.isNondeterministicModel(), model.getNondeterminismVariables()) { + PartitionRefiner::PartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getColumnVariables(), !model.isNondeterministicModel(), model.getNondeterminismVariables()), totalSignatureTime(0), totalRefinementTime(0) { // Intentionally left empty. } @@ -50,7 +50,7 @@ namespace storm { auto signatureEnd = std::chrono::high_resolution_clock::now(); totalSignatureTime += (signatureEnd - signatureStart); STORM_LOG_TRACE("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); - + auto refinementStart = std::chrono::high_resolution_clock::now(); newPartition = signatureRefiner.refine(oldPartition, signature); auto refinementEnd = std::chrono::high_resolution_clock::now(); @@ -78,8 +78,11 @@ namespace storm { Partition PartitionRefiner::internalRefine(Signature const& signature, SignatureRefiner& signatureRefiner, Partition const& oldPartition) { STORM_LOG_TRACE("Signature " << refinements << " DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); + auto refinementStart = std::chrono::high_resolution_clock::now(); auto newPartition = signatureRefiner.refine(oldPartition, signature); - + auto refinementEnd = std::chrono::high_resolution_clock::now(); + totalRefinementTime += (refinementEnd - refinementStart); + ++refinements; return newPartition; } @@ -132,6 +135,16 @@ namespace storm { return status; } + template + std::chrono::high_resolution_clock::duration PartitionRefiner::getTotalSignatureTime() const { + return totalSignatureTime; + } + + template + std::chrono::high_resolution_clock::duration PartitionRefiner::getTotalRefinementTime() const { + return totalRefinementTime; + } + template class PartitionRefiner; template class PartitionRefiner; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.h b/src/storm/storage/dd/bisimulation/PartitionRefiner.h index d4e59a207..4716a811a 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.h @@ -53,6 +53,9 @@ namespace storm { */ Status getStatus() const; + std::chrono::high_resolution_clock::duration getTotalSignatureTime() const; + std::chrono::high_resolution_clock::duration getTotalRefinementTime() const; + protected: Partition internalRefine(SignatureComputer& stateSignatureComputer, SignatureRefiner& signatureRefiner, Partition const& oldPartition, Partition const& targetPartition, SignatureMode const& mode = SignatureMode::Eager); Partition internalRefine(Signature const& signature, SignatureRefiner& signatureRefiner, Partition const& oldPartition);