From 64b9c176e76a2df824f824b045790caa0510311d Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 12 Aug 2020 10:31:31 +0200
Subject: [PATCH] symbolic Ctmc: Added method to compute the probability
 matrix.

---
 src/storm/models/symbolic/Ctmc.cpp | 4 ++++
 src/storm/models/symbolic/Ctmc.h   | 6 ++++++
 2 files changed, 10 insertions(+)

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::DdType Type, typename ValueType>
+            storm::dd::Add<Type, ValueType> Ctmc<Type, ValueType>::computeProbabilityMatrix() const {
+                return this->getTransitionMatrix() / this->getExitRateVector();
+            }
             
             template<storm::dd::DdType Type, typename ValueType>
             template<typename NewValueType>
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<Type, ValueType> 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<Type, ValueType> computeProbabilityMatrix() const;
 
                 template<typename NewValueType>
                 std::shared_ptr<Ctmc<Type, NewValueType>> toValueType() const;