storm::pomdp::api Namespace Reference

Functions
template<typename ValueType >
storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result	underapproximateWithCutoffs (std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > pomdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, uint64_t sizeThreshold, std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > > additionalPomdpStateValues=std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > >())
	Uses the belief exploration with cut-offs to under-approximate the given objective on a POMDP.
template<typename ValueType >
storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result	underapproximateWithoutHeuristicValues (std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > pomdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, uint64_t sizeThreshold, std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > > pomdpStateValues)
	Uses the belief exploration with cut-offs without the pre-processing to generate cut-off values to under-approximate the given objective on a POMDP.
template<typename ValueType >
storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >	createInteractiveUnfoldingModelChecker (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > pomdp, bool useClipping)
	Create a model checker with the correct settings for an interactive unfolding.
template<typename ValueType >
void	startInteractiveExploration (storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > > &modelchecker, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > > additionalPomdpStateValues=std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > >())
	Start an interactive unfolding to under approximate the given objective.
template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	extractSchedulerAsMarkovChain (typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result modelcheckingResult)
	Extract the scheduler generated by an under-approximation from the given result struct.
template<typename ValueType >
storm::storage::Scheduler< ValueType >	getCutoffScheduler (typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result modelcheckingResult, uint64_t schedId)
	Get a specific scheduler used to generate cut-off values from the result struct.
template<typename ValueType >
uint64_t	getNumberOfPreprocessingSchedulers (typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result modelcheckingResult)
	Get the overall number of schedulers generated by the pre-processing for the under-approximation from the result struct.

Function Documentation

createInteractiveUnfoldingModelChecker()

template<typename ValueType >

storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > > storm::pomdp::api::createInteractiveUnfoldingModelChecker	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Pomdp< ValueType > >	pomdp,
		bool	useClipping
	)

Create a model checker with the correct settings for an interactive unfolding.

Needs to be called first to set-up the unfolding.

Template Parameters

ValueType

number type to be used

Parameters

env	the environment to use
pomdp	the input pomdp to be checked
useClipping	true if clipping is to be used in addition to cut-offs

Returns

the model checker object, configured for an interactive unfolding

Definition at line 66 of file verification.h.

extractSchedulerAsMarkovChain()

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::pomdp::api::extractSchedulerAsMarkovChain

(

typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result

modelcheckingResult

)

Extract the scheduler generated by an under-approximation from the given result struct.

The scheduler is represented by a Markov chain.

Template Parameters

ValueType

number type to be used

Parameters

modelcheckingResult

the result struct containing the scheduler

Returns

the scheduler represented by a Markov chain.

Definition at line 104 of file verification.h.

getCutoffScheduler()

template<typename ValueType >

storm::storage::Scheduler< ValueType > storm::pomdp::api::getCutoffScheduler	(	typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result	modelcheckingResult,
		uint64_t	schedId
	)

Get a specific scheduler used to generate cut-off values from the result struct.

Template Parameters

ValueType

number type to be used

Parameters

modelcheckingResult	the result struct
schedId	the ID of the scheduler used during the exploration. This corresponds to the labels in the scheduler MC.

Returns

the desired scheduler

Definition at line 117 of file verification.h.

getNumberOfPreprocessingSchedulers()

template<typename ValueType >

uint64_t storm::pomdp::api::getNumberOfPreprocessingSchedulers

(

typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result

modelcheckingResult

)

Get the overall number of schedulers generated by the pre-processing for the under-approximation from the result struct.

Template Parameters

ValueType

number type to be used

Parameters

modelcheckingResult

the result struct

Returns

the number of schedulers

Definition at line 130 of file verification.h.

startInteractiveExploration()

template<typename ValueType >

void storm::pomdp::api::startInteractiveExploration	(	storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > > &	modelchecker,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task,
		std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > >	additionalPomdpStateValues = std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>>()
	)

Start an interactive unfolding to under approximate the given objective.

Template Parameters

ValueType

number type to be used

Parameters

modelchecker	the model checker object configured for the interactive unfolding
task	the check task to be performed
additionalPomdpStateValues	additional values that can be used for cut-offs in the under-approximation (generated by finite memory schedulers). Each element of the outer vector represents a scheduler. Each scheduler itself is represented by a vector of maps representing (memory node x state) -> value

Definition at line 90 of file verification.h.

underapproximateWithCutoffs()

template<typename ValueType >

storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result storm::pomdp::api::underapproximateWithCutoffs	(	std::shared_ptr< storm::models::sparse::Pomdp< ValueType > >	pomdp,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task,
		uint64_t	sizeThreshold,
		std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > >	additionalPomdpStateValues = std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>>()
	)

Uses the belief exploration with cut-offs to under-approximate the given objective on a POMDP.

Template Parameters

ValueType

number type to be used

Parameters

pomdp	the input pomdp to be checked
task	the check task to be performed
sizeThreshold	number of states up to which the belief MDP should be unfolded
pomdpStateValues	additional values that can be used for cut-offs in the under-approximation (generated by finite memory schedulers). Each element of the outer vector represents a scheduler. Each scheduler itself is represented by a vector of maps representing (memory node x state) -> value

Returns

the result structure

Definition at line 19 of file verification.h.

underapproximateWithoutHeuristicValues()

template<typename ValueType >

storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker< storm::models::sparse::Pomdp< ValueType > >::Result storm::pomdp::api::underapproximateWithoutHeuristicValues	(	std::shared_ptr< storm::models::sparse::Pomdp< ValueType > >	pomdp,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task,
		uint64_t	sizeThreshold,
		std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > >	pomdpStateValues
	)

Uses the belief exploration with cut-offs without the pre-processing to generate cut-off values to under-approximate the given objective on a POMDP.

Cut-off values need to be provided in the form of a vector of vectors representing finite memory schedulers.

Template Parameters

ValueType

number type to be used

Parameters

pomdp	the input pomdp to be checked
task	the check task to be performed
sizeThreshold	number of states up to which the belief MDP should be unfolded
pomdpStateValues	additional values that can be used for cut-offs in the under-approximation (generated by finite memory schedulers). Each element of the outer vector represents a scheduler. Each scheduler itself is represented by a vector of maps representing (memory node x state) -> value

Returns

the result structure

Definition at line 44 of file verification.h.