We are pleased to announce the release of Spot 1.1.
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 release features several improvements developped with our
collegues from the Mazaryk University (also authors of the ltl3ba
translator) as detailed in the following paper:
Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír
Křetínský, Jan Strejček: Compositional Approach to Suspension and
Other Improvements to LTL Translation. To appear in the
proceedings of SPIN'13.
You can find the new release here:
http://spot.lip6.fr/dl/spot-1.1.tar.gz
A summary of the changes follows. Please report any issue
to <spot(a)lrde.epita.fr>.
New in spot 1.1 (2013-04-28):
* New features in the library:
- The postprocessor class now takes an optional option_map
argument that can be used to specify fine-tuning options, making
it easier to benchmark different scenarios while developing new
postprocessings.
- A new translator class implements a complete translation chain,
from LTL/PSL to TGBA/BA/Monitor. It performs pre- and
post-processings in addition to the core translation, and offers
an interface similar to that used in the postprocessor class, to
specify the intent of the translation.
- The degeneralization algorithm has learned three new tricks:
level reset, level caching, and SCC-based ordering. The former
two are enabled by default. Benchmarking has shown that the
latter one does not always have a positive effect, so it is
disabled by default. (See SPIN'13 paper.)
- The scc_filter() function, which removes dead SCCs and also
simplify acceptance conditions, has learnt how to simplify
acceptance conditions in a few tricky situations that were not
simplified previously. (See SPIN'13 paper.)
- An experimental "don't care" (direct) simulation has been
implemented. This simulations consider the acceptance
of out-of-SCC transitions as "don't care". It is not
enabled by default because it currently is very slow.
- remove_x() is a function that take a formula, and rewrite it
without the X operator. The rewriting is only correct for
stutter-insensitive LTL formulas (See K. Etessami's paper in IFP
vol. 75(6). 2000) This algorithm is accessible from the
command-line using ltlfilt's --remove-x option.
- is_stutter_insensitive() takes any LTL formula, and check
whether it is stutter-insensitive. This algorithm is accessible
from the command-line using ltlfilt's --stutter-insensitive
option.
- A new translation, called compsusp(), for "Compositional
Suspension" is implemented on top of ltl_to_tgba_fm().
(See SPIN'13 paper.)
- Some experimental LTL rewriting rules that trie to gather
suspendable formulas are implemented and can be activated
with the favor_event_univ option of ltl_simplifier. As
always please check doc/tl/tl.tex for the list of rules.
- Several functions have been introduced to check the
strength of an SCC.
is_inherently_weak_scc()
is_weak_scc()
is_syntactic_weak_scc()
is_complete_scc()
is_terminal_scc()
is_syntactic_terminal_scc()
Beware that the costly is_weak_scc() function introduced in Spot
1.0, which is based on a cycle enumeration, has been renammed to
is_inherently_weak_scc() to match established vocabulary.
* Command-line tools:
- ltl2tgba and ltl2tgta now honor a new --extra-options (or -x)
flag to fine-tune the algorithms used. The available options
are documented in the spot-x (7) manpage. For instance use '-x
comp-susp' to use the afore-mentioned compositional suspension.
- The output format of 'ltlcross --json' has been changed slightly.
In a future version we will offer some reporting script that turn
such JSON output into various tables and graphs, and these change
are required to make the format usable for other benchmarks (not
just ltlcross).
- ltlcross will now count the number of non-accepting, terminal,
weak, and strong SCCs, as well as the number of terminal, weak,
and strong automata produced by each tool.
* Documentation:
- org-mode files used to generate the documentation about
command-line tools (shown at http://spot.lip6.fr/userdoc/tools.html)
is distributed in doc/org/. The resulting html files are also
in doc/userdoc/.
* Bug fixes:
- There was a memory leak in the LTL simplification code, that could
only be triggered when disabling advanced simplifications.
- The translation of the PSL formula !{xxx} was incorrect when xxx
simplified to false.
- Various warnings triggered by new compilers.
--
Alexandre Duret-Lutz
