Commit 2fad1ff6 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* NEWS: Reorder and fix some typos.

parent 1341c656
Pipeline #2166 passed with stages
in 257 minutes and 55 seconds
......@@ -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()).
- 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.
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()).
- 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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment