Spot

Download

spot@lrde.epita.fr

February 2010

2 participants
2 discussions

Parameters for the "ltl2tgba" tool
by ehlers＠alan.cs.uni-sb.de 26 Feb '10

26 Feb '10

Dear all, included in the SPOT distribution is the tool "ltl2tgba" that converts LTL formulas to equivalent Büchi automata. For the research I am currently working on, I need to convert LTL formulas to as-small-as-possible Büchi automata (that are not transition-based, so I am using the tool with the "-N" parameter to obtain SPIN never-claims). So far, for all my benchmarks, I am calling the tool with the following parameter combinations: ltl2tgba -N -R3 -r4 ltl2tgba -N -R3 -r7 ltl2tgba -N -R3 -r4 ltl2tgba -N -R3 -r7 ltl2tgba -N -R3 -r4 ltl2tgba -N -R3 -r7 After that, I take the smallest automata obtained. So far, I am only interested in the number of states. Now my question is: Given that I have enough time, which other parameter combinations might lead to automata that that are smaller than any automaton obtained when using the parameter combinations given above? As an example, can it be the case that "-R2q" is sometimes better than "-R3"? Phrased in other words, I'd like to know some set of parameter combinations "A" such that for all LTL formulas "f", I can simply run "ltl2tgba" on "f" trying all parameters combinations in "A" and take the minimal automaton found. For the resulting automaton, it should be assured that there's no smaller automaton obtainable with "ltl2tgba" from "f" for any possible parameter combination. At the same time, "A" should be as small as possible. I hope that someone finds some time to reply and apologies for using the SPOT framework in such a restricted way. Best regards, Ruediger Ehlers

1 0

Spot 0.5 has been released
by Alexandre Duret-Lutz 01 Feb '10

01 Feb '10

We're pleased to announce the release of Spot 0.5. Spot is a model-checking library developed collaboratively by LRDE and LIP6. It provides algorithms and data structures to implement the automata-theoretic approach to LTL model checking. This release includes more than two year of work, with contributions from Damien Lefortier, Guillaume Sadegh, Félix Abecassis, and Alexandre Duret-Lutz. We would also like to thank Akim Demaille, Denis Poitrenaud, and Kristin Y. Rozier for their bug reports and help. You can find the new release here: http://spot.lip6.fr/dl/spot-0.5.tar.gz Before listing what is new in this release, let me mention that we have setup two mailing lists so you can stay informed, or discuss spot: - <spot-announce(a)lrde.epita.fr> is read-only and will be used to announce new releases. You may subscribe at https://www.lrde.epita.fr/mailman/listinfo/spot-announce - <spot(a)lrde.epita.fr> can be used to discuss anything related to Spot. You may subscribe at https://www.lrde.epita.fr/mailman/listinfo/spot-announce What is new in spot 0.5 (2010-02-01): * Two new LTL translations have been implemented: - eltl_to_tgba_lacim() is a symbolic translation for ELTL based on Couvreur's LaCIM'00 paper. For this translation (available with ltl2tgba's option -le), all operators are described as finite automata. A default set of operators is provided for LTL (option -lo) and user may add more automaton operators. - ltl_to_taa() is a translation based on Tauriainen's PhD thesis. LTL is translated to "self-loop" alternating automata and then to Transition-based Generalized Automata. (ltl2tgba's option -taa). The "Couvreur/FM" translation remains the best LTL translation available in Spot. * The data structures used to represent LTL formulae have been overhauled, and it resulted in a big performence improvement (in time and memory consumption) for the LTL translation. * Two complementation algorithms for state-based Büchi automata have been implemented: - tgba_kv_complement is an on-the-fly implementation of the Kupferman-Vardi construction (TCS'05) for generalized acceptance conditions. - tgba_safra_complement is an implementation of Safra's complementation. This algorithm takes a degeneralized Büchi automaton as input, but our implementation for the Streett->Büchi step will produce a generalized automaton in the end. * ltl2tgba has gained several options and the help text has been reorganized. Please run src/tgbatest/ltl2tgba without arguments for details. Couvreur/FM is now the default translation. * The ltl2tgba.py CGI script can now run standalone. It also offers the Tauriainen/TAA translation, and some options for SCC-based reductions. * Automata using BDD-encoded transitions relation can now be pruned for useless states symbolically using the delete_unaccepting_scc() function. This is ltl2tgba's -R3b option. * The SCC-based simplification (ltl2tgba's -R3 option) has been rewritten and improved. * The "*" symbol, previously parsed as a synonym for "&" is no longer recognized. This makes room for an upcoming support of rational operators. * More benchmarks in the bench/ directory: - gspn-ssp/ some benchmarks published at ACSD'07, - ltlcounter/ translation of a class of LTL formulae used by Rozier & Vardi at SPIN'07 - scc-stats/ SCC statistics after translation of LTL formulae - split-product/ parallelizing gain after splitting LTL automata * An experimental Kripke interface has been developed to simplify the integration of third party tools that do not use acceptance conditions and that have label on states instead of transitions. This interface has not been used yet. * Experimental interface with the Nips virtual machine. It is not very useful as Spot isn't able to retrieve any property information from the model. This will just check assertions. * Distribution: - The Boost C++ library is now required. - Update to Autoconf 2.65, Automake 1.11.1, Libtool 2.2.6b, Bison 2.4.1, and Swig 1.3.40. - Thanks to the newest Automake, "make check" will now run in parallel if you use "make -j2 check" or more. * Bug fixes: - Disable warnings from the garbage collection of BuDDy, it could break the standard output of ltl2tgba. - Fix several C++ constructs to ensure Spot will build with GCC 4.3, 4.4, and older 3.x releases, as well as with Intel's ICC compiler. - A very old bug in the hash function for LTL formulae caused Spot to sometimes (but very rarely) consider two different LTL formulae as equal. -- Alexandre Duret-Lutz

1 0