This maintenance release fixes a couple of translation bugs, and adds several small utility features to the command-line and online tools. Special thanks to Joachim Klein for some useful suggestions. Unless some serious bugs are reported, this is likely to be the last release of Spot 1.2. The current development version of Spot, which will probably released as Spot 2.0 next year, is so much ahead of this code base that maintaining this version is starting to be a burden. By the way, I should probably issue a friendly warning to those using Spot as a C++ library: the changes in version 2.0 will be big enough so that there is no way to maintain compatibility with code written for the current version. It will require changes to existing code, the first of which being to switch to C++11. (Spot 1.2.5 should compile fine with C++11, so you can already make that switch.) You can download the new release here: http://spot.lip6.fr/dl/spot-1.2.5.tar.gz New in spot 1.2.5 (2014-08-21) * New features: - The online ltl2tgba translator will automatically attempt to parse a formula using LBT's syntax if it cannot parse it using the normal infix syntax. It also has an option to display formulas using LBT's syntax. - ltl2tgba and dstar2tgba have a new experimental option --hoaf to output automata in the Hanoï Omega Automaton Format whose current draft is at http://adl.github.io/hoaf/ The corresponding C++ function is spot::hoaf_reachable() in tgbaalgos/hoaf.hh. - 'randltl 4' is now a shorthand for 'randltl p0 p1 p2 p3'. - ltlcross has a new option --save-bogus=FILENAME to save any formula for which a problem (other than timeout) was detected during translation or using the resulting automatas. * Documentation: - The man page for ltl2tgba has some new notes and references about TGBA and about monitors. * Bug fixes: - Fix incorrect simplification of promises in the translation of the M operator (you may suffer from the bug even if you do not use this operator as some LTL patterns are automatically reduced to it). - Fix simplification of bounded repetition in SERE formulas. - Fix incorrect translation of PSL formulas of the form !{f} where f is unsatisifable. A similar bug was fixed for {f} in Spot 1.1.4, but for some reason it was not fixed for !{f}. - Fix parsing of neverclaims produced by Modella. - Fix a memory leak in the little-used conversion from transition-based alternating automata to tgba. - Fix a harmless uninitialized read in BuDDy. - When writing to the terminal, ltlcross used to display each formula in bright white, to make them stand out. It turns out this was actually hiding the formulas for people using a terminal with white background... This version displays formula in bright blue instead. - 'randltl -n -1 --seed 0' and 'randltl -n -1 --seed 1' used to generate nearly the same list of formulas, shifted by one, because the PRNG write reset with an incremented seed between each output formula. The PRNG is now reset only once. -- Alexandre Duret-Lutz