Template Class StateGeneration

Inheritance Relationships

Base Type

Class Documentation

template<typename StateType, typename ValueType>
class StateGeneration : public smc_storm::state_generation::StateGenerationBase<ValueType>

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 Types

using StateDescription = state_properties::StateDescription<StateType, ValueType>

Public Functions

StateGeneration(const storm::storage::SymbolicModelDescription &model, const storm::logic::Formula &formula, const std::string &reward_model, const bool store_compressed_states, std::default_random_engine &random_generator)

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)

  • random_generator – A random number generator, used to pick one of the possible destinations

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

Get the variable information related to the loaded model.

Returns:

A const reference to the VariableInformation instance

virtual void resetModel() override

Load the initial state in the model.

virtual const AvailableActions<ValueType> &getAvailableActions() override

Return the set of available actions from the current state.

Returns:

A vector of pairs with action ID and associated reward

virtual ValueType runAction(const uint64_t action_id) override

Execute a specific action: if the action has multiple destinations, pick one based on likelihood.

Parameters:

action_id – The ID of the action to execute

Returns:

The single transition reward, obtained by picking a specific destination

virtual ValueType getStateReward() override

Get the reward associated to the current state.

Returns:

The reward associated to the curr. state

virtual state_properties::StateInfoType getStateInfo() override

Retrieve the state’s information, checking how it evaluates against the requested property.

Returns:

Whether the state satisfies or not the property, or is in a terminal state

const storm::generator::CompressedState &getCurrentState() const