diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index e2e0b10d7..8cf964ca5 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -238,10 +238,9 @@ namespace storm { std::shared_ptr> preprocessSparseMarkovAutomaton(std::shared_ptr> const& model) { std::shared_ptr> result = model; model->close(); - if (model->hasOnlyTrivialNondeterminism()) { - STORM_LOG_WARN_COND(false, "Non-deterministic choices in MA seem to be unnecessary. Consider using a CTMC instead."); - // Activate again if transformation is correct - //result = model->convertToCTMC(); + if (model->isConvertibleToCtmc()) { + STORM_LOG_WARN_COND(false, "MA is convertible to a CTMC, consider using a CTMC instead."); + result = model->convertToCtmc(); } return result; } diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 2b74432ad..82a566496 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -533,7 +533,7 @@ namespace storm { if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC // TODO Matthias: change components which were not moved accordingly - model = ma->convertToCTMC(); + model = ma->convertToCtmc(); } else { model = ma; } @@ -592,7 +592,7 @@ namespace storm { if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC // TODO Matthias: change components which were not moved accordingly - model = ma->convertToCTMC(); + model = ma->convertToCtmc(); } else { model = ma; } diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 437e46942..9c077e2c4 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -169,6 +169,11 @@ namespace storm { } } + template + bool MarkovAutomaton::isConvertibleToCtmc() const { + return markovianStates.full(); + } + template bool MarkovAutomaton::hasOnlyTrivialNondeterminism() const { // Check every state @@ -197,7 +202,7 @@ namespace storm { } template - std::shared_ptr> MarkovAutomaton::convertToCTMC() const { + std::shared_ptr> MarkovAutomaton::convertToCtmc() const { STORM_LOG_TRACE("MA matrix:" << std::endl << this->getTransitionMatrix()); STORM_LOG_TRACE("Markovian states: " << getMarkovianStates()); diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h index 89c73f83c..b5a7f347f 100644 --- a/src/storm/models/sparse/MarkovAutomaton.h +++ b/src/storm/models/sparse/MarkovAutomaton.h @@ -134,14 +134,19 @@ namespace storm { */ void close(); + /*! + * Determines whether the Markov automaton can be converted to a CTMC without changing any measures. + */ + bool isConvertibleToCtmc() const; + bool hasOnlyTrivialNondeterminism() const; /*! - * Convert the MA into a MA by eliminating all states with probabilistic choices. + * Convert the MA to a CTMC. May only be called if the MA is convertible to a CTMC. * - * @return Ctmc. + * @return The resulting CTMC. */ - std::shared_ptr> convertToCTMC() const; + std::shared_ptr> convertToCtmc() const; virtual void printModelInformationToStream(std::ostream& out) const override;