1. About
2. Download
3. Compiling
4. Usage
5. Input Format
6. Acknowledgement
7. Contact

About

libSFTA is a library that implements symbolically encoded nondeterministic bottom-up finite tree automata and standard operations on them. Search here for further information. Note: The libSFTA library is now obsolete, check libvata for its successor.

Download

To download the library, run $ git clone git://github.com/ondrik/libsfta.git.

Compiling

For compiling the library, see the README file in the root directory.

Usage

The library comes with a simple interface program that performs the following operations:

1. Load. This performs validation of the file with the input automaton.
   usage: sfta --load <file>
2. Union. Given two input automata, this performs computation of an automaton that accepts the language that is the union of languages of the input automata.
   usage: sfta --union <file1> <file2>
3. Intersection. Given two input automata, this performs computation of an automaton that accepts the language that is the intersection of languages of the input automata.
   usage: sfta --intersection <file1> <file2>

Input Format

The program expects an input to be formated in Timbuk style:

<file>            : 'Ops' <label_list> <automaton>

<label_list>      : <label_decl> <label_decl> ... // a list of label declarations

<label_decl>      : string ':' int // a symbol declaration (the name and the arity)

<automaton>       : 'Automaton' string 'States' <state_list> 'Final States' <state_list> 'Transitions' <transition_list>

<state_list>      : <state> <state> ... // a list of states

<state>           : string // the name of a state

<transition_list> : <transition> <transition> ... // a list of transitions

<transition>      : <label> '(' <state> ',' <state> ',' ... ')' '->' <state> // a transition

<label>           : string // the name of a label

An example could look like this:

Ops a:0 b:1 c:2

Automaton A
States q0 q1 q2
Final States q2 
Transitions
a() -> q0
b(q0) -> q1
c(q1, q1) -> q1
c(q1, q1) -> q2
c(q2, q2) -> q2

Acknowledgement

This work was supported by the Czech Science Foundation (within projects P103/10/0306 and 102/09/H042), the Czech Ministry of Education (projects COST OC10009 and MSM 0021630528), and the internal BUT project FIT-10-1.

Contact

If you have further questions, do not hesitate to contact authors (Lukas Holik, Ondrej Lengal and Tomas Vojnar).