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(a)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.
