diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 587a28a7b..e7c296b07 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -171,7 +171,7 @@ namespace storm { template bool MarkovAutomaton::isConvertibleToCtmc() const { - return markovianStates.full(); + return isClosed() && markovianStates.full(); } template @@ -203,6 +203,21 @@ namespace storm { template std::shared_ptr> MarkovAutomaton::convertToCtmc() const { + if (isClosed() && markovianStates.full()) { + storm::storage::sparse::ModelComponents components(this->getTransitionMatrix(), this->getStateLabeling(), this->getRewardModels(), false); + components.transitionMatrix.makeRowGroupingTrivial(); + components.exitRates = this->getExitRates(); + if (this->hasChoiceLabeling()) { + components.choiceLabeling = this->getChoiceLabeling(); + } + if (this->hasStateValuations()) { + components.stateValuations = this->getStateValuations(); + } + if (this->hasChoiceOrigins()) { + components.choiceOrigins = this->getChoiceOrigins(); + } + return std::make_shared>(std::move(components)); + } STORM_LOG_TRACE("MA matrix:" << std::endl << this->getTransitionMatrix()); STORM_LOG_TRACE("Markovian states: " << getMarkovianStates()); @@ -249,12 +264,10 @@ namespace storm { //TODO update reward models and choice labels according to kept states STORM_LOG_WARN_COND(this->getRewardModels().empty(), "Conversion of MA to CTMC does not preserve rewards."); - std::unordered_map rewardModels = this->getRewardModels(); STORM_LOG_WARN_COND(!this->hasChoiceLabeling(), "Conversion of MA to CTMC does not preserve choice labels."); STORM_LOG_WARN_COND(!this->hasStateValuations(), "Conversion of MA to CTMC does not preserve choice labels."); STORM_LOG_WARN_COND(!this->hasChoiceOrigins(), "Conversion of MA to CTMC does not preserve choice labels."); - - return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels)); + return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling)); }