[Spot-announce] Spot 1.1 released

We are pleased to announce the release of Spot 1.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 release features several improvements developped with our collegues from the Mazaryk University (also authors of the ltl3ba translator) as detailed in the following paper: Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček: Compositional Approach to Suspension and Other Improvements to LTL Translation. To appear in the proceedings of SPIN'13. You can find the new release here: http://spot.lip6.fr/dl/spot-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 (2013-04-28): * New features in the library: - The postprocessor class now takes an optional option_map argument that can be used to specify fine-tuning options, making it easier to benchmark different scenarios while developing new postprocessings. - A new translator class implements a complete translation chain, from LTL/PSL to TGBA/BA/Monitor. It performs pre- and post-processings in addition to the core translation, and offers an interface similar to that used in the postprocessor class, to specify the intent of the translation. - The degeneralization algorithm has learned three new tricks: level reset, level caching, and SCC-based ordering. The former two are enabled by default. Benchmarking has shown that the latter one does not always have a positive effect, so it is disabled by default. (See SPIN'13 paper.) - The scc_filter() function, which removes dead SCCs and also simplify acceptance conditions, has learnt how to simplify acceptance conditions in a few tricky situations that were not simplified previously. (See SPIN'13 paper.) - An experimental "don't care" (direct) simulation has been implemented. This simulations consider the acceptance of out-of-SCC transitions as "don't care". It is not enabled by default because it currently is very slow. - remove_x() is a function that take a formula, and rewrite it without the X operator. The rewriting is only correct for stutter-insensitive LTL formulas (See K. Etessami's paper in IFP vol. 75(6). 2000) This algorithm is accessible from the command-line using ltlfilt's --remove-x option. - is_stutter_insensitive() takes any LTL formula, and check whether it is stutter-insensitive. This algorithm is accessible from the command-line using ltlfilt's --stutter-insensitive option. - A new translation, called compsusp(), for "Compositional Suspension" is implemented on top of ltl_to_tgba_fm(). (See SPIN'13 paper.) - Some experimental LTL rewriting rules that trie to gather suspendable formulas are implemented and can be activated with the favor_event_univ option of ltl_simplifier. As always please check doc/tl/tl.tex for the list of rules. - Several functions have been introduced to check the strength of an SCC. is_inherently_weak_scc() is_weak_scc() is_syntactic_weak_scc() is_complete_scc() is_terminal_scc() is_syntactic_terminal_scc() Beware that the costly is_weak_scc() function introduced in Spot 1.0, which is based on a cycle enumeration, has been renammed to is_inherently_weak_scc() to match established vocabulary. * Command-line tools: - ltl2tgba and ltl2tgta now honor a new --extra-options (or -x) flag to fine-tune the algorithms used. The available options are documented in the spot-x (7) manpage. For instance use '-x comp-susp' to use the afore-mentioned compositional suspension. - The output format of 'ltlcross --json' has been changed slightly. In a future version we will offer some reporting script that turn such JSON output into various tables and graphs, and these change are required to make the format usable for other benchmarks (not just ltlcross). - ltlcross will now count the number of non-accepting, terminal, weak, and strong SCCs, as well as the number of terminal, weak, and strong automata produced by each tool. * Documentation: - org-mode files used to generate the documentation about command-line tools (shown at http://spot.lip6.fr/userdoc/tools.html) is distributed in doc/org/. The resulting html files are also in doc/userdoc/. * Bug fixes: - There was a memory leak in the LTL simplification code, that could only be triggered when disabling advanced simplifications. - The translation of the PSL formula !{xxx} was incorrect when xxx simplified to false. - Various warnings triggered by new compilers. -- Alexandre Duret-Lutz