diff --git a/src/storm/models/symbolic/Ctmc.cpp b/src/storm/models/symbolic/Ctmc.cpp index d54b3156d..26e20c3bf 100644 --- a/src/storm/models/symbolic/Ctmc.cpp +++ b/src/storm/models/symbolic/Ctmc.cpp @@ -94,6 +94,10 @@ namespace storm { } } + template + storm::dd::Add Ctmc::computeProbabilityMatrix() const { + return this->getTransitionMatrix() / this->getExitRateVector(); + } template template diff --git a/src/storm/models/symbolic/Ctmc.h b/src/storm/models/symbolic/Ctmc.h index c73340946..34d601f4a 100644 --- a/src/storm/models/symbolic/Ctmc.h +++ b/src/storm/models/symbolic/Ctmc.h @@ -142,6 +142,12 @@ namespace storm { storm::dd::Add const& getExitRateVector() const; 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::dd::Add computeProbabilityMatrix() const; template std::shared_ptr> toValueType() const;