Template Class StateExpansionHandler

• Defined in File state_expansion_handler.hpp

Class Documentation

template<typename StateType, typename ValueType>
class StateExpansionHandler

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

StateExpansionHandler()

void init(const uint64_t state_size)

Init the state storage structures, if required.

Parameters:

state_size – the dimension of the model’s state

uint32_t stateExpansionCallback(const storm::generator::CompressedState &state)

Callback to process the next states from the one under expansion. It must assign a numeric ID to them.

Parameters:

state – The state ID to process

Returns:

The int ID associated to the processed next state