Reference

Special Features

SMC Plugins

With SMC Storm, we introduce the possibility of having specific actions that are mapped to external plugins, that can be defined using C++, instead of programming them in the JANI format.

Plugins can be developed using the SmcPluginBase class provided in the smc_plugins package.

JANI models making use of plugins, can be executed only by means of its custom cache-less states expansion modality (using the –disable-explored-states-caching flag). Additionally, the paths to the folders containing all required plugins shall be provided when invoking SMC Storm (using –plugin-paths).

Here an example for verifying the plugin-based model called sum_dice_throws_plugins.jani using smc_storm:

smc_storm --model sum_dice_throws_plugins.jani --properties-names sum-to-nine-in-three --show-statistics --plugin-paths \<path-to-smc_storm-lib-folder\>,\<path-to-smc_plugins-lib-folder\> --disable-explored-states-caching

In order to develop a model that makes use of plugins, a specific plugins entry needs to be provided in the JANI file. Its JSON-schema is provided below:

schema({
"plugins": Array.of(
    {
        "plugin_id": String,                    // Name of plugin to load, related to the plugin implementation
        "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
        }),
    }),
})

In smc_storm we enforce that the edges associated to the plugins contain only the target locations. No assignment is allowed in the JANI edges associated to a plugin.