Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Pomdp.cpp
Go to the documentation of this file.
2
6
7namespace storm {
8namespace models {
9namespace sparse {
10
11template<typename ValueType, typename RewardModelType>
13 storm::models::sparse::StateLabeling const &stateLabeling,
14 std::unordered_map<std::string, RewardModelType> const &rewardModels)
15 : Mdp<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels, storm::models::ModelType::Pomdp) {
17}
18
19template<typename ValueType, typename RewardModelType>
21 std::unordered_map<std::string, RewardModelType> &&rewardModels)
22 : Mdp<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels, storm::models::ModelType::Pomdp) {
24}
25
26template<typename ValueType, typename RewardModelType>
28 : Mdp<ValueType, RewardModelType>(components, storm::models::ModelType::Pomdp),
29 observations(components.observabilityClasses.value()),
30 canonicFlag(canonicFlag),
31 observationValuations(components.observationValuations) {
33}
34
35template<typename ValueType, typename RewardModelType>
37 : Mdp<ValueType, RewardModelType>(components, storm::models::ModelType::Pomdp),
38 observations(components.observabilityClasses.value()),
39 canonicFlag(canonicFlag),
40 observationValuations(components.observationValuations) {
42}
43
44template<typename ValueType, typename RewardModelType>
46 this->printModelInformationHeaderToStream(out);
47 out << "Choices: \t" << this->getNumberOfChoices() << '\n';
48 out << "Observations: \t" << this->nrObservations << '\n';
49 this->printModelInformationFooterToStream(out);
50}
51
52template<typename ValueType, typename RewardModelType>
54 uint64_t highestEntry = 0;
55 for (uint32_t entry : observations) {
56 if (entry > highestEntry) {
57 highestEntry = entry;
58 }
59 }
60 nrObservations = highestEntry + 1; // Smallest entry should be zero.
61 // In debug mode, ensure that every observability is used.
62}
63
64template<typename ValueType, typename RewardModelType>
66 return observations.at(state);
67}
68
69template<typename ValueType, typename RewardModelType>
71 return nrObservations;
72}
73
74template<typename ValueType, typename RewardModelType>
76 std::map<uint32_t, uint64_t> counts;
77 for (auto const &obs : observations) {
78 auto insertionRes = counts.emplace(obs, 1ull);
79 if (!insertionRes.second) {
80 ++insertionRes.first->second;
81 }
82 }
83 uint64_t result = 0;
84 for (auto const &count : counts) {
85 result = std::max(result, count.second);
86 }
87 return result;
88}
89
90template<typename ValueType, typename RewardModelType>
91std::vector<uint32_t> const &Pomdp<ValueType, RewardModelType>::getObservations() const {
92 return observations;
93}
94
95template<typename ValueType, typename RewardModelType>
96void Pomdp<ValueType, RewardModelType>::updateObservations(std::vector<uint32_t> &&newObservations, bool preservesCanonicity) {
97 observations = std::move(newObservations);
98 computeNrObservations();
99 setIsCanonic(isCanonic() && preservesCanonicity);
100}
101
102template<typename ValueType, typename RewardModelType>
104 return "<" + std::to_string(getObservation(state)) + ">";
105}
106
107template<typename ValueType, typename RewardModelType>
108std::vector<uint64_t> Pomdp<ValueType, RewardModelType>::getStatesWithObservation(uint32_t observation) const {
109 std::vector<uint64_t> result;
110 for (uint64_t state = 0; state < this->getNumberOfStates(); ++state) {
111 if (this->getObservation(state) == observation) {
112 result.push_back(state);
113 }
114 }
115 return result;
116}
117
118template<typename ValueType, typename RewardModelType>
120 return static_cast<bool>(observationValuations);
121}
122
123template<typename ValueType, typename RewardModelType>
127
128template<typename ValueType, typename RewardModelType>
129std::optional<storm::storage::sparse::StateValuations> const &Pomdp<ValueType, RewardModelType>::getOptionalObservationValuations() const {
130 return observationValuations;
131}
132
133template<typename ValueType, typename RewardModelType>
135 return canonicFlag;
136}
137
138template<typename ValueType, typename RewardModelType>
140 this->canonicFlag = newValue;
141}
142
143template<typename ValueType, typename RewardModelType>
147
148template<typename ValueType, typename RewardModelType>
150 std::size_t seed = 0;
151 boost::hash_combine(seed, sparse::Model<ValueType, RewardModelType>::hash());
152 boost::hash_combine(seed, boost::hash_range(observations.begin(), observations.end()));
153 return seed;
154}
155
156template class Pomdp<double>;
158template class Pomdp<storm::RationalNumber>;
159template class Pomdp<storm::Interval>;
160template class Pomdp<storm::RationalFunction>;
161} // namespace sparse
162} // namespace models
163} // namespace storm
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:13
Base class for all sparse models.
Definition Model.h:32
CRewardModelType RewardModelType
Definition Model.h:35
This class represents a partially observable Markov decision process.
Definition Pomdp.h:13
virtual bool isPartiallyObservable() const override
Definition Pomdp.cpp:144
uint64_t getNrObservations() const
Definition Pomdp.cpp:70
storm::storage::sparse::StateValuations const & getObservationValuations() const
Definition Pomdp.cpp:124
Pomdp(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 Pomdp.cpp:12
virtual void printModelInformationToStream(std::ostream &out) const override
Prints information about the model to the specified stream.
Definition Pomdp.cpp:45
void updateObservations(std::vector< uint32_t > &&newObservations, bool preservesCanonicity)
Changes the observations to the given ones and updates redundant informations (like the number of obs...
Definition Pomdp.cpp:96
std::vector< uint64_t > getStatesWithObservation(uint32_t observation) const
Definition Pomdp.cpp:108
std::optional< storm::storage::sparse::StateValuations > const & getOptionalObservationValuations() const
Definition Pomdp.cpp:129
virtual std::size_t hash() const override
Definition Pomdp.cpp:149
uint32_t getObservation(uint64_t state) const
Definition Pomdp.cpp:65
uint64_t getMaxNrStatesWithSameObservation() const
Returns the number of hidden values, i.e.
Definition Pomdp.cpp:75
void setIsCanonic(bool newValue=true)
Definition Pomdp.cpp:139
bool hasObservationValuations() const
Definition Pomdp.cpp:119
std::vector< uint32_t > const & getObservations() const
Definition Pomdp.cpp:91
virtual std::string additionalDotStateInfo(uint64_t state) const override
Return a string that is additonally added to the state information in the dot stream.
Definition Pomdp.cpp:103
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.