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>.
--
Alexandre Duret-Lutz
