Namespaces
namespace	detail

Classes
class	ClippingBeliefAbstraction
	Approximates a belief by clipping it to an observation-specific grid point. More...
class	FreudenthalTriangulationBeliefAbstraction
	Abstracts a belief by triangulating it using the Freudenthal triangulation. More...
struct	NoAbstractionType
	Auxiliary struct used to identify cases where no abstraction of beliefs shall be applied. More...
class	RewardBoundedBeliefSplitter
	Abstracts a given belief by splitting it into sub-beliefs based on the (state-action) reward of the POMDP. More...
struct	StandardDiscoverCallback
	Stores ordinary successor transitions in exploration information. More...
struct	ClippingDiscoverCallback
	Stores successor transitions together with clipping metadata. More...
struct	RewardAwareDiscoverCallback
	Stores reward-aware successor transitions and their reward vectors. More...
class	BeliefExploration
	Class to perform belief exploration. More...
struct	BeliefExplorationTransition
	A successor entry recorded while exploring one action of a belief. More...
struct	BeliefExplorationTransition< ValueType, ExtraTransitionData >
struct	BeliefExplorationTransition< ValueType, FirstExtraTransitionData, OtherExtraTransitionData... >
class	BeliefExplorationMatrix
	Sparse transition data for the explored part of a belief MDP. More...
struct	ExplorationInformation
	Mutable state of one belief-MDP exploration. More...
class	ExplorationQueue
class	FirstStateNextStateGenerator
	This class implements a first-state-next-state generator interface for exploring the belief MDP of a given POMDP. More...
class	BeliefBuilder
	Constructs a belief. More...
class	Belief
	Represents a belief of a Pomdp, i.e. More...
class	BeliefCollector
	Interns beliefs and assigns them consecutive identifiers. More...
struct	BeliefNumerics
	Numeric predicates used when comparing and hashing beliefs. More...
class	BeliefBasedModelChecker
	Builds and checks a finite belief MDP approximation of a POMDP. More...
struct	BeliefBasedModelCheckerOptions
struct	BeliefBasedModelCheckerStatistics
	Statistics recorded during a belief-based model-checking run. More...
struct	BeliefBasedModelCheckerResult
	Result of a belief-based model-checking run. More...
struct	RewardBound
	One reward dimension of a reward-bounded reachability property. More...
struct	PropertyInformation
	Property data consumed by the belief MDP construction. More...

Typedefs
template<typename BeliefMdpValueType, typename BeliefType>
using	StandardExplorationInformation = ExplorationInformation<BeliefMdpValueType, BeliefType>
	Exploration information without transition metadata.
template<typename BeliefMdpValueType, typename BeliefType>
using	RewardAwareExplorationInformation = ExplorationInformation<BeliefMdpValueType, BeliefType, std::vector<BeliefMdpValueType>>
	Exploration information that stores a reward vector on each transition.
template<typename BeliefMdpValueType, typename BeliefType>
using	ClippingExplorationInformation
	Exploration information that stores optional clipping probability and reward-adjustment metadata.
using	BeliefStateType = uint64_t
	Shared identifiers and sparse-container types used by the belief subsystem.
using	BeliefObservationType = uint32_t
using	BeliefId = uint64_t
using	BeliefActionObservationType = uint32_t
template<typename BeliefValueType>
using	BeliefFlatMap = boost::container::flat_map<BeliefStateType, BeliefValueType>

Enumerations
enum class	FreudenthalTriangulationMode { Static , Dynamic }
	Selects a fixed grid resolution or a suitable coarser resolution per belief. More...
enum class	ExplorationQueueOrder { Unordered , FIFO , LIFO }
	Order used to select the next discovered belief for exploration. More...
enum	explorationTerminationCriterion { MAX_EXPLORATION_SIZE , MAX_EXPLORATION_TIME , MAX_EXPLORATION_SIZE_AND_TIME , NONE }
	Criterion that ends exploration and leaves the queued beliefs as the explicit frontier. More...

Functions
std::shared_ptr< storm::logic::Formula const >	createFormulaForBeliefMdp (PropertyInformation const &propertyInformation)
template<typename MatrixType>
bool	hasUniqueTransitionRewardsInChoice (MatrixType const &matrix, uint64_t choice, uint64_t numRewardModels)
template<typename BeliefMdpValueType, typename BeliefType, typename... ExtraTransitionData>
std::pair< std::shared_ptr< models::sparse::Mdp< BeliefMdpValueType > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (ExplorationInformation< BeliefMdpValueType, BeliefType, ExtraTransitionData... > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, BeliefMdpValueType >(BeliefType const &)> const &computeCutOffValueMap)
	Builds a belief MDP from the given exploration information and property information.
template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (ExplorationInformation< double, Belief< double > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, double >(Belief< double > const &)> const &computeCutOffValueMap)
template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (ExplorationInformation< storm::RationalNumber, Belief< double > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< double > const &)> const &computeCutOffValueMap)
template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (ExplorationInformation< double, Belief< storm::RationalNumber > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, double >(Belief< storm::RationalNumber > const &)> const &computeCutOffValueMap)
template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (ExplorationInformation< storm::RationalNumber, Belief< storm::RationalNumber > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< storm::RationalNumber > const &)> const &computeCutOffValueMap)
template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (ClippingExplorationInformation< double, Belief< double > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, double >(Belief< double > const &)> const &computeCutOffValueMap)
template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (ClippingExplorationInformation< storm::RationalNumber, Belief< double > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< double > const &)> const &computeCutOffValueMap)
template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (ClippingExplorationInformation< double, Belief< storm::RationalNumber > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, double >(Belief< storm::RationalNumber > const &)> const &computeCutOffValueMap)
template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (ClippingExplorationInformation< storm::RationalNumber, Belief< storm::RationalNumber > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< storm::RationalNumber > const &)> const &computeCutOffValueMap)
template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (RewardAwareExplorationInformation< double, Belief< double > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, double >(Belief< double > const &)> const &computeCutOffValueMap)
template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (RewardAwareExplorationInformation< storm::RationalNumber, Belief< double > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< double > const &)> const &computeCutOffValueMap)
template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (RewardAwareExplorationInformation< double, Belief< storm::RationalNumber > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, double >(Belief< storm::RationalNumber > const &)> const &computeCutOffValueMap)
template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > >	buildBeliefMdp (RewardAwareExplorationInformation< storm::RationalNumber, Belief< storm::RationalNumber > > const &explorationInformation, PropertyInformation const &propertyInformation, std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< storm::RationalNumber > const &)> const &computeCutOffValueMap)
void	validateRewardModelSelection (PropertyInformation const &propertyInformation, std::vector< std::string > const &rewardModelNames)
template<typename PomdpModelType, typename BeliefType, typename BeliefMdpValueType, typename InfoType>
BeliefExploration< BeliefMdpValueType, PomdpModelType, BeliefType >::TerminationCallback	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	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 > >	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 >	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 >	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={})

Variables
constexpr NoAbstractionType	NoAbstraction {0}
template<class A>
constexpr bool	isNoAbstraction = std::is_same_v<std::remove_cv_t<A>, NoAbstractionType>
constexpr BeliefActionObservationType	DefaultActionObservation = 0
constexpr bool	BeliefFlatMapIsOrdered = true
constexpr BeliefObservationType	InvalidObservation = std::numeric_limits<BeliefObservationType>::max()
	Required e.g. for comparing two beliefs.
constexpr BeliefId	InvalidBeliefId = std::numeric_limits<BeliefId>::max()

Typedef Documentation

◆ BeliefActionObservationType

using storm::pomdp::beliefs::BeliefActionObservationType = uint32_t

Definition at line 13 of file types.h.

◆ BeliefFlatMap

template<typename BeliefValueType>

using storm::pomdp::beliefs::BeliefFlatMap = boost::container::flat_map<BeliefStateType, BeliefValueType>

Definition at line 17 of file types.h.

◆ BeliefId

using storm::pomdp::beliefs::BeliefId = uint64_t

Definition at line 12 of file types.h.

◆ BeliefObservationType

using storm::pomdp::beliefs::BeliefObservationType = uint32_t

Definition at line 11 of file types.h.

◆ BeliefStateType

using storm::pomdp::beliefs::BeliefStateType = uint64_t

Shared identifiers and sparse-container types used by the belief subsystem.

Definition at line 10 of file types.h.

◆ ClippingExplorationInformation

template<typename BeliefMdpValueType, typename BeliefType>

using storm::pomdp::beliefs::ClippingExplorationInformation

Initial value:

ExplorationInformation<BeliefMdpValueType, BeliefType, std::optional<BeliefMdpValueType>, std::optional<BeliefMdpValueType>>

storm::pomdp::beliefs::ExplorationInformation

Mutable state of one belief-MDP exploration.

Definition ExplorationInformation.h:21

Exploration information that stores optional clipping probability and reward-adjustment metadata.

Definition at line 54 of file ExplorationInformation.h.

◆ RewardAwareExplorationInformation

template<typename BeliefMdpValueType, typename BeliefType>

using storm::pomdp::beliefs::RewardAwareExplorationInformation = ExplorationInformation<BeliefMdpValueType, BeliefType, std::vector<BeliefMdpValueType>>

Exploration information that stores a reward vector on each transition.

Definition at line 50 of file ExplorationInformation.h.

◆ StandardExplorationInformation

template<typename BeliefMdpValueType, typename BeliefType>

using storm::pomdp::beliefs::StandardExplorationInformation = ExplorationInformation<BeliefMdpValueType, BeliefType>

Exploration information without transition metadata.

Definition at line 46 of file ExplorationInformation.h.

Enumeration Type Documentation

◆ ExplorationQueueOrder

enum class storm::pomdp::beliefs::ExplorationQueueOrder

strong

Order used to select the next discovered belief for exploration.

Enumerator
Unordered
FIFO
LIFO

Definition at line 4 of file ExplorationQueueOrder.h.

◆ explorationTerminationCriterion

enum storm::pomdp::beliefs::explorationTerminationCriterion

Criterion that ends exploration and leaves the queued beliefs as the explicit frontier.

Enumerator
MAX_EXPLORATION_SIZE
MAX_EXPLORATION_TIME
MAX_EXPLORATION_SIZE_AND_TIME
NONE

Definition at line 11 of file BeliefBasedModelCheckerOptions.h.

◆ FreudenthalTriangulationMode

enum class storm::pomdp::beliefs::FreudenthalTriangulationMode

strong

Selects a fixed grid resolution or a suitable coarser resolution per belief.

Enumerator
Static
Dynamic

Definition at line 13 of file FreudenthalTriangulationBeliefAbstraction.h.

Function Documentation

◆ buildBeliefMdp() [1/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	ClippingExplorationInformation< double, Belief< double > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, double >(Belief< double > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdp() [2/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	ClippingExplorationInformation< double, Belief< storm::RationalNumber > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, double >(Belief< storm::RationalNumber > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdp() [3/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	ClippingExplorationInformation< storm::RationalNumber, Belief< double > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< double > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdp() [4/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	ClippingExplorationInformation< storm::RationalNumber, Belief< storm::RationalNumber > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< storm::RationalNumber > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdp() [5/13]

template<typename BeliefMdpValueType, typename BeliefType, typename... ExtraTransitionData>

std::pair< std::shared_ptr< models::sparse::Mdp< BeliefMdpValueType > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	ExplorationInformation< BeliefMdpValueType, BeliefType, ExtraTransitionData... > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, BeliefMdpValueType >(BeliefType const &)> const &	computeCutOffValueMap )

Builds a belief MDP from the given exploration information and property information.

Frontier beliefs receive explicit cut-off choices from computeCutOffValueMap.

The reward-aware belief exploration does not classify beliefs as terminal. A target observation alone does not decide whether the accumulated rewards satisfy the bound, in particular when there are lower bounds. Such beliefs therefore remain explored or frontier states; their transition reward vectors are retained on their ordinary edges. For reward-bounded minimisation, the cut-off target earns one reward per self-loop in each lower-bounded dimension and zero in upper-only dimensions, providing an optimistic continuation. Dimensions with both lower and upper reward bounds are not supported for minimisation, even when exploration completes.

Template Parameters

BeliefMdpValueType	ValueType of the belief MDP
BeliefType	Type of the belief
ExtraTransitionData	Types of additional data to store for transitions (e.g. reward vectors)

Parameters

explorationInformation	object containing information about the exploration of the belief space (explored beliefs, transitions, etc.)
propertyInformation	object containing information about the property to verify
computeCutOffValueMap	function to compute all cut-off values for a belief given the provided information. A separate cut-off action is added for each value, allowing the model checker to choose the best one. This choice can later be retraced.

Exceptions

storm::exceptions::NotSupportedException if reward-bounded minimisation has a dimension with both lower and upper reward bounds

Returns: the belief MDP and a mapping from represented belief states to their belief IDs; synthetic target and bottom sinks are omitted from the mapping

Definition at line 96 of file BeliefMdpBuilder.cpp.

◆ buildBeliefMdp() [6/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	ExplorationInformation< double, Belief< double > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, double >(Belief< double > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdp() [7/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	ExplorationInformation< double, Belief< storm::RationalNumber > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, double >(Belief< storm::RationalNumber > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdp() [8/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	ExplorationInformation< storm::RationalNumber, Belief< double > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< double > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdp() [9/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	ExplorationInformation< storm::RationalNumber, Belief< storm::RationalNumber > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< storm::RationalNumber > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdp() [10/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	RewardAwareExplorationInformation< double, Belief< double > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, double >(Belief< double > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdp() [11/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< double > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	RewardAwareExplorationInformation< double, Belief< storm::RationalNumber > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, double >(Belief< storm::RationalNumber > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdp() [12/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	RewardAwareExplorationInformation< storm::RationalNumber, Belief< double > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< double > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdp() [13/13]

template std::pair< std::shared_ptr< models::sparse::Mdp< storm::RationalNumber > >, std::unordered_map< uint64_t, BeliefId > > storm::pomdp::beliefs::buildBeliefMdp	(	RewardAwareExplorationInformation< storm::RationalNumber, Belief< storm::RationalNumber > > const &	explorationInformation,
		PropertyInformation const &	propertyInformation,
		std::function< std::unordered_map< std::string, storm::RationalNumber >(Belief< storm::RationalNumber > const &)> const &	computeCutOffValueMap )

◆ buildBeliefMdpFromInfo()

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.

Every frontier belief becomes an explicit state with one selectable cut-off action per preprocessing bound.

Definition at line 169 of file BeliefBasedModelChecker.cpp.

◆ checkRewardAwareUnfoldOrDiscretize()

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 = {} )

Definition at line 297 of file BeliefBasedModelChecker.cpp.

◆ checkUnfoldOrDiscretize()

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 = {} )

Definition at line 195 of file BeliefBasedModelChecker.cpp.

◆ createFormulaForBeliefMdp()

std::shared_ptr< storm::logic::Formula const > storm::pomdp::beliefs::createFormulaForBeliefMdp ( PropertyInformation const & propertyInformation )

Definition at line 22 of file BeliefMdpBuilder.cpp.

◆ getTerminalBeliefCallback()

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.

Terminal beliefs receive their fixed value directly; all other unfinished beliefs remain explicit frontier states.

Definition at line 81 of file BeliefBasedModelChecker.cpp.

◆ getTerminationCallback()

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.

Definition at line 55 of file BeliefBasedModelChecker.cpp.

◆ hasUniqueTransitionRewardsInChoice()

template<typename MatrixType>

bool storm::pomdp::beliefs::hasUniqueTransitionRewardsInChoice	(	MatrixType const &	matrix,
		uint64_t	choice,
		uint64_t	numRewardModels )

Definition at line 76 of file BeliefMdpBuilder.cpp.

◆ validateRewardModelSelection()

void storm::pomdp::beliefs::validateRewardModelSelection	(	PropertyInformation const &	propertyInformation,
		std::vector< std::string > const &	rewardModelNames )

Definition at line 27 of file BeliefBasedModelChecker.cpp.

Variable Documentation

◆ BeliefFlatMapIsOrdered

bool storm::pomdp::beliefs::BeliefFlatMapIsOrdered = true

constexpr

Definition at line 18 of file types.h.

◆ DefaultActionObservation

BeliefActionObservationType storm::pomdp::beliefs::DefaultActionObservation = 0

constexpr

Definition at line 14 of file types.h.

◆ InvalidBeliefId

BeliefId storm::pomdp::beliefs::InvalidBeliefId = std::numeric_limits<BeliefId>::max()

constexpr

Definition at line 21 of file types.h.

◆ InvalidObservation

BeliefObservationType storm::pomdp::beliefs::InvalidObservation = std::numeric_limits<BeliefObservationType>::max()

constexpr

Required e.g. for comparing two beliefs.

Definition at line 20 of file types.h.

◆ isNoAbstraction

template<class A>

bool storm::pomdp::beliefs::isNoAbstraction = std::is_same_v<std::remove_cv_t<A>, NoAbstractionType>

inlineconstexpr

Definition at line 17 of file NoAbstraction.h.

◆ NoAbstraction

NoAbstractionType storm::pomdp::beliefs::NoAbstraction {0}

inlineconstexpr

Definition at line 14 of file NoAbstraction.h.

Namespaces

Classes

Typedefs

Enumerations

Functions

Variables

Typedef Documentation

◆ BeliefActionObservationType

◆ BeliefFlatMap

◆ BeliefId

◆ BeliefObservationType

◆ BeliefStateType

◆ ClippingExplorationInformation

◆ RewardAwareExplorationInformation

◆ StandardExplorationInformation

Enumeration Type Documentation

◆ ExplorationQueueOrder

◆ explorationTerminationCriterion

◆ FreudenthalTriangulationMode

Function Documentation

◆ buildBeliefMdp() [1/13]

◆ buildBeliefMdp() [2/13]

◆ buildBeliefMdp() [3/13]

◆ buildBeliefMdp() [4/13]

◆ buildBeliefMdp() [5/13]

◆ buildBeliefMdp() [6/13]

◆ buildBeliefMdp() [7/13]

◆ buildBeliefMdp() [8/13]

◆ buildBeliefMdp() [9/13]

◆ buildBeliefMdp() [10/13]

◆ buildBeliefMdp() [11/13]

◆ buildBeliefMdp() [12/13]

◆ buildBeliefMdp() [13/13]

◆ buildBeliefMdpFromInfo()

◆ checkRewardAwareUnfoldOrDiscretize()

◆ checkUnfoldOrDiscretize()

◆ createFormulaForBeliefMdp()

◆ getTerminalBeliefCallback()

◆ getTerminationCallback()

◆ hasUniqueTransitionRewardsInChoice()

◆ validateRewardModelSelection()

Variable Documentation

◆ BeliefFlatMapIsOrdered

◆ DefaultActionObservation

◆ InvalidBeliefId

◆ InvalidObservation

◆ isNoAbstraction

◆ NoAbstraction