From 2fad1ff6de7a248f8770709a1cf6ce5d16ed69e6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 8 Jun 2018 17:40:36 +0200 Subject: [PATCH] * NEWS: Reorder and fix some typos. --- NEWS | 130 +++++++++++++++++++++++++++++------------------------------ 1 file changed, 64 insertions(+), 66 deletions(-) diff --git a/NEWS b/NEWS index b91319830..1e9291ae2 100644 --- a/NEWS +++ b/NEWS @@ -2,13 +2,6 @@ New in spot 2.5.3.dev (not yet released) Command-line tools: - - autcross' tool specifications now have %M replaced by the name of - the input automaton. - - - autcross now aborts if there is any parser diagnostic for the - input automata (previous versions would use the input automaton - whenever the parser would manage to read something). - - autfilt learned --is-colored to filter automata that use exactly one acceptance set per mark or transition. @@ -16,6 +9,13 @@ New in spot 2.5.3.dev (not yet released) to keep automata that have universal branching, or that make non-deterministic choices. + - autcross' tool specifications now have %M replaced by the name of + the input automaton. + + - autcross now aborts if there is any parser diagnostic for the + input automata (previous versions would use the input automaton + whenever the parser would manage to read something). + - ltlcross, ltldo, and autcross learned shorthands to call delag, ltl2dra, ltl2dgra, and nba2dpa. @@ -48,8 +48,42 @@ New in spot 2.5.3.dev (not yet released) Library: - - print_dot(), used print automata in GraphViz's format, underwent - several changes: + - The PSL/LTL simplification routine learned the following: + + q R Xf = X(q R f) if q is suspendable + q U Xf = X(q U f) if q is suspendable + {SERE;1} = {1} if {SERE} accepts [*0] + {SERE;1} = {SERE} if {SERE} does not accept [*0] + + - spot::product() and spot::product_or() learned to produce an + automaton with a simpler acceptance condition if one of the + argument is a weak automaton. In this case the resulting + acceptance condition is (usually) that of the other argument. + + - gf_guarantee_to_ba() is a specialized construction for translating + formulas of the form GF(guarantee) to BA or DBA, and + fg_safety_to_dca() is a specialized construction for translating + formulas of the form FG(safety) to DCA. These are generalizations + of some constructions proposed by J. Esparza, J. Křentínský, and + S. Sickert (LICS'18). + + These are now used by the main translation routine, and can be + disabled by passing -x '!gf-guarantee' to ltl2tgba. For example, + here are the size of deterministic transition-based Büchi automata + constructed from four GF(guarantee) formulas with two versions of + Spot, and converted to other types of deterministic automata by + other tools. + + ltl2tgba -D rabinizer 4 + 2.5 2.6 delag ltl2dra + ------------------------- ----------- ------------- + GF(a <-> XXa) 9 4 4 9 + GF(a <-> XXXa) 27 8 8 25 + GF(((a & Xb) | XXc) & Xd) 6 4 16 5 + GF((b | Fa) & (b R Xb)) 6 2 3 3 + + - print_dot(), used to print automata in GraphViz's format, + underwent several changes: * option "a", for printing the acceptance condition, is now enabled by default. Option "A", introduced in Spot 2.4, can be @@ -79,64 +113,24 @@ New in spot 2.5.3.dev (not yet released) usually the default. - spot::twa_graph::merge_states() is a new method that merges states - with the exact same outgoing edges. As it performs no reordering of - the edges, it is better to call it when you know that the edges in - the twa_graph are sorted (e.g. after a call to merge_edges()). + with the exact same outgoing edges. As it performs no reordering + of the edges, it is better to call it when you know that the edges + in the twa_graph are sorted (e.g. after a call to merge_edges()). - - cleanup_parity() and cleanup_parity_here() are smarter and now - remove from the acceptance condition the parity colors that are - not used in the automaton. - - - twa_graph::purge_unreachable_states() now takes a function which - is called with the new numbering of states. This is useful to - update an external structure that references states of the twa + - spot::twa_graph::purge_unreachable_states() now takes a function + which is called with the new numbering of states. This is useful + to update an external structure that references states of the twa that we want to purge. - - the PSL simplification routines learned that {SERE;1} can be - simplified to {1} or {SERE} depending on whether SERE accepts - the empty word or not. - - - gf_guarantee_to_ba() is a specialized construction for translating - formulas of the form GF(guarantee) to BA or DBA, and - fg_safety_to_dca() is a specialized construction for translating - formulas of the form FG(safety) to DCA. These are generalizations - of some constructions proposed by J. Esparza, J. Křentínský, and - S. Sickert (LICS'18). - - These are now used by the main translation routine, and can be - disabled by passing -x '!gf-guarantee' to ltl2tgba. For example, - here are the size of deterministic transition-based Büchi automata - constructed from four GF(guarantee) formulas with two versions of - Spot, and converted to other types of deterministic automata by - other tools. - - ltl2tgba -D rabinizer 4 - 2.5 2.6 delag ltl2dra - ------------------------- ----------- ------------- - GF(a <-> XXa) 9 4 4 9 - GF(a <-> XXXa) 27 8 8 25 - GF(((a & Xb) | XXc) & Xd) 6 4 16 5 - GF((b | Fa) & (b R Xb)) 6 2 3 3 - - - Slightly improved log output for the SAT-based minimization - functions. The CSV log files now include an additional column - with the size of the reference automaton, and they now have a - header line. These log files give more details and are more - accurate in the case of incremental SAT-solving. The python - bindings for sat_minimize() now have a display_log and return_log - options; there are demonstrated on the new - https://spot.lrde.epita.fr/ipynb/satmin.html page. + - spot::cleanup_parity() and spot::cleanup_parity_here() are smarter + and now remove from the acceptance condition the parity colors + that are not used in the automaton. - spot::contains() and spot::are_equivalent() can be used to check language containement between two automata or formulas. They are most welcome in Python, since we used to redefine them every now and them. - - spot::product() and spot::product_or() learned to produce an - automaton with a simpler acceptance condition if one of the - argument is a weak automaton. In this case the resulting - acceptance condition is (usually) that of the other argument. - - spot::remove_alternation() was slightly improved on very-weak alternating automata: the labeling of the outgoing transitions in the resulting TGBA makes it more likely that simulation-based @@ -145,15 +139,15 @@ New in spot 2.5.3.dev (not yet released) - When applied to automata that are not WDBA-realizable, spot::minimize_wdba() was changed to produce an automaton recognizing a language that includes the original one. As a - consequence spot::minimize_obligation() now only needs one - containement check instead of two. + consequence spot::minimize_obligation() and + spot::is_wdba_realizable() now only need one containement check + instead of two. - - The LTL simplification routine learned the following reductions, - where f is any formula, and q is a "suspendable" formula (a.k.a. - both a pure eventuality and purely universal). - - q R Xf = X(q R f) - q U Xf = X(q U f) + - Slightly improved log output for the SAT-based minimization + functions. The CSV log files now include an additional column + with the size of the reference automaton, and they now have a + header line. These log files give more details and are more + accurate in the case of incremental SAT-solving. Python: @@ -166,6 +160,10 @@ New in spot 2.5.3.dev (not yet released) as arguments to functions that expect formulas. Previously this was done only for a few functions. + - The Python bindings for sat_minimize() now have display_log and + return_log options; these are demonstrated on the new + https://spot.lrde.epita.fr/ipynb/satmin.html page. + Bugs fixed: - print_dot() will correctly escape strings containing \n in HTML