Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ObservationTraceUnfolder.h
Go to the documentation of this file.
2
3namespace storm {
4namespace pomdp {
10template<typename ValueType>
12 public:
19 ObservationTraceUnfolder(storm::models::sparse::Pomdp<ValueType> const& model, std::vector<ValueType> const& risk,
20 std::shared_ptr<storm::expressions::ExpressionManager>& exprManager);
26 std::shared_ptr<storm::models::sparse::Mdp<ValueType>> transform(std::vector<uint32_t> const& observations);
32 std::shared_ptr<storm::models::sparse::Mdp<ValueType>> extend(uint32_t observation);
37 void reset(uint32_t observation);
38
39 private:
41 std::vector<ValueType> risk; // TODO reconsider holding this as a reference, but there were some strange bugs
42 std::shared_ptr<storm::expressions::ExpressionManager>& exprManager;
43 std::vector<storm::storage::BitVector> statesPerObservation;
44 std::vector<uint32_t> traceSoFar;
46};
47
48} // namespace pomdp
49} // namespace storm
This class represents a partially observable Markov decision process.
Definition Pomdp.h:15
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.
LabParser.cpp.
Definition cli.cpp:18