Develop your plugins

Import this package in your project

In case you want to develop your own plugins, or add support for plugins in your model checker, you will need to make a new plugin class inheriting from the base class SmcPluginBase, available here <https://github.com/convince-project/smc_verifiable_plugins/blob/main/include/smc_verifiable_plugins/smc_plugin_base.hpp>_.

This can be achieved either by automatically fetching this package in your CMake project (recommended) or by building this package on your machine.

Fetch this package in CMake

In the CMakeLists.txt file related to your project, you can add the following snippet to automatically download this package and make it available:

FetchContent_Declare(
    smc_verifiable_plugins
    GIT_REPOSITORY https://github.com/convince-project/smc_verifiable_plugins
    GIT_TAG 0.0.1
)
FetchContent_MakeAvailable(smc_verifiable_plugins)

At this point, for each executable and library that needs to use this library, you can add the dependency to this package:

add_library(<your_plugin_name> SHARED <related-src-files>)
target_link_libraries(<your_plugin_name> PUBLIC smc_verifiable_plugins <other-dependencies>)

Installing the package locally

Alternatively, if you want to install the package locally, you have to first build this package:

cd <path-to-this-repo>
mkdir build
cd build
cmake .. -DCMAKE_BUILD_TYPE=Release && make -j4

And, in the project depending on this library, do the following:

find_package(smc_verifiable_plugins REQUIRED)

add_library(<your_plugin_name> SHARED <related-src-files>)
target_link_libraries(<your_plugin_name> PUBLIC smc_verifiable_plugins <other-dependencies>)

Develop your plugin

Let’s look at how to develop a simple SMC Plugin by looking at the exemplary plugin <https://github.com/convince-project/smc_verifiable_plugins/blob/main/plugins/include/int_accumulation_smc_plugin.hpp>_ IntAccumulationSmcPlugin provided in this package.

#pragma once
#include "smc_verifiable_plugins/smc_plugin_base.hpp"
#include <vector>

namespace smc_verifiable_plugins {

class IntAccumulationSmcPlugin : public SmcPluginBase {
public:
    IntAccumulationSmcPlugin();

    ~IntAccumulationSmcPlugin();

    std::string getPluginName() override {
        return "int_accumulation_smc_plugin";
    }

private:
    void processInitParameters(const DataExchange& config) override;

    DataExchange processReset() override;

    DataExchange processInputParameters(const DataExchange& input_data) override;

    int64_t _current_state = 0U;
    const std::string _input_label;
    const std::string _output_label;
};
}  // namespace smc_verifiable_plugins

The first thing to notice is that we included the base class SmcPluginBase header file, and we inherited the new plugin from there.

Additionally, we declared the constructor, destructor and, more importantly, the getPluginName, processInitParameters, processReset and processInputParameters methods, that are overriding the ones from the base class.

In general, these methods are everything there is to be developed when making a new plugin.

The DataExchange type

This type is the communication interface between a model checker and a plugin.

It consists of a std::unordered_map<std::string, std::variant<int64_t, double, bool>>, that serves as a map between a label and a value, that can be either an integer, a real or a boolean value.

The methods to override

getPluginName

This function returns a string, telling the name of the plugin. This needs to match with the library name defined in CMake.

processInitParameters

This method is in charge of configuring the specific instance of the plugin.

In this example, we expect that no configuration parameter is defined, so our method will look like this:

void IntAccumulationSmcPlugin::processInitParameters(const DataExchange& config) {
    if (!config.empty()) {
        throw std::invalid_argument("Invalid configuration provided. Expected no params.");
    }
};

but one could, for example, configure a max. bound for the accumulated value, or add a configuration to always consider the absolute value, or more sophisticated things, depending on the application.

processReset

This method is executed each time we want to start a new simulation (or trace) in the model checker, and therefore we need to reset the model to its initial state. This must affect also the plugin’s output variables, therefore we need to return a DataExchange variable.

For our example, we want the accumulated value to be reset to its initial value, that is 0, and then report this as a return value:

IntAccumulationSmcPlugin::DataExchange IntAccumulationSmcPlugin::processReset() {
    _current_state = 0U;
    return {{_output_label, _current_state}};
}

processInputParameters

The last method we need to implement, is the one processing an input and providing the resulting output.

The amount of output variables provided by this method and the processReset one should match.

In this example, all we want is to read the input value, sum it to the internal accumulated value and return that sum in the output variable.

This is achieved with the following snippet:

IntAccumulationSmcPlugin::DataExchange IntAccumulationSmcPlugin::processInputParameters(const DataExchange& input_data) {
    if (input_data.size() != 1U && !input_data.contains(_input_label)) {
        throw std::invalid_argument("Invalid input provided. Expected only one integer.");
    }
    _current_state += std::get<int64_t>(input_data.at(_input_label));
    return {{_output_label, _current_state}};
}

Generate the plugins’s loader

The last thing to do, is to call the GENERATE_PLUGIN_LOADER macro, to generate the function used to load the plugin at runtime.

In this case, it looks like this:

GENERATE_PLUGIN_LOADER(IntAccumulationSmcPlugin);

The definition of this macro can be found in the utils.hpp file <https://github.com/convince-project/smc_verifiable_plugins/blob/main/include/smc_verifiable_plugins/utils.hpp>.