storm::pomdp::transformer::detail Namespace Reference

Classes
struct	Dimension
	Contains information for a single dimension of the unfolding. More...
struct	StateEpochCollector
struct	ExplorationResult

Typedefs
using	StateIdType = uint64_t
using	ChoiceIdType = uint64_t
using	EpochType = std::vector<int64_t>
using	StateEpochPair = std::pair<StateIdType, EpochType>

Functions
template<typename ValueType>
bool	rewardsFitInt64 (storm::models::sparse::Model< ValueType > const &model, storm::models::sparse::StandardRewardModel< ValueType > const &rewardModel)
	Checks whether all individual and combined rewards fit into int64_t, assuming nonnegative integer rewards.
template<typename ValueType>
std::vector< Dimension< ValueType > >	extractDimensions (storm::models::sparse::Model< ValueType > const &model, storm::logic::BoundedUntilFormula const &boundedUntilFormula, std::vector< uint64_t > const &levelWidths)
	Extracts the dimension information from the input formula.
int64_t	mod (int64_t a, int64_t b)
	Helper function to compute the modulos.
template<typename ValueType>
EpochType	computeInitialEpoch (std::vector< Dimension< ValueType > > const &dimensions)
template<typename ValueType>
EpochType	computeSuccessorEpoch (StateIdType currentState, EpochType const &currentEpoch, ChoiceIdType choice, std::vector< Dimension< ValueType > > const &dimensions)
template<typename ValueType, typename LevelRewardSetterType>
void	computeLevelReward (EpochType const &successorEpoch, std::vector< Dimension< ValueType > > const &dimensions, LevelRewardSetterType const &setLevelReward)
template<typename ValueType>
void	applyEpochAbstraction (EpochType &epoch, std::vector< Dimension< ValueType > > const &dimensions)
template<typename ValueType, typename ActiveDimensionSetterType>
void	computeActiveDimensions (EpochType const &epoch, std::vector< Dimension< ValueType > > const &dimensions, ActiveDimensionSetterType const &setActiveDimension)
template<typename ValueType>
ExplorationResult< ValueType >	exploreUnfolding (storm::models::sparse::Model< ValueType > const &model, std::vector< Dimension< ValueType > > const &dimensions)
template<typename ValueType>
storm::storage::sparse::ModelComponents< ValueType >	constructComponents (storm::models::sparse::Model< ValueType > const &originalModel, std::vector< Dimension< ValueType > > const &dimensions, std::set< std::string > const &preservedRewardModels, ExplorationResult< ValueType > &&explorationResult)
template<typename ValueType>
std::shared_ptr< storm::logic::Formula >	constructFormula (storm::logic::BoundedUntilFormula boundedUntilFormula, std::vector< Dimension< ValueType > > const &dimensions)

Typedef Documentation

ChoiceIdType

using storm::pomdp::transformer::detail::ChoiceIdType = uint64_t

Definition at line 28 of file RewardBoundUnfolder.cpp.

EpochType

using storm::pomdp::transformer::detail::EpochType = std::vector<int64_t>

Definition at line 29 of file RewardBoundUnfolder.cpp.

StateEpochPair

using storm::pomdp::transformer::detail::StateEpochPair = std::pair<StateIdType, EpochType>

Definition at line 30 of file RewardBoundUnfolder.cpp.

StateIdType

using storm::pomdp::transformer::detail::StateIdType = uint64_t

Definition at line 27 of file RewardBoundUnfolder.cpp.

Function Documentation

applyEpochAbstraction()

template<typename ValueType>

void storm::pomdp::transformer::detail::applyEpochAbstraction	(	EpochType &	epoch,
		std::vector< Dimension< ValueType > > const &	dimensions )

Definition at line 213 of file RewardBoundUnfolder.cpp.

computeActiveDimensions()

template<typename ValueType, typename ActiveDimensionSetterType>

void storm::pomdp::transformer::detail::computeActiveDimensions	(	EpochType const &	epoch,
		std::vector< Dimension< ValueType > > const &	dimensions,
		ActiveDimensionSetterType const &	setActiveDimension )

Definition at line 232 of file RewardBoundUnfolder.cpp.

computeInitialEpoch()

template<typename ValueType>

EpochType storm::pomdp::transformer::detail::computeInitialEpoch

(

std::vector< Dimension< ValueType > > const &

dimensions

)

Definition at line 166 of file RewardBoundUnfolder.cpp.

computeLevelReward()

template<typename ValueType, typename LevelRewardSetterType>

void storm::pomdp::transformer::detail::computeLevelReward	(	EpochType const &	successorEpoch,
		std::vector< Dimension< ValueType > > const &	dimensions,
		LevelRewardSetterType const &	setLevelReward )

Definition at line 197 of file RewardBoundUnfolder.cpp.

computeSuccessorEpoch()

template<typename ValueType>

EpochType storm::pomdp::transformer::detail::computeSuccessorEpoch	(	StateIdType	currentState,
		EpochType const &	currentEpoch,
		ChoiceIdType	choice,
		std::vector< Dimension< ValueType > > const &	dimensions )

Definition at line 180 of file RewardBoundUnfolder.cpp.

constructComponents()

template<typename ValueType>

storm::storage::sparse::ModelComponents< ValueType > storm::pomdp::transformer::detail::constructComponents	(	storm::models::sparse::Model< ValueType > const &	originalModel,
		std::vector< Dimension< ValueType > > const &	dimensions,
		std::set< std::string > const &	preservedRewardModels,
		ExplorationResult< ValueType > &&	explorationResult )

Definition at line 345 of file RewardBoundUnfolder.cpp.

constructFormula()

template<typename ValueType>

std::shared_ptr< storm::logic::Formula > storm::pomdp::transformer::detail::constructFormula	(	storm::logic::BoundedUntilFormula	boundedUntilFormula,
		std::vector< Dimension< ValueType > > const &	dimensions )

Definition at line 463 of file RewardBoundUnfolder.cpp.

exploreUnfolding()

template<typename ValueType>

ExplorationResult< ValueType > storm::pomdp::transformer::detail::exploreUnfolding	(	storm::models::sparse::Model< ValueType > const &	model,
		std::vector< Dimension< ValueType > > const &	dimensions )

Definition at line 266 of file RewardBoundUnfolder.cpp.

extractDimensions()

template<typename ValueType>

std::vector< Dimension< ValueType > > storm::pomdp::transformer::detail::extractDimensions	(	storm::models::sparse::Model< ValueType > const &	model,
		storm::logic::BoundedUntilFormula const &	boundedUntilFormula,
		std::vector< uint64_t > const &	levelWidths )

Extracts the dimension information from the input formula.

Also performs various sanity/compatibility checks.

Definition at line 79 of file RewardBoundUnfolder.cpp.

mod()

int64_t storm::pomdp::transformer::detail::mod	(	int64_t	a,
		int64_t	b )

Helper function to compute the modulos.

Note

operator% is not the modulos for negative numerators. E.g. -1 % 3 = -1, but mod(-1, 3) = 2

Definition at line 160 of file RewardBoundUnfolder.cpp.

rewardsFitInt64()

template<typename ValueType>

bool storm::pomdp::transformer::detail::rewardsFitInt64	(	storm::models::sparse::Model< ValueType > const &	model,
		storm::models::sparse::StandardRewardModel< ValueType > const &	rewardModel )

Checks whether all individual and combined rewards fit into int64_t, assuming nonnegative integer rewards.

Definition at line 49 of file RewardBoundUnfolder.cpp.