[Lrde Annonce] Spot 2.0 has been released

We are happy to announce the release of Spot 2.0! Spot is a C++ library for model checking and manipulation of temporal logic formula and omega-automata. It also comes with command-line tools and Python bindings. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.0.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Spot 2.0 is the result of 28 months of work, as we starting working on this branch after the release of Spot 1.2.1 (Dec 2013). It includes contributions from Alexandre Lewkowicz, Amaury Fauchille, Étienne Renault, Laurent Xu, Thibaud Michaud, and myself. For people upgrading from Spot 1.2.6 (or older), the main news are as follows: * Automata now support acceptance conditions expressed as arbitrary formulas over "marks" that must be seen infinitely often or finitely often. * The C++ API has been seriously overhauled and now requires a C++11 compiler. Backward compatibility has been broken in many ways: see https://spot.lrde.epita.fr/upgrade2.html for help about migrating old code. But now that the dust has settled, you should not expect further API breakage in upcoming 2.x releases. * The shell commands now include tools for processing automata. See https://spot.lrde.epita.fr/tools.html for a list of all the tools, and check https://spot.lrde.epita.fr/autfilt.html in particular. The default interchange format is the Hanoi Omega Automata format (HOA), but other formats are supported as well. * The Python bindings are more complete, and even allow prototyping low-level algorithms (for instance the page https://spot.lrde.epita.fr/ipynb/product.html shows how to implement a product of two automata with arbitrary acceptance). Python bindings also interface nicely with IPython/Jupyter notebooks. See https://spot.lrde.epita.fr/tut.html for short examples of various tasks implemented in shell, C++, and Python. For those upgrading from 1.99.9, the difference with Spot 2.0 is rather thin. The following changes were included in Spot 2.0 (2016-04-11): Command-line tools: * ltlfilt now also support the --accept-word=WORD and --reject-word=WORD options that were introduced in autfilt in the previous version. Python: * The output of spot.atomic_prop_collect() is printable and can now be passed directly to spot.ltsmin.model.kripke(). Library: * digraph::valid_trans() renamed to digraph::is_valid_edge(). Documentation: * The concepts page (https://spot.lrde.epita.fr/concepts.html) now includes a highlevel description of the architecture, and some notes aboute automata properties. * More Doxygen documentation for spot::formula and spot::digraph. See https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-0/NEWS for the complete history of NEWS entries across previous releases. Please direct any feedback to <spot(a)lrde.epita.fr>fr>. -- Alexandre Duret-Lutz