8 Aug
2016
8 Aug
'16
5:28 p.m.
We are happy to announce the release of Spot 2.1.
Spot 2.1 is mainly a collection of small improvements that have
accumulated since the release of Spot 2.0 four months ago. A
detailed list of those is given below.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.1.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
As always, please direct any feedback to <spot(a)lrde.epita.fr>fr>.
New in spot 2.1 (2016-08-08)
Command-line tools:
* All tools that input formulas or automata (i.e., autfilt,
dstar2tgba, ltl2tgba, ltl2tgta, ltlcross, ltldo, ltlfilt,
ltlgrind) now have a more homogeneous handling of the default
input.
- If no formula/automaton have been specified, and the standard
input is a not a tty, then the default is to read that. This is a
change for ltl2tgba and ltl2tgta. In particular, it simplifies
genltl --dac | ltl2tgba -F- | autfilt ...
into
genltl --dac | ltl2tgba | autfilt ...
- If standard input is a tty and no other input has been
specified, then an error message is printed. This is a change for
autfilt, dstar2tgba, ltlcross, ltldo, ltlfilt, ltlgrind, that used
to expect the user to type formula or automata at the terminal,
confusing people.
- All tools now accept - as a shorthand for -F-, to force reading
input from the standard input (regardless of whether it is a tty
or not). This is a change for ltl2tgba, ltl2tgta, ltlcross, and
ltldo.
* ltldo has a new option --errors=... to specify how to deal
with errors from executed tools.
* ltlcross and ltldo learned to bypass the shell when executing
simple commands (with support for single or double-quoted
arguments, and redirection of stdin and stdout, but nothing more).
* ltlcross and ltldo learned a new syntax to specify that an input
formula should be written in some given syntax after rewriting
some operators away. For instance the defaults arguments passed
to ltl2dstar have been changed from
--output-format=hoa %L %O
into
--output-format=hoa %[WM]L %O
where [WM] specifies that operators W and M should be rewritten
away. As a consequence running
ltldo ltl2dstar -f 'a M b'
will now work and call ltl2dstar on the equivalent formula
'b U (a & b)' instead. The operators that can be listed between
brackets are the same as those of ltlfilt --unabbreviate option.
* ltlcross learned to show some counterexamples when diagnosing
failures of cross-comparison checks against random state spaces.
* autfilt learned to filter automata by count of SCCs (--sccs=RANGE)
or by type of SCCs (--accepting-sccs=RANGE,
--rejecting-sccs=RANGE, trivial-sccs=RANGE, --terminal-sccs=RANGE,
--weak-sccs=RANGE, --inherently-weak-sccs=RANGE).
* autfilt learned --remove-unused-ap to remove atomic propositions
that are declared in the input automaton, but not actually used.
This of course makes sense only for input/output formats that
declare atomic propositions (HOA & DSTAR).
* autfilt learned two options to filter automata by count of used or
unused atomic propositions: --used-ap=RANGE --unused-ap=RANGE.
These differ from --ap=RANGE that only consider *declared* atomic
propositions, regardless of whether they are actually used.
* autfilt learned to filter automata by count of nondeterministsic
states with --nondet-states=RANGE.
* autfilt learned to filter automata representing stutter-invariant
properties with --is-stutter-invariant.
* autfilt learned two new options to highlight non-determinism:
--highlight-nondet-states=NUM and --highlight-nondet-states=NUM
where NUM is a color number. Additionally --highlight-nondet=NUM is
a shorthand for using the two.
* autfilt learned to highlight a run matching a given word using the
--highlight-word=[NUM,]WORD option. However currently this only
work on automata with Fin-less acceptance.
* autfilt learned two options --generalized-rabin and
--generalized-streett to convert the acceptance conditions.
* genltl learned three new families: --dac-patterns=1..45,
--eh-patterns=1..12, and --sb-patterns=1..27. Unlike other options
these do not output scalable patterns, but simply a list of formulas
appearing in these three papers: Dwyer et al (FMSP'98), Etessami &
Holzmann (Concur'00), Somenzi & Bloem (CAV'00).
* genltl learned two options, --positive and --negative, to control
wether formulas should be output after negation or not (or both).
* The formater used by --format (for ltlfilt, ltlgrind, genltl,
randltl) or --stats (for autfilt, dstar2tgba, ltl2tgba, ltldo,
randaut) learned to recognize double-quoted fields and double the
double-quotes output inbetween as expected from RFC4180-compliant
CSV files. For instance
ltl2tgba -f 'a U "b+c"' --stats='"%f",%s'
will output
"a U ""b+c""",2
* The --csv-escape option of genltl, ltlfilt, ltlgrind, and randltl
is now deprecated. The option is still here, but hidden and
undocumented.
* The --stats option of autfilt, dstar2tgba, ltl2tgba, ltldo,
randaut learned to display the output (or input if that makes
sense) automaton as a HOA one-liner using %h (or %H), helping to
create CSV files contained automata.
* autfilt and dstar2tgba learned to read automata from columns in
CSV files, specified using the same filename/COLUMN syntax used by
tools reading formulas.
* Arguments passed to -x (in ltl2tgba, ltl2tgta, autfilt, dstar2tgba)
that are not used are now reported as they might be typos.
This ocurred a couple of times in our test-suite. A similar
check is done for the arguments of autfilt --sat-minimize=...
Library:
* The print_hoa() function will now output version 1.1 of the HOA
format when passed the "1.1" option (i.e., use -H1.1 from any
command-line tool). As far as Spot is concerned, this allows
negated properties to be expressed. Version 1 of the HOA format
is still the default, but we plan to default to version 1.1 in the
future.
* The "highlight-states" and "highlight-edges" named properties,
which were introduced in 1.99.8, will now be output using
"spot.highlight.edges:" and "spot.highlight.states:" headers if
version 1.1 of the HOA format is selected. The automaton parser
was secretly able of reading that since 1.99.8, but that is now
documented at https://spot.lrde.epita.fr/hoa.html#extensions
* highlight_nondet_states() and highlight_nondet_edges() are
new functions that define the above two named properties.
* is_deterministic(), is_terminal(), is_weak(), and
is_inherently_weak(), count_nondet_states(),
highlight_nondet_edges(), highlight_nondet_states() will update
the corresponding properties of the automaton as a side-effect of
their check.
* the sbacc() function, used by "ltl2tgba -S" and "autfilt -S" to
convert automata to state-based acceptance, learned some tricks
(using SCCs, pulling accepting marks common to all outgoing edges,
and pushing acceptance marks common to all incoming edges) to
reduce the number of additional states needed.
* to_generalized_rabin() and to_generalized_streett() are two new
functions that convert the acceptance condition as requested
without changing the transition structure.
* language_containment_checker now has default values for all
parameters of its constructor.
* spot::twa_run has a new method, project(), that can be used to
project a run found in a product onto one of the original operand.
This is for instance used by autfilt --highlight-word.
The old spot::project_twa_run() function has been removed: it was
not used anywhere in Spot, and had an obvious bug in its
implementation, so it cannot be missed by anyone.
* spot::twa has two new methods that supplement is_empty():
twa::accepting_run() and twa::accepting_word(). They compute
what their names suggest. Note that twa::accepting_run(), unlike
the two others, is currently restricted to automata with Fin-less
acceptance.
* spot::check_stutter_invariance() can now work on non-deterministic
automata for which no corresponding formula is known. This
implies that "autfilt --check=stutter" will now label all
automata, not just deterministic automata.
* New LTL and PSL simplification rules:
- if e is pure eventuality and g => e, then e U g = Fg
- if u is purely universal and u => g, then u R g = Gg
- {s[*0..j]}[]->b = {s[*1..j]}[]->b
- {s[*0..j]}<>->b = {s[*1..j]}<>->b
* spot::twa::succ_iterable renamed to
spot::internal::twa_succ_iterable to make it clear this is not for
public consumption.
* spot::fair_kripke::state_acceptance_conditions() renamed to
spot::fair_kripke::state_acceptance_mark() for consistency. This
is backward incompatible, but we are not aware of any actual use
of this method.
Python:
* The __format__() method for formula supports the same
operator-rewritting feature introduced in ltldo and ltlcross.
So "{:[i]s}".format(f) is the same as
"{:s}".format(f.unabbreviate("i")).
* Bindings for language_containment_checker were added.
* Bindings for randomize() were added.
* Iterating over edges via "aut.out(s)" or "aut.edges()"
now allows modifying the edge fields.
* Under IPython the spot.ltsmin module now offers a
%%pml magic to define promela models, compile them
with spins, and dynamically load them. This is
akin to the %%dve magic that was already supported.
* The %%dve and %%pml magics honor the SPOT_TMPDIR and
TMPDIR environment variables. This especially helps
when the current directory is read-only.
Documentation:
* A new example page shows how to test the equivalence of
two LTL/PSL formulas. https://spot.lrde.epita.fr/tut04.html
* A new page discusses explicit vs. on-the-fly interfaces for
exploring automata in C++. https://spot.lrde.epita.fr/tut50.html
* Another new page shows how to implement an on-the-fly Kripke
structure for a custom state space.
https://spot.lrde.epita.fr/tut51.html
* The concepts.html page now lists all named properties
used by automata.
Bug fixes:
* When ltlcross found a bug using a product of complemented
automata, the error message would report "Comp(Ni)*Comp(Pj)" as
non-empty while the actual culprit was "Comp(Nj)*Comp(Pi)".
* Fix some non-deterministic execution of minimize_wdba(), causing
test-suite failures with the future G++ 7, and clang 3.9.
* print_lbtt() had a memory leak when printing states without
successors.
--
Alexandre Duret-Lutz