Developing PLCverif plug-ins

This section describes the common concepts and aspects of plug-in development for PLCverif. This includes plug-ins providing jobs, language frontends, reductions, but also the plug-ins extending the verification job, such as reporting and verification back-end plugins.

[info] Eclipse plug-ins vs. PLCverif plug-ins

Note that the term plug-in indicates in general an OSGi bundle in the Eclipse universe, i.e., a bunch of code with a defined life-cycle. A plug-in may implement several extensions to extension points. We will refer specifically as PLCverif plug-in to an Eclipse plug-in (OSGi bundle) that implements at least one extension that is defined by PLCverif. Where it does not cause confusion, we may refer to a PLCverif plug-in simply as plug-in. If we need to emphasize the difference, we may refer to an OSGi bundle as Eclipse plug-in.

The concrete extension points where new plug-ins can increase the feature set of PLCverif are described in the next section.

[info] Extensions vs. extension points

In the Eclipse universe an extension point is a defined interface to provide a certain functionality. The implementation of this interface is a so-called extension.

[info] Activating a new plugin

After a new PLCverif plug-in is created it has to be activated before it is used in the product. This is done by adding the plugin to the relevant feature.xml file.

  • Example: To activate a newly created cern.plcverif.libary.backend.<plugin_name>.gui plugin, add it to the cern.plcverif.library.gui.feature.

Common features of the PLCverif plug-ins

In order to create a new PLCverif plug-in, at least the following steps are required:

  • Define extension. Create a new Eclipse plug-in which implements an OSGi extension to the extension point that is desired to be extended. By convention, these extension points are defined in the cern.plcverif.*.extensions plug-ins.
  • Create factory class. The PLCverif extension points require some metadata (depending on the extension points) and a factory implementation (client). This factory implementation will be used to instantiate and configure the concrete worker class instances.
    • The interfaces that these client classes shall implement are typically named as IXxxxxxExtension (where Xxxxxx depends on the extension point).
    • These interfaces typically contain the following three methods to be implemented:
      • createXxxxxx(): it is expected to create a non-configured worker class instance. That worker class is typically expected to implement the IXxxxxx interface. This method is to be used by external tools building on top of PLCverif which prefer to configure the extension directly and not via settings. This type of configuration may not be supported by all the extensions.
      • createXxxxxx(SettingsElement): it is expected to create a pre-configured worker class instance. The given settings element describes the subtree of the settings node tree which corresponds to the current extension. The settings element may not define all settings of the extension.
      • fillSettingsHelp(SettingsHelp): this method should describe itself and all its settings via the given SettingsHelp object.
    • Typically a unique textual identifier (command ID, cmd_id) is required to be defined in the extension too. This will be used to identify the PLCverif plug-in. Note that this command ID should be unique across all plug-ins as this will be used to identify the corresponding installation-specific settings too (it will be located in the settings/<cmd_id>.settings file).
  • Create worker class. The factory class (implementing IXxxxxxExtension) described above needs to create worker classes (implementing IXxxxxx). These classes need to implement various methods depending on the functionality they need to provide.
    • Typically, these worker classes shall have a constructor that takes a SettingsElement object. The factory class' IXxxxxxExtension.createXxxxxx(SettingsElement) implementation typically calls that constructor and returns the created object.
    • These worker classes are expected to implement a retrieveSettings() method that returns a SettingsElement object. This settings element should describe all the settings that were used in the execution of the functionality provided by this PLCverif plug-in. Note that this is not simply about returning the object that was given to the createXxxxxx(SettingsElement)! The returned settings subtree should contain all implicit settings as well, including plug-in defaults and installation-specific settings. This is important in order to be able to reproduce each execution. See the subsection on Types of settings to understand the different types of settings and their priorities.

GUI plug-ins

If all the above is done, the feature provided by the newly created PLCverif plug-in can be used. However, if a GUI representation is desired as well, another plug-in providing extension for another extension point is needed as well. Each job may define their own ways to extend the graphical representation depending on their needs. As it is expected to be the most common job, we describe here how to create a GUI extension for the verification job, i.e., for the verification case editor.

  • Define extension. Create a new Eclipse plug-in which implements an OSGi extension to the cern.plcverif.verif.extensions.gui.part extension point, independently from which type of PLCverif plug-in is to be represented.
    • class: the class that will implement the IVerifGuiPartExtension interface
    • settings_node: the settings node this extension represents. This is always job.backend for the verification backends.
    • settings_value: the same as cmd_id for the other plug-in (the unique command ID that will identify this backend)
    • label: human-readable name of this plug-in that will be shown on the GUI
    • priority: relative importance of the plug-in. Will be used to order the items of the backend selection. Plug-ins with lower priority numbers will be closer to the top of the list.
    • Create factory class. Implement the IVerifGuiPartExtension interface in a class. This factory will have to create the panel for a a given form. This class should be the one set for class above. When the createPart method is called by PLCverif, the parent composite, the parent data binding, the verification case context (that contains information about the model to be verified) and the installation-specific settings of this plug-in (if available) are passed as parameters.
    • Create worker class. Implement the IPvGuiPart<VerificationCaseContext> interface. This will represent a panel that will be included in the parent form. In its createPart the SWT GUI objects and the data bindings shall be created. The parent composite and the parent data binding (corresponding to the job.backend settings node) will be passed to IVerifGuiPartExtension.createPart, which is expected to pass this on to the IPvGuiPart.createPart.

Preference page. Each plug-in may have installation-specific settings. These are backed by settings files. If desired, a GUI can be provided for these settings too which will be shown in the Preferences window. In order to create a preferences page, follow the steps above.

  • Add dependencies. Add org.eclipse.ui and cern.plcverif.base.gui to the plug-ins dependencies.
  • Create preference page class. Create a class implementing the IWorkbenchPreferencePage interface. Typically it is a good idea to extend the FieldEditorPreferencePage abstract class.

    • The init(IWorkbench) method should set the preference store using the setPreferenceStore() method. For installation-specific PLCverif settings the settings store should be created using the SettingsPreferenceStoreFactory.createStore(String, SettingsElement) method, where the first argument is the command ID of the plug-in, the second argument is the default settings to be used in the store.

      • If the plug-in has defaults both in the specific settings and in a settings file, the SettingsPreferenceStoreUtil.mergePluginSettings can be used to merge those.
      • If the plug-in's default settings are all defined in the descendant of the specific settings (as initial values for the fields), it is enough to convert a new instance of the specific settings class to generic settings using SpecificSettingsSerializer.toGenericSettings().

      Example.

          @Override
          public void init(IWorkbench workbench) {
              try {
                  Settings defaultSettings = SpecificSettingsSerializer.toGenericSettings(new DummyBackendSettings());
      
                  setPreferenceStore(SettingsPreferenceStoreFactory.createStore(DummyBackendExtension.CMD_ID,
                          defaultSettings.toSingle()));
              } catch (IOException | SettingsParserException | SettingsSerializerException e) {
                  throw new RuntimeException(e); // NOPMD
              }
          }
      
    • The createFieldEditors() should create the field editors using the addField() method. The parent composite can be accessed via the getFieldEditorParent() method.

      Example.

      @Override
      protected void createFieldEditors() {
          final Composite parent = getFieldEditorParent();
      
          addField(
               new RadioGroupFieldEditor("result", "Desired verification result", 1,
                  new String[][] { 
                      { "Satisfied", ResultEnum.Satisfied.name() },
                      { "Violated", ResultEnum.Violated.name() },
                      { "Unknown", ResultEnum.Unknown.name() },
                      { "Error", ResultEnum.Error.name() }},
                  parent));
      }
      
  • Create extension. Register the created preference page in the plugin.xml by creating an extension for the org.eclipse.ui.preferencePages extension point.

    • The class should be the newly created preference page class.
    • The name will determine the page name in the Preferences window.
    • The category shall be cern.plcverif.base.gui.preferences.rootpage in order to show the page under the PLCverif category.
    • The id can be any unique identifier, for example the FQN of the implementing class.

    Example.

    <extension
            point="org.eclipse.ui.preferencePages">
        <page
            category="cern.plcverif.base.gui.preferences.rootpage"
            class="com.dummy.plcverif.backend.gui.DummyBackendPreferencePage"
            id="com.dummy.plcverif.backend.gui.DummyBackendPreferencePage"
            name="Dummy Backend">
        </page>
    </extension>
    
  • The modification of the installation-specific settings should now be reflected by the settings file located at settings/<cmd_id>.settings.

Settings handling

When PLCverif is executed, this PLCverif execution is described by a settings tree that contains all the necessary settings. The subtree of this relevant to a given a PLCverif plug-in are passed to it in the IXxxxxxExtension.createXxxxxx. This needs to be merged with the plug-in's default settings and the installation-specific settings. The final, effective settings shall be made available via the IXxxxxx.retrieveSettings() method.

The suggested way to handle the settings is via the specific settings, which allows automated parsing, serialization and help generation via the defined annotations. Here are the typical steps to implement settings handling in a PLCverif plug-in based on specific settings:

  • Create a create a specific descendant of the AbstractSpecificSettings class to represent the settings of the plug-in.

    • The annotations that can be used in this class are described here.

      Example.

         public class DummyBackendSettings extends AbstractSpecificSettings {
             @PlcverifSettingsElement(name = "result",
                 description = "The verification result to be given by the dummy backend.",
                 mandatory = PlcverifSettingsMandatory.OPTIONAL)
             private ResultEnum result = ResultEnum.Violated;
      
             public ResultEnum getResult() {
                 return result;
             }
         }
      
  • The settings passed by PLCverif need to be parsed on the constructor of the IXxxxxx implementation, which will receive the settings passed to the IXxxxxxBackend.createXxxxxx(SettingsElement).

    Example.

      public DummyBackend(SettingsElement settings) {
              try {
                  this.settings = SpecificSettingsSerializer.parse(settings, DummyBackendSettings.class);
              } catch (SettingsParserException e) {
                  throw new PlcverifPlatformException("Unable to parse the settings of the Dummy backend.", e);
              }
          }
    
  • The IXxxxxx.retriveSettings shall return the settings actually used for the verification, including the eventual plug-in-default settings which were not included in the settings passed to the constructor (i.e., don't just return the object which was passed to the constructor).

    Example.

      @Override
      public SettingsElement retrieveSettings() {
          try {
              return SpecificSettingsSerializer.toGenericSettings(this.settings);
          } catch (SettingsParserException | SettingsSerializerException e) {
              throw new PlcverifPlatformException("Unable to serialize the settings of the Dummy backend.", e);
          }
      }
    
  • If all settings are represented by annotated fields in the above way, the help can be automatically generated based on the annotations in the IBackendExtension.fillSettingsHelp method.

    Example.

      @Override
      public void fillSettingsHelp(SettingsHelp help) {
          help.addPluginDetails(CMD_ID, "Dummy backend implementation", DummyBackendExtension.class);
    
          SpecificSettingsSerializer.fillSettingsHelp(help, DummyBackendSettings.class);
      }
    

results matching ""

    No results matching ""