From f3ebfaa90f2d8fa13e810683eb6c214273285853 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 1 Aug 2017 21:23:08 +0200 Subject: [PATCH] more work on MDP bisimulation --- src/storm/api/bisimulation.h | 2 +- src/storm/models/ModelBase.h | 11 +++ src/storm/models/symbolic/Model.cpp | 4 - src/storm/models/symbolic/Model.h | 4 +- .../storage/dd/BisimulationDecomposition.cpp | 21 +++-- .../storage/dd/BisimulationDecomposition.h | 6 +- .../dd/bisimulation/MdpPartitionRefiner.cpp | 28 ++++-- .../dd/bisimulation/MdpPartitionRefiner.h | 11 ++- .../storage/dd/bisimulation/Partition.cpp | 39 +++++++-- src/storm/storage/dd/bisimulation/Partition.h | 10 ++- .../dd/bisimulation/PartitionRefiner.cpp | 86 +++++++++++-------- .../dd/bisimulation/PartitionRefiner.h | 4 +- .../dd/bisimulation/QuotientExtractor.cpp | 28 +++--- .../dd/bisimulation/QuotientExtractor.h | 11 +-- .../dd/bisimulation/SignatureRefiner.cpp | 2 +- .../dd/bisimulation/SignatureRefiner.h | 9 +- 16 files changed, 181 insertions(+), 95 deletions(-) diff --git a/src/storm/api/bisimulation.h b/src/storm/api/bisimulation.h index c59c62b09..825b8e4c8 100644 --- a/src/storm/api/bisimulation.h +++ b/src/storm/api/bisimulation.h @@ -57,7 +57,7 @@ namespace storm { template typename std::enable_if::value, std::shared_ptr>>::type performBisimulationMinimization(std::shared_ptr> const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager) { - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is currently only available for DTMCs and CTMCs."); + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is currently only available for DTMCs and CTMCs."); STORM_LOG_THROW(bisimulationType == storm::storage::BisimulationType::Strong, storm::exceptions::NotSupportedException, "Currently only strong bisimulation is supported."); storm::dd::BisimulationDecomposition decomposition(*model, formulas, bisimulationType); diff --git a/src/storm/models/ModelBase.h b/src/storm/models/ModelBase.h index cbef9a9dc..e6fb3f52f 100644 --- a/src/storm/models/ModelBase.h +++ b/src/storm/models/ModelBase.h @@ -38,6 +38,17 @@ namespace storm { return std::dynamic_pointer_cast(this->shared_from_this()); } + /*! + * Casts the model into the model type given by the template parameter. + * + * @return A shared pointer of the requested type that points to the model if the cast succeeded and a null + * pointer otherwise. + */ + template + std::shared_ptr as() const { + return std::dynamic_pointer_cast(this->shared_from_this()); + } + /*! * @brief Return the actual type of the model. * diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 27a37534f..7801241a3 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -7,10 +7,6 @@ #include "storm/adapters/AddExpressionAdapter.h" -#include "storm/storage/dd/DdManager.h" -#include "storm/storage/dd/Add.h" -#include "storm/storage/dd/Bdd.h" - #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/utility/macros.h" diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index dbd74634c..68d84cded 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -9,6 +9,7 @@ #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/Variable.h" #include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" #include "storm/models/Model.h" #include "storm/utility/OsDetection.h" @@ -22,9 +23,6 @@ namespace storm { template class Dd; - template - class Add; - template class DdManager; diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index e7b27efaf..77aa64f1d 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -1,10 +1,12 @@ #include "storm/storage/dd/BisimulationDecomposition.h" +#include "storm/storage/dd/bisimulation/Partition.h" #include "storm/storage/dd/bisimulation/PartitionRefiner.h" - +#include "storm/storage/dd/bisimulation/MdpPartitionRefiner.h" #include "storm/storage/dd/bisimulation/QuotientExtractor.h" #include "storm/models/symbolic/Model.h" +#include "storm/models/symbolic/Mdp.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" @@ -14,19 +16,28 @@ namespace storm { namespace dd { using namespace bisimulation; + + template + std::unique_ptr> createRefiner(storm::models::symbolic::Model const& model, Partition const& initialPartition) { + if (model.isOfType(storm::models::ModelType::Mdp)) { + return std::make_unique>(*model.template as>(), initialPartition); + } else { + return std::make_unique>(model, initialPartition); + } + } template - BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType) : BisimulationDecomposition(model, bisimulation::Partition::create(model, bisimulationType)) { + BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, bisimulationType), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { // Intentionally left empty. } template - BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType) : BisimulationDecomposition(model, bisimulation::Partition::create(model, formulas, bisimulationType)) { + BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas, bisimulationType), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { // Intentionally left empty. } template - BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, Partition const& initialPartition) : model(model), refiner(std::make_unique>(model, initialPartition)) { + BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, Partition const& initialPartition, bisimulation::PreservationInformation const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) { STORM_LOG_THROW(!model.hasRewardModel(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support preserving rewards."); } @@ -61,7 +72,7 @@ namespace storm { STORM_LOG_TRACE("Starting quotient extraction."); QuotientExtractor extractor; - std::shared_ptr> quotient = extractor.extract(model, refiner->getStatePartition()); + std::shared_ptr> quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation); STORM_LOG_TRACE("Quotient extraction done."); return quotient; diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h index 85bd1a48b..efc5a0a7f 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.h +++ b/src/storm/storage/dd/BisimulationDecomposition.h @@ -6,6 +6,7 @@ #include "storm/storage/dd/DdType.h" #include "storm/storage/bisimulation/BisimulationType.h" #include "storm/storage/dd/bisimulation/SignatureMode.h" +#include "storm/storage/dd/bisimulation/PreservationInformation.h" #include "storm/logic/Formula.h" @@ -34,7 +35,7 @@ namespace storm { public: BisimulationDecomposition(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType); BisimulationDecomposition(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType); - BisimulationDecomposition(storm::models::symbolic::Model const& model, bisimulation::Partition const& initialPartition); + BisimulationDecomposition(storm::models::symbolic::Model const& model, bisimulation::Partition const& initialPartition, bisimulation::PreservationInformation const& preservationInformation); ~BisimulationDecomposition(); @@ -52,6 +53,9 @@ namespace storm { // The model for which to compute the bisimulation decomposition. storm::models::symbolic::Model const& model; + // The object capturing what is preserved. + bisimulation::PreservationInformation preservationInformation; + // The refiner to use. std::unique_ptr> refiner; }; diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index 033f5f5f0..78c89e7bf 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp @@ -1,22 +1,30 @@ #include "storm/storage/dd/bisimulation/MdpPartitionRefiner.h" +#include "storm/models/symbolic/Mdp.h" + namespace storm { namespace dd { namespace bisimulation { template - MdpPartitionRefiner::MdpPartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition) : PartitionRefiner(model, initialStatePartition) { - // Start by initializing the choice signature refiner. - std::set choiceSignatureVariables; - std::set_union(model.getRowMetaVariables().begin(), model.getRowMetaVariables().end(), model.getNondeterminismVariables().begin(), model.getNondeterminismVariables().end(), std::inserter(choiceSignatureVariables, choiceSignatureVariables.begin())); - choiceSignatureRefiner = SignatureRefiner(model.getManager(), this->statePartition.getBlockVariable(), choiceSignatureVariables); + MdpPartitionRefiner::MdpPartitionRefiner(storm::models::symbolic::Mdp const& mdp, Partition const& initialStatePartition) : PartitionRefiner(mdp, initialStatePartition), choicePartition(Partition::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())) { - // Create dummy choice partition that is refined to the right result in the first call to refine. + // Initialize the choice signature refiner. + std::set choiceSignatureVariables; + std::set_union(mdp.getRowVariables().begin(), mdp.getRowVariables().end(), mdp.getNondeterminismVariables().begin(), mdp.getNondeterminismVariables().end(), std::inserter(choiceSignatureVariables, choiceSignatureVariables.begin())); + choiceSignatureRefiner = SignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), choiceSignatureVariables); } template bool MdpPartitionRefiner::refine(bisimulation::SignatureMode const& mode) { - // Magic here. + Partition newChoicePartition = this->internalRefine(choiceSignatureRefiner, choicePartition, mode); + + if (newChoicePartition == choicePartition) { + this->status = Status::FixedPoint; + return false; + } else { + return PartitionRefiner::refine(mode); + } } template @@ -24,6 +32,12 @@ namespace storm { return choicePartition; } + template class MdpPartitionRefiner; + + template class MdpPartitionRefiner; + template class MdpPartitionRefiner; + template class MdpPartitionRefiner; + } } } diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h index 1037811d5..4abdcb427 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h @@ -3,13 +3,20 @@ #include "storm/storage/dd/bisimulation/PartitionRefiner.h" namespace storm { + namespace models { + namespace symbolic { + template + class Mdp; + } + } + namespace dd { namespace bisimulation { template class MdpPartitionRefiner : public PartitionRefiner { public: - MdpPartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition); + MdpPartitionRefiner(storm::models::symbolic::Mdp const& mdp, Partition const& initialStatePartition); /*! * Refines the partition. @@ -17,7 +24,7 @@ namespace storm { * @param mode The signature mode to use. * @return False iff the partition is stable and no refinement was actually performed. */ - bool refine(bisimulation::SignatureMode const& mode = bisimulation::SignatureMode::Eager); + virtual bool refine(bisimulation::SignatureMode const& mode = bisimulation::SignatureMode::Eager) override; /*! * Retrieves the current choice partition in the refinement process. diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index 187c235e1..bde87a5b9 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -8,6 +8,8 @@ #include "storm/logic/AtomicExpressionFormula.h" #include "storm/logic/AtomicLabelFormula.h" +#include "storm/models/symbolic/Mdp.h" + #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/BisimulationSettings.h" @@ -19,6 +21,11 @@ namespace storm { namespace dd { namespace bisimulation { + template + Partition::Partition() : nextFreeBlockIndex(0) { + // Intentionally left empty. + } + template Partition::Partition(storm::dd::Add const& partitionAdd, std::pair const& blockVariables, uint64_t nextFreeBlockIndex) : partition(partitionAdd), blockVariables(blockVariables), nextFreeBlockIndex(nextFreeBlockIndex) { // Intentionally left empty. @@ -45,7 +52,7 @@ namespace storm { } template - Partition Partition::create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, PreservationInformation const& preservationInformation) { + Partition Partition::create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, PreservationInformation const& preservationInformation) { std::vector expressionVector; for (auto const& expression : preservationInformation.getExpressions()) { @@ -57,7 +64,6 @@ namespace storm { template Partition Partition::create(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const& bisimulationType) { - STORM_LOG_THROW(bisimulationType == storm::storage::BisimulationType::Strong, storm::exceptions::NotSupportedException, "Currently only strong bisimulation is supported."); storm::dd::DdManager& manager = model.getManager(); @@ -72,6 +78,13 @@ namespace storm { auto const& ddMetaVariable = manager.getMetaVariable(metaVariable); numberOfDdVariables += ddMetaVariable.getNumberOfDdVariables(); } + if (model.getType() == storm::models::ModelType::Mdp) { + auto mdp = model.template as>(); + for (auto const& metaVariable : mdp->getNondeterminismVariables()) { + auto const& ddMetaVariable = manager.getMetaVariable(metaVariable); + numberOfDdVariables += ddMetaVariable.getNumberOfDdVariables(); + } + } std::pair blockVariables = createBlockVariables(manager, numberOfDdVariables); std::pair, uint64_t> partitionBddAndBlockCount = createPartitionBdd(manager, model, stateSets, blockVariables.first); @@ -84,6 +97,18 @@ namespace storm { } } + template + Partition Partition::createTrivialChoicePartition(storm::models::symbolic::NondeterministicModel const& model, std::pair const& blockVariables) { + storm::dd::Bdd choicePartitionBdd = !model.getIllegalSuccessorMask() && model.getManager().getEncoding(blockVariables.first, 0, false); + + // Store the partition as an ADD only in the case of CUDD. + if (DdType == storm::dd::DdType::CUDD) { + return Partition(choicePartitionBdd.template toAdd(), blockVariables, 1); + } else { + return Partition(choicePartitionBdd, blockVariables, 1); + } + } + template uint64_t Partition::getNumberOfStates() const { return this->getStates().getNonZeroCount(); @@ -123,6 +148,11 @@ namespace storm { return boost::get>(partition); } + template + std::pair const& Partition::getBlockVariables() const { + return blockVariables; + } + template storm::expressions::Variable const& Partition::getBlockVariable() const { return blockVariables.first; @@ -147,11 +177,6 @@ namespace storm { } } - template - PreservationInformation const& Partition::getPreservationInformation() const { - return *preservationInformation; - } - template void enumerateBlocksRec(std::vector> const& stateSets, storm::dd::Bdd const& currentStateSet, uint64_t offset, storm::expressions::Variable const& blockVariable, std::function const&)> const& callback) { if (currentStateSet.isZero()) { diff --git a/src/storm/storage/dd/bisimulation/Partition.h b/src/storm/storage/dd/bisimulation/Partition.h index 59183a332..3a620e681 100644 --- a/src/storm/storage/dd/bisimulation/Partition.h +++ b/src/storm/storage/dd/bisimulation/Partition.h @@ -11,6 +11,7 @@ #include "storm/storage/bisimulation/BisimulationType.h" #include "storm/models/symbolic/Model.h" +#include "storm/models/symbolic/NondeterministicModel.h" namespace storm { namespace logic { @@ -20,19 +21,21 @@ namespace storm { namespace dd { namespace bisimulation { + template class PreservationInformation; template class Partition { public: - Partition() = default; + Partition(); bool operator==(Partition const& other); Partition replacePartition(storm::dd::Add const& newPartitionAdd, uint64_t nextFreeBlockIndex) const; Partition replacePartition(storm::dd::Bdd const& newPartitionBdd, uint64_t nextFreeBlockIndex) const; - static Partition create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, PreservationInformation const& preservationInformation); + static Partition create(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType, PreservationInformation const& preservationInformation); + static Partition createTrivialChoicePartition(storm::models::symbolic::NondeterministicModel const& model, std::pair const& blockVariables); uint64_t getNumberOfStates() const; uint64_t getNumberOfBlocks() const; @@ -42,7 +45,8 @@ namespace storm { storm::dd::Add const& asAdd() const; storm::dd::Bdd const& asBdd() const; - + + std::pair const& getBlockVariables() const; storm::expressions::Variable const& getBlockVariable() const; storm::expressions::Variable const& getPrimedBlockVariable() const; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index d2061ee07..b0dfa2aeb 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -10,44 +10,8 @@ namespace storm { } template - bool PartitionRefiner::refine(bisimulation::SignatureMode const& mode) { - this->status = Status::InComputation; - - this->signatureComputer.setSignatureMode(mode); - auto start = std::chrono::high_resolution_clock::now(); - - std::chrono::milliseconds::rep signatureTime = 0; - std::chrono::milliseconds::rep refinementTime = 0; - - bool alreadyRefined = false; - uint64_t index = 0; - Partition newStatePartition; - auto signatureIterator = signatureComputer.compute(statePartition); - while (signatureIterator.hasNext() && !alreadyRefined) { - auto signatureStart = std::chrono::high_resolution_clock::now(); - auto signature = signatureIterator.next(); - auto signatureEnd = std::chrono::high_resolution_clock::now(); - totalSignatureTime += (signatureEnd - signatureStart); - STORM_LOG_DEBUG("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); - - auto refinementStart = std::chrono::high_resolution_clock::now(); - newStatePartition = signatureRefiner.refine(statePartition, signature); - auto refinementEnd = std::chrono::high_resolution_clock::now(); - totalRefinementTime += (refinementEnd - refinementStart); - - signatureTime += std::chrono::duration_cast(signatureEnd - signatureStart).count(); - refinementTime = std::chrono::duration_cast(refinementEnd - refinementStart).count(); - - // Potentially exit early in case we have refined the partition already. - if (newStatePartition.getNumberOfBlocks() > statePartition.getNumberOfBlocks()) { - alreadyRefined = true; - } - } - - auto totalTimeInRefinement = std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - start).count(); - ++refinements; - STORM_LOG_DEBUG("Refinement " << refinements << " produced " << newStatePartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms)."); - + bool PartitionRefiner::refine(SignatureMode const& mode) { + Partition newStatePartition = this->internalRefine(signatureRefiner, statePartition, mode); if (statePartition == newStatePartition) { this->status = Status::FixedPoint; return false; @@ -57,6 +21,52 @@ namespace storm { } } + template + Partition PartitionRefiner::internalRefine(SignatureRefiner& signatureRefiner, Partition const& oldPartition, SignatureMode const& mode) { + auto start = std::chrono::high_resolution_clock::now(); + + if (this->status != Status::FixedPoint) { + this->status = Status::InComputation; + + this->signatureComputer.setSignatureMode(mode); + + std::chrono::milliseconds::rep signatureTime = 0; + std::chrono::milliseconds::rep refinementTime = 0; + + bool refined = false; + uint64_t index = 0; + Partition newPartition; + auto signatureIterator = signatureComputer.compute(oldPartition); + while (signatureIterator.hasNext() && !refined) { + auto signatureStart = std::chrono::high_resolution_clock::now(); + auto signature = signatureIterator.next(); + auto signatureEnd = std::chrono::high_resolution_clock::now(); + totalSignatureTime += (signatureEnd - signatureStart); + STORM_LOG_DEBUG("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); + + auto refinementStart = std::chrono::high_resolution_clock::now(); + newPartition = signatureRefiner.refine(statePartition, signature); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + totalRefinementTime += (refinementEnd - refinementStart); + + signatureTime += std::chrono::duration_cast(signatureEnd - signatureStart).count(); + refinementTime = std::chrono::duration_cast(refinementEnd - refinementStart).count(); + + // Potentially exit early in case we have refined the partition already. + if (newPartition.getNumberOfBlocks() > oldPartition.getNumberOfBlocks()) { + refined = true; + } + } + + auto totalTimeInRefinement = std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - start).count(); + ++refinements; + STORM_LOG_DEBUG("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms)."); + return newPartition; + } else { + return oldPartition; + } + } + template Partition const& PartitionRefiner::getStatePartition() const { return statePartition; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.h b/src/storm/storage/dd/bisimulation/PartitionRefiner.h index c5ccae949..b259de135 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.h @@ -28,7 +28,7 @@ namespace storm { * @param mode The signature mode to use. * @return False iff the partition is stable and no refinement was actually performed. */ - bool refine(bisimulation::SignatureMode const& mode = bisimulation::SignatureMode::Eager); + virtual bool refine(SignatureMode const& mode = SignatureMode::Eager); /*! * Retrieves the current state partition in the refinement process. @@ -41,6 +41,8 @@ namespace storm { Status getStatus() const; protected: + Partition internalRefine(SignatureRefiner& signatureRefiner, Partition const& oldPartition, SignatureMode const& mode = SignatureMode::Eager); + // The current status. Status status; diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 2fb31b2d1..ccaeaa774 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -480,13 +480,13 @@ namespace storm { } template - std::shared_ptr> QuotientExtractor::extract(storm::models::symbolic::Model const& model, Partition const& partition) { + std::shared_ptr> QuotientExtractor::extract(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation) { auto start = std::chrono::high_resolution_clock::now(); std::shared_ptr> result; if (quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Sparse) { - result = extractSparseQuotient(model, partition); + result = extractSparseQuotient(model, partition, preservationInformation); } else { - result = extractDdQuotient(model, partition); + 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."); @@ -497,7 +497,7 @@ namespace storm { } template - std::shared_ptr> QuotientExtractor::extractSparseQuotient(storm::models::symbolic::Model const& model, Partition const& partition) { + std::shared_ptr> QuotientExtractor::extractSparseQuotient(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation) { InternalSparseQuotientExtractor sparseExtractor(model.getManager(), model.getRowVariables()); auto states = partition.getStates().swapVariables(model.getRowColumnMetaVariablePairs()); @@ -507,10 +507,10 @@ namespace storm { quotientStateLabeling.addLabel("init", sparseExtractor.extractStates(model.getInitialStates(), partition)); quotientStateLabeling.addLabel("deadlock", sparseExtractor.extractStates(model.getDeadlockStates(), partition)); - for (auto const& label : partition.getPreservationInformation().getLabels()) { + for (auto const& label : preservationInformation.getLabels()) { quotientStateLabeling.addLabel(label, sparseExtractor.extractStates(model.getStates(label), partition)); } - for (auto const& expression : partition.getPreservationInformation().getExpressions()) { + for (auto const& expression : preservationInformation.getExpressions()) { std::stringstream stream; stream << expression; std::string expressionAsString = stream.str(); @@ -533,12 +533,12 @@ namespace storm { } template - std::shared_ptr> QuotientExtractor::extractDdQuotient(storm::models::symbolic::Model const& model, Partition const& partition) { - return extractQuotientUsingBlockVariables(model, partition); + std::shared_ptr> QuotientExtractor::extractDdQuotient(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation) { + return extractQuotientUsingBlockVariables(model, partition, preservationInformation); } template - std::shared_ptr> QuotientExtractor::extractQuotientUsingBlockVariables(storm::models::symbolic::Model const& model, Partition const& partition) { + std::shared_ptr> QuotientExtractor::extractQuotientUsingBlockVariables(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) { @@ -568,10 +568,10 @@ namespace storm { storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates; std::map> preservedLabelBdds; - for (auto const& label : partition.getPreservationInformation().getLabels()) { + for (auto const& label : preservationInformation.getLabels()) { preservedLabelBdds.emplace(label, (model.getStates(label) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables())); } - for (auto const& expression : partition.getPreservationInformation().getExpressions()) { + for (auto const& expression : preservationInformation.getExpressions()) { std::stringstream stream; stream << expression; std::string expressionAsString = stream.str(); @@ -597,7 +597,7 @@ namespace storm { } template - std::shared_ptr> QuotientExtractor::extractQuotientUsingOriginalVariables(storm::models::symbolic::Model const& model, Partition const& partition) { + 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) { @@ -619,10 +619,10 @@ namespace storm { storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(model.getColumnVariables()) && reachableStates; std::map> preservedLabelBdds; - for (auto const& label : partition.getPreservationInformation().getLabels()) { + for (auto const& label : preservationInformation.getLabels()) { preservedLabelBdds.emplace(label, (model.getStates(label) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables())); } - for (auto const& expression : partition.getPreservationInformation().getExpressions()) { + for (auto const& expression : preservationInformation.getExpressions()) { std::stringstream stream; stream << expression; std::string expressionAsString = stream.str(); diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.h b/src/storm/storage/dd/bisimulation/QuotientExtractor.h index 14b518016..dda06a3d3 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.h +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.h @@ -8,6 +8,7 @@ #include "storm/models/sparse/Model.h" #include "storm/storage/dd/bisimulation/Partition.h" +#include "storm/storage/dd/bisimulation/PreservationInformation.h" #include "storm/settings/modules/BisimulationSettings.h" @@ -20,14 +21,14 @@ namespace storm { public: QuotientExtractor(); - std::shared_ptr> extract(storm::models::symbolic::Model const& model, Partition const& partition); + std::shared_ptr> extract(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation); private: - std::shared_ptr> extractSparseQuotient(storm::models::symbolic::Model const& model, Partition const& partition); + std::shared_ptr> extractSparseQuotient(storm::models::symbolic::Model const& model, Partition const& partition, PreservationInformation const& preservationInformation); - std::shared_ptr> extractDdQuotient(storm::models::symbolic::Model const& model, Partition const& partition); - std::shared_ptr> extractQuotientUsingBlockVariables(storm::models::symbolic::Model const& model, Partition const& partition); - std::shared_ptr> extractQuotientUsingOriginalVariables(storm::models::symbolic::Model const& model, Partition const& partition); + 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; storm::settings::modules::BisimulationSettings::QuotientFormat quotientFormat; diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index 3f101776d..028fb7767 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -444,7 +444,7 @@ namespace storm { }; template - SignatureRefiner::SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables) : manager(manager), stateVariables(stateVariables) { + SignatureRefiner::SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables) : manager(&manager), stateVariables(stateVariables) { uint64_t lastStateLevel = 0; for (auto const& stateVariable : stateVariables) { lastStateLevel = std::max(lastStateLevel, manager.getMetaVariable(stateVariable).getHighestLevel()); diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.h b/src/storm/storage/dd/bisimulation/SignatureRefiner.h index 32532dc62..ba6777d13 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.h +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.h @@ -1,5 +1,7 @@ #pragma once +#include + #include "storm/storage/dd/DdType.h" #include "storm/storage/dd/bisimulation/Partition.h" @@ -15,6 +17,7 @@ namespace storm { template class SignatureRefiner { public: + SignatureRefiner() = default; SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables); ~SignatureRefiner(); @@ -23,13 +26,13 @@ namespace storm { private: // The manager responsible for the DDs. - storm::dd::DdManager const& manager; + storm::dd::DdManager const* manager; // The variables encodin the states. - std::set const& stateVariables; + std::set stateVariables; // The internal refiner. - std::unique_ptr> internalRefiner; + std::shared_ptr> internalRefiner; }; }