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@lrde.epita.fr>. As always, please direct any feedback to <spot@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