esbmc/libltl2ba - Githubissues

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: franz.brausse@manchester.ac.uk

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)

COMPILING

unpack the archive:

tar -xzf libltl2ba-2.0.tar.gz cd libltl2ba-2.0

compile the program

make

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

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

esbmc / libltl2ba

readme