Template Class StateGeneration

Class Documentation

template<typename StateType, typename ValueType>
class StateGeneration

Class that loads an input model and property to generate states and verify if the input property holds.

Template Parameters:

  • StateType – Variab;e type to identify states and actions

  • ValueType – Variable type of computed results (e.g. rewards)

Public Functions

StateGeneration(const storm::storage::SymbolicModelDescription &model, const storm::logic::Formula &formula, const std::string &reward_model, samples::ExplorationInformation<StateType, ValueType> &exploration_information)

Extension of the constructor above, in case we evaluate Rewards.

Parameters:

  • model – The model to generate the next states from

  • formula – The formula to evaluate on the generated states

  • reward_model – Name of the reward model to use for assigning costs on states and actions. Empty for P properties

  • exploration_information – Structure that keeps track of the already explored states

inline const storm::generator::VariableInformation &getVariableInformation() const

Get the variable information related to the loaded model.

Returns:

A const reference to the VariableInformation instance

inline bool rewardLoaded() const

Check if a reward model is loaded and therefore it needs to be evaluated.

Returns:

true if we loaded a reward model, false otherwise

inline size_t getRewardIndex() const

Get the index of the reward model of our interest.

Returns:

Index matching to the reward model we are evaluating

void load(const storm::generator::CompressedState &state)

Load a compressed state in the NextStateGenerator.

Parameters:

state – The compressed state to load

std::vector<StateType> getInitialStates()

Get the initial states of the loaded model.

Returns:

A list of state IDs

storm::generator::StateBehavior<ValueType, StateType> expand()

Expand the loaded state to get the next states.

Returns:

A generator used to access the generated information

void computeInitialStates()
StateType getFirstInitialState() const
std::size_t getNumberOfInitialStates() const
bool isConditionState() const

Check whether the loaded state satisfies the condition formula.

Returns:

true if the condition formula is satisfied, false otherwise

bool isTargetState() const

Check whether the loaded state satisfies the target formula.

Returns:

true if the target formula is satisfied, false otherwise

inline size_t getLowerBound() const

Getter for the min amount of steps to compute before checking for target and condition formulae.

Returns:

The lower bound of the property

inline size_t getUpperBound() const

Getter for the max amount of steps, after which the property is marked as unsatisfied.

Returns:

The upper bound of the property

inline bool getIsTerminalVerified() const

Flag indicating that a terminal state should be considered as verified, regardless of the target formula.

Returns:

true if any terminal state that does not break the condition formula is verified, false otherwise