Etienne and I are happy to announce the release of Spot 1.99.4.

While this version includes a few new features listed below, its main focus was the complete overhaul of the temporal formula subsystem. Writing code that handle LTL/PSL formulas is now a lot easier, and can be done in C++ or Python as easily.

You can get the new release here:

http://www.lrde.epita.fr/dload/spot/spot-1.99.4.tar.gz

See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to spot@lrde.epita.fr.

New in spot 1.99.4 (2015-10-01)

New features:

* autfilt's --sat-minimize now takes a "colored" option to constrain all transitions (or states) in the output automaton to belong to exactly one acceptance sets. This is useful when targeting parity acceptance.

* autfilt has a new --product-or option. This builds a synchronized product of two (completed of needed) automata in order to recognize the *sum* of their languages. This works by just using the disjunction of their acceptance conditions (with appropriate renumbering of the acceptance sets).

For consistency, the --product option (that builds a synchronized product that recognizes the *intersection* of the languages) now also has a --product-and alias.

* the parser for ltl2dstar's format has been merged with the parser for the other automata formats. This implies two things: - autfilt and dstar2tgba (despite its name) can now both read automata written in any of the four supported syntaxes (ltl2dstar's, lbtt's, HOA, never claim). - "dstar2tgba some files..." now behaves exactly like "autfilt --tgba --high --small some files...". (But dstar2tgba does not offer all the filtering and transformations options of autfilt.)

Major code changes and reorganization:

* The class hierarchy for temporal formulas has been entirely rewritten. This change is actually quite massive (~13200 lines removed, ~8200 lines added), and brings some nice benefits: - LTL/PSL formulas are now represented by lightweight formula objects (instead of pointers to children of an abstract formula class) that perform reference counting automatically. - There is no hierachy anymore: all operators are represented by a single type of node in the syntax tree, and an enumerator is used to distinguish between operators. - Visitors have been replaced by member functions such as map() or traverse(), that take a function (usually written as a lambda function) and apply it to the nodes of the tree. - As a consequence, writing algorithms that manipulate formula is more friendly, and several algorithms that spanned a few pages have been reduced to a few lines. The page https://spot.lrde.epita.fr/tut03.html illustrates the new interface, in both C++ and Python.

* Directories ltlast/, ltlenv/, and ltlvisit/, have been merged into a single tl/ directory (for temporal logic). This is motivated by the fact that these formulas are not restricted to LTL, and by the fact that we no longuer use the "visitor" pattern.

* The LTL/PSL parser is now declared in tl/parse.hh (instead of ltlparse/public.hh).

* The spot::ltl namespace has been merged with the spot namespace.

* The dupexp_dfs() function has been renamed to copy(), and has learned to preserve named states if required.

* Atomic propositions can be declared without going through an environment using the spot::formula::ap() static function. They can be registered for an automaton directly using the spot::twa::register_ap() method. The vector of atomic propositions used by an automaton can now be retrieved using the spot::twa::ap() method.