1. ABOUT

The libltl2ba software is a modification of LTL2BA and incorporates the changes
from LTL2C. It aims at making the functionality of both available in form of a
library while maintaining compatibility with the original algorithms.

For bug-reports and/or questions about libltl2ba, please contact Franz Brauße:
<[email protected]>

LTL2C has been written by Jeremy Morse.  It is based on LTL2BA version 1.1 and
adds output formats for dot and the ESBMC model checker.

LTL2BA has originally been written by Denis Oddoux and was 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)

2. COMPILING

unpack the archive:
> tar -xzf libltl2ba-2.0.tar.gz
> cd libltl2ba-2.0

compile the program
> make

3. EXECUTING

run the program
> ./ltl2ba -f 'formula'

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

Propositonal Symbols:
        true, false
        any lowercase string
        {C expression}

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

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

Use spaces between any symbols. Unary operators bind stronger than binary ones.
Precedence (high to low) and associativity of binary operators is as follows:

        U, V  : right
        &&    : left
        ||    : left
        <->   : none
        ->    : right

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
> ./ltl2ba -h
to see the possible options for executing the program

4. LICENSE

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