diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index 8a5915004..74a563363 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -44,18 +44,11 @@ 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/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index b88524f6c..ff114b482 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -4,6 +4,7 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Ctmc.h" +#include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/sparse/Dtmc.h" @@ -541,7 +542,7 @@ namespace storm { 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) { + if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::Mdp) { std::set blockVariableSet = {partition.getBlockVariable()}; std::set blockPrimeVariableSet = {partition.getPrimedBlockVariable()}; std::vector> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())}; @@ -554,9 +555,12 @@ namespace storm { } storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); + partitionAsAdd.exportToDot("partition.dot"); auto start = std::chrono::high_resolution_clock::now(); storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockVariableSet, blockPrimeVariableSet), model.getColumnVariables()); + quotientTransitionMatrix.exportToDot("trans-1.dot"); quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd.renameVariables(model.getColumnVariables(), model.getRowVariables()), model.getRowVariables()); + quotientTransitionMatrix.exportToDot("quottrans.dot"); 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::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); @@ -588,8 +592,12 @@ namespace storm { 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, {})); - } else { + } 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, {})); + } 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, {})); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported quotient type."); } } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type."); diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp index ae82f91e9..682085468 100644 --- a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp @@ -119,9 +119,6 @@ namespace storm { return this->getQualitativeTransitionMatrixAsBdd().andExists(partition.asBdd(), columnVariables).template toAdd(); } else { 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));