We are happy to announce the release of Spot 1.99.7.

You can find the new release here:

http://www.lrde.epita.fr/dload/spot/spot-1.99.7.tar.gz

See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to spot@lrde.epita.fr.

As their names suggest, all the 1.99.x versions are intermediate releases before a Spot 2.0 release. While each of them may fix bugs and bring additional features, the most important part is that they clean up the C++ and Python API. This clean up unfortunately introduces a lot of backward incompatible changes, but the good news is that the largest changes are now over. If you have some old code compatible with 1.2.6 and want to port it to the upcoming 2.0 version, you may consider working with 1.99.7.

A list of newsworthy changes introduced by this release is given below.

New in spot 1.99.7 (2016-01-15)

Command-line tools:

* BACKWARD INCOMPATIBLE CHANGE: All tools that output automata now use the HOA format by default instead of the GraphViz output. This makes it easier to pipe several commands together.

If you have an old script that relies on GraphViz being the default output and that you do not want to update, use export SPOT_DEFAULT_FORMAT=dot to get the old behavior back.

* Tools that output automata now accept -d as a shorthand for --dot since requesting the GraphViz (a.k.a. dot) output by hand is now more frequent. randaut's short option for specifying edge-density used to be -d: it has been renamed to -e.

* The SPOT_DEFAULT_FORMAT environment variable can be set to 'dot' or 'hoa' to force a default output format for automata. Additional options may also be added, as in SPOT_DEFAULT_FORMAT='hoa=iv'.

* autfilt has a new option: --is-inherently-weak.

* The --check=strength option of all tools that produce automata will also test if an automaton is inherently weak.

Library:

* Installed headers now assume that they will be included as #include <spot/subdir/header.hh> instead of #include <subdir/header.hh>

This implies that when Spot headers are installed in /usr/include/spot/... (the default when using the Debian packages) or /usr/local/include/spot/... (the default when compiling from source), then it is no longuer necessary to add -I/usr/include/spot or -I/usr/local/include/spot when compiling, as /usr/include and /usr/local/include are usually searched by default.

Inside the source distribution, the subdirectory src/ has been renamed to spot/, so that the root of the source tree can also be put on the preprocessor's search path to compile against a non-installed version of Spot. Similarly, iface/ltsmin/ has been renamed to spot/ltsmin/, so that installed and non-installed directories can be used similarly.

* twa::~twa() is now calling get_dict()->unregister_all_my_variable(this); so this does not need to be done in any subclass.

* is_inherently_weak_automaton() is a new function, and check_strength() has been modified to also check inherently weak automata.

* decompose_strength() is now extracting inherently weak SCCs instead of just weak SCCs. This gets rid of some corner cases that used to require ad hoc handling.

* acc_cond::acc_code's methods append_or(), append_and(), and shift_left() have been replaced by operators |=, &=, <<=, and for completeness the operators |, &, and << have been added.

* Several methods have been removed from the acc_cond class because they were simply redundant with the methods of acc_cond::mark_t, and more complex to use.

acc_cond::marks(...) -> use acc_cond::mark_t(...) acc_cond::sets(m) -> use m.sets() acc_cond::has(m, u) -> use m.has(u) acc_cond::cup(l, r) -> use l | r acc_cond::cap(l, r) -> use l & r acc_cond::set_minus(l, r) -> use l - r

Additionally, the following methods/functions have been renamed:

acc_cond::is_tt() -> acc_cond::is_t() acc_cond::is_ff() -> acc_cond::is_f() parse_acc_code() -> acc_cond::acc_code(...)

* Automata property flags (those that tell whether the automaton is deterministic, weak, stutter-invariant, etc.) are now stored using three-valued logic: in addition to "maybe"/"yes" they can now also represent "no". This is some preparation for the upcomming support of the HOA v1.1 format, but it also saves time in some algorithms (e.g, is_deterministic() can now return immediately on automata marked as not deterministic).

* The automaton parser now accept negated properties as they will be introduced in HOA v1.1, and will check for some inconsistencies. These properties are stored and used when appropriate, but they are not yet output by the HOA printer.

Python:

* Iterating over the transitions leaving a state (the twa_graph::out() C++ function) is now possible in Python. See https://spot.lrde.epita.fr/tut21.html for a demonstration.

* Membership to acceptance sets can be specified using Python list when calling for instance the Python version of twa_graph::new_edge(). See https://spot.lrde.epita.fr/tut22.html for a demonstration.

* Automaton states can be named via the set_state_names() method. See https://spot.lrde.epita.fr/ipynb/product.html for an example.

Documentation:

* There is a new page explaining how to compile example programs and and link them with Spot. https://spot.lrde.epita.fr/compile.html

* Python bindings for manipulating acceptance conditions are demonstrated by https://spot.lrde.epita.fr/ipynb/acc_cond.html, and a Python implementation of the product of two automata is illustrated by https://spot.lrde.epita.fr/ipynb/product.html

Source code reorganisation:

* A lot of directories have been shuffled around in the distribution: src/ -> spot/ (see rational above) iface/ltsmin/ (code) -> spot/ltsmin/ wrap/python/ -> python/ src/tests/ -> tests/core/ src/sanity/ -> tests/sanity/ iface/ltsmin/ (tests) -> tests/ltsmin/ wrap/python/tests -> tests/python/

Bug fixes:

* twa_graph would incorrectly replace named-states during purge_dead_states and purge_unreachable_states. * twa::ap() would contain duplicates when an atomic proposition was registered several times. * product() would incorrectly mark the product of two sttuter-sensitive automata as stutter-sensitive as well. * complete() could incorrectly reuse an existing (but accepting!) state as a sink.