libFAUDES Developer Page

As a C++ library, libFAUDES provides its data-types and functions by class and function definitions in C++ header files. Thus, the natural way to use the library is to develop a C++ application that includes the headers and links against libFAUDES.

Below, we give a short overview on how to access libFAUDES data-types and functions from a C++ program. More detailed information is provided as follows:

Sets

libFAUDES models sets of states, events and transitions by the classes EventSet, StateSet and TransSet, respectively. The implementation is based on the Standard Template Library (STL), using sorted containers for the internal representation. libFAUDES sets provide access to elements (insert, delete, exists, find etc) including iterators, convenience operators (union, intersection and difference) and file IO.

The below code snipped demonstrates elementary usage of event sets. Detailed documentation can be found in the C++ API Reference Section Container Classes.

  EventSet al1;                      // declare alphabet

  al1.Name("MyAlpahbet");            // set name of this alphabet

  al1.Insert("alpha");               // insert event alpha
  al1.Insert("beta");                // insert event beta

  al1.Write("myalph.txt");           // write to file

  EventSet al2;                      // declare another alphabet
  al2.Read("other.txt");             // read from file

  EventSet intersect = al1 * al2;    // compute intersection

Generators

libFAUDES implements the five tuple automaton G = (Q, Sigma, delta, Qo, Qm) with

by Generator classes. The generator data structure resembles the definition of the automaton by implementing the Generator members as libFAUDES sets. The class provides methods to access the set members individually by a symbolic name or index, to iterate over sets, and for file IO.

The below code snipped demonstrates basic usage. More details can be found in the C++ API Reference Section Generator Classes.

  Generator g1;                      // declare generator

  g1.InsState("I");                  // introduce idle state
  g1.InsState("B");                  // introduce busy state

  g1.InsEvent("a");                  // introduce event a
  g1.InsEvent("b");                  // introduce event b

  g1.SetTransition("I", "a", "B");   // set transition I-(a)->B
  g1.SetTransition("B", "b", "I");   // set transition B-(b)->I

  g1.SetInitState("I");              // indicate that idle is an initial state
  g1.SetMarkedState("I");            // indicate that idle is a marked state

  g1.Write();                        // show generator on console
  g1.Write("very_simple.gen");       // write generator to file
  g1.GraphWrite("very_simple.jpg");  // run graphiz' dot to convert to an image

  Generator g2;
  g2.Read("nice_example.gen");       // read some generator file

Operations on Generators

libFAUDES comes with a set of general purpose operations on generators, addressing regular expressions, determinism, minimal realisation etc; see the C++ API Reference, Section Generator Functions. Functions related to more specific topics are provided by plug-ins; see Section PlugIns.

As a concise example, we present how to compute a synchronous composition of two generators:

  Generator g1("g1.gen");           // declare/read generator g1
  Generator g2("g2.gen");           // declare/read generator g1

  Generator g1g2;                   // declare result
  Parallel(g1, g2, g1g2);           // perform operation
  
  g1g2.Write("tmp_g1g2.gen");       // write result

The respective generators are taken from tutorial 3:

Generator G1 Generator G2
G1 || G2

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