BeliefBasedModelChecker.cpp File Reference

#include "storm-pomdp/beliefs/verification/BeliefBasedModelChecker.h"
#include "storm-pomdp/beliefs/abstraction/ClippingBeliefAbstraction.h"
#include "storm-pomdp/beliefs/abstraction/FreudenthalTriangulationBeliefAbstraction.h"
#include "storm-pomdp/beliefs/abstraction/RewardBoundedBeliefSplitter.h"
#include "storm-pomdp/beliefs/exploration/BeliefExploration.h"
#include "storm-pomdp/beliefs/exploration/BeliefMdpBuilder.h"
#include "storm-pomdp/beliefs/storage/Belief.h"
#include "storm-pomdp/beliefs/verification/BeliefBasedModelCheckerOptions.h"
#include "storm/api/verification.h"
#include "storm/exceptions/IllegalArgumentException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/models/sparse/Pomdp.h"
#include "storm/transformer/GoalStateMerger.h"
#include "storm/transformer/TransitionToActionRewardTransformer.h"
#include "storm/utility/OptionalRef.h"
#include "storm/utility/Stopwatch.h"
#include "storm/utility/constants.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include <sstream>

Include dependency graph for BeliefBasedModelChecker.cpp:

Go to the source code of this file.

Namespaces
namespace	storm
namespace	storm::pomdp
namespace	storm::pomdp::beliefs

Functions
void	storm::pomdp::beliefs::validateRewardModelSelection (PropertyInformation const &propertyInformation, std::vector< std::string > const &rewardModelNames)
template<typename PomdpModelType, typename BeliefType, typename BeliefMdpValueType, typename InfoType>
BeliefExploration< BeliefMdpValueType, PomdpModelType, BeliefType >::TerminationCallback	storm::pomdp::beliefs::getTerminationCallback (storm::pomdp::beliefs::BeliefBasedModelCheckerOptions< BeliefMdpValueType > const &options, InfoType &info, storm::utility::Stopwatch &swExplore)
	Creates the callback that ends exploration and turns the queued beliefs into the frontier.
template<typename PomdpModelType, typename BeliefType, typename BeliefMdpValueType>
BeliefExploration< BeliefMdpValueType, PomdpModelType, BeliefType >::TerminalBeliefCallback	storm::pomdp::beliefs::getTerminalBeliefCallback (PropertyInformation const &propertyInformation, storm::pomdp::beliefs::BeliefBasedModelCheckerOptions< BeliefMdpValueType > const &options, storm::pomdp::storage::PreprocessingPomdpValueBounds< typename PomdpModelType::ValueType > const &valueBounds)
	Creates a callback that recognizes property targets and optional zero-gap cut-offs as terminal beliefs.
template<typename PomdpModelType, typename BeliefType, typename BeliefMdpValueType, typename InfoType>
std::pair< std::shared_ptr< models::sparse::Mdp< BeliefMdpValueType > >, std::unordered_map< uint64_t, BeliefId > >	storm::pomdp::beliefs::buildBeliefMdpFromInfo (PropertyInformation const &propertyInformation, storm::pomdp::storage::PreprocessingPomdpValueBounds< typename PomdpModelType::ValueType > const &valueBounds, InfoType const &info)
	Converts exploration information into a finite MDP.
template<typename PomdpModelType, typename BeliefType, typename BeliefMdpValueType, typename AbstractionType, typename InfoType = StandardExplorationInformation<BeliefMdpValueType, BeliefType>>
BeliefBasedModelCheckerResult< BeliefMdpValueType >	storm::pomdp::beliefs::checkUnfoldOrDiscretize (storm::Environment const &env, PomdpModelType const &pomdp, PropertyInformation const &propertyInformation, storm::pomdp::beliefs::BeliefBasedModelCheckerOptions< BeliefMdpValueType > const &options, storage::BeliefExplorationBounds< typename PomdpModelType::ValueType > const &valueBounds, storm::OptionalRef< AbstractionType > abstraction={})
template<typename PomdpModelType, typename BeliefType, typename BeliefMdpValueType>
BeliefBasedModelCheckerResult< BeliefMdpValueType >	storm::pomdp::beliefs::checkRewardAwareUnfoldOrDiscretize (storm::Environment const &env, PomdpModelType const &pomdp, PropertyInformation const &propertyInformation, storm::pomdp::beliefs::BeliefBasedModelCheckerOptions< BeliefMdpValueType > const &options, storage::BeliefExplorationBounds< typename PomdpModelType::ValueType > const &valueBounds, RewardBoundedBeliefSplitter< BeliefMdpValueType, PomdpModelType, BeliefType > &rewardSplitter, storm::OptionalRef< FreudenthalTriangulationBeliefAbstraction< BeliefType > > abstraction={})