Browse Source

re-enabling conversion of MA to CTMC if the MA only has Markovian states

tempestpy_adaptions
dehnert 7 years ago
parent
commit
0d18886966
  1. 7
      src/storm-cli-utilities/model-handling.h
  2. 4
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  3. 7
      src/storm/models/sparse/MarkovAutomaton.cpp
  4. 11
      src/storm/models/sparse/MarkovAutomaton.h

7
src/storm-cli-utilities/model-handling.h

@ -238,10 +238,9 @@ namespace storm {
std::shared_ptr<storm::models::sparse::Model<ValueType>> preprocessSparseMarkovAutomaton(std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> const& model) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> 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;
}

4
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;
}

7
src/storm/models/sparse/MarkovAutomaton.cpp

@ -169,6 +169,11 @@ namespace storm {
}
}
template <typename ValueType, typename RewardModelType>
bool MarkovAutomaton<ValueType, RewardModelType>::isConvertibleToCtmc() const {
return markovianStates.full();
}
template <typename ValueType, typename RewardModelType>
bool MarkovAutomaton<ValueType, RewardModelType>::hasOnlyTrivialNondeterminism() const {
// Check every state
@ -197,7 +202,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType>
std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> MarkovAutomaton<ValueType, RewardModelType>::convertToCTMC() const {
std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> MarkovAutomaton<ValueType, RewardModelType>::convertToCtmc() const {
STORM_LOG_TRACE("MA matrix:" << std::endl << this->getTransitionMatrix());
STORM_LOG_TRACE("Markovian states: " << getMarkovianStates());

11
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<storm::models::sparse::Ctmc<ValueType, RewardModelType>> convertToCTMC() const;
std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> convertToCtmc() const;
virtual void printModelInformationToStream(std::ostream& out) const override;

Loading…
Cancel
Save