This is to announce the release of Spot 1.1.1.
The main motivation for this release is to fix a bug introduced in
version 1.1 in the post-processing of (degeneralized) Büchi automata.
Although the NEWS excerpt at the end of this email shows several
new features, most of them are related to the discovery and fix of
this bug:
1) With this release, ltl2tgba --ba --lbtt has been changed to
output automata using the state-based acceptance flavor of
the LBTT format. This makes more sense when you work with
Büchi automata.
2) This lead to the discovery that previously, when --lbtt always
output automata with transition-based acceptance, there were
some rare formulas where ltl2tgba --ba --lbtt could output
automata that where not Büchi automata (although they had
the correct language), and worse: ltl2tgba --spin could
output an incorrect neverclaim.
3) fixing this required to reimplement two functions we started using
in 1.0 but that messed the structure of Büchi automata: namely
reverse simulation and SCC-based simplification of acceptance
condition.
Two small and easy options have also been added to ltlcross.
You can find the new release here:
http://spot.lip6.fr/dl/spot-1.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.1 (2013-05-13):
* New features:
- lbtt_reachable(), the function that outputs a TGBA in LBTT's
format, has a new option to indicate that the TGBA being printed
is in fact a Büchi automaton. In this case it outputs an LBTT
automaton with state-based acceptance.
The output of the guards has also been changed in two ways:
1. atomic propositions that do not match p[0-9]+ are always
double-quoted. This avoids issues where t or f were used as
atomic propositions in the formula, output as-is in the
automaton, and read back as true or false. Other names that
correspond to LBT operators would cause problem as well.
2. formulas that label transitions are now output as
irredundant-sums-of-products.
- 'ltl2tgba --ba --lbtt' will now output automata with state-based
acceptance. You can use 'ltl2tgba --ba --lbtt=t' to force the
output of transition-based acceptance like in the previous
versions.
Some illustrations of this point and the previous one can be
found in the man page for ltl2tgba(1).
- There is a new function scc_filter_states() that removes all
useless states from a TGBA. It is actually an abbridged version
of scc_filter() that does not alter the acceptance conditions of
the automaton. scc_filter_state() should be used when
post-processing TGBAs that actually represent BAs.
- simulation_sba(), cosimulation_sba(), and
iterated_simulations_sba() are new functions that apply to TGBAs
that actually represent BAs. They preserve the imporant
property that if a state of the BA is is accepting, the outgoing
transitions of that state are all accepting in the TGBA that
represent the BA. This is something that was not preserved by
functions cosimultion() and iterated_simulations() as mentionned
in the bug fixes below.
- ltlcross has a new option --seed, that makes it possible to
change the seed used by the random graph generator.
- ltlcross has a new option --products=N to check the result of
each translation against N different state spaces, and everage
the statistics of these N products. N default to 1; larger
values increase the chances to detect inconsistencies in the
translations, and also make the average size of the product
built against the translated automata a more pertinent
statistic.
- bdd_dict::unregister_all_typed_variables() is a new function,
making it easy to unregister all BDD variables of a given type
owned by some object.
* Bug fixes:
- genltl --gh-r generated the wrong formulas due to a typo.
- ltlfilt --eventual and --universal were not handled properly.
- ltlfilt --stutter-invariant would trigger an assert on PSL formulas.
- ltl2tgba, ltl2tgta, ltlcross, and ltlfilt, would all choke on empty
lines in a file of formulas. They now ignore empty lines.
- The iterated simulation applied on degeneralized TGBA was bogus
for two reasons: one was that cosimulation was applied using the
generic cosimulation for TGBA, and the second is that
SCC-filtering, performed between iterations, was also a
TGBA-based algorithm. Both of these algorithms could lose the
property that if a TGBA represents a BA, all the outgoing
transitions of a state should be accepting. As a consequence, some
formulas where translated to incorrect Büchi automata.
--
Alexandre Duret-Lutz
