Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Ctmc.h
Go to the documentation of this file.
1#pragma once
2
4
5namespace storm {
6namespace models {
7namespace sparse {
8
12template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
13class Ctmc : public DeterministicModel<ValueType, RewardModelType> {
14 public:
23 std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
24
33 std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>());
34
42
43 Ctmc(Ctmc<ValueType, RewardModelType> const& ctmc) = default;
47
53 std::vector<ValueType> const& getExitRateVector() const;
54
60 std::vector<ValueType>& getExitRateVector();
61
62 virtual void reduceToStateBasedRewards() override;
63
69
70 private:
77 static std::vector<ValueType> createExitRateVector(storm::storage::SparseMatrix<ValueType> const& rateMatrix);
78
79 // A vector containing the exit rates of all states.
80 std::vector<ValueType> exitRates;
81};
82
83} // namespace sparse
84} // namespace models
85} // namespace storm
This class represents a continuous-time Markov chain.
Definition Ctmc.h:13
Ctmc & operator=(Ctmc< ValueType, RewardModelType > const &ctmc)=default
storm::storage::SparseMatrix< ValueType > computeProbabilityMatrix() const
Definition Ctmc.cpp:83
Ctmc & operator=(Ctmc< ValueType, RewardModelType > &&ctmc)=default
virtual void reduceToStateBasedRewards() override
Converts the transition rewards of all reward models to state-based rewards.
Definition Ctmc.cpp:76
Ctmc(Ctmc< ValueType, RewardModelType > const &ctmc)=default
Ctmc(Ctmc< ValueType, RewardModelType > &&ctmc)=default
std::vector< ValueType > const & getExitRateVector() const
Retrieves the vector of exit rates of the model.
Definition Ctmc.cpp:57
The base class of all sparse deterministic models.
This class manages the labeling of the state space with a number of (atomic) labels.
A class that holds a possibly non-square matrix in the compressed row storage format.