Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BeliefManager.h
Go to the documentation of this file.
1#pragma once
2
3#include <boost/container/flat_map.hpp>
4#include <boost/container/flat_set.hpp>
5#include <optional>
6#include <unordered_map>
7#include <vector>
8
14
15namespace storm {
16namespace storage {
17// Forward declaration
18template<typename ValueType>
19class SparseMatrix;
20
21template<typename PomdpType, typename BeliefValueType = typename PomdpType::ValueType, typename StateType = uint64_t>
23 public:
24 typedef typename PomdpType::ValueType ValueType;
25 typedef boost::container::flat_map<StateType, BeliefValueType> BeliefType; // iterating over this shall be ordered (for correct hash computation)
26 typedef boost::container::flat_set<StateType> BeliefSupportType;
27 typedef uint64_t BeliefId;
28
30
31 BeliefManager(PomdpType const &pomdp, BeliefValueType const &precision, TriangulationMode const &triangulationMode);
32
33 void setRewardModel(std::optional<std::string> rewardModelName = std::nullopt);
34
35 void unsetRewardModel();
36
38 std::vector<BeliefId> gridPoints;
39 std::vector<BeliefValueType> weights;
40 uint64_t size() const;
41 };
42
51
52 BeliefId noId() const;
53
54 bool isEqual(BeliefId const &first, BeliefId const &second) const;
55
56 std::string toString(BeliefId const &beliefId) const;
57
58 std::string toString(Triangulation const &t) const;
59
60 ValueType getWeightedSum(BeliefId const &beliefId, std::vector<ValueType> const &summands);
61
62 std::pair<bool, ValueType> getWeightedSum(BeliefId const &beliefId, std::unordered_map<StateType, ValueType> const &summands);
63
64 BeliefId const &getInitialBelief() const;
65
66 ValueType getBeliefActionReward(BeliefId const &beliefId, uint64_t const &localActionIndex) const;
67
68 uint32_t getBeliefObservation(BeliefId beliefId);
69
70 uint64_t getBeliefNumberOfChoices(BeliefId beliefId);
71
77 uint64_t getRepresentativeState(BeliefId const &beliefId);
78
79 Triangulation triangulateBelief(BeliefId beliefId, BeliefValueType resolution);
80
81 template<typename DistributionType>
82 void addToDistribution(DistributionType &distr, StateType const &state, BeliefValueType const &value);
83
84 void joinSupport(BeliefId const &beliefId, BeliefSupportType &support);
85
87
88 std::vector<std::pair<BeliefId, ValueType>> expandAndTriangulate(BeliefId const &beliefId, uint64_t actionIndex,
89 std::vector<BeliefValueType> const &observationResolutions);
90
91 std::vector<std::pair<BeliefId, ValueType>> expandAndClip(BeliefId const &beliefId, uint64_t actionIndex,
92 std::vector<uint64_t> const &observationResolutions);
93
94 std::vector<std::pair<BeliefId, ValueType>> expand(BeliefId const &beliefId, uint64_t actionIndex);
95
96 BeliefClipping clipBeliefToGrid(BeliefId const &beliefId, uint64_t resolution, storm::storage::BitVector isInfinite = storm::storage::BitVector());
97
98 std::string getObservationLabel(BeliefId const &beliefId);
99
100 std::vector<BeliefValueType> computeMatrixBeliefProduct(BeliefId const &beliefId, storm::storage::SparseMatrix<BeliefValueType> &matrix);
101
102 private:
103 std::vector<BeliefValueType> getBeliefAsVector(BeliefId const &beliefId);
104
105 std::vector<BeliefValueType> getBeliefAsVector(const BeliefType &belief);
106
107 BeliefClipping clipBeliefToGrid(BeliefType const &belief, uint64_t resolution, const storm::storage::BitVector &isInfinite);
108
109 template<typename DistributionType>
110 void adjustDistribution(DistributionType &distr);
111
112 struct BeliefHash {
113 std::size_t operator()(const BeliefType &belief) const;
114 };
115
116 struct Belief_equal_to {
117 bool operator()(const BeliefType &lhBelief, const BeliefType &rhBelief) const;
118 };
119
120 struct FreudenthalDiff {
121 FreudenthalDiff(StateType const &dimension, BeliefValueType diff);
122
123 StateType dimension; // i
124 BeliefValueType diff; // d[i]
125 bool operator>(FreudenthalDiff const &other) const;
126 };
127
128 BeliefType const &getBelief(BeliefId const &id) const;
129
130 BeliefId getId(BeliefType const &belief) const;
131
132 std::string toString(BeliefType const &belief) const;
133
134 bool isEqual(BeliefType const &first, BeliefType const &second) const;
135
136 bool assertBelief(BeliefType const &belief) const;
137
138 bool assertTriangulation(BeliefType const &belief, Triangulation const &triangulation) const;
139
140 uint32_t getBeliefObservation(BeliefType belief) const;
141
142 void triangulateBeliefFreudenthal(BeliefType const &belief, BeliefValueType const &resolution, Triangulation &result);
143
144 void triangulateBeliefDynamic(BeliefType const &belief, BeliefValueType const &resolution, Triangulation &result);
145
146 Triangulation triangulateBelief(BeliefType const &belief, BeliefValueType const &resolution);
147
148 std::vector<std::pair<BeliefId, ValueType>> expandInternal(
149 BeliefId const &beliefId, uint64_t actionIndex, std::optional<std::vector<BeliefValueType>> const &observationTriangulationResolutions = std::nullopt,
150 std::optional<std::vector<uint64_t>> const &observationGridClippingResolutions = std::nullopt);
151
152 BeliefId computeInitialBelief();
153
154 BeliefId getOrAddBeliefId(BeliefType const &belief);
155
156 PomdpType const &pomdp;
157 std::vector<ValueType> pomdpActionRewardVector;
158
159 std::vector<BeliefType> beliefs;
160 std::vector<std::unordered_map<BeliefType, BeliefId, BeliefHash, Belief_equal_to>> beliefToIdMap;
161 BeliefId initialBeliefId;
162
164
165 std::shared_ptr<storm::solver::LpSolver<BeliefValueType>> lpSolver;
166
167 TriangulationMode triangulationMode;
168};
169} // namespace storage
170} // namespace storm
std::vector< BeliefValueType > computeMatrixBeliefProduct(BeliefId const &beliefId, storm::storage::SparseMatrix< BeliefValueType > &matrix)
void joinSupport(BeliefId const &beliefId, BeliefSupportType &support)
boost::container::flat_set< StateType > BeliefSupportType
PomdpType::ValueType ValueType
std::vector< std::pair< BeliefId, ValueType > > expandAndTriangulate(BeliefId const &beliefId, uint64_t actionIndex, std::vector< BeliefValueType > const &observationResolutions)
boost::container::flat_map< StateType, BeliefValueType > BeliefType
uint32_t getBeliefObservation(BeliefId beliefId)
void setRewardModel(std::optional< std::string > rewardModelName=std::nullopt)
std::string toString(BeliefId const &beliefId) const
uint64_t getBeliefNumberOfChoices(BeliefId beliefId)
uint64_t getRepresentativeState(BeliefId const &beliefId)
Returns the first state in the belief as a representative.
std::vector< std::pair< BeliefId, ValueType > > expand(BeliefId const &beliefId, uint64_t actionIndex)
BeliefId const & getInitialBelief() const
std::vector< std::pair< BeliefId, ValueType > > expandAndClip(BeliefId const &beliefId, uint64_t actionIndex, std::vector< uint64_t > const &observationResolutions)
ValueType getBeliefActionReward(BeliefId const &beliefId, uint64_t const &localActionIndex) const
BeliefId getNumberOfBeliefIds() const
void addToDistribution(DistributionType &distr, StateType const &state, BeliefValueType const &value)
std::string getObservationLabel(BeliefId const &beliefId)
ValueType getWeightedSum(BeliefId const &beliefId, std::vector< ValueType > const &summands)
BeliefClipping clipBeliefToGrid(BeliefId const &beliefId, uint64_t resolution, storm::storage::BitVector isInfinite=storm::storage::BitVector())
bool isEqual(BeliefId const &first, BeliefId const &second) const
Triangulation triangulateBelief(BeliefId beliefId, BeliefValueType resolution)
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
A class that holds a possibly non-square matrix in the compressed row storage format.
LabParser.cpp.
Definition cli.cpp:18
std::vector< BeliefValueType > weights