diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 7801241a3..46c8ad35c 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -172,6 +172,16 @@ namespace storm { return columnVariables; } + template + std::set Model::getRowAndNondeterminismVariables() const { + return rowVariables; + } + + template + std::set Model::getColumnAndNondeterminismVariables() const { + return columnVariables; + } + template std::vector> const& Model::getRowColumnMetaVariablePairs() const { return rowColumnMetaVariablePairs; diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index 68d84cded..395028ae9 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -221,6 +221,20 @@ namespace storm { */ std::set const& getColumnVariables() const; + /*! + * Retrieves all meta variables used to encode rows and nondetermism. + * + * @return All meta variables used to encode rows and nondetermism. + */ + virtual std::set getRowAndNondeterminismVariables() const; + + /*! + * Retrieves all meta variables used to encode columns and nondetermism. + * + * @return All meta variables used to encode columns and nondetermism. + */ + virtual std::set getColumnAndNondeterminismVariables() const; + /*! * Retrieves the pairs of row and column meta variables. * diff --git a/src/storm/models/symbolic/NondeterministicModel.cpp b/src/storm/models/symbolic/NondeterministicModel.cpp index 6545e27c0..32baf1cd2 100644 --- a/src/storm/models/symbolic/NondeterministicModel.cpp +++ b/src/storm/models/symbolic/NondeterministicModel.cpp @@ -62,6 +62,20 @@ namespace storm { return nondeterminismVariables; } + template + std::set NondeterministicModel::getRowAndNondeterminismVariables() const { + std::set result; + std::set_union(this->getRowVariables().begin(), this->getRowVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin())); + return result; + } + + template + std::set NondeterministicModel::getColumnAndNondeterminismVariables() const { + std::set result; + std::set_union(this->getColumnVariables().begin(), this->getColumnVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin())); + return result; + } + template storm::dd::Bdd const& NondeterministicModel::getIllegalMask() const { return illegalMask; diff --git a/src/storm/models/symbolic/NondeterministicModel.h b/src/storm/models/symbolic/NondeterministicModel.h index 45dc27b0a..b3d5b7cb6 100644 --- a/src/storm/models/symbolic/NondeterministicModel.h +++ b/src/storm/models/symbolic/NondeterministicModel.h @@ -99,6 +99,9 @@ namespace storm { */ std::set const& getNondeterminismVariables() const; + virtual std::set getRowAndNondeterminismVariables() const override; + virtual std::set getColumnAndNondeterminismVariables() const override; + /*! * Retrieves a BDD characterizing all illegal nondeterminism encodings in the model. * diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index 78c89e7bf..86b0cf495 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp @@ -7,23 +7,36 @@ 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())) { - - // 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); + 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()) { + // Intentionally left empty. } template bool MdpPartitionRefiner::refine(bisimulation::SignatureMode const& mode) { - Partition newChoicePartition = this->internalRefine(choiceSignatureRefiner, choicePartition, mode); + // In this procedure, we will + // (1) refine the partition of nondeterministic choices based on the state partition. For this, we use + // the signature computer/refiner of the superclass. These objects use the full transition matrix. + // (2) if the choice partition was in fact split, the state partition also needs to be refined. + // For this, we use the signature computer/refiner of this class. + + STORM_LOG_TRACE("Refining choice partition."); + Partition newChoicePartition = this->internalRefine(this->signatureComputer, this->signatureRefiner, choicePartition, this->statePartition, mode); if (newChoicePartition == choicePartition) { this->status = Status::FixedPoint; return false; } else { - return PartitionRefiner::refine(mode); + // If the choice partition changed, refine the state partition. Use eager mode as abstracting from the probabilities is not worth doing. + STORM_LOG_TRACE("Refining state partition."); + Partition newStatePartition = this->internalRefine(this->stateSignatureComputer, this->stateSignatureRefiner, this->statePartition, this->choicePartition, SignatureMode::Eager); + + if (newStatePartition == this->statePartition) { + this->status = Status::FixedPoint; + return false; + } else { + this->statePartition = newStatePartition; + return true; + } } } diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h index 4abdcb427..c513386ee 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h @@ -34,9 +34,12 @@ namespace storm { private: // The choice partition in the refinement process. Partition choicePartition; + + // The object used to compute the state signatures. + SignatureComputer stateSignatureComputer; - // The object used to refine the choice partition based on the signatures. - SignatureRefiner choiceSignatureRefiner; + // The object used to refine the state partition based on the signatures. + SignatureRefiner stateSignatureRefiner; }; } diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index b0dfa2aeb..bd9890adf 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -5,13 +5,13 @@ 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.getRowVariables()) { + 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()) { // Intentionally left empty. } template bool PartitionRefiner::refine(SignatureMode const& mode) { - Partition newStatePartition = this->internalRefine(signatureRefiner, statePartition, mode); + Partition newStatePartition = this->internalRefine(signatureComputer, signatureRefiner, statePartition, statePartition, mode); if (statePartition == newStatePartition) { this->status = Status::FixedPoint; return false; @@ -22,13 +22,13 @@ namespace storm { } template - Partition PartitionRefiner::internalRefine(SignatureRefiner& signatureRefiner, Partition const& oldPartition, SignatureMode const& mode) { + Partition PartitionRefiner::internalRefine(SignatureComputer& signatureComputer, SignatureRefiner& signatureRefiner, Partition const& oldPartition, Partition const& targetPartition, SignatureMode const& mode) { auto start = std::chrono::high_resolution_clock::now(); if (this->status != Status::FixedPoint) { this->status = Status::InComputation; - this->signatureComputer.setSignatureMode(mode); + signatureComputer.setSignatureMode(mode); std::chrono::milliseconds::rep signatureTime = 0; std::chrono::milliseconds::rep refinementTime = 0; @@ -36,7 +36,7 @@ namespace storm { bool refined = false; uint64_t index = 0; Partition newPartition; - auto signatureIterator = signatureComputer.compute(oldPartition); + auto signatureIterator = signatureComputer.compute(targetPartition); while (signatureIterator.hasNext() && !refined) { auto signatureStart = std::chrono::high_resolution_clock::now(); auto signature = signatureIterator.next(); @@ -44,11 +44,18 @@ namespace storm { totalSignatureTime += (signatureEnd - signatureStart); 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); + } + auto refinementStart = std::chrono::high_resolution_clock::now(); newPartition = signatureRefiner.refine(statePartition, signature); auto refinementEnd = std::chrono::high_resolution_clock::now(); totalRefinementTime += (refinementEnd - refinementStart); + newPartition.asAdd().exportToDot("newpart" + std::to_string(refinements) + ".dot"); + signatureTime += std::chrono::duration_cast(signatureEnd - signatureStart).count(); refinementTime = std::chrono::duration_cast(refinementEnd - refinementStart).count(); diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.h b/src/storm/storage/dd/bisimulation/PartitionRefiner.h index b259de135..2bd090c3d 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.h @@ -41,7 +41,7 @@ namespace storm { Status getStatus() const; protected: - Partition internalRefine(SignatureRefiner& signatureRefiner, Partition const& oldPartition, SignatureMode const& mode = SignatureMode::Eager); + Partition internalRefine(SignatureComputer& stateSignatureComputer, SignatureRefiner& signatureRefiner, Partition const& oldPartition, Partition const& targetPartition, SignatureMode const& mode = SignatureMode::Eager); // The current status. Status status; diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp index 6eca5cf06..e847dd9bc 100644 --- a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp @@ -40,11 +40,33 @@ namespace storm { } template - SignatureComputer::SignatureComputer(storm::models::symbolic::Model const& model, SignatureMode const& mode) : model(model), transitionMatrix(model.getTransitionMatrix()) { + SignatureComputer::SignatureComputer(storm::models::symbolic::Model const& model, SignatureMode const& mode) : SignatureComputer(model.getTransitionMatrix(), boost::none, model.getColumnVariables(), mode) { + // Intentionally left empty. + } + + template + SignatureComputer::SignatureComputer(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, SignatureMode const& mode) : SignatureComputer(transitionMatrix, boost::none, columnVariables, mode) { + // 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) { + // 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) { if (DdType == storm::dd::DdType::Sylvan) { this->transitionMatrix = this->transitionMatrix.notZero().ite(this->transitionMatrix, this->transitionMatrix.getDdManager().template getAddUndefined()); } - this->setSignatureMode(mode); + + if (qualitativeTransitionMatrix) { + if (DdType == storm::dd::DdType::Sylvan) { + this->transitionMatrix01 = qualitativeTransitionMatrix.get().ite(this->transitionMatrix.getDdManager().template getAddOne(), this->transitionMatrix.getDdManager().template getAddUndefined()); + } else { + this->transitionMatrix01 = qualitativeTransitionMatrix.get().template toAdd(); + } + } } template @@ -54,13 +76,6 @@ namespace storm { template void SignatureComputer::setSignatureMode(SignatureMode const& newMode) { - if (newMode == SignatureMode::Lazy && !transitionMatrix01) { - if (DdType == storm::dd::DdType::Sylvan) { - this->transitionMatrix01 = model.getQualitativeTransitionMatrix().ite(this->transitionMatrix.getDdManager().template getAddOne(), this->transitionMatrix.getDdManager().template getAddUndefined()); - } else { - this->transitionMatrix01 = model.getQualitativeTransitionMatrix().template toAdd(); - } - } this->mode = newMode; } @@ -71,20 +86,37 @@ 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(), model.getColumnVariables())); + return Signature(this->transitionMatrix.multiplyMatrix(partition.asBdd(), columnVariables)); } else { - return Signature(this->transitionMatrix.multiplyMatrix(partition.asAdd(), model.getColumnVariables())); + 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; } } template Signature SignatureComputer::getQualitativeSignature(Partition const& partition) const { - STORM_LOG_ASSERT(this->transitionMatrix01, "Need qualitative transition matrix for this step."); + 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()); + } else { + this->transitionMatrix01 = this->transitionMatrix.notZero().template toAdd(); + } + } + if (partition.storedAsBdd()) { - return Signature(this->transitionMatrix01.get().multiplyMatrix(partition.asBdd(), model.getColumnVariables())); + return Signature(this->transitionMatrix01.get().multiplyMatrix(partition.asBdd(), columnVariables)); } else { - return Signature(this->transitionMatrix01.get().multiplyMatrix(partition.asAdd(), model.getColumnVariables())); + return Signature(this->transitionMatrix01.get().multiplyMatrix(partition.asAdd(), columnVariables)); } } diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.h b/src/storm/storage/dd/bisimulation/SignatureComputer.h index 426d9e329..6bce20d57 100644 --- a/src/storm/storage/dd/bisimulation/SignatureComputer.h +++ b/src/storm/storage/dd/bisimulation/SignatureComputer.h @@ -43,28 +43,32 @@ namespace storm { 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); void setSignatureMode(SignatureMode const& newMode); SignatureIterator compute(Partition const& partition); private: + /// Methods to compute the signatures. Signature getFullSignature(Partition const& partition) const; - Signature getQualitativeSignature(Partition const& partition) const; SignatureMode const& getSignatureMode() const; - - storm::models::symbolic::Model const& model; - - // The transition matrix to use for the signature computation. + + /// The transition matrix to use for the signature computation. storm::dd::Add transitionMatrix; + + /// The set of variables from which to abstract when performing matrix-vector multiplication. + std::set columnVariables; - // The mode to use for signature computation. + /// The mode to use for signature computation. SignatureMode mode; - // Only used when using lazy signatures is enabled. - boost::optional> transitionMatrix01; + /// Only used when using lazy signatures is enabled. + mutable boost::optional> transitionMatrix01; }; }