Spot-announce

Download

spot-announce@lrde.epita.fr

August 2016

1 participants
1 discussions

Spot 2.1 was released
by Alexandre Duret-Lutz 08 Aug '16

08 Aug '16

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>. 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

1 0