From d0840f783a76849ac5d74fa9265f568713a34168 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 2 Aug 2017 21:58:54 +0200 Subject: [PATCH] further in debugging MDP bisimulation --- .../dd/bisimulation/MdpPartitionRefiner.cpp | 10 ++- .../dd/bisimulation/PartitionRefiner.cpp | 6 +- .../dd/bisimulation/SignatureComputer.cpp | 88 ++++++++++++------- .../dd/bisimulation/SignatureComputer.h | 17 ++-- .../storage/dd/bisimulation/SignatureMode.h | 2 +- 5 files changed, 80 insertions(+), 43 deletions(-) diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index 86b0cf495..914656d89 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp @@ -7,8 +7,10 @@ namespace storm { namespace bisimulation { template - MdpPartitionRefiner::MdpPartitionRefiner(storm::models::symbolic::Mdp const& mdp, Partition const& initialStatePartition) : PartitionRefiner(mdp, initialStatePartition), choicePartition(Partition::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureComputer(mdp.getQualitativeTransitionMatrix(false), mdp.getColumnAndNondeterminismVariables()), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables()) { + MdpPartitionRefiner::MdpPartitionRefiner(storm::models::symbolic::Mdp const& mdp, Partition const& initialStatePartition) : PartitionRefiner(mdp, initialStatePartition), choicePartition(Partition::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureComputer(mdp.getQualitativeTransitionMatrix(), mdp.getColumnAndNondeterminismVariables(), SignatureMode::Qualitative, true), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables()) { // Intentionally left empty. + + mdp.getTransitionMatrix().exportToDot("fulltrans.dot"); } template @@ -26,9 +28,11 @@ namespace storm { this->status = Status::FixedPoint; return false; } else { - // If the choice partition changed, refine the state partition. Use eager mode as abstracting from the probabilities is not worth doing. + this->choicePartition = newChoicePartition; + + // If the choice partition changed, refine the state partition. Use qualitative mode we must properly abstract from choice counts. STORM_LOG_TRACE("Refining state partition."); - Partition newStatePartition = this->internalRefine(this->stateSignatureComputer, this->stateSignatureRefiner, this->statePartition, this->choicePartition, SignatureMode::Eager); + Partition newStatePartition = this->internalRefine(this->stateSignatureComputer, this->stateSignatureRefiner, this->statePartition, this->choicePartition, SignatureMode::Qualitative); if (newStatePartition == this->statePartition) { this->status = Status::FixedPoint; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index bd9890adf..b3e19cdc2 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -45,9 +45,9 @@ namespace storm { STORM_LOG_DEBUG("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes."); signature.getSignatureAdd().exportToDot("sig" + std::to_string(refinements) + ".dot"); - if (refinements == 1) { - exit(-1); - } +// if (refinements == 1) { +// exit(-1); +// } auto refinementStart = std::chrono::high_resolution_clock::now(); newPartition = signatureRefiner.refine(statePartition, signature); diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp index e847dd9bc..ae82f91e9 100644 --- a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp @@ -16,23 +16,35 @@ namespace storm { template bool SignatureIterator::hasNext() const { - if (signatureComputer.getSignatureMode() == SignatureMode::Eager) { - return position < 1; - } else { - return position < 2; + switch (signatureComputer.getSignatureMode()) { + case SignatureMode::Qualitative: + case SignatureMode::Eager: return position < 1; + case SignatureMode::Lazy: return position < 2; } } template Signature SignatureIterator::next() { auto mode = signatureComputer.getSignatureMode(); - STORM_LOG_THROW((mode == SignatureMode::Eager && position < 1) || (mode == SignatureMode::Lazy && position < 2), storm::exceptions::OutOfRangeException, "Iterator is out of range."); + STORM_LOG_THROW((mode == SignatureMode::Eager && position < 1) || (mode == SignatureMode::Lazy && position < 2) || (mode == SignatureMode::Qualitative && position < 1), storm::exceptions::OutOfRangeException, "Iterator is out of range."); Signature result; - if (mode == SignatureMode::Eager || position == 1) { - result = signatureComputer.getFullSignature(partition); - } else if (position == 0) { - result = signatureComputer.getQualitativeSignature(partition); + if (mode == SignatureMode::Eager) { + if (position == 0) { + result = signatureComputer.getFullSignature(partition); + } + } else if (mode == SignatureMode::Lazy) { + if (position == 0) { + result = signatureComputer.getQualitativeSignature(partition); + } else { + result = signatureComputer.getFullSignature(partition); + } + } else if (mode == SignatureMode::Qualitative) { + if (position == 0) { + result = signatureComputer.getQualitativeSignature(partition); + } + } else { + STORM_LOG_ASSERT(false, "Unknown signature mode."); } ++position; @@ -40,29 +52,29 @@ namespace storm { } template - SignatureComputer::SignatureComputer(storm::models::symbolic::Model const& model, SignatureMode const& mode) : SignatureComputer(model.getTransitionMatrix(), boost::none, model.getColumnVariables(), mode) { + SignatureComputer::SignatureComputer(storm::models::symbolic::Model const& model, SignatureMode const& mode, bool ensureQualitative) : SignatureComputer(model.getTransitionMatrix(), boost::none, model.getColumnVariables(), mode, ensureQualitative) { // Intentionally left empty. } template - SignatureComputer::SignatureComputer(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, SignatureMode const& mode) : SignatureComputer(transitionMatrix, boost::none, columnVariables, mode) { + SignatureComputer::SignatureComputer(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, SignatureMode const& mode, bool ensureQualitative) : SignatureComputer(transitionMatrix, boost::none, columnVariables, mode, ensureQualitative) { // Intentionally left empty. } template - SignatureComputer::SignatureComputer(storm::dd::Bdd const& qualitativeTransitionMatrix, std::set const& columnVariables, SignatureMode const& mode) : SignatureComputer(qualitativeTransitionMatrix.template toAdd(), boost::none, columnVariables, mode) { + SignatureComputer::SignatureComputer(storm::dd::Bdd const& qualitativeTransitionMatrix, std::set const& columnVariables, SignatureMode const& mode, bool ensureQualitative) : SignatureComputer(qualitativeTransitionMatrix.template toAdd(), boost::none, columnVariables, mode, ensureQualitative) { // Intentionally left empty. } template - SignatureComputer::SignatureComputer(storm::dd::Add const& transitionMatrix, boost::optional> const& qualitativeTransitionMatrix, std::set const& columnVariables, SignatureMode const& mode) : transitionMatrix(transitionMatrix), columnVariables(columnVariables), mode(mode) { + SignatureComputer::SignatureComputer(storm::dd::Add const& transitionMatrix, boost::optional> const& qualitativeTransitionMatrix, std::set const& columnVariables, SignatureMode const& mode, bool ensureQualitative) : transitionMatrix(transitionMatrix), columnVariables(columnVariables), mode(mode), ensureQualitative(ensureQualitative) { if (DdType == storm::dd::DdType::Sylvan) { this->transitionMatrix = this->transitionMatrix.notZero().ite(this->transitionMatrix, this->transitionMatrix.getDdManager().template getAddUndefined()); } if (qualitativeTransitionMatrix) { - if (DdType == storm::dd::DdType::Sylvan) { - this->transitionMatrix01 = qualitativeTransitionMatrix.get().ite(this->transitionMatrix.getDdManager().template getAddOne(), this->transitionMatrix.getDdManager().template getAddUndefined()); + if (DdType == storm::dd::DdType::Sylvan || ensureQualitative) { + this->transitionMatrix01 = qualitativeTransitionMatrix.get(); } else { this->transitionMatrix01 = qualitativeTransitionMatrix.get().template toAdd(); } @@ -86,40 +98,54 @@ namespace storm { template Signature SignatureComputer::getFullSignature(Partition const& partition) const { - this->transitionMatrix.exportToDot("trans.dot"); if (partition.storedAsBdd()) { return Signature(this->transitionMatrix.multiplyMatrix(partition.asBdd(), columnVariables)); } else { - auto result = Signature(this->transitionMatrix.multiplyMatrix(partition.asAdd(), columnVariables)); - - std::cout << "abstracting vars" << std::endl; - for (auto const& v : columnVariables) { - std::cout << v.getName() << std::endl; - } - std::cout << "----" << std::endl; - result.getSignatureAdd().exportToDot("fullsig.dot"); - - return result; + return Signature(this->transitionMatrix.multiplyMatrix(partition.asAdd(), columnVariables)); } } template Signature SignatureComputer::getQualitativeSignature(Partition const& partition) const { - if (this->mode == SignatureMode::Lazy && !transitionMatrix01) { - if (DdType == storm::dd::DdType::Sylvan) { - this->transitionMatrix01 = this->transitionMatrix.notZero().ite(this->transitionMatrix.getDdManager().template getAddOne(), this->transitionMatrix.getDdManager().template getAddUndefined()); + if (!transitionMatrix01) { + if (DdType == storm::dd::DdType::Sylvan || this->ensureQualitative) { + this->transitionMatrix01 = this->transitionMatrix.notZero(); } else { this->transitionMatrix01 = this->transitionMatrix.notZero().template toAdd(); } } if (partition.storedAsBdd()) { - return Signature(this->transitionMatrix01.get().multiplyMatrix(partition.asBdd(), columnVariables)); + return this->getQualitativeTransitionMatrixAsBdd().andExists(partition.asBdd(), columnVariables).template toAdd(); } else { - return Signature(this->transitionMatrix01.get().multiplyMatrix(partition.asAdd(), columnVariables)); + if (this->qualitativeTransitionMatrixIsBdd()) { + this->getQualitativeTransitionMatrixAsBdd().template toAdd().exportToDot("lasttrans.dot"); + partition.asAdd().exportToDot("lastpart.dot"); + this->getQualitativeTransitionMatrixAsBdd().andExists(partition.asAdd().toBdd(), columnVariables).template toAdd().exportToDot("lastresult.dot"); + return Signature(this->getQualitativeTransitionMatrixAsBdd().andExists(partition.asAdd().toBdd(), columnVariables).template toAdd()); + } else { + return Signature(this->getQualitativeTransitionMatrixAsAdd().multiplyMatrix(partition.asAdd(), columnVariables)); + } } } + template + bool SignatureComputer::qualitativeTransitionMatrixIsBdd() const { + return transitionMatrix01.get().which() == 0; + } + + template + storm::dd::Bdd const& SignatureComputer::getQualitativeTransitionMatrixAsBdd() const { + STORM_LOG_ASSERT(this->transitionMatrix01, "Missing qualitative transition matrix."); + return boost::get>(this->transitionMatrix01.get()); + } + + template + storm::dd::Add const& SignatureComputer::getQualitativeTransitionMatrixAsAdd() const { + STORM_LOG_ASSERT(this->transitionMatrix01, "Missing qualitative transition matrix."); + return boost::get>(this->transitionMatrix01.get()); + } + template class SignatureIterator; template class SignatureIterator; template class SignatureIterator; diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.h b/src/storm/storage/dd/bisimulation/SignatureComputer.h index 6bce20d57..421acc90a 100644 --- a/src/storm/storage/dd/bisimulation/SignatureComputer.h +++ b/src/storm/storage/dd/bisimulation/SignatureComputer.h @@ -42,10 +42,10 @@ namespace storm { public: friend class SignatureIterator; - SignatureComputer(storm::models::symbolic::Model const& model, SignatureMode const& mode = SignatureMode::Eager); - SignatureComputer(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, SignatureMode const& mode = SignatureMode::Eager); - SignatureComputer(storm::dd::Bdd const& qualitativeTransitionMatrix, std::set const& columnVariables, SignatureMode const& mode = SignatureMode::Eager); - SignatureComputer(storm::dd::Add const& transitionMatrix, boost::optional> const& qualitativeTransitionMatrix, std::set const& columnVariables, SignatureMode const& mode = SignatureMode::Eager); + SignatureComputer(storm::models::symbolic::Model const& model, SignatureMode const& mode = SignatureMode::Eager, bool ensureQualitative = false); + SignatureComputer(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, SignatureMode const& mode = SignatureMode::Eager, bool ensureQualitative = false); + SignatureComputer(storm::dd::Bdd const& qualitativeTransitionMatrix, std::set const& columnVariables, SignatureMode const& mode = SignatureMode::Eager, bool ensureQualitative = false); + SignatureComputer(storm::dd::Add const& transitionMatrix, boost::optional> const& qualitativeTransitionMatrix, std::set const& columnVariables, SignatureMode const& mode = SignatureMode::Eager, bool ensureQualitative = false); void setSignatureMode(SignatureMode const& newMode); @@ -56,6 +56,10 @@ namespace storm { Signature getFullSignature(Partition const& partition) const; Signature getQualitativeSignature(Partition const& partition) const; + bool qualitativeTransitionMatrixIsBdd() const; + storm::dd::Bdd const& getQualitativeTransitionMatrixAsBdd() const; + storm::dd::Add const& getQualitativeTransitionMatrixAsAdd() const; + SignatureMode const& getSignatureMode() const; /// The transition matrix to use for the signature computation. @@ -67,8 +71,11 @@ namespace storm { /// The mode to use for signature computation. SignatureMode mode; + /// A flag indicating whether the qualitative signature needs to make sure that the result is in fact qualitative. + bool ensureQualitative; + /// Only used when using lazy signatures is enabled. - mutable boost::optional> transitionMatrix01; + mutable boost::optional, storm::dd::Add>> transitionMatrix01; }; } diff --git a/src/storm/storage/dd/bisimulation/SignatureMode.h b/src/storm/storage/dd/bisimulation/SignatureMode.h index bcec54b6f..41457ba76 100644 --- a/src/storm/storage/dd/bisimulation/SignatureMode.h +++ b/src/storm/storage/dd/bisimulation/SignatureMode.h @@ -4,7 +4,7 @@ namespace storm { namespace dd { namespace bisimulation { - enum class SignatureMode { Eager, Lazy }; + enum class SignatureMode { Eager, Lazy, Qualitative }; } }