Class SmcPluginInstance

Class Documentation

class SmcPluginInstance

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

Public Types

enum class ExprType

Values:

enumerator BOOL
enumerator INT
enumerator REAL
using PluginAndModelVariable = std::pair<std::string, storm::expressions::Variable>
using PluginAndModelVariableVector = std::vector<PluginAndModelVariable>
using PluginToModelExpressionMap = std::unordered_map<std::string, std::pair<ExprType, 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.

void appendInitData(const std::string &ref, const storm::expressions::Expression &expr_v, const ExprType &expr_t)

Appends initialization data to the plugin instance.

Parameters:

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

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

  • expr_t – The type of the value in the configuration parameter.

const smc_verifiable_plugins::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 &expr_v, const ExprType &expr_t)

Appends input data to the plugin instance.

Parameters:

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

  • expr_v – The expression to assign to the input data.

  • expr_t – The type of the expression 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.

void assignConstantValues(const std::map<storm::expressions::Variable, storm::expressions::Expression> &user_constants)
std::unique_ptr<smc_verifiable_plugins::SmcPluginBase> generatePluginInstance() const

Generate a plugin instance related to the loaded plugin information.

Public Static Functions

static ExprType getExprType(const std::string &type_str)