Template Class ExplorationInformation

Defined in File exploration_information.hpp

Class Documentation

template<typename StateType, typename ValueType> class ExplorationInformation

Class holding information about the explored states.

Template Parameters:

StateType – variable type for state and action identifiers
ValueType – variable type for the results (e.g. Rewards)

Public Types

typedef state_properties::StateInfoType StateInfoType

typedef StateType ActionType

typedef std::unordered_map<StateType, StateInfoType> StateInfoMap

typedef std::unordered_map<StateType, storm::generator::CompressedState> IdToStateMap

typedef IdToStateMap::const_iterator const_iterator

typedef std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> MatrixType

Public Functions

ExplorationInformation(const bool store_expanded_states)

Constructor for the ExplorationInformation class.

Parameters:: store_expanded_states – If true, the class will store all expanded raw states in memory

const storm::generator::CompressedState &getCompressedState(const StateType &state) const

Return the compressed state associated to the input state id.

Parameters:: state – the ID of the requested compressed state
Returns:: A compressed state

const_iterator findUnexploredState(const StateType &state) const

const_iterator unexploredStatesEnd() const

void removeUnexploredState(const_iterator it)

void addUnexploredState(const StateType &state_id, const storm::generator::CompressedState &compressed_state)

void assignStateToRowGroup(const StateType &state, const ActionType &row_group)

StateType assignStateToNextRowGroup(const StateType &state)

StateType getNextRowGroup() const

void newRowGroup(const ActionType &action)

void newRowGroup()

void terminateCurrentRowGroup()

void moveActionToBackOfMatrix(const ActionType &action)

StateType getActionCount() const

size_t getNumberOfUnexploredStates() const

size_t getNumberOfDiscoveredStates() const

const StateType &getRowGroup(const StateType &state) const

const StateType &getUnexploredMarker() const

bool isUnexplored(const StateType &state) const

bool isTerminal(const StateType &state) const

Check if the input state does not need to be expanded further States that are not to expand are: VERIFY_PROPERTY, BREAK_CONDITION, IS_TERMINAL.

Parameters:: state – The ID of the state we need to check
Returns:: true if the state is final, false otherwise

StateInfoType getStateInfo(const StateType &state) const

Return the StateInfo of the input state (if available)

Parameters:: state – The ID of the state we are evaluating
Returns:: Optionally, the StateInfo assigned to a specific state

const ValueType &getStateReward(const StateType &stateId) const

const ActionType &getStartRowOfGroup(const StateType &group) const

size_t getRowGroupSize(const StateType &group) const

bool onlyOneActionAvailable(const StateType &group) const

void addStateInfo(const StateType &state, const StateInfoType info)

Assign a specific StateInfo to the provided state.

Parameters:

state – The ID of the state to mark
info – The new label to assign to a specific state: it overwrites.

void addStateReward(const StateType &state_id, const ValueType &state_reward)

void addTerminalState(const StateType &state)

Used for compatibility: assigns the IS_TERMINAL label to the provided state.

Parameters:: state – the ID of the state to mark

std::vector<storm::storage::MatrixEntry<StateType, ValueType>> &getRowOfMatrix(const ActionType &row)

const std::vector<storm::storage::MatrixEntry<StateType, ValueType>> &getRowOfMatrix(const ActionType &row) const

const ValueType &getActionReward(const ActionType &action_id) const

void addActionsToMatrix(const size_t &count)

void addActionReward(const ActionType &action_id, const ValueType &action_reward)