Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Dtmc.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 Dtmc : public DeterministicModel<ValueType, RewardModelType> {
14 public:
22 Dtmc(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling,
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 Dtmc(Dtmc<ValueType, RewardModelType> const& dtmc) = default;
45
48
49 virtual ~Dtmc() = default;
50
51 virtual void reduceToStateBasedRewards() override;
52};
53
54} // namespace sparse
55} // namespace models
56} // namespace storm
The base class of all sparse deterministic models.
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
Dtmc & operator=(Dtmc< ValueType, RewardModelType > const &dtmc)=default
Dtmc(Dtmc< ValueType, RewardModelType > &&dtmc)=default
virtual void reduceToStateBasedRewards() override
Converts the transition rewards of all reward models to state-based rewards.
Definition Dtmc.cpp:39
Dtmc(Dtmc< ValueType, RewardModelType > const &dtmc)=default
virtual ~Dtmc()=default
Dtmc & operator=(Dtmc< ValueType, RewardModelType > &&dtmc)=default
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.