Storm 1.13.0.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:
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
DeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents< ValueType, RewardModelType > const &components)
Constructs a model from the given data.
Dtmc(storm::storage::sparse::ModelComponents< ValueType, RewardModelType > const &components)
Constructs a model from the given data.
Definition Dtmc.cpp:29
Dtmc(storm::storage::SparseMatrix< ValueType > &&transitionMatrix, storm::models::sparse::StateLabeling &&stateLabeling, std::unordered_map< std::string, RewardModelType > &&rewardModels=std::unordered_map< std::string, RewardModelType >())
Constructs a model by moving the given data.
Definition Dtmc.cpp:21
Dtmc & operator=(Dtmc< ValueType, RewardModelType > const &dtmc)=default
Dtmc(storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &&components)
Definition Dtmc.cpp:35
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
Dtmc(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::models::sparse::StateLabeling const &stateLabeling, std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >())
Constructs a model from the given data.
Definition Dtmc.cpp:13
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.