PLASMA Lab book

Plugins

There are two types of plugins, Simulator and Checker. Both follow the same structure, the difference being in their purpose, thus the interfaces implemented by Simulator/Checker classes. A plugin is build around two main classes: a Factory, and a Model/Property class.

Note: There is a strong relation between Simulator and Model (resp. Checker and Property). A Simulator will execute a Model (resp. check). In the PLASMA Lab architecture, they are regrouped under the same object, heriting from AbstractModel (resp. AbstractRequirement). A Model (resp. Property) will execute (resp. verify) itself.

But we make a distinction between the Simulator/Model (resp. Checker/Property) and the textual content, the model (resp. property).

Both type of plugins are closely related since they are supposed to be complementary. Given a model, the Simulator will generate execution traces of various length. These traces will then be checked against a set of property by the Checker.

Factory

The Factory can be seen as the plugin entry point. It implements methods to retrieve the plugin’s name and description. But its main task is to instantiate the class which is implementing the Simulator or Checker interface. Factories implement the AbstractModelFactory or AbstractRequirementFactory interfaces, both inherits from the AbstractDataFactory.

PLASMA Lab plugin system use the Java Simple Plugin Framework. To load a plugin, the class must implement the Plugin interface and have the tag @PluginImplementation before the class declaration.

More details aswell as a 5min tutorial can be found on their website:

Algorithm

Algorithms were designed to use the plugin framework too but this possibility wasn't implemented. Although they aren't a plugin per se, algorithm factories implement the Plugin interface and are registered in the PluginLoader.