1. LICENSE

LTL3BA - Version 1.1.3 - September 2016
Written by Tomas Babiak, FI MU, Brno, Czech Republic                          
Copyright (c) 2012  Tomas Babiak

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
                                                                  
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 LTL3BA software is based on LTL2BA - Version 1.1.
Modifications are based on the paper presented at TACAS 2012:
  T. Babiak, M. Kretinsky, V. 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

LTL3BA needs BuDDy (Binary Decision Diagram) library.
BuDDy is available at http://sourceforge.net/projects/buddy/
LTL3BA was tested with BuDDy version 2.4

3. COMPILING

open the archive :
> gunzip ltl3ba-1.1.3.tar.gz
> tar xf ltl3ba-1.1.3.tar
> cd ltl3ba-1.1.3

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

Add path to libbdd.a also into the library path (LD_LIBRARY_PATH).

compile the program
> make

3. EXECUTING

run the program
> ./ltl3ba -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 never claim in Promela that can be given to the
Spin model checker to verify properties on a system.

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