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>.
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.htmlhttps://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
