Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NondeterministicBeliefTracker.h
Go to the documentation of this file.
1#pragma once
3
4namespace storm {
5namespace generator {
10template<typename ValueType>
12 public:
15 uint64_t getActionsForObservation(uint32_t observation) const;
16 ValueType getRisk(uint64_t) const;
17 void setRiskPerState(std::vector<ValueType> const& risk);
18 uint64_t getFreshId();
19 uint32_t getObservation(uint64_t state) const;
20 uint64_t getObservationOffset(uint64_t state) const;
21 uint64_t getState(uint32_t obs, uint64_t offset) const;
22 uint64_t getNumberOfStates() const;
23 uint64_t numberOfStatesPerObservation(uint32_t observation) const;
24
25 private:
27 std::vector<ValueType> riskPerState;
28 std::vector<uint64_t> numberActionsPerObservation;
29 uint64_t beliefIdCounter = 0;
30 std::vector<uint64_t> observationOffsetId;
31 std::vector<std::vector<uint64_t>> statePerObservationAndOffset;
32};
33
34template<typename ValueType>
36template<typename ValueType>
38
42template<typename ValueType>
44 public:
45 SparseBeliefState(std::shared_ptr<BeliefStateManager<ValueType>> const& manager, uint64_t state);
51 void update(uint32_t newObservation, std::unordered_set<SparseBeliefState>& previousBeliefs) const;
52 std::size_t hash() const noexcept;
58 ValueType get(uint64_t state) const;
63 ValueType getRisk() const;
64
65 // Various getters
66 std::string toString() const;
67 bool isValid() const;
68 uint64_t getSupportSize() const;
70 std::map<uint64_t, ValueType> const& getBeliefMap() const;
71
72 friend bool operator== <>(SparseBeliefState<ValueType> const& lhs, SparseBeliefState<ValueType> const& rhs);
73
74 private:
75 void updateHelper(std::vector<std::map<uint64_t, ValueType>> const& partialBeliefs, std::vector<ValueType> const& sums,
76 typename std::map<uint64_t, ValueType>::const_iterator nextStateIt, uint32_t newObservation,
77 std::unordered_set<SparseBeliefState<ValueType>>& previousBeliefs) const;
78 SparseBeliefState(std::shared_ptr<BeliefStateManager<ValueType>> const& manager, std::map<uint64_t, ValueType> const& belief, std::size_t newHash,
79 ValueType const& risk, uint64_t prevId);
80 std::shared_ptr<BeliefStateManager<ValueType>> manager;
81
82 std::map<uint64_t, ValueType> belief; // map is ordered for unique hashing.
83 std::size_t prestoredhash = 0;
84 ValueType risk;
85 uint64_t id;
86 uint64_t prevId;
87};
88
92template<typename ValueType>
94template<typename ValueType>
96
97template<typename ValueType>
99 public:
100 ObservationDenseBeliefState(std::shared_ptr<BeliefStateManager<ValueType>> const& manager, uint64_t state);
101 void update(uint32_t newObservation, std::unordered_set<ObservationDenseBeliefState>& previousBeliefs) const;
102 std::size_t hash() const noexcept;
103 ValueType get(uint64_t state) const;
104 ValueType getRisk() const;
105 std::string toString() const;
106 uint64_t getSupportSize() const;
108 friend bool operator== <>(ObservationDenseBeliefState<ValueType> const& lhs, ObservationDenseBeliefState<ValueType> const& rhs);
109
110 private:
111 void updateHelper(std::vector<std::map<uint64_t, ValueType>> const& partialBeliefs, std::vector<ValueType> const& sums, uint64_t currentEntry,
112 uint32_t newObservation, std::unordered_set<ObservationDenseBeliefState<ValueType>>& previousBeliefs) const;
113 ObservationDenseBeliefState(std::shared_ptr<BeliefStateManager<ValueType>> const& manager, uint32_t observation, std::vector<ValueType> const& belief,
114 std::size_t newHash, ValueType const& risk, uint64_t prevId);
115 std::shared_ptr<BeliefStateManager<ValueType>> manager;
116
117 std::vector<ValueType> belief;
118 uint64_t observation = 0;
119 std::size_t prestoredhash = 0;
120 ValueType risk;
121 uint64_t id;
122 uint64_t prevId;
123};
124
132template<typename ValueType, typename BeliefState>
134 public:
135 struct Options {
136 uint64_t trackTimeOut = 0;
137 uint64_t timeOut = 0; // for reduction, in milliseconds, 0 is no timeout
138 ValueType wiggle; // tolerance, anything above 0 means that we are incomplete.
139 };
147 bool reset(uint32_t observation);
153 bool track(uint64_t newObservation);
158 std::unordered_set<BeliefState> const& getCurrentBeliefs() const;
163 uint32_t getCurrentObservation() const;
168 uint64_t getNumberOfBeliefs() const;
174 ValueType getCurrentRisk(bool max = true);
179 void setRisk(std::vector<ValueType> const& risk);
185 uint64_t getCurrentDimension() const;
190 uint64_t reduce();
195 bool hasTimedOut() const;
196
197 private:
199 std::shared_ptr<BeliefStateManager<ValueType>> manager;
200 std::unordered_set<BeliefState> beliefs;
201 bool reductionTimedOut = false;
202 Options options;
203 uint32_t lastObservation;
204};
205} // namespace generator
206} // namespace storm
207
208//
209namespace std {
210template<typename T>
211struct hash<storm::generator::SparseBeliefState<T>> {
212 std::size_t operator()(storm::generator::SparseBeliefState<T> const& s) const noexcept {
213 return s.hash();
214 }
215};
216template<typename T>
217struct hash<storm::generator::ObservationDenseBeliefState<T>> {
219 return s.hash();
220 }
221};
222} // namespace std
This class keeps track of common information of a set of beliefs.
storm::models::sparse::Pomdp< ValueType > const & getPomdp() const
uint64_t getState(uint32_t obs, uint64_t offset) const
uint64_t numberOfStatesPerObservation(uint32_t observation) const
void setRiskPerState(std::vector< ValueType > const &risk)
uint64_t getActionsForObservation(uint32_t observation) const
This tracker implements state estimation for POMDPs.
std::unordered_set< BeliefState > const & getCurrentBeliefs() const
Provides access to the current beliefs.
uint64_t reduce()
Apply reductions to the belief state.
ValueType getCurrentRisk(bool max=true)
What is the (worst-case/best-case) risk over all beliefs.
void setRisk(std::vector< ValueType > const &risk)
Sets the state-risk to use for all beliefs.
uint64_t getCurrentDimension() const
What is the dimension of the current set of beliefs, i.e., what is the number of states we could poss...
uint32_t getCurrentObservation() const
What was the last obervation that we made?
bool hasTimedOut() const
Did we time out during the computation?
bool reset(uint32_t observation)
Start with a new trace.
uint64_t getNumberOfBeliefs() const
How many beliefs are we currently tracking?
bool track(uint64_t newObservation)
Extend the observed trace with the new observation.
ObservationDenseBeliefState stores beliefs in a dense format (per observation).
void update(uint32_t newObservation, std::unordered_set< ObservationDenseBeliefState > &previousBeliefs) const
SparseBeliefState stores beliefs in a sparse format.
void setSupport(storm::storage::BitVector &) const
void update(uint32_t newObservation, std::unordered_set< SparseBeliefState > &previousBeliefs) const
Update the belief using the new observation.
std::map< uint64_t, ValueType > const & getBeliefMap() const
ValueType get(uint64_t state) const
Get the estimate to be in the given state.
ValueType getRisk() const
Get the weighted risk.
This class represents a partially observable Markov decision process.
Definition Pomdp.h:15
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
bool operator==(SparseBeliefState< ValueType > const &lhs, SparseBeliefState< ValueType > const &rhs)
LabParser.cpp.
Definition cli.cpp:18
std::size_t operator()(storm::generator::ObservationDenseBeliefState< T > const &s) const noexcept
std::size_t operator()(storm::generator::SparseBeliefState< T > const &s) const noexcept