Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Dtmc.h
Go to the documentation of this file.
1#ifndef STORM_MODELS_SPARSE_DTMC_H_
2#define STORM_MODELS_SPARSE_DTMC_H_
3
5
6namespace storm {
7namespace models {
8namespace sparse {
9
13template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
14class Dtmc : public DeterministicModel<ValueType, RewardModelType> {
15 public:
23 Dtmc(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling,
24 std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
25
34 std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>());
35
43
44 Dtmc(Dtmc<ValueType, RewardModelType> const& dtmc) = default;
46
49
50 virtual ~Dtmc() = default;
51
52 virtual void reduceToStateBasedRewards() override;
53};
54
55} // namespace sparse
56} // namespace models
57} // namespace storm
58
59#endif /* STORM_MODELS_SPARSE_DTMC_H_ */
The base class of all sparse deterministic models.
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
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:41
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.
LabParser.cpp.
Definition cli.cpp:18