Read Me

1. LICENSE

LTL3DRA - Version 0.2.5 - August 2017
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 2 of the License, or
(at your option) any later version. GNU GPL is included in this
distribution, in a file called 'LICENSE'

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.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA

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

3. COMPILING

open the archive :
> gunzip ltl3dra-0.1.tar.gz
> tar xf ltl3dra-0.1.tar
> cd ltl3dra-0.1

Edit Makefile and set paths to BuDDy's files "bdd.h" and "libbdd.a".
(Edit BUDDY_INCLUDE and BUDDY_LIB)

compile the program
> make

3. 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

4. TGDRA3DOT & TGDRA
Since version 0.2 LTL3DRA comes with tgdra3dot and tgdra utilities.
    tgdra3dot  - a perl utility that parses a output of
                 > ltl3dra -d -f "formula" command and produces a .dot
                 file with the corresponding TGDRA.
               - USAGE
                 > ltl3dra -d -f "formula" | tgdra3dot
    tgdra - translates given formula(s) by ltl3dra, converts the TGDRA(s)
            into .dot file(s) and displays them using xdot
          - requires perl and xdot
          - USAGE
            > tgdra -f "GFa"

5. BUGS

Please send bug-reports to xblahoud@fi.muni.cz