Library Extensions by C++ Plug-Ins

Extending libFAUDES by a C++ plug-in in general involves

The overall procedure involves some effort, but we feel it provides a good trade-off in that it makes additional functions easily accessible to a broader audience. However, run-time interface, user reference and luabindings are optional features and one may very well restrict a plug-in to a plain C++ implementation of data-types and algorithms.

We give a walk-through to the above steps by the example plug-in.

Relevant Files

The standard library distribution comes with a number of plug-ins, including the example plug-in. The latter integrates an alternative accessibility function AlternativeAccessible() into libFAUDES and is meant as a template for your own plug-in. The example plug-in directory is organized as follows:

example -+- README                            short overview on purpose of this plug-in
         +- Makefile.plugin                   makefile to integrate this plug-in with the build system
         +- src --+- pex_altaccess.h          declaration of function AlternativeAccessible()
         |        +- pex_altaccess.cpp        definition of function AlternativeAccessible()
         |        +- pex_include.h            header to include all other headers of this plug-in
         |        +- doxygen/faudes_images    images for doxygen documentation
         |        +- registry/pex_*.rti       run-time interface definitions, see below
         |        +- registry/example_*.fref  run-time interface documentation, see below
         |        +- registry/pex_interface.i SWIG interface, see below
         +- Makefile.tutorial                 extra dependencies for this plug-in's tutorial
         +- tutorial +- pex_tutorial.cpp      mini application to illustrate intended usage
                     +- data -+- *            input data to run tutorial with       
                              +- *.prot       reference protocol, see below

The directory name implicitly defines the libFAUDES plug-in name i.e. example. Furthermore, all source files start with a common prefix, i.e. pex_, in order to avoid confusion with other plug-ins.

Algorithm Implementation

The example algorithm to implement converts a given generator to an accessible generator without affecting the closed and marked languages. This is done by removing all states that cannot be reached from any initial state. For the below generator G, the states to remove are labelled 7, 8 and 9.

The proposed implementation in src/pex_altaccess.cpp is organized in two stages

void AlternativeAccessible(vGenerator& rGen) {
  // create a todo stack for state indices
  std::stack<Idx> todo;
  // create an empty StateSet for the set of accessible state
  StateSet accessible_states;
  // iterator for a StateSet
  StateSet::Iterator sit;
  // initialize the algorithm by pushing all initial states on the todo stack
  for (sit = rGen.InitStatesBegin(); sit != rGen.InitStatesEnd(); ++sit) {
  // process the todo stack until it's empty
  while (not todo.empty()) {
    // get and delete the next state index from the todo stack
    const Idx current =;
    // insert the current state in the set of accessible states
    // create transition iterator for the states of the current state
    TransSet::Iterator tit = rGen.TransRelBegin(current);
    TransSet::Iterator tit_end = rGen.TransRelEnd(current);
    // push successor states ton todo stack if not already discovered
    while (tit != tit_end) {
      if (not accessible_states.Exists(tit->X2)) {
  // delete the states and transitions which are not accessible
  rGen.DelStates(rGen.States() - accessible_states);

The function starts by setting up required data structures. These consist of a todo stack and a so-called StateSet, which is the FAUDES implementation of a container to hold a set of unique states. Then all initial states are pushed on the to-do stack as they are reachable by definition. The main processing is done by removing the current top element of the to-do stack, storing this state in the set of accessible states and following all transition paths that lead from this state to an unprocessed state. At last the non-accessible states and the transitions leading to these states are removed by calling a single operation on the set difference of the automaton's states and the accessible states.

As it can be seen, the algorithm is implemented by using abstract data-types from either the C++ standard library or from the FAUDES library. In particular, it does not depend on the internal data structure of the Generator class.

Doxygen Documentation

The build system runs doxygen on all *.cpp and *.h files in the make search path and thus includes the plug-in sources to the doxygen documentation. By convention, the overall include file of each plug-in is used to give an overview, perhaps including key functions and data-types as well as licensing and copyright information. Provided the all further plug-in source code complies with doxygen documentation comments, all relevant functions will nicely appear in the libFAUDES C++ API reference.

For the example plug-in overview, we add a doxygen section to pex_include.h and define it to belong to the doxygen group AllPlugins:

@defgroup ExamplePlugin Example Plugin

@ingroup AllPlugins

@section Overview

This example demonstrates the libFAUDES plug-in mechanism and  
may serve as a template for setting up ... etc.

@section License

The example plug-in is distributed with libFAUDES and under the terms of
the LGPL.

@section Contents


We document our add-on function in pex_altaccess.h by a technical description. We also tag the function to be a member of the doxygen group ExamplePlugin, such that it will appear in our overview section Contents. The macro FAUDES_API expands to a platform dependent directive to share the symbol for dynamic linking.

 * Alternative accessibility algorithm. 
 * We use the alternative accessibility algorithm from tutorial 6 
 * for our example plug-in. The implementation uses a to-do stack ... etc.
 * <h4>Example:</h4>
 * <table width=100%> 
 * <tr>
 * <td> @image html pex_g_notacc.png </td>
 * </tr>
 * </table>
 * @param rGen
 *   Input generator
 * @ingroup ExamplePlugin 
 extern FAUDES_API void AlternativeAccessible(vGenerator& rGen);

Note that the above doxygen documentation refers to an image file, namely pex_g_notacc.png. You are meant to supply the file in the source directory .plugins/example/src/doxygen/faudes_images. Since the build system merges all image files to one destination directory, the plug-in prefix pex_ is essential. It is good practice to provide a tutorial that actually produces any example data, incl. images files.


Each plug-in is meant to provide a number of small C++ applications that demonstrate the intended usage of the implemented C++ API and to document test cases. Tutorials are located in example/tutorial/.

 * @file pex_tutorial.cpp  
 * Tutorial, example plug-in. More text ...
 * @ingroup Tutorials
 * @include pex_tutorial.cpp

#include "libfaudes.h"

int main() {

  // Apply algorithm to provided input data
  Generator gen("data/g_notacc.gen");

  // Record test case
  FAUDES_TEST_DUMP("test alt access",gen)

  // Validate result

  return 0;

Makefile. Dependencies to build the tutorials are included by Makefile.plugin from Makefile.tutorial. The latter must be set up accordingly to integrate the tutorial with the libFAUDES build system.

Doxygen. Tutorial code is listed in the C++ API reference, Section see Tutorials. This is achieved by specifying the source of each tutorial to be in group @ingroup Tutorials.

File-I/O. By convention, any input data is provided in the directory example/tutorial/data. For tutorials that generated file output, such files should either be named tmp_* or placed in example/tutorial/results/*, in order to facilitate clean-up by the build system.

Test cases. The above example uses the macro FAUDES_TEST_DUMP(m,d) to record the correct behaviour for later validation. The file name of the protocol is set to a mangled version of the tutorial source with prefix tmp_ and suffix .prot, e.g. tmp_pex_example_cpp.prot. Once the routine is considered correct, the proposed procedure is to rename the protocol by dropping prefix tmp_ and to use it as reference henceforth. The macro FAUDES_TEST_DIFF() will exit the tutorial on differences between the reference protocol and the actual protocol. The main Makefile provides a target test that scans all tutorials for reference protocols and performs the respective validation.


The libFAUDES main makefile copies headers to the libFAUDES include directory, compiles sources to objects and, finally, links objects to obtain the libFAUDES library and utility executables. While processing the main makefile, the build system includes plugins/example/Makefile.plugin. The latter extends the variables SOURCES, OBJECTS, and HEADERS in order to indicate additional targets. It also extends the make search path VPATH. The example Makefile.plugin is organized as follows:

1. Define relevant paths and source files.

Note that we only use variables with prefix PEX in order to avoid confusion with variables in the main makefile.

# Relevant paths
PEX_NAME   = example
PEX_BASE   = ./plugins/$(PEX_NAME)
PEX_SRCDIR = ./plugins/$(PEX_NAME)/src

# List source files
PEX_CPPFILES = pex_altaccess.cpp
PEX_INCLUDE = pex_include.h

# Generate paths 
2. Contribute to auto-generated header files.

Applications that use libFAUDES are meant to include all relevant headers by the #include "libfaudes.h" directive. This in turn includes the auto-generated files include/allplugins.h and include/configuration.h. They list include directives for all activated plug-ins and define run-time behaviour macros, respectively.

The example plug-in requires pex_include.h to be registered with allplugins.h and adds the macro FAUDES_PLUGIN_EXAMPLE to configuration.h.

# Append my overall include file to libfaudes.h
	cp -pR $< $@
	echo "#include \"$(PEX_INCLUDE)\"" >> $(INCLUDEDIR)/allplugins.h
	echo "/* example plugin configuration */" >> $(INCLUDEDIR)/configuration.h
	echo "#define  FAUDES_PLUGIN_EXAMPLE" >> $(INCLUDEDIR)/configuration.h
	echo " " >> $(INCLUDEDIR)/configuration.h
3. Advertise plug-in to the libFAUDES build system.

This includes all additional sources, headers and objects. The variable VPATH directs the make tool to find sources when resolving (implicit) rules.

# Advertise plug-in to libFAUDES build system

Run-Time Interface

libFAUDES provides a registry for data-types and functions as a basis for applications that transparently pass on libFAUDES extensions to the user; see C++ API, Section RTI, for technical details. The build system tries to minimise the effort that is required for a plug-in to participate in this optional feature.

The example plug-in provides only one function, which is registered via the XML file src/registry/pex_definitions.rti:

<?xml version="1.0" encoding="ISO-8859-1" standalone="no"?>
<!DOCTYPE Registry SYSTEM "registry.dtd">

<FunctionDefinition name="Example::AltAccessible" ctype="faudes::AlternativeAccessible"> 

<Documentation ref="example_index.html"> 
Alternative implementation to remove inaccessible states  and related transitions.
Example       reachability  reachable     accessible    

<Signature name="Default"> 
<Parameter name="Gen" ftype="Generator" access="InOut"/> 



The above token stream declares a function from the plug-in Example with name AltAccessible to be implemented by the C++ function faudes::AlternativeAccessible. It gives a short description and a reference to a more detailed HTML documentation. It is up to you whether you design one document per function or whether you collect groups of related functions.

By convention the list of keywords establishes a two level hierarchical structure, where the first keyword specifies a section and the second keyword specifies a subsection. It is mandatory to provide section index pages following the naming convention sectionname_index.fref, i.e. example_index.fref for the example plug-in. In most cases, the first keyword aka the section name will coincide with the plug-in name. Advanced applications may use additional keywords when implementing a search by keyword.

Regarding signature(s), the libFAUDES run-time interface imposes the following restrictions:

Of course, any referenced HTML documentation must be provided. For convenience, the build-system pre-processes any documentation by the tool ref2html (provided with libFAUDES). The example plug-in is fine with one page of documentation only, as given in the below src/registry/example_index.fref.

<ReferencePage chapter="Reference" section="Example" page="Index" title="Example PlugIn">

<h1>Example PlugIn</h1>

Example plug-in for demonstration purposes [...]

The example plug-in addresses developers [...]

<ffnct_reference name="AltAccessible">
The function AltAccessible [...] 
Arguments must be such that [...] 



The special markup ReferencePage, ffnct_reference, fdetails and fconditions are used by the build-system to fill in appropriate headings and signature information. For more details and recommendations regarding the organisation of HTML documentation, see the build-system documentation.

The libFAUDES build system expects run-time interface files to be advertised via Makefile.plugin. For our example plug-in, we announce one *.rti file and one *.fref file by appending the following lines to Makefile.plugin:

# advertise rti defs
PEX_RTIDEFS = pex_definitions.rti
PEX_RTIFREF = example_index.fref

PEX_RTIHTML := $(PEX_RTIFREF:%.fref=%.html)


To trigger the re-build of the RTI registry, run the main makefile with targets make rti-clean and make rti-prepare.


The build system tries to minimise the effort that is required to access additional functions via luafaudes. It does so using the tool SWIG to automatically convert so called interface definitions to C wrapper code; see

The libFAUDES build system expects interface files to be advertised via Makefile.plugin. For our example plug-in, we announce one SWIG module and one interface file by appending the following lines to Makefile.plugin:

# advertise luabindings
LBP_INTERFACES += $(PEX_SRCDIR)/registry/pex_interface.i 

Note the prefix LBP that refers to the luabindings plug-in.

The actual interface pex_interface.i file resides in the example plug-in:

// Set SWIG module name
// Note: must match libFAUDES plug-in name
%module example

// Indicate plugin to rti function definitions
#ifndef SwigModule
#define SwigModule "SwigExample"

// Load std faudes interface
%include "faudesmodule.i"

// Extra Lua functions: copy to faudes name space
%luacode {
-- Copy example to faudes name space
for k,v in pairs(example) do faudes[k]=v end

// Add topic to mini help system
SwigHelpTopic("Example","Example plug-in function");

// Include RTI generated functioninterface 
#if SwigModule=="SwigExample"
%include "../../../include/rtiautoload.i"

Since our plug-in provides only functions that are registered with the run-time interface, the interface file in this case is just a skeleton. The build system will fill in our function by generating the file include/rtiautoload.i.

It is good practice to supply comprehensive Lua scripts in the tutorial directory that illustrate the intended usage of the plug-ins data-types and functions.

To trigger the re-build of luabindings, run the main makefile with targets make luabindings-clean and make luabindings-prepare. The libFAUDES archive provides a copy of SWIG for convenience, however, installation is required.

libFAUDES 2.29d --- 2019.12.01 --- with "synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-pushdown-timed-simulator-iodevice-luabindings"