Template Class StateGenerationCacheless

Inheritance Relationships

Base Type

Class Documentation

template<typename ValueType>
class StateGenerationCacheless : 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 Functions

StateGenerationCacheless(const storm::storage::SymbolicModelDescription &model, const storm::logic::Formula &formula, const std::string &reward_model, std::default_random_engine &random_generator, const std::vector<model_checker::SmcPluginInstance> &loaded_plugins)

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

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

inline const state_properties::StateVariableInformation<ValueType> &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

inline const state_properties::StateVariableData<ValueType> &getCurrentState() const