storm::pomdp::ObservationTraceUnfolder< ValueType > Class Template Reference

Observation-trace unrolling to allow model checking for monitoring. More...

#include <ObservationTraceUnfolder.h>

Public Member Functions
	ObservationTraceUnfolder (storm::models::sparse::Pomdp< ValueType > const &model, std::vector< ValueType > const &risk, std::shared_ptr< storm::expressions::ExpressionManager > &exprManager)
	Initialize.
std::shared_ptr< storm::models::sparse::Mdp< ValueType > >	transform (std::vector< uint32_t > const &observations)
	Transform in one shot.
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.

Detailed Description

template<typename ValueType>
class storm::pomdp::ObservationTraceUnfolder< ValueType >

Observation-trace unrolling to allow model checking for monitoring.

This approach is outlined in Junges, Hazem, Seshia – Runtime Monitoring for Markov Decision Processes

Template Parameters

ValueType

ValueType for probabilities

Definition at line 11 of file ObservationTraceUnfolder.h.

Constructor & Destructor Documentation

ObservationTraceUnfolder()

template<typename ValueType >

storm::pomdp::ObservationTraceUnfolder< ValueType >::ObservationTraceUnfolder	(	storm::models::sparse::Pomdp< ValueType > const &	model,
		std::vector< ValueType > const &	risk,
		std::shared_ptr< storm::expressions::ExpressionManager > &	exprManager
	)

Initialize.

Parameters

model	the MDP with state-based observations
risk	the state risk
exprManager	an Expression Manager

Definition at line 13 of file ObservationTraceUnfolder.cpp.

Member Function Documentation

extend()

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Mdp< ValueType > > storm::pomdp::ObservationTraceUnfolder< ValueType >::extend

(

uint32_t

observation

)

Transform incrementaly.

Parameters

observation

Returns

Definition at line 185 of file ObservationTraceUnfolder.cpp.

reset()

template<typename ValueType >

void storm::pomdp::ObservationTraceUnfolder< ValueType >::reset

(

uint32_t

observation

)

When using the incremental approach, reset the observations made so far.

Parameters

observation

The new initial observation

Definition at line 191 of file ObservationTraceUnfolder.cpp.

transform()

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Mdp< ValueType > > storm::pomdp::ObservationTraceUnfolder< ValueType >::transform

(

std::vector< uint32_t > const &

observations

)

Transform in one shot.

Parameters

observations

Returns

Definition at line 24 of file ObservationTraceUnfolder.cpp.

---

The documentation for this class was generated from the following files:

• src/storm-pomdp/transformer/ObservationTraceUnfolder.h
• src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp