Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
MakeStateSetObservationClosed.cpp
Go to the documentation of this file.
3
4namespace storm {
5namespace transformer {
6
7template<typename ValueType>
9
10template<typename ValueType>
11std::pair<std::shared_ptr<storm::models::sparse::Pomdp<ValueType>>, std::set<uint32_t>> MakeStateSetObservationClosed<ValueType>::transform(
12 storm::storage::BitVector const& stateSet) const {
13 // Collect observations of target states
14 std::set<uint32_t> oldObservations;
15 for (auto const state : stateSet) {
16 oldObservations.insert(pomdp->getObservation(state));
17 }
18
19 // Collect observations that belong to both, target states and non-target states.
20 // Add a fresh observation for each of them
21 std::map<uint32_t, uint32_t> oldToNewObservationMap;
22 uint32_t freshObs = pomdp->getNrObservations();
23 for (uint64_t state = stateSet.getNextUnsetIndex(0); state < stateSet.size(); state = stateSet.getNextUnsetIndex(state + 1)) {
24 uint32_t obs = pomdp->getObservation(state);
25 if (oldObservations.count(obs) > 0) {
26 // this observation belongs to both, target and non-target states.
27 if (oldToNewObservationMap.emplace(obs, freshObs).second) {
28 // We actually inserted something, i.e., we have not seen this observation before.
29 // For the next observation (that is different from obs) we want to insert another fresh observation index
30 // This is to preserve the assumption that states with the same observation have the same enabled actions.
31 ++freshObs;
32 }
33 }
34 }
35
36 // Check whether the state set already is observation closed.
37 if (oldToNewObservationMap.empty()) {
38 return {pomdp, std::move(oldObservations)};
39 } else {
40 // Create new observations
41 auto newObservationVector = pomdp->getObservations();
42 for (auto const state : stateSet) {
43 auto findRes = oldToNewObservationMap.find(pomdp->getObservation(state));
44 if (findRes != oldToNewObservationMap.end()) {
45 newObservationVector[state] = findRes->second;
46 }
47 }
48 // Create a copy of the pomdp and change observations accordingly.
49 // This transformation preserves canonicity.
50 auto transformed = std::make_shared<storm::models::sparse::Pomdp<ValueType>>(*pomdp);
51 transformed->updateObservations(std::move(newObservationVector), true);
52
53 // Finally, get the new set of target observations
54 std::set<uint32_t> newObservations;
55 for (auto const& obs : oldObservations) {
56 auto findRes = oldToNewObservationMap.find(obs);
57 if (findRes == oldToNewObservationMap.end()) {
58 newObservations.insert(obs);
59 } else {
60 newObservations.insert(findRes->second);
61 }
62 }
63
64 return {transformed, std::move(newObservations)};
65 }
66}
67
70} // namespace transformer
71} // namespace storm
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
size_t size() const
Retrieves the number of bits this bit vector can store.
uint_fast64_t getNextUnsetIndex(uint_fast64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to false in the bit vector.
std::pair< std::shared_ptr< storm::models::sparse::Pomdp< ValueType > >, std::set< uint32_t > > transform(storm::storage::BitVector const &stateSet) const
Ensures that the given set of states is observation closed, potentially, adding new observation(s) A ...
MakeStateSetObservationClosed(std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > pomdp)
LabParser.cpp.
Definition cli.cpp:18