Template Class StateGenerationBase

• Defined in File state_generation_base.hpp

Inheritance Relationships

Derived Types

• public smc_storm::state_generation::StateGeneration< StateType, ValueType > (Template Class StateGeneration)

• public smc_storm::state_generation::StateGenerationCacheless< ValueType > (Template Class StateGenerationCacheless)

Class Documentation

template<typename ValueType>
class StateGenerationBase

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

Template Parameters:

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

Subclassed by smc_storm::state_generation::StateGeneration< StateType, ValueType >, smc_storm::state_generation::StateGenerationCacheless< ValueType >

Public Functions

virtual ~StateGenerationBase() = default

inline const state_properties::PropertyDescription &getPropertyDescription() const

Get the loaded property description.

Returns:

A PropertyDescription object, containing the property under evaluation

virtual void resetModel() = 0

Load the initial state in the model.

virtual const AvailableActions<ValueType> &getAvailableActions() = 0

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) = 0

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() = 0

Get the reward associated to the current state.

Returns:

The reward associated to the curr. state

virtual state_properties::StateInfoType getStateInfo() = 0

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

Protected Functions

inline StateGenerationBase(const storm::logic::Formula &formula, const bool store_compressed_states, std::default_random_engine &random_generator)

Protected Attributes

state_properties::PropertyDescription _property_description

mutable std::reference_wrapper<std::default_random_engine> _random_generator

const bool _store_compressed_states