Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ObservationTraceUnfolder.h
Go to the documentation of this file.
1#pragma once
2
4
5namespace storm {
6namespace pomdp {
12template<typename ValueType>
14 public:
21 ObservationTraceUnfolder(storm::models::sparse::Pomdp<ValueType> const& model, std::vector<ValueType> const& risk,
22 std::shared_ptr<storm::expressions::ExpressionManager>& exprManager);
28 std::shared_ptr<storm::models::sparse::Mdp<ValueType>> transform(std::vector<uint32_t> const& observations);
34 std::shared_ptr<storm::models::sparse::Mdp<ValueType>> extend(uint32_t observation);
39 void reset(uint32_t observation);
40
41 private:
43 std::vector<ValueType> risk; // TODO reconsider holding this as a reference, but there were some strange bugs
44 std::shared_ptr<storm::expressions::ExpressionManager>& exprManager;
45 std::vector<storm::storage::BitVector> statesPerObservation;
46 std::vector<uint32_t> traceSoFar;
48};
49
50} // namespace pomdp
51} // namespace storm
This class represents a partially observable Markov decision process.
Definition Pomdp.h:13
Observation-trace unrolling to allow model checking for monitoring.
std::shared_ptr< storm::models::sparse::Mdp< ValueType > > extend(uint32_t observation)
Transform incrementaly.
void reset(uint32_t observation)
When using the incremental approach, reset the observations made so far.
std::shared_ptr< storm::models::sparse::Mdp< ValueType > > transform(std::vector< uint32_t > const &observations)
Transform in one shot.