Lua-extensions provide a light-weight mechanism to extend libFAUDES by functions implemented as luafaudes scripts. This libFAUDES distribution includes the following lua-extensions:

FaultTolerantControl Functions related to fault-accommodating control and fault-hiding control reconfiguration, including construction procedures for fault-accommodating models of sensors and actuators.

As with C++ plug-ins, lua-extensions are transparently passed on to any application that interfaces to libFAUDES via the run-time-interface, e.g., luafaudes or DESTool. Extension developers can advertise their functions by end-user documentation that seamlessly integrates with the libFAUDES reference.

Lua-extensions are distributed as single container files (*.flx) for luafaudes function definitions, reference pages, tutorials and validation code. Packaging and installation of lua-extensions is done by the command-line tool flxinstall. In contrast to C++ plug-ins, no external development tools (compilers, etc.) are required.

Installing and Removing Extensions

The standard libFAUDES distribution maintaines extensions in libfaudes/stdflx. To introduce an additional extension, you may copy the respective *.flx-file to libfaudes/stdflx and run flxinstall -i as in the below example. The installation process will generate and distribute relevant files and replace any previously installed extensions. For removal of all extensions from a libFAUDES distribution, run flxinstall -r

Note: By default, flxinstall expects the directory layout of standard libFAUDES distributions, e.g., libfaudes/doc and libfaudes/bin. There are various command-line options to adapt to other targets. For the particular situation of DESTool, the appropriate configuration of flxinstall is conveniently achieved by invoking DESTool with command-line switch -x to launch the extension manager GUI.


To install the example extension extintro.flx from the tutorial, run

> cd ./libfaudes
> cp ./plugins/luabindings/tutorial/extintro.flx ./stdflx/
> ./bin/flxinstall -i ./stdflx ./

Here, the -i switch indicates installation. The following command-line parameters except the last one specify the extensions to install, either individual *.flx files or directories containing *.flx files. The last command-line argument specifies the target directory, i.e., the directory in which the libFAUDES distribution resides.

To remove the example extension extintro.flx, run

> cd ./libfaudes
> rm ./stdflx/extintro.flx
> ./bin/flxinstall -i ./stdflx ./

For removal of all extensions, run

> cd ./libfaudes
> ./bin/flxinstall -r ./

You may inspect the reference documentation (libfaudes/doc/reference/index.html) to verify installation/removal of extensions.

Technical Background

Providing Lua-functions and reference documentation via lua-extensions, the installation process needs to extract sources and integrate them with an existing target libFAUDES distribution. Here, flxinstall relies on certain conventions of the target directory layout. More precisely, the subdirectories libfaudes/doc and libfaudes/bin must be present in the target directory and organized as in the standard libFAUDES distribution.

Regarding Lua-functions, the installation process assembles the file luafaudes.flx and places it in libfaudes/bin next to luafaudes. On startup, luafaudes will automatically load the extension file when present. Extensions typically are set up to produce some diagnostic output. This can be observed with the command-line option -d.

In order to load an alternative extension file (e.g. for testing/debugging) you may run luafaudes with the command-line option -x file.flx, e.g.

> cd ./libfaudes
> ./bin/luafaudes -d -x extension_file.flx

From the Lua-promt, faudes.Help() will list all reference sections, including those introduced by lua-extensions. Thus, for the example extention, faudes.Help("ExtIntro") should list the two functions provided by extintro.flx. Functions provided by extensions can be invoked like any other faudes function.

Technically, lua-extensions can depend on each other, i.e., a function provided by one extension can be invoked from a function provided by another extension. However, the current framework does not address such dependencies explicitly and, for organisational reasons, it is strongly recommended to design extensions to be self-contained.

Creating Extensions: an Example

The below example outlines the .flx-file format and demonstrates how to create a lua-extension. The example comes in two versions, namely the full version extintro.flx (including documentation, tutorial, etc) and a minimal version extintro_minimal.flx. Both files are located in libfaudes/plugins/luafaudes/tutorial. They have been packaged by the tool flxinstall; see below for further details.

Lua-extension files are XML compliant and have the outer tag LuaExtension. As a mandatory attribute, LuaExtension must provide a unique name, ExtIntro for this example. The LuaExtension element must be composed from Lua-function definitions, using tags LuaFunctionDefinition. The latter again must provide a name attribute, where the value must be prefixed with the name of the extension.

<?xml version="1.0" encoding="ISO-8859-1" standalone="no"?>
<!DOCTYPE luaextension SYSTEM "">

<LuaExtension name="ExtIntro">

<LuaFunctionDefinition name="ExtIntro::LargeGenerator">

<LuaFunctionDefinition name="ExtIntro::IsLargeGenerator">

[... more functions, reference documentation, images, tutorials ...]


Optionally, an extension may provide reference documentation, embedded image files, tutorials and a test protocol for validation. The respective sections are illustrated below.

Rather than to set up a lua-extension by hand, it is recommended to maintain the indivdual components in separate files and to use flxinstall for packaging. The example extension extintro.flx was composed by

> cd libfaudes/
> ./bin/flxinstall -c plugins/luafaudes/tutorial/extintro ./stdflx/extintro.flx

The last parameter always specifies the destination .flx-file, to be composed from the specified sources. The tool accepts source files with suffix .rti, .fref, .png, .svg, .jpg, .jpeg, .gen or .lua for lua-function definitions, reference pages, images or tutorials, respectively. The special source data is interpreted as a directory with supporting data files of any type, which will be plain copied to corresponding binary data sections.

For convenience, the specification of exactly one source argument will be interpreted as a source directory that contains source files as decribed above. For the examle, we have the following layout:

extintro -+- islargegenerator.rti            -- function definition
          +- islargegenerator.rti            -- function definition
          +- extintro_index.fref             -- main index of reference
          +- extintro_largegenerator.fref    -- another reference page
          +- extintro_example.lua            -- lua script as a tutorial
          +- extintro_l3gen.png              -- image used in the reference pages
          +- data/*                          -- input data for tutorial

To inspect the contents of an extension file without installing it to libFAUDES, flxinstall can extract its components to any destination directory:

> cd libfaudes/
> ./bin/flxinstall -x plugins/luafaudes/extensions/extintro.flx /tmp/where-ever

Note: The current version of flxinstall maps all filenames to lower case. Thus, when a reference page embeds an image file or when a turorial reads input data, filenames must be specified in lower case. Furthermore, flxinstall is not expected work with non-ASCII filenames. Thus, at the current stage, you are best of in restricting filenames to lower-case ASCII.

Luafaudes functions

LuaFunctionDefinitions must comply with the restrictions and conventions as specified in the C++ API documentation of the luabindings plug-in.

Any documenation URL referenced by a function definition must be provided by the extension. For the example, the extension must provide a reference page extintro_largegenerator.fref, which on installation compiles to the HTML page extintro_largegenerator.html. If an extension does not provide any reference documentation, the install tool flxinstall will automatically generate an index page; here extintro_index.html. In this case, you should refer to extintro_index.html#function_name in the function definition.

<LuaFunctionDefinition name="ExtIntro::LargeGenerator">
<Documentation ref="extintro_largegenerator.html#LargeGenerator"> 
Construct a generator by random.
<Keywords> "ExtIntro" "large generators" "first example" </Keywords>

<Signature name="LargeGen(#Q,#Sigma,GRes)">
<Parameter name="SizeQ"      ftype="Integer"   access="In"/>
<Parameter name="SizeSigma"  ftype="Integer"   access="In"/>
<Parameter name="Res"        ftype="Generator" access="Out" />

% embedded script

-- Define my function (mangled version of variant name)
function faudes.LargeGen_Q_Sigma_GRes(qn,sn,gen)

-- Function reports on execution
faudes.Print(string.format('LargeGenerator(...): qn=%d sn=%d',qn,sn))

-- Declare local variables
local tn,tmax,x1,x2,ev,i

-- Clear result
-- Set events
for i=1,sn do 

-- Set states
for i=1,qn do

-- Set transitions
while tn>0 and tmax>0 do
 if not gen:ExistsTransition(x1,ev,x2) then

-- End of function definition



Reference Pages

Reference pages are formated as the reference pages from the run-time-interface, see also the build system. In the context of lua-extensions, the following conventions apply:

  • the chapter must be set to Reference, i.e. chapter="Reference";

  • the section must match the extension name, here section="ExtIntro";

  • there must be exacly one page with label Index, i.e. page="Index";

When processing the lua-extension, each reference page is extracted to an HTML page. The filename of the page is composed by (1) dropping any preceeding number from the page label, (2) prepending the extension name separated by an underscore, (3) appending the suffix .html and mapping all to lower case. In our example, the two pages are named extintro_index.html and extintro_largegenerator.html. This convention is relevant when referring to the documentation of a function. Note that, if you package your extension with flxinstall, the name of the respective source files do not affect the resulting HTML files.

<ReferencePage chapter="Reference" section="ExtIntro" page="Index" title="LuaExtensions - Introduction">
<h1> LuaExtensions - Introduction </h1>
Lua-extensions provide a light-weight mechanism to extend libFAUDES
by functions implemented as luafaudes scripts. 


We give some references to Lua related literature.

<fliterature name="L1">
<fauthors>R. Ierusalimschy, L.H .de Figueiredo, W. Celes</fauthors>
<ftitle>Lua 5.1 Reference Manual</ftitle>
<fjournal><a href=""></a>, ISBN 85-903798-3-3</fjournal>


For literature references, as in the above example, care must be taken to avoid conflicts. The extension name as a prefix is better idea than just a single letter.

<ReferencePage chapter="Reference" section="ExtIntro" page="1_LargeGenerator" title="LuaExtension - Large Generators">
LuaExtension - Large Generators

<ffnct_reference name="LargeGenerator">
The function <ffnct>LargeGenerator</ffnct> sets up a generator by random,
where the number of states and the number of events are specified as parameters.
This function is expected to be completely useles, except for demonstration


Result for <fimath>qn=12</fimath> and <fimath>sn=5</fimath>
<img  fsrc="FAUDES_IMAGES/extintro_l3gen.png" alt="large generator" width="600px"/>


There are no conditions on the parameters. The resulting generator
may be non-deterministic.




Image Files

Any images used for the reference pages must be embedded in the extension file. During installation, embedded files get extracted to the libfaudes/doc/images directory with file-name as specified by the name attribute, mapped to lower case. Supported image formates are identified by the file-name suffixes .png, .svg, .jpg or .jpeg, respectively. The actual content is Base64 encoded binary data with two extra "=", one at the beginning and one at the end.

<ImageFile name="extintro_lg3gen.png"> 

As a special feature for the graphical representation of automata, flxinstall will sense the situation when for one basename there are files present with .gen, .png and .svg suffix. In this case, a reference page will be generated to represent the scalable image from the svg-file and the token data from the gen-file. As with libFAUDES plug-ins, the extra representation can be embedded in the documentation by an fimage element:

<ReferencePage chapter="Reference" section="ExtIntro" page="1_LargeGenerator" title="LuaExtension - Large Generators">
LuaExtension - Large Generators

[ ... ]

<!-- plain bitmap image only -->
<img fsrc="FAUDES_IMAGES/extintro_l3gen.png"/>

<!-- bitmap image linked to separate reference page -->
<fimage fsrc="FAUDES_IMAGES/extintro_l3gen"/>

[ ... ]



Tutorials can be provided for further illustration and effective advertisement of the extension. Typically, they are also used to generate the example output for the reference pages.

Tutorials are plain Lua scripts that reside within tags LuaTutorial. For the example extension, we provide the following test scenario.

<LuaTutorial name="extintro_example.lua"> 
-- Tutorial to illustrate the lua-extension "ExtIntro"

-- Read input data
l1gen = faudes.Generator("data/gen_lg.gen")

-- Apply test and report
if l1 then
  print("l1gen is a large generator [expected]")
  print("l1gen is not a large generator [test case error]")

-- Record test case
FAUDES_TEST_DUMP("lgen test 1",l1)

-- Constrcut a small generator
l2gen = faudes.Generator()

-- Produce graphical output for documentation

-- Apply test and report
if l2 then
  print("l2gen is a large generator [test case error]")
  print("l2gen is not a large generator [expected]")

-- Record test case
FAUDES_TEST_DUMP("lgen test 2",l2)

-- Validate results

Note: When composing a lua-extension by flxinstall -c, the outer element tags will be added automatically. Thus, the source file should be a plain Lua script.

By convention, any input data used in a tutorial is read from the directory data relative to the tutorials location. The corresponding files can be packaged with the extension by using the tags DataFile and specifying filename and content (either as Base64 encoded binary or as token stream). When flxinstall -c is used to compose the extension, the source data is interpreted as data directory and any file within that directory is represented as DataFile section.

The above tutorial uses the functions FAUDES_TEST_DUMP(m,d) and FAUDES_TEST_DIFF() for elementary validation. The provided tests can be performed by flxinstall -t. When distributing an extension with libFAUDES, validation is performed at the make-target test; see also test cases.

The provided example comes with two files in the data directory: a generator input and the reference protocol for validation.

<DataFile name="gen_lg.gen">
=PEdlbmVyYXRvcj [...] KCiJsYXJnZSBn=== 
<DataFile name="extintro_example_lua.prot"> 

libFAUDES 2.32b --- 2024.03.01 --- with "synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-luabindings-hybrid-example-pybindings"