Never say "never": here is yet another bug fix release for Spot 1.2. The most important fix is for a simplification rule for some unlikely PSL pattern. Then we have some improved compatibilities with some newer versions of the tools we use in the build, some fixes to the HOA format (as output by ltl2tgba --hoaf) that the current development version of Spot 2.0 is able to read, and some improved errors checks for ltlcross. You can download the new release here: http://spot.lip6.fr/dl/spot-1.2.6.tar.gz New in spot 1.2.6 (2014-12-06) * New features: - ltlcross --verbose is a new option to see what is being done * Bug fixes: - Remove one incorrect simplification rule for PSL discovered via checks on random formulaes. (The bug was very unlikely to trigger on non-random formulas, because it requires a SERE with an entire subexpression that is unsatisfiable.) - When the automaton resulting from the translation of a positive formula is deterministic, ltlcross will compute its complement to perform additional checks against other translations of the positive formula. The same procedure should be performed with automata obtained from negated formulas, but because of a typo this was not the case. - the neverclaim parser will now diagnose redefinitions of state labels. - the acceptance specification in the HOA format output have been adjusted to match recent changes in the format specifications. - atomic propositions are correctly escaped in the HOA output. - the build rules for documentation have been made compatible with version 8.0 of Org-mode. (This was only a problem if you build from the git repository, or if you want to edit the documentation.) - recent to changes to libstd++ (as shipped by g++ 4.9.2) have demonstrated that the order of transitions output by the LTL->TGBA translation used to be dependent on the implementation of the STL. This is now fixed. - some developpement version of libstd++ had a bug (PR 63698) in the assignment of std::set, and that was triggered in two places in Spot. The workaround (not assigning sets) is actually more efficient, so we can consider it as a bug fix, even though libstd++ has also been fixed. - all parsers would report wrong line numbers while processing files with DOS style newlines. - add support for SWIG 3.0. -- Alexandre Duret-Lutz