[Spot-announce] Spot 2.3 released

We are happy to announce the release of Spot 2.3. Spot is a library of algorithms for manipulating LTL formulas and omega-automata (objects as commonly used in model checking). This new release features some exiting news such as - faster emptiness checks for automata that are not explored on-the-fly, - several improvements to the SAT-based minimization procedure, - preliminary support for alternating automata, - membership tests for all classes of the Manna and Pnueli hierarchy of temporal properties. See below for more details. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.3.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. The contributors to this release are Maximilien Colange, Alexandre Gbaguidi Aisse, Étienne Renault, and myself. As always, please direct any feedback to <spot(a)lrde.epita.fr>fr>. New in spot 2.3 (2017-01-19) Build: * While Spot only relies on C++11 features, the configure script learned --enable-c++14 to compile in C++14 mode. This allows us check that nothing breaks when we will switch to C++14. * Spot is now distributed with PicoSAT 965, and uses it for SAT-based minimization of automata without relying on temporary files. It is still possible to use an external SAT solver by setting the SPOT_SATSOLVER environment variable. * The development Debian packages for Spot now install static libraries as well. * We now install configuration files for users of pkg-config. Tools: * ltlcross supports translators that output alternating automata in the HOA format. Cross-comparison checks will only work with weak alternating automata (not necessarily *very* weak), but "ltlcross --no-check --product=0 --csv=..." will work with any alternating automaton if you just want satistics. * autfilt can read alternating automata. This is still experimental (see below). Some of the algorithms proposed by autfilt will refuse to work because they have not yet been updated to work with alternating automata, but in any case they should display a diagnostic: if you see a crash, please report it. * autfilt has three new filters: --is-very-weak, --is-alternating, and --is-semi-deterministic. * the --check option of autfilt/ltl2tgba/ltldo/dstar2tgba can now take "semi-determinism" as argument. * autfilt --highlight-languages will color states that recognize identical languages. (Only works for deterministic automata.) * 'autfilt --sat-minimize' and 'ltl2tgba -x sat-minimize' have undergone some backward incompatible changes. They use binary search by default, and support different options than they used too. See spot-x(7) for details. The defaults are those that were best for the benchmark in bench/dtgbasat/. * ltlfilt learned --recurrence and --persistence to match formulas belonging to these two classes of the temporal hierarchy. Unlike --syntactic-recurrence and --syntactic-persistence, the new checks are automata-based and will also match pathological formulas. See https://spot.lrde.epita.fr/hierarchy.html * The --format option of ltlfilt/genltl/randltl/ltlgrind learned to print the class of a formula in the temporal hierarchy of Manna & Pnueli using %h. See https://spot.lrde.epita.fr/hierarchy.html * ltldo and ltlcross learned a --relabel option to force the relabeling of atomic propositions to p0, p1, etc. This is more useful with ltldo, as it allows calling a tool that restricts the atomic propositions it supports, and the output automaton will then be fixed to use the original atomic propositions. * ltldo and ltlcross have learned how to call ltl3hoa, so 'ltl3hoa -f %f>%O' can be abbreviated to just 'ltl3hoa'. Library: * A twa is required to have at least one state, the initial state. An automaton can only be empty while it is being constructed, but should not be passed to other algorithms. * Couvreur's emptiness check has been rewritten to use the explicit interface when possible, to avoid overkill memory allocations. The new version has further optimizations for weak and terminal automata. Overall, this new version is roughly 4x faster on explicit automata than the former one. The old version has been kept for backward compatibility, but will be removed eventually. * The new version of the Couvreur emptiness check is now the default one, used by twa::is_empty() and twa::accepting_run(). Always prefer these functions over an explicit call to Couvreur. * experimental support for alternating automata: - twa_graph objects can now represent alternating automata. Use twa_graph::new_univ_edge() and twa_graph::set_univ_init_state() to create universal edges an initial states; and use twa_graph::univ_dests() to iterate over the universal destinations of an edge. - the automaton parser will now read alternating automata in the HOA format. The HOA and dot printers can output them. - the file twaalgos/alternation.hh contains a few algorithms specific to alternating automata: + remove_alternation() will transform *weak* alternating automata into TGBA. + the class outedge_combiner can be used to perform "and" and "or" on the outgoing edges of some alternating automaton. - scc_info has been adjusted to handle universal edges as if they were existential edges. As a consequence, acceptance information is not accurate. - postprocessor will call remove_alternation() right away, so it can be used as a way to transform alternating automata into different sub-types of (generalized) Büchi automata. Note that although prostprocessor optimize the resulting automata, it still has no simplification algorithms that work at the alternating automaton level. - See https://spot.lrde.epita.fr/tut23.html https://spot.lrde.epita.fr/tut24.html and https://spot.lrde.epita.fr/tut31.html for some code examples. * twa objects have two new properties, very-weak and semi-deterministic, that can be set or retrieved via twa::prop_very_weak()/twa::prop_semi_deterministic(), and that can be tested by is_very_weak_automaton()/is_semi_deterministic(). * twa::prop_set has a new attribute used in twa::prop_copy() and twa::prop_keep() to indicate that determinism may be improved by an algorithm. In other words properties like deterministic/semi-deterministic/unambiguous should be preserved only if they are positive. * language_map() and highlight_languages() are new functions that implement autfilt's --highlight-languages option mentionned above. * dtgba_sat_minimize_dichotomy() and dwba_sat_minimize_dichotomy() use language_map() to estimate a lower bound for binary search. * The encoding part of SAT-based minimization consumes less memory. * SAT-based minimization of automata can now be done using two incremental techniques that take a solved minimization and attempt to forbid the use of some states. This is done either by adding clauses, or by using assumptions. * If the environment variable "SPOT_XCNF" is set during incremental SAT-based minimization, XCNF files suitable for the incremental SAT competition will be generated. This requires the use of an exteral SAT solver, setup with "SPOT_SATSOLVER". See spot-x(7). * The new function mp_class(f) returns the class of the formula f in the temporal hierarchy of Manna & Pnueli. Python: * spot.show_mp_hierarchy() can be used to display the membership of a formula to the Manna & Pnueli hierarchy, in notebooks. An example is in https://spot.lrde.epita.fr/ipynb/formulas.html * The on-line translator will now display the temporal hierarchy in the "Formula > property information" output. Bugs fixed: * The minimize_wdba() function was not correctly minimizing automata with useless SCCs. This was not an issue for the LTL translation (where useless SCCs are always removed first), but it was an issue when deciding if a formula was safety or guarantee. As a consequence, some tricky safety or guarantee properties were only recognized as obligations. * When ltlcross was running a translator taking the Spin syntax as input (%s) it would not automatically relabel any unsupported atomic propositions as ltldo already do. * When running "autfilt --sat-minimize" on a automaton representing an obligation property, the result would always be a complete automaton even without the -C option. * ltlcross --products=0 --csv should not output any product-related column in the CSV output since it has nothing to display there. -- Alexandre Duret-Lutz