Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Dtmc.cpp
Go to the documentation of this file.
2
5
6namespace storm {
7namespace models {
8namespace sparse {
9
10template<typename ValueType, typename RewardModelType>
12 storm::models::sparse::StateLabeling const& stateLabeling,
13 std::unordered_map<std::string, RewardModelType> const& rewardModels)
14 : Dtmc<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels)) {
15 // Intentionally left empty
16}
17
18template<typename ValueType, typename RewardModelType>
20 std::unordered_map<std::string, RewardModelType>&& rewardModels)
22 storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels))) {
23 // Intentionally left empty
24}
25
26template<typename ValueType, typename RewardModelType>
31
32template<typename ValueType, typename RewardModelType>
37
38template<typename ValueType, typename RewardModelType>
40 for (auto& rewardModel : this->getRewardModels()) {
41 rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), true);
42 }
43}
44
45template class Dtmc<double>;
47template class Dtmc<storm::RationalNumber>;
48template class Dtmc<storm::Interval>;
50} // namespace sparse
51} // namespace models
52} // namespace storm
virtual void reduceToStateBasedRewards()=0
Converts the transition rewards of all reward models to state-based rewards.
The base class of all sparse deterministic models.
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
virtual void reduceToStateBasedRewards() override
Converts the transition rewards of all reward models to state-based rewards.
Definition Dtmc.cpp:39
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:11
CRewardModelType RewardModelType
Definition Model.h:35
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.