This is to announce the release of Spot 1.1.1. The main motivation for this release is to fix a bug introduced in version 1.1 in the post-processing of (degeneralized) Büchi automata. Although the NEWS excerpt at the end of this email shows several new features, most of them are related to the discovery and fix of this bug: 1) With this release, ltl2tgba --ba --lbtt has been changed to output automata using the state-based acceptance flavor of the LBTT format. This makes more sense when you work with Büchi automata. 2) This lead to the discovery that previously, when --lbtt always output automata with transition-based acceptance, there were some rare formulas where ltl2tgba --ba --lbtt could output automata that where not Büchi automata (although they had the correct language), and worse: ltl2tgba --spin could output an incorrect neverclaim. 3) fixing this required to reimplement two functions we started using in 1.0 but that messed the structure of Büchi automata: namely reverse simulation and SCC-based simplification of acceptance condition. Two small and easy options have also been added to ltlcross. You can find the new release here: http://spot.lip6.fr/dl/spot-1.1.1.tar.gz A summary of the changes follows. Please report any issue to <spot(a)lrde.epita.fr>fr>. New in spot 1.1.1 (2013-05-13): * New features: - lbtt_reachable(), the function that outputs a TGBA in LBTT's format, has a new option to indicate that the TGBA being printed is in fact a Büchi automaton. In this case it outputs an LBTT automaton with state-based acceptance. The output of the guards has also been changed in two ways: 1. atomic propositions that do not match p[0-9]+ are always double-quoted. This avoids issues where t or f were used as atomic propositions in the formula, output as-is in the automaton, and read back as true or false. Other names that correspond to LBT operators would cause problem as well. 2. formulas that label transitions are now output as irredundant-sums-of-products. - 'ltl2tgba --ba --lbtt' will now output automata with state-based acceptance. You can use 'ltl2tgba --ba --lbtt=t' to force the output of transition-based acceptance like in the previous versions. Some illustrations of this point and the previous one can be found in the man page for ltl2tgba(1). - There is a new function scc_filter_states() that removes all useless states from a TGBA. It is actually an abbridged version of scc_filter() that does not alter the acceptance conditions of the automaton. scc_filter_state() should be used when post-processing TGBAs that actually represent BAs. - simulation_sba(), cosimulation_sba(), and iterated_simulations_sba() are new functions that apply to TGBAs that actually represent BAs. They preserve the imporant property that if a state of the BA is is accepting, the outgoing transitions of that state are all accepting in the TGBA that represent the BA. This is something that was not preserved by functions cosimultion() and iterated_simulations() as mentionned in the bug fixes below. - ltlcross has a new option --seed, that makes it possible to change the seed used by the random graph generator. - ltlcross has a new option --products=N to check the result of each translation against N different state spaces, and everage the statistics of these N products. N default to 1; larger values increase the chances to detect inconsistencies in the translations, and also make the average size of the product built against the translated automata a more pertinent statistic. - bdd_dict::unregister_all_typed_variables() is a new function, making it easy to unregister all BDD variables of a given type owned by some object. * Bug fixes: - genltl --gh-r generated the wrong formulas due to a typo. - ltlfilt --eventual and --universal were not handled properly. - ltlfilt --stutter-invariant would trigger an assert on PSL formulas. - ltl2tgba, ltl2tgta, ltlcross, and ltlfilt, would all choke on empty lines in a file of formulas. They now ignore empty lines. - The iterated simulation applied on degeneralized TGBA was bogus for two reasons: one was that cosimulation was applied using the generic cosimulation for TGBA, and the second is that SCC-filtering, performed between iterations, was also a TGBA-based algorithm. Both of these algorithms could lose the property that if a TGBA represents a BA, all the outgoing transitions of a state should be accepting. As a consequence, some formulas where translated to incorrect Büchi automata. -- Alexandre Duret-Lutz