Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Mdp.cpp
Go to the documentation of this file.
2
8
9namespace storm {
10namespace models {
11namespace sparse {
12
13template<typename ValueType, typename RewardModelType>
15 std::unordered_map<std::string, RewardModelType> const& rewardModels, ModelType type)
16 : Mdp<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels),
17 type) {
18 // Intentionally left empty
19}
20
21template<typename ValueType, typename RewardModelType>
23 std::unordered_map<std::string, RewardModelType>&& rewardModels, ModelType type)
25 storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels)),
26 type) {
27 // Intentionally left empty
28}
29
30template<typename ValueType, typename RewardModelType>
32 : NondeterministicModel<ValueType, RewardModelType>(type, components) {
34 // Intentionally left empty
35}
36
37template<typename ValueType, typename RewardModelType>
39 : NondeterministicModel<ValueType, RewardModelType>(type, std::move(components)) {
41 // Intentionally left empty
43
44template class Mdp<double>;
46template class Mdp<storm::RationalNumber>;
47template class Mdp<storm::Interval>;
48template class Mdp<storm::RationalFunction>;
49} // namespace sparse
50} // namespace models
51} // 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:14
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.