Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Mdp.cpp
Go to the documentation of this file.
2
6
7namespace storm {
8namespace models {
9namespace sparse {
10
11template<typename ValueType, typename RewardModelType>
13 std::unordered_map<std::string, RewardModelType> const& rewardModels, ModelType type)
14 : Mdp<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels),
15 type) {
16 // Intentionally left empty
17}
18
19template<typename ValueType, typename RewardModelType>
21 std::unordered_map<std::string, RewardModelType>&& rewardModels, ModelType type)
23 storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels)),
24 type) {
25 // Intentionally left empty
26}
27
28template<typename ValueType, typename RewardModelType>
34
35template<typename ValueType, typename RewardModelType>
42template class Mdp<double>;
44template class Mdp<storm::RationalNumber>;
45template class Mdp<storm::Interval>;
46template class Mdp<storm::RationalFunction>;
47} // namespace sparse
48} // namespace models
49} // namespace storm
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:13
Mdp(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 >(), ModelType type=ModelType::Mdp)
Constructs a model from the given data.
Definition Mdp.cpp:12
CRewardModelType RewardModelType
Definition Model.h:35
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.