[Spot-announce] Spot 1.0.1 released

We are pleased to announce the release of Spot 1.0.1. 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 maintainance release mainly addresses a couple of minor bugs uncovered in the last three months, and prunes some old code. The main change is probably that LBTT has been removed from the distribution, as promised in the previous release notes. You can find the new release here: http://spot.lip6.fr/dl/spot-1.0.1.tar.gz A summary of the changes follows. Please report any issue to <spot(a)lrde.epita.fr>fr>. New in spot 1.0.1 (2013-01-23): * Bug fixes: - Two executions of the simulation reductions could produce two isomorphic automata, but with transitions in a different order. - ltlcross did not diagnose write errors to temporary files, and certain versions of g++ would warn about it. - "P0.init" is parsed as an atomic even without the double quotes, but it was always output with double quotes. This version will not quote this atomic proposition anymore. - "U", "W", "M", "R" were correctly parsed as atomic propositions (instead of binary operators) when placed in double quotes, but on output they were output without quotes, making the result unparsable. - the to_lbt_string() functions would always output a trailing space. This is not the case anymore. - tgba_product::transition_annotation() would segfault when called in a product against a Kripke structure. * Minor improvements: - Four new LTL simplifications rules: GF(a|Xb) = GF(a|b) GF(a|Fb) = GF(a|b) FG(a&Xb) = FG(a&b) FG(a&Gb) = FG(a&b) - The on-line version of ltl2tgba now displays edge and transition counts, just as the ltlcross tool. - ltlcross will display the number of timeouts at the end of its execution. - ltlcross will diagnose tools with missing input or output %-sequence before attempting to run any of them. - The parser for LBT's prefix-style LTL formulas will now read atomic propositions that are not of the form p1, p2... This makes it possible to process formulas written in ltl2dstar's syntax. * Pruning: - lbtt has been removed from the distribution. A copy of the last version we distributed is still available at http://spot.lip6.fr/dl/lbtt-1.2.1a.tar.gz and our test suite will use it if it is installed, but the same tests are already performed by ltlcross. - the bench/ltl2tgba/ benchmark, that used lbtt to compare various LTL-to-Büchi translators, has been updated to use ltlcross. It now output summary tables in LaTeX. Support for Modella (no longer available online), and Wring (requires a too old Perl version) have been dropped. - the half-baked and underdocumented "Event TGBA" support in src/evtgba*/ has been removed, as it was last worked on in 2004.