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 – Variable 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, const bool store_compressed_states)

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

  • store_compressed_states – Whether to store the explored compressed states (for trace generation)

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

Get the variable information related to the loaded model.

Returns:

A const reference to the VariableInformation instance

void loadInitialState()

Load the initial state in the NextStateGenerator (basically a model reset).

void load(const StateType &state_id)

Load a compressed state in the NextStateGenerator.

Parameters:

state – The compressed state to load

const state_properties::StateDescription<StateType, ValueType> &processLoadedState()
inline const state_properties::PropertyDescription &getPropertyDescription() const