This package provides the base class and examples to develop plugins useable for Statistical Model Checking, that can be integrated into formal models for verifying them using smc_storm.

SMC plugins have to develop two operations:

• reset: Set the plugin to its initial state.
• step: Advance the automaton to its next state.

In smc_storm we implemented an extension of the JANI format to load SMC plugins and advance their state each time a specific action-name from a specific automaton is executed.

An exemplary SMC plugin is provided here, together with its header class. In the following section, we provide an explanation of how a new SMC plugin can be developed.

All plugins are expected to inherit from the SmcPluginBase class provided here.

For each new SMC plugin class, the following methods need to be overridden:

• getPluginName: Method that returns the name of the plugin instance.
• processInitParameters: Method to process the configuration parameters, required to set each new plugin object instance.
• processReset: Method to set the plugin instance to its initial state.
• processInputParameters: Method to process the input parameters provided to the plugins, and step the SMC plugin object to its next state.

Plugins can be loaded by using the function loadSMCPlugin(plugin_folder, plugin_name) from the utils.hpp file. This executes the following steps:

• Generate a path to the SMC plugin's binary file, based on the provided plugin_folder and plugin_name.
• Generate a new object instance by running the getSMCPlugin() function in the loaded library.
• Store the new object in a std::unique_ptr and return it.

The getSMCPlugin() function is a C extern function that must be provided in each plugin library:\n in the utils.hpp file we provide the macro smc_verifiable_plugins::GENERATE_SMC_PLUGIN_LOADER that can generate such a function.

An exemplary use of this function can be found at the end of this exemplary SMC plugin.

Once this library is built, it can be loaded from any other CMake project by using the find function. Afterwards, new plugin libraries can be obtained using CMake's add_library function:

find_package(smc_verifiable_plugins REQUIRED)
...
# Generate the library associated to the plugin "new_plugin_name"
add_library(new_plugin_name SHARED path_to_plugin_folder/new_plugin_name.cpp)
target_include_directories(new_plugin_name PUBLIC ${smc_verifiable_plugins_INCLUDE_DIR})

It is important to ensure that the name of the plugin (from the getPluginName method) and the name of the library are matching: this constraint comes from the loadSMCPlugin function mentioned in the previous section.

When associating SMC plugins to JANI, we need to define when the plugin instance needs to be updated, and how it is parametrized.

In SMC Storm, we extended the JANI format to be able to load plugins, and get their next state each time a specific automaton's action-name is executed.

SMC plugins can be configured in the plugins section of the JANI file. The related JSON-Schema is provided below, and shows the fields required to instantiate a single SMC plugin:

schema(
  "plugins": Array.of(
    {
        "plugin_id": String,                    // Name of plugin to load
        "automaton_id": String,                 // Name of the automaton associated to the plugin
        "action_name": String,                  // Name of the action in the automaton that advances the plugin to the next step
        "init": Array.of(                       // Configuration (constant) parameters for initializing the plugin
        {
            "name": String,                     // Name of the init config param to configure in the plugin
            "type": ("int", "bool", "real"),
            "value": (int, bool, real)
        }),
        "input": Array.of(                      // Definition of what to provide as input to the plugin
        {
            "name": String,                      // Referring to plugin's internal names
            "type": ("int", "bool", "real"),
            "value": Expression                 // Value passed to the plugin: any valid JANI Expression works
        }),
        "output": Array.of(
        {
            "ref": String,                      // Referring to the JANI variable storing the output value
            "value": String                     // Referring to the plugin's internal name
        }),
    })
)

To use this package, it is enough to build it. It will be exported automatically in the cmake user configuration, so that it can be found using CMake's find(smc_verifiable_plugins REQUIRED) macro. After running that macro, the variable smc_verifiable_plugins_INCLUDE_DIR with the path to the include folder, and the variable smc_verifiable_plugins_PLUGINS_PATH with the path to the library folder, will be provided, and can be used to locate the existing plugins' libraries.

The following steps are necessary to build the package:

cd smc_verifiable_plugins
mkdir build
cd build
cmake .. -DCMAKE_BUILD_TYPE=RelWithDebInfo && make -j8

Optionally, to ensure the build was successful, the tests can be executed:

ctest