6 Mar
2013
6 Mar
'13
10:59 a.m.
e are pleased to announce the release of Spot 1.0.2.
Spot is a model-checking library developed collaboratively by LRDE
and LIP6. It provides algorithms and data structures to implement
the automata-theoretic approach to LTL model checking.
This second maintainance release fixes couple of bugs, the most
serious being in web interface, and adds two minor new features.
You can find the new release here:
http://spot.lip6.fr/dl/spot-1.0.2.tar.gz
A summary of the changes follows. Please report any issue
to <spot(a)lrde.epita.fr>fr>.
New in spot 1.0.2 (2013-03-06):
* New features:
- the on-line ltl2tgba.html interface can output deterministic or
non-deterministic monitors. However, and unlike the ltl2tgba
command-line tool, it doesn't different output formats.
- the class ltl::ltl_simplifier now has an option to rewrite Boolean
subformulaes as irredundante-sum-of-product during the simplification
of any LTL/PSL formula. The service is also available as a method
ltl_simplifier::boolean_to_isop() that applies this rewriting
to a Boolean formula and implements a cache.
ltlfilt as a new option --boolean-to-isop to try to apply the
above rewriting from the command-line:
% ltlfilt --boolean-to-isop -f 'GF((a->b)&(b->c))'
GF((!a & !b) | (b & c))
This is currently not used anywhere else in the library.
* Bug fixes:
- 'ltl2tgba --high' is documented to be the same as 'ltl2tgba',
but by default ltl2tgba forgot to enable LTL simplifications based
on language containment, which --high do enable. There are now
enabled by default.
- the on-line ltl2tgba.html interface failed to output monitors,
testing automata, and generalized testing automata due to two
issues with the Python bindings. It also used to display
Testing Automaton Options when the desired output was set to Monitor.
- bench/ltl2tgba would not work in a VPATH build.
- a typo caused some .dir-locals.el configuration parameters to be
silently ignored by emacs
- improved Doxygen comments for formula_to_bdd, bdd_to_formula,
and bdd_dict.
- src/tgbatest/ltl2tgba (not to be confused with src/bin/ltl2tgba)
would have a memory leak when passed the conflicting option -M
and -O. It probably has many other problems. Do not use
src/tgbatest/ltl2tgba if you are not writing a test case for
Spot. Use src/bin/ltl2tgba instead.
--
Alexandre Duret-Lutz