I have subscribed Thomas Medioni to the list.
He is a master student from Paris 6 who will be working on
implementing various algorithms for generic acceptance conditions,
starting with some conversions between different acceptance
conditions.
His initial task is to implement --sum-or and --sum-and
(https://gitlab.lrde.epita.fr/spot/spot/issues/231)
--
Alexandre Duret-Lutz
We are happy to announce the release of Spot 2.3.1.
This is a maintenance release that only contains minor bug fixes, and
minor enhancements, as listed below.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.3.1.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
The contributors to this release are Arthur Remaud, Étienne Renault,
Maximilien Colange, Vincent Tourneur, and myself. As always, please
direct any feedback to <spot(a)lrde.epita.fr>.
As always, please direct any feedback to <spot(a)lrde.epita.fr>.
New in spot 2.3.1 (2017-02-20)
Tools:
- ltldo learnt to act like a portfolio: --smallest and --greatest
will select the best output automaton for each formula translated.
See https://spot.lrde.epita.fr/ltldo.html#portfolio for examples.
- The colors used in the output of ltlcross have been adjusted to
work better with white backgrounds and black backgrounds.
- The option (y) has been added to --dot. It splits the universal
edges with the same targets but different colors.
- genltl learnt three new families for formulas: --kr-n2=RANGE,
--kr-nlogn=RANGE, and --kr-n=RANGE. These formulas, from
Kupferman & Rosenberg [MoChArt'10] are recognizable by
deterministic Büchi automata with at least 2^2^n states.
Library:
- spot::twa_run::as_twa() has an option to preserve state names.
- the method spot::twa::is_alternating(), introduced in Spot 2.3 was
badly named and has been deprecated. Use the negation of the new
spot::twa::is_existential() instead.
Bugs fixed:
- spot::otf_product() was incorrectly registering atomic
propositions.
- spot::ltsmin_model::kripke() forgot to register the "dead"
proposition.
- The spot::acc_word type (used to construct acceptance condition)
was using some non-standard anonymous struct. It is unlikely that
this type was actually used outside Spot, but if you do use it,
spot::acc_word::op and spot::acc_word::type had to be renamed as
spot::acc_word::sub.op and spot::acc_word::sub.type.
- alternation_removal() was not always reporting the unsupported
non-weak automata.
- a long-standing typo in the configure code checking for Python
caused any user-defined CPPFLAGS to be ignored while building
Spot.
- The display of clusters with universal edges was confused, because the
intermediate node was not in the cluster even if one of the target was
in the same one.
--
Alexandre Duret-Lutz
