Class SmcPluginInstance

Class Documentation

class SmcPluginInstance

Object to keep all information regarding a plugin instantiation in one place.

Public Types

using PluginAndModelVariable = std::pair<std::string, storm::expressions::Variable>
using PluginAndModelVariableVector = std::vector<std::pair<std::string, storm::expressions::Variable>>
using PluginToModelExpressionMap = std::unordered_map<std::string, storm::expressions::Expression>

Public Functions

SmcPluginInstance() = delete
SmcPluginInstance(const std::vector<std::filesystem::path> &available_paths, const std::string &plugin_name, const std::string &automaton_id, const std::string &action_name, const uint64_t action_id)

Constructs a new SmcPluginInstance object.

Parameters:

  • available_paths – A vector of filesystem paths where plugins are available.

  • plugin_name – The name of the plugin to be used.

  • automaton_id – The ID of the automaton associated with this plugin instance.

  • action_name – The name of the automaton’s action associated with this plugin instance (for debug reasons).

  • action_id – The ID of the automaton’s action associated with this plugin instance.

inline const std::string &getAutomatonName() const

Get the name of the automaton associated to this plugin instance description.

Returns:

The string describing the automaton name.

inline const uint64_t getActionId() const

Get the index associated to the action name provided in the plugin configuration.

Returns:

The index related to the provided action, resulting from the JANI model.

inline const std::string &getActionName() const

Get the action name provided in the plugin configuration.

Returns:

The action name provided in the plugin configuration.

template<typename T>
void appendInitData(const std::string &ref, const T &value)

Appends initialization data to the plugin instance.

Template Parameters:

T – The type of the value to be appended.

Parameters:

  • ref – The name of the config parameter in the plugin.

  • value – The value to assign to the configuration parameter.

inline const smc_verifiable_plugins::SmcPluginBase::DataExchange &getInitData() const

Get the initialization data for the plugin.

Returns:

The DataExchange object containing all initialization data for the plugin.

inline const PluginToModelExpressionMap &getInputVariablesMap() const

Get the mapping between the plugin input variables and the associated model variables.

Returns:

A constant reference to map relating the plugin’s input data to model’s variables.

inline const PluginAndModelVariableVector &getOutputVariablesMap() const

Get the mapping between the plugin output variables and the associated model variables.

Returns:

A constant reference to map relating the plugin’s output data to model’s variables.

void appendInputData(const std::string &ref, const storm::expressions::Expression &value)

Appends input data to the plugin instance.

Template Parameters:

T – The type of the value to be appended.

Parameters:

  • ref – A reference string to identify the input data in the plugin.

  • value – The value to assign to the input data.

void appendOutputData(const storm::expressions::Variable &ref, const std::string &value)

Appends output data to the plugin instance.

Parameters:

  • ref – A reference string, associated to the JANI variable storing the output value.

  • value – The name of the output value that will be provided by the plugin.

void sortOutputData()

Sort the entries in the output data vectors based on the variable index from the Jani Model.

std::unique_ptr<smc_verifiable_plugins::SmcPluginBase> generatePluginInstance() const

Generate a plugin instance related to the loaded plugin information.