Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Mdp.h
Go to the documentation of this file.
1#ifndef STORM_MODELS_SPARSE_MDP_H_
2#define STORM_MODELS_SPARSE_MDP_H_
3
5
6namespace storm {
7namespace models {
8namespace sparse {
9
13template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
14class Mdp : public NondeterministicModel<ValueType, RewardModelType> {
15 public:
23 Mdp(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>(),
26
35 std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>(), ModelType type = ModelType::Mdp);
36
44
45 Mdp(Mdp<ValueType, RewardModelType> const& other) = default;
47
50
51 virtual ~Mdp() = default;
52};
53
54} // namespace sparse
55} // namespace models
56} // namespace storm
57
58#endif /* STORM_MODELS_SPARSE_MDP_H_ */
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
Mdp & operator=(Mdp< ValueType, RewardModelType > &&other)=default
Mdp(Mdp< ValueType, RewardModelType > &&other)=default
Mdp & operator=(Mdp< ValueType, RewardModelType > const &other)=default
Mdp(Mdp< ValueType, RewardModelType > const &other)=default
virtual ~Mdp()=default
The base class of sparse nondeterministic 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.
LabParser.cpp.
Definition cli.cpp:18