diff --git a/src/storm/models/sparse/Ctmc.cpp b/src/storm/models/sparse/Ctmc.cpp index 9b36ded21..584b85847 100644 --- a/src/storm/models/sparse/Ctmc.cpp +++ b/src/storm/models/sparse/Ctmc.cpp @@ -79,6 +79,18 @@ namespace storm { } } + template + storm::storage::SparseMatrix Ctmc::computeProbabilityMatrix() const { + // Turn the rates into probabilities by scaling each row with the exit rate of the state. + storm::storage::SparseMatrix result(this->getTransitionMatrix()); + for (uint_fast64_t row = 0; row < result.getRowCount(); ++row) { + for (auto& entry : result.getRow(row)) { + entry.setValue(entry.getValue() / exitRates[row]); + } + } + return result; + } + template class Ctmc; #ifdef STORM_HAVE_CARL diff --git a/src/storm/models/sparse/Ctmc.h b/src/storm/models/sparse/Ctmc.h index ed5a46329..58859d5dd 100644 --- a/src/storm/models/sparse/Ctmc.h +++ b/src/storm/models/sparse/Ctmc.h @@ -64,6 +64,12 @@ namespace storm { virtual void reduceToStateBasedRewards() override; + /*! + * @return the probabilistic transition matrix P + * @note getTransitionMatrix() retrieves the exit rate matrix R, where R(s,s') = r(s) * P(s,s') + */ + storm::storage::SparseMatrix computeProbabilityMatrix() const; + private: /*! * Computes the exit rate vector based on the given rate matrix.