Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Mdp.cpp
Go to the documentation of this file.
2
7
9
10namespace storm {
11namespace models {
12namespace sparse {
13
14template<typename ValueType, typename RewardModelType>
16 std::unordered_map<std::string, RewardModelType> const& rewardModels, ModelType type)
17 : Mdp<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels),
18 type) {
19 // Intentionally left empty
20}
21
22template<typename ValueType, typename RewardModelType>
24 std::unordered_map<std::string, RewardModelType>&& rewardModels, ModelType type)
26 storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels)),
27 type) {
28 // Intentionally left empty
29}
30
31template<typename ValueType, typename RewardModelType>
33 : NondeterministicModel<ValueType, RewardModelType>(type, components) {
35 // Intentionally left empty
36}
37
38template<typename ValueType, typename RewardModelType>
40 : NondeterministicModel<ValueType, RewardModelType>(type, std::move(components)) {
42 // Intentionally left empty
44
45template class Mdp<double>;
46template class Mdp<storm::RationalNumber>;
47
49template class Mdp<storm::RationalFunction>;
50template class Mdp<storm::Interval>;
51} // namespace sparse
52} // namespace models
53} // namespace storm
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
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:15
CRewardModelType RewardModelType
Definition Model.h:36
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