verification.h File Reference

#include "storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.h"
#include "storm/environment/Environment.h"

Include dependency graph for verification.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces
namespace	storm
	LabParser.cpp.
namespace	storm::pomdp
namespace	storm::pomdp::api

Functions
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<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.
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.
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<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.
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<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.