Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Classes | Public Types | Public Member Functions | List of all members
storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType > Class Template Reference

#include <BeliefMdpExplorer.h>

Classes

struct  SuccessorObservationInformation
 

Public Types

enum class  Status { Uninitialized , Exploring , ModelFinished , ModelChecked }
 
typedef PomdpType::ValueType ValueType
 
typedef storm::storage::BeliefManager< PomdpType, BeliefValueType > BeliefManagerType
 
typedef BeliefManagerType::BeliefId BeliefId
 
typedef uint64_t MdpStateType
 

Public Member Functions

 BeliefMdpExplorer (std::shared_ptr< BeliefManagerType > beliefManager, storm::pomdp::storage::PreprocessingPomdpValueBounds< ValueType > const &pomdpValueBounds, ExplorationHeuristic explorationHeuristic=ExplorationHeuristic::BreadthFirst)
 
 BeliefMdpExplorer (BeliefMdpExplorer &&other)=default
 
BeliefManagerType const & getBeliefManager () const
 
void startNewExploration (std::optional< ValueType > extraTargetStateValue=boost::none, std::optional< ValueType > extraBottomStateValue=std::nullopt)
 
void restartExploration ()
 Restarts the exploration to allow re-exploring each state.
 
bool hasUnexploredState () const
 
std::vector< uint64_t > getUnexploredStates ()
 
BeliefId exploreNextState ()
 
void addChoiceLabelToCurrentState (uint64_t const &localActionIndex, std::string const &label)
 
void addTransitionsToExtraStates (uint64_t const &localActionIndex, ValueType const &targetStateValue=storm::utility::zero< ValueType >(), ValueType const &bottomStateValue=storm::utility::zero< ValueType >())
 
void addSelfloopTransition (uint64_t const &localActionIndex=0, ValueType const &value=storm::utility::one< ValueType >())
 
bool addTransitionToBelief (uint64_t const &localActionIndex, BeliefId const &transitionTarget, ValueType const &value, bool ignoreNewBeliefs)
 Adds the next transition to the given successor belief.
 
void computeRewardAtCurrentState (uint64_t const &localActionIndex, ValueType extraReward=storm::utility::zero< ValueType >())
 
void addRewardToCurrentState (uint64_t const &localActionIndex, ValueType rewardValue)
 Adds the provided reward value to the given action of the current state.
 
void setCurrentStateIsTarget ()
 
void setCurrentStateIsTruncated ()
 
void setCurrentStateIsClipped ()
 
void setCurrentChoiceIsDelayed (uint64_t const &localActionIndex)
 
bool currentStateHasOldBehavior () const
 
bool getCurrentStateWasTruncated () const
 
bool getCurrentStateWasClipped () const
 
bool stateIsOptimalSchedulerReachable (MdpStateType mdpState) const
 Retrieves whether the current state can be reached under an optimal scheduler This requires a previous call of computeOptimalChoicesAndReachableMdpStates.
 
bool actionIsOptimal (uint64_t const &globalActionIndex) const
 Retrieves whether the given action at the current state was optimal in the most recent check.
 
bool currentStateIsOptimalSchedulerReachable () const
 Retrieves whether the current state can be reached under a scheduler that was optimal in the most recent check.
 
bool actionAtCurrentStateWasOptimal (uint64_t const &localActionIndex) const
 Retrieves whether the given action at the current state was optimal in the most recent check.
 
bool getCurrentStateActionExplorationWasDelayed (uint64_t const &localActionIndex) const
 
void restoreOldBehaviorAtCurrentState (uint64_t const &localActionIndex)
 Inserts transitions and rewards at the given action as in the MDP of the previous exploration.
 
void finishExploration ()
 
void dropUnexploredStates ()
 
std::shared_ptr< storm::models::sparse::Mdp< ValueType > > getExploredMdp () const
 
MdpStateType getCurrentNumberOfMdpStates () const
 
MdpStateType getCurrentNumberOfMdpChoices () const
 
MdpStateType getStartOfCurrentRowGroup () const
 
uint64_t getSizeOfCurrentRowGroup () const
 
uint64_t getRowGroupSizeOfState (uint64_t state) const
 
bool needsActionAdjustment (uint64_t numActionsNeeded)
 
ValueType getLowerValueBoundAtCurrentState () const
 
ValueType getUpperValueBoundAtCurrentState () const
 
ValueType computeLowerValueBoundAtBelief (BeliefId const &beliefId) const
 
ValueType computeUpperValueBoundAtBelief (BeliefId const &beliefId) const
 
ValueType computeLowerValueBoundForScheduler (BeliefId const &beliefId, uint64_t schedulerId) const
 
ValueType computeUpperValueBoundForScheduler (BeliefId const &beliefId, uint64_t schedulerId) const
 
std::pair< bool, ValueType > computeFMSchedulerValueForMemoryNode (BeliefId const &beliefId, uint64_t memoryNode) const
 
storm::storage::Scheduler< ValueType > getUpperValueBoundScheduler (uint64_t schedulerId) const
 
storm::storage::Scheduler< ValueType > getLowerValueBoundScheduler (uint64_t schedulerId) const
 
std::vector< storm::storage::Scheduler< ValueType > > getUpperValueBoundSchedulers () const
 
std::vector< storm::storage::Scheduler< ValueType > > getLowerValueBoundSchedulers () const
 
void computeValuesOfExploredMdp (storm::Environment const &env, storm::solver::OptimizationDirection const &dir)
 
bool hasComputedValues () const
 
bool hasFMSchedulerValues () const
 
std::vector< ValueType > const & getValuesOfExploredMdp () const
 
ValueType const & getComputedValueAtInitialState () const
 
MdpStateType getBeliefId (MdpStateType exploredMdpState) const
 
void gatherSuccessorObservationInformationAtCurrentState (uint64_t localActionIndex, std::map< uint32_t, SuccessorObservationInformation > &gatheredSuccessorObservations)
 
void gatherSuccessorObservationInformationAtMdpChoice (uint64_t mdpChoice, std::map< uint32_t, SuccessorObservationInformation > &gatheredSuccessorObservations)
 
bool currentStateHasSuccessorObservationInObservationSet (uint64_t localActionIndex, storm::storage::BitVector const &observationSet)
 
void takeCurrentValuesAsUpperBounds ()
 
void takeCurrentValuesAsLowerBounds ()
 
void computeOptimalChoicesAndReachableMdpStates (ValueType const &ancillaryChoicesEpsilon, bool relativeDifference)
 Computes the set of states that are reachable via a path that is consistent with an optimal MDP scheduler.
 
std::vector< BeliefId > getBeliefsWithObservationInMdp (uint32_t obs) const
 
std::vector< BeliefId > getBeliefsInMdp ()
 
void addClippingRewardToCurrentState (uint64_t const &localActionIndex, ValueType rewardValue)
 
ValueType getTrivialUpperBoundAtPOMDPState (uint64_t const &pomdpState)
 
ValueType getTrivialLowerBoundAtPOMDPState (uint64_t const &pomdpState)
 
void setExtremeValueBound (storm::pomdp::storage::ExtremePOMDPValueBound< ValueType > valueBound)
 
ValueType getExtremeValueBoundAtPOMDPState (uint64_t const &pomdpState)
 
MdpStateType getExploredMdpState (BeliefId const &beliefId) const
 
bool beliefHasMdpState (BeliefId const &beliefId) const
 
storm::storage::BitVector getStateExtremeBoundIsInfinite ()
 
uint64_t getNrSchedulersForUpperBounds ()
 
uint64_t getNrSchedulersForLowerBounds ()
 
void markAsGridBelief (BeliefId const &beliefId)
 
bool isMarkedAsGridBelief (BeliefId const &beliefId)
 
const std::shared_ptr< storm::storage::Scheduler< BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType > > & getSchedulerForExploredMdp () const
 
void setFMSchedValueList (std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > > valueList)
 
uint64_t getNrOfMemoryNodesForObservation (uint32_t observation) const
 
void storeExplorationState ()
 
void restoreExplorationState ()
 
void adjustActions (uint64_t totalNumberOfActions)
 
std::vector< BeliefValueType > computeProductWithSparseMatrix (BeliefId const &beliefId, storm::storage::SparseMatrix< BeliefValueType > &matrix) const
 

Detailed Description

template<typename PomdpType, typename BeliefValueType = typename PomdpType::ValueType>
class storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >

Definition at line 27 of file BeliefMdpExplorer.h.

Member Typedef Documentation

◆ BeliefId

template<typename PomdpType , typename BeliefValueType = typename PomdpType::ValueType>
typedef BeliefManagerType::BeliefId storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::BeliefId

Definition at line 31 of file BeliefMdpExplorer.h.

◆ BeliefManagerType

template<typename PomdpType , typename BeliefValueType = typename PomdpType::ValueType>
typedef storm::storage::BeliefManager<PomdpType, BeliefValueType> storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::BeliefManagerType

Definition at line 30 of file BeliefMdpExplorer.h.

◆ MdpStateType

template<typename PomdpType , typename BeliefValueType = typename PomdpType::ValueType>
typedef uint64_t storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::MdpStateType

Definition at line 32 of file BeliefMdpExplorer.h.

◆ ValueType

template<typename PomdpType , typename BeliefValueType = typename PomdpType::ValueType>
typedef PomdpType::ValueType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType

Definition at line 29 of file BeliefMdpExplorer.h.

Member Enumeration Documentation

◆ Status

template<typename PomdpType , typename BeliefValueType = typename PomdpType::ValueType>
enum class storm::builder::BeliefMdpExplorer::Status
strong
Enumerator
Uninitialized 
Exploring 
ModelFinished 
ModelChecked 

Definition at line 43 of file BeliefMdpExplorer.h.

Constructor & Destructor Documentation

◆ BeliefMdpExplorer() [1/2]

template<typename PomdpType , typename BeliefValueType >
storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::BeliefMdpExplorer ( std::shared_ptr< BeliefManagerType >  beliefManager,
storm::pomdp::storage::PreprocessingPomdpValueBounds< ValueType > const &  pomdpValueBounds,
ExplorationHeuristic  explorationHeuristic = ExplorationHeuristic::BreadthFirst 
)

Definition at line 38 of file BeliefMdpExplorer.cpp.

◆ BeliefMdpExplorer() [2/2]

template<typename PomdpType , typename BeliefValueType = typename PomdpType::ValueType>
storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::BeliefMdpExplorer ( BeliefMdpExplorer< PomdpType, BeliefValueType > &&  other)
default

Member Function Documentation

◆ actionAtCurrentStateWasOptimal()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::actionAtCurrentStateWasOptimal ( uint64_t const &  localActionIndex) const

Retrieves whether the given action at the current state was optimal in the most recent check.

This requires (i) a previous call of computeOptimalChoicesAndReachableMdpStates and (ii) that the current state has old behavior.

Definition at line 436 of file BeliefMdpExplorer.cpp.

◆ actionIsOptimal()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::actionIsOptimal ( uint64_t const &  globalActionIndex) const

Retrieves whether the given action at the current state was optimal in the most recent check.

This requires a previous call of computeOptimalChoicesAndReachableMdpStates.

Definition at line 419 of file BeliefMdpExplorer.cpp.

◆ addChoiceLabelToCurrentState()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::addChoiceLabelToCurrentState ( uint64_t const &  localActionIndex,
std::string const &  label 
)

Definition at line 1254 of file BeliefMdpExplorer.cpp.

◆ addClippingRewardToCurrentState()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::addClippingRewardToCurrentState ( uint64_t const &  localActionIndex,
ValueType  rewardValue 
)

Definition at line 350 of file BeliefMdpExplorer.cpp.

◆ addRewardToCurrentState()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::addRewardToCurrentState ( uint64_t const &  localActionIndex,
ValueType  rewardValue 
)

Adds the provided reward value to the given action of the current state.

Parameters
localActionIndex
rewardValue

Definition at line 340 of file BeliefMdpExplorer.cpp.

◆ addSelfloopTransition()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::addSelfloopTransition ( uint64_t const &  localActionIndex = 0,
ValueType const &  value = storm::utility::one<ValueType>() 
)

Definition at line 295 of file BeliefMdpExplorer.cpp.

◆ addTransitionsToExtraStates()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::addTransitionsToExtraStates ( uint64_t const &  localActionIndex,
ValueType const &  targetStateValue = storm::utility::zero<ValueType>(),
ValueType const &  bottomStateValue = storm::utility::zero<ValueType>() 
)

Definition at line 277 of file BeliefMdpExplorer.cpp.

◆ addTransitionToBelief()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::addTransitionToBelief ( uint64_t const &  localActionIndex,
BeliefId const &  transitionTarget,
ValueType const &  value,
bool  ignoreNewBeliefs 
)

Adds the next transition to the given successor belief.

Parameters
localActionIndex
transitionTarget
value
ignoreNewBeliefsIf true, beliefs that were not found before are not inserted, i.e. we might not insert the transition.
Returns
true iff a transition was actually inserted. False can only happen if ignoreNewBeliefs is true.

Definition at line 305 of file BeliefMdpExplorer.cpp.

◆ adjustActions()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::adjustActions ( uint64_t  totalNumberOfActions)

Definition at line 1370 of file BeliefMdpExplorer.cpp.

◆ beliefHasMdpState()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::beliefHasMdpState ( BeliefId const &  beliefId) const

Definition at line 1061 of file BeliefMdpExplorer.cpp.

◆ computeFMSchedulerValueForMemoryNode()

template<typename PomdpType , typename BeliefValueType >
std::pair< bool, typename BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType > storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::computeFMSchedulerValueForMemoryNode ( BeliefId const &  beliefId,
uint64_t  memoryNode 
) const

Definition at line 905 of file BeliefMdpExplorer.cpp.

◆ computeLowerValueBoundAtBelief()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::computeLowerValueBoundAtBelief ( BeliefId const &  beliefId) const

Definition at line 863 of file BeliefMdpExplorer.cpp.

◆ computeLowerValueBoundForScheduler()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::computeLowerValueBoundForScheduler ( BeliefId const &  beliefId,
uint64_t  schedulerId 
) const

Definition at line 887 of file BeliefMdpExplorer.cpp.

◆ computeOptimalChoicesAndReachableMdpStates()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::computeOptimalChoicesAndReachableMdpStates ( ValueType const &  ancillaryChoicesEpsilon,
bool  relativeDifference 
)

Computes the set of states that are reachable via a path that is consistent with an optimal MDP scheduler.

States that are only reachable via target states will not be in this set.

Parameters
ancillaryChoicesEpsilonif the difference of a 1-step value of a choice is only epsilon away from the optimal value, the choice will be included.
relativeif set, we consider the relative difference to detect ancillaryChoices

Definition at line 1022 of file BeliefMdpExplorer.cpp.

◆ computeProductWithSparseMatrix()

template<typename PomdpType , typename BeliefValueType >
std::vector< BeliefValueType > storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::computeProductWithSparseMatrix ( BeliefId const &  beliefId,
storm::storage::SparseMatrix< BeliefValueType > &  matrix 
) const

Definition at line 1364 of file BeliefMdpExplorer.cpp.

◆ computeRewardAtCurrentState()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::computeRewardAtCurrentState ( uint64_t const &  localActionIndex,
ValueType  extraReward = storm::utility::zero<ValueType>() 
)

Definition at line 330 of file BeliefMdpExplorer.cpp.

◆ computeUpperValueBoundAtBelief()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::computeUpperValueBoundAtBelief ( BeliefId const &  beliefId) const

Definition at line 875 of file BeliefMdpExplorer.cpp.

◆ computeUpperValueBoundForScheduler()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::computeUpperValueBoundForScheduler ( BeliefId const &  beliefId,
uint64_t  schedulerId 
) const

Definition at line 896 of file BeliefMdpExplorer.cpp.

◆ computeValuesOfExploredMdp()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::computeValuesOfExploredMdp ( storm::Environment const &  env,
storm::solver::OptimizationDirection const &  dir 
)

Definition at line 915 of file BeliefMdpExplorer.cpp.

◆ currentStateHasOldBehavior()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::currentStateHasOldBehavior ( ) const

Definition at line 386 of file BeliefMdpExplorer.cpp.

◆ currentStateHasSuccessorObservationInObservationSet()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::currentStateHasSuccessorObservationInObservationSet ( uint64_t  localActionIndex,
storm::storage::BitVector const &  observationSet 
)

Definition at line 998 of file BeliefMdpExplorer.cpp.

◆ currentStateIsOptimalSchedulerReachable()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::currentStateIsOptimalSchedulerReachable ( ) const

Retrieves whether the current state can be reached under a scheduler that was optimal in the most recent check.

This requires (i) a previous call of computeOptimalChoicesAndReachableMdpStates and (ii) that the current state has old behavior.

Definition at line 426 of file BeliefMdpExplorer.cpp.

◆ dropUnexploredStates()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::dropUnexploredStates ( )

Definition at line 685 of file BeliefMdpExplorer.cpp.

◆ exploreNextState()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::BeliefId storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::exploreNextState ( )

Definition at line 239 of file BeliefMdpExplorer.cpp.

◆ finishExploration()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::finishExploration ( )

Definition at line 516 of file BeliefMdpExplorer.cpp.

◆ gatherSuccessorObservationInformationAtCurrentState()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::gatherSuccessorObservationInformationAtCurrentState ( uint64_t  localActionIndex,
std::map< uint32_t, SuccessorObservationInformation > &  gatheredSuccessorObservations 
)

Definition at line 970 of file BeliefMdpExplorer.cpp.

◆ gatherSuccessorObservationInformationAtMdpChoice()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::gatherSuccessorObservationInformationAtMdpChoice ( uint64_t  mdpChoice,
std::map< uint32_t, SuccessorObservationInformation > &  gatheredSuccessorObservations 
)

Definition at line 979 of file BeliefMdpExplorer.cpp.

◆ getBeliefId()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::MdpStateType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getBeliefId ( MdpStateType  exploredMdpState) const

Definition at line 963 of file BeliefMdpExplorer.cpp.

◆ getBeliefManager()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::BeliefManagerType const & storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getBeliefManager ( ) const

Definition at line 46 of file BeliefMdpExplorer.cpp.

◆ getBeliefsInMdp()

template<typename PomdpType , typename BeliefValueType >
std::vector< typename BeliefMdpExplorer< PomdpType, BeliefValueType >::BeliefId > storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getBeliefsInMdp ( )

Definition at line 1259 of file BeliefMdpExplorer.cpp.

◆ getBeliefsWithObservationInMdp()

template<typename PomdpType , typename BeliefValueType >
std::vector< typename BeliefMdpExplorer< PomdpType, BeliefValueType >::BeliefId > storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getBeliefsWithObservationInMdp ( uint32_t  obs) const

Definition at line 1264 of file BeliefMdpExplorer.cpp.

◆ getComputedValueAtInitialState()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType const & storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getComputedValueAtInitialState ( ) const

Definition at line 956 of file BeliefMdpExplorer.cpp.

◆ getCurrentNumberOfMdpChoices()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::MdpStateType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getCurrentNumberOfMdpChoices ( ) const

Definition at line 812 of file BeliefMdpExplorer.cpp.

◆ getCurrentNumberOfMdpStates()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::MdpStateType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getCurrentNumberOfMdpStates ( ) const

Definition at line 806 of file BeliefMdpExplorer.cpp.

◆ getCurrentStateActionExplorationWasDelayed()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getCurrentStateActionExplorationWasDelayed ( uint64_t const &  localActionIndex) const

Definition at line 447 of file BeliefMdpExplorer.cpp.

◆ getCurrentStateWasClipped()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getCurrentStateWasClipped ( ) const

Definition at line 402 of file BeliefMdpExplorer.cpp.

◆ getCurrentStateWasTruncated()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getCurrentStateWasTruncated ( ) const

Definition at line 393 of file BeliefMdpExplorer.cpp.

◆ getExploredMdp()

template<typename PomdpType , typename BeliefValueType >
std::shared_ptr< storm::models::sparse::Mdp< typename BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType > > storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getExploredMdp ( ) const

Definition at line 799 of file BeliefMdpExplorer.cpp.

◆ getExploredMdpState()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::MdpStateType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getExploredMdpState ( BeliefId const &  beliefId) const

Definition at line 1136 of file BeliefMdpExplorer.cpp.

◆ getExtremeValueBoundAtPOMDPState()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getExtremeValueBoundAtPOMDPState ( uint64_t const &  pomdpState)

Definition at line 1305 of file BeliefMdpExplorer.cpp.

◆ getLowerValueBoundAtCurrentState()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getLowerValueBoundAtCurrentState ( ) const

Definition at line 851 of file BeliefMdpExplorer.cpp.

◆ getLowerValueBoundScheduler()

template<typename PomdpType , typename BeliefValueType >
storm::storage::Scheduler< typename BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType > storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getLowerValueBoundScheduler ( uint64_t  schedulerId) const

Definition at line 1327 of file BeliefMdpExplorer.cpp.

◆ getLowerValueBoundSchedulers()

template<typename PomdpType , typename BeliefValueType >
std::vector< storm::storage::Scheduler< typename BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType > > storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getLowerValueBoundSchedulers ( ) const

Definition at line 1345 of file BeliefMdpExplorer.cpp.

◆ getNrOfMemoryNodesForObservation()

template<typename PomdpType , typename BeliefValueType >
uint64_t storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getNrOfMemoryNodesForObservation ( uint32_t  observation) const

Definition at line 1300 of file BeliefMdpExplorer.cpp.

◆ getNrSchedulersForLowerBounds()

template<typename PomdpType , typename BeliefValueType >
uint64_t storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getNrSchedulersForLowerBounds ( )

Definition at line 1321 of file BeliefMdpExplorer.cpp.

◆ getNrSchedulersForUpperBounds()

template<typename PomdpType , typename BeliefValueType >
uint64_t storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getNrSchedulersForUpperBounds ( )

Definition at line 1316 of file BeliefMdpExplorer.cpp.

◆ getRowGroupSizeOfState()

template<typename PomdpType , typename BeliefValueType >
uint64_t storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getRowGroupSizeOfState ( uint64_t  state) const

Definition at line 832 of file BeliefMdpExplorer.cpp.

◆ getSchedulerForExploredMdp()

template<typename PomdpType , typename BeliefValueType >
const std::shared_ptr< storm::storage::Scheduler< typename BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType > > & storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getSchedulerForExploredMdp ( ) const

Definition at line 950 of file BeliefMdpExplorer.cpp.

◆ getSizeOfCurrentRowGroup()

template<typename PomdpType , typename BeliefValueType >
uint64_t storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getSizeOfCurrentRowGroup ( ) const

Definition at line 825 of file BeliefMdpExplorer.cpp.

◆ getStartOfCurrentRowGroup()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::MdpStateType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getStartOfCurrentRowGroup ( ) const

Definition at line 818 of file BeliefMdpExplorer.cpp.

◆ getStateExtremeBoundIsInfinite()

template<typename PomdpType , typename BeliefValueType >
storm::storage::BitVector storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getStateExtremeBoundIsInfinite ( )

Definition at line 1311 of file BeliefMdpExplorer.cpp.

◆ getTrivialLowerBoundAtPOMDPState()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getTrivialLowerBoundAtPOMDPState ( uint64_t const &  pomdpState)

Definition at line 1284 of file BeliefMdpExplorer.cpp.

◆ getTrivialUpperBoundAtPOMDPState()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getTrivialUpperBoundAtPOMDPState ( uint64_t const &  pomdpState)

Definition at line 1278 of file BeliefMdpExplorer.cpp.

◆ getUnexploredStates()

template<typename PomdpType , typename BeliefValueType >
std::vector< uint64_t > storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getUnexploredStates ( )

Definition at line 228 of file BeliefMdpExplorer.cpp.

◆ getUpperValueBoundAtCurrentState()

template<typename PomdpType , typename BeliefValueType >
BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getUpperValueBoundAtCurrentState ( ) const

Definition at line 857 of file BeliefMdpExplorer.cpp.

◆ getUpperValueBoundScheduler()

template<typename PomdpType , typename BeliefValueType >
storm::storage::Scheduler< typename BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType > storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getUpperValueBoundScheduler ( uint64_t  schedulerId) const

Definition at line 1336 of file BeliefMdpExplorer.cpp.

◆ getUpperValueBoundSchedulers()

template<typename PomdpType , typename BeliefValueType >
std::vector< storm::storage::Scheduler< typename BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType > > storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getUpperValueBoundSchedulers ( ) const

Definition at line 1352 of file BeliefMdpExplorer.cpp.

◆ getValuesOfExploredMdp()

template<typename PomdpType , typename BeliefValueType >
std::vector< typename BeliefMdpExplorer< PomdpType, BeliefValueType >::ValueType > const & storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::getValuesOfExploredMdp ( ) const

Definition at line 942 of file BeliefMdpExplorer.cpp.

◆ hasComputedValues()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::hasComputedValues ( ) const

Definition at line 937 of file BeliefMdpExplorer.cpp.

◆ hasFMSchedulerValues()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::hasFMSchedulerValues ( ) const

Definition at line 1359 of file BeliefMdpExplorer.cpp.

◆ hasUnexploredState()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::hasUnexploredState ( ) const

Definition at line 222 of file BeliefMdpExplorer.cpp.

◆ isMarkedAsGridBelief()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::isMarkedAsGridBelief ( BeliefId const &  beliefId)

Definition at line 1131 of file BeliefMdpExplorer.cpp.

◆ markAsGridBelief()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::markAsGridBelief ( BeliefId const &  beliefId)

Definition at line 1126 of file BeliefMdpExplorer.cpp.

◆ needsActionAdjustment()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::needsActionAdjustment ( uint64_t  numActionsNeeded)

Definition at line 845 of file BeliefMdpExplorer.cpp.

◆ restartExploration()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::restartExploration ( )

Restarts the exploration to allow re-exploring each state.

After calling this, the "currently explored" MDP has the same number of states and choices as the "old" one, but the choices are still empty This method inserts the initial state of the MDP in the exploration queue. While re-exploring, the reference to the old MDP remains valid.

Definition at line 123 of file BeliefMdpExplorer.cpp.

◆ restoreExplorationState()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::restoreExplorationState ( )

Definition at line 190 of file BeliefMdpExplorer.cpp.

◆ restoreOldBehaviorAtCurrentState()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::restoreOldBehaviorAtCurrentState ( uint64_t const &  localActionIndex)

Inserts transitions and rewards at the given action as in the MDP of the previous exploration.

Does NOT set whether the state is truncated and/or target. Will add "old" states that have not been considered before into the exploration queue

Parameters
localActionIndex

Definition at line 458 of file BeliefMdpExplorer.cpp.

◆ setCurrentChoiceIsDelayed()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::setCurrentChoiceIsDelayed ( uint64_t const &  localActionIndex)

Definition at line 379 of file BeliefMdpExplorer.cpp.

◆ setCurrentStateIsClipped()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::setCurrentStateIsClipped ( )

Definition at line 371 of file BeliefMdpExplorer.cpp.

◆ setCurrentStateIsTarget()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::setCurrentStateIsTarget ( )

Definition at line 357 of file BeliefMdpExplorer.cpp.

◆ setCurrentStateIsTruncated()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::setCurrentStateIsTruncated ( )

Definition at line 364 of file BeliefMdpExplorer.cpp.

◆ setExtremeValueBound()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::setExtremeValueBound ( storm::pomdp::storage::ExtremePOMDPValueBound< ValueType >  valueBound)

Definition at line 1290 of file BeliefMdpExplorer.cpp.

◆ setFMSchedValueList()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::setFMSchedValueList ( std::vector< std::vector< std::unordered_map< uint64_t, ValueType > > >  valueList)

Definition at line 1295 of file BeliefMdpExplorer.cpp.

◆ startNewExploration()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::startNewExploration ( std::optional< ValueType >  extraTargetStateValue = boost::none,
std::optional< ValueType >  extraBottomStateValue = std::nullopt 
)

Definition at line 51 of file BeliefMdpExplorer.cpp.

◆ stateIsOptimalSchedulerReachable()

template<typename PomdpType , typename BeliefValueType >
bool storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::stateIsOptimalSchedulerReachable ( MdpStateType  mdpState) const

Retrieves whether the current state can be reached under an optimal scheduler This requires a previous call of computeOptimalChoicesAndReachableMdpStates.

Definition at line 411 of file BeliefMdpExplorer.cpp.

◆ storeExplorationState()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::storeExplorationState ( )

Definition at line 166 of file BeliefMdpExplorer.cpp.

◆ takeCurrentValuesAsLowerBounds()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::takeCurrentValuesAsLowerBounds ( )

Definition at line 1016 of file BeliefMdpExplorer.cpp.

◆ takeCurrentValuesAsUpperBounds()

template<typename PomdpType , typename BeliefValueType >
void storm::builder::BeliefMdpExplorer< PomdpType, BeliefValueType >::takeCurrentValuesAsUpperBounds ( )

Definition at line 1010 of file BeliefMdpExplorer.cpp.

The documentation for this class was generated from the following files: