RewardBoundUnfolder.cpp File Reference

#include "storm-pomdp/transformer/RewardBoundUnfolder.h"
#include <limits>
#include <queue>
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/logic/AtomicLabelFormula.h"
#include "storm/logic/BinaryBooleanStateFormula.h"
#include "storm/logic/BoundedUntilFormula.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/logic/ProbabilityOperatorFormula.h"
#include "storm/logic/UntilFormula.h"
#include "storm/models/sparse/Pomdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/utility/builder.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/NotSupportedException.h"

Include dependency graph for RewardBoundUnfolder.cpp:

Go to the source code of this file.

Classes
struct	storm::pomdp::transformer::detail::Dimension< ValueType >
	Contains information for a single dimension of the unfolding. More...
struct	storm::pomdp::transformer::detail::StateEpochCollector
struct	storm::pomdp::transformer::detail::ExplorationResult< ValueType >

Namespaces
namespace	storm
namespace	storm::pomdp
namespace	storm::pomdp::transformer
namespace	storm::pomdp::transformer::detail

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

Functions
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.
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.
int64_t	storm::pomdp::transformer::detail::mod (int64_t a, int64_t b)
	Helper function to compute the modulos.
template<typename ValueType>
EpochType	storm::pomdp::transformer::detail::computeInitialEpoch (std::vector< Dimension< ValueType > > const &dimensions)
template<typename ValueType>
EpochType	storm::pomdp::transformer::detail::computeSuccessorEpoch (StateIdType currentState, EpochType const &currentEpoch, ChoiceIdType choice, std::vector< Dimension< ValueType > > const &dimensions)
template<typename ValueType, typename LevelRewardSetterType>
void	storm::pomdp::transformer::detail::computeLevelReward (EpochType const &successorEpoch, std::vector< Dimension< ValueType > > const &dimensions, LevelRewardSetterType const &setLevelReward)
template<typename ValueType>
void	storm::pomdp::transformer::detail::applyEpochAbstraction (EpochType &epoch, std::vector< Dimension< ValueType > > const &dimensions)
template<typename ValueType, typename ActiveDimensionSetterType>
void	storm::pomdp::transformer::detail::computeActiveDimensions (EpochType const &epoch, std::vector< Dimension< ValueType > > const &dimensions, ActiveDimensionSetterType const &setActiveDimension)
template<typename ValueType>
ExplorationResult< ValueType >	storm::pomdp::transformer::detail::exploreUnfolding (storm::models::sparse::Model< ValueType > const &model, std::vector< Dimension< ValueType > > const &dimensions)
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)
template<typename ValueType>
std::shared_ptr< storm::logic::Formula >	storm::pomdp::transformer::detail::constructFormula (storm::logic::BoundedUntilFormula boundedUntilFormula, std::vector< Dimension< ValueType > > const &dimensions)