1. LICENSE

LTL3DRA
Written by Tomas Babiak and Frantisek Blahoudek, FI MU, Brno, Czech Republic
Copyright (c) 2013  Tomas Babiak and Frantisek Blahoudek

Based on:

LTL2BA - Version 1.0 - October 2001
Written by Denis Oddoux, LIAFA, France
Copyright (c) 2001  Denis Oddoux

LTL2BA - Version 1.1 - August 2007
Modified by Paul Gastin, LSV, France
Copyright (c) 2007  Paul Gastin
Available at http://www.lsv.ens-cachan.fr/~gastin/ltl2ba

LTL3BA - Version 1.0 - March 2012
Copyright (c) 2013  Tomas Babiak
Available at https://sourceforge.net/projects/ltl3ba/


This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 3 of the License, or
(at your option) any later version. 

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

GNU GPL is included in this distribution, in a file called 'LICENSE'.
If not, see <https://www.gnu.org/licenses/>.

The algorithms used in LTL3DRA are described in:
  T. Babiak, F. Blahoudek, M. Kretinsky, and J. Strejcek
  "Effective Translation of LTL to Deterministic Rabin Automata:
     Beyond the (F,G)-Fragment (2013)"
  In 11th International Symposium on Automated Technology
    for Verification and Analysis (ATVA 2013)

The LTL3BA software was written by Tomas Babiak and the algorithms are
  described in:
  T. Babiak, M. Kretinsky, F. Rehak, and J. Strejcek
  "LTL to Buchi Automata Translation: Fast and More Deterministic"
  In 18th International Conference on Tools and Algorithms for the
  Construction and Analysis of Systems (TACAS 2012)

The LTL2BA software was written by Denis Oddoux and modified by Paul
Gastin.  It is based on the translation algorithm presented at CAV '01:
  P.Gastin and D.Oddoux
  "Fast LTL to B�chi Automata Translation"
  in 13th International Conference on Computer Aided Verification, CAV 2001,
  G. Berry, H. Comon, A. Finkel (Eds.)
  Paris, France, July 18-22, 2001,
  Proceedings - LNCS 2102, pp. 53-65

Part of the code included is issued from the SPIN software Version 3.4.1
The SPIN software is written by Gerard J. Holzmann, originally as part
of ``Design and Validation of Protocols,'' ISBN 0-13-539925-4,
1991, Prentice Hall, Englewood Cliffs, NJ, 07632
Here are the files that contain some code from Spin v3.4.1 :

  cache.c  (originally tl_cache.c)
  lex.c    (           tl_lex.c  )
  ltl2ba.h (           tl.h      )
  main.c   (           tl_main.c )
  mem.c    (           tl_mem.c  )
  parse.c  (           tl_parse.c)
  rewrt.c  (           tl_rewrt.c)
  trans.c  (           tl_trans.c)

2. REQUIREMENTS

LTL3DRA needs BuDDy (Binary Decision Diagram) library.
BuDDy is available at http://sourceforge.net/projects/buddy/
LTL3DRA was tested with BuDDy version 2.4. You can use the
script install_buddy.sh or the followint command to install
BuDDy system-wide.
> make install_buddy

3. COMPILING

open the archive :
> tar -xvf ltl3dra-0.2.6.tar.gz
> cd ltl3dra-0.2.6

If you did not install BuDDy system-wide, you should edit  Makefile
and set paths to BuDDy's files "bdd.h" and "libbdd.a". You should
also include BUDDY_LIB into your LD_PATH
(Edit BUDDY_INCLUDE and BUDDY_LIB)

compile the program
> make

You can install into the default locations using
> make install

4. EXECUTING

run the program
> ./ltl3dra -f "formula"

The formula is an LTL formula, and may contain propositional symbols,
boolean operators, temporal operators, and parentheses.
The syntax used is the one used in the 'Spin' model-checker

Propositonal Symbols:
        true, false
        any lowercase string

Boolean operators:
        !   (negation)
        ->  (implication)
        <-> (equivalence)
        &&  (and)
        ||  (or)

Temporal operators:
        G []  (always)
        F <>  (eventually)
        U     (until)
        R V   (release)
        X     (next)

Use spaces between any symbols.

The result is a TGDRA in the HOA format v1.

To produce a DRA in ltl2dstar format v2 run
> ./ltl3dra -L -f "formula"

run the command
> ./ltl3dra
to see the possible options for executing the program

5. BUGS

Please send bug-reports to [email protected]