alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

release Spot 2.9

Browse source 
* configure.ac, doc/org/setup.org, NEWS: Set version to 2.9.
This commit is contained in:
Alexandre Duret-Lutz 2020-04-30 09:00:35 +02:00
parent ce2529b27b
commit eeb5713a30
3 changed files with 20 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

20
NEWS
View file

@ -1,4 +1,4 @@
New in spot 2.8.7.dev (not yet released) New in spot 2.9 (2020-04-30)
Command-line tools: Command-line tools:
@ -22,7 +22,7 @@ New in spot 2.8.7.dev (not yet released)
select a range of their input formulas or automata (assuming a select a range of their input formulas or automata (assuming a
1-based numbering). 1-based numbering).
- When running translators ltlcross will now display {names} when - When running translators, ltlcross will now display {names} when
supplied. supplied.
- ltlcross is now using the generic emptiness check procedure - ltlcross is now using the generic emptiness check procedure
@ -96,8 +96,13 @@ New in spot 2.8.7.dev (not yet released)
and the automaton is adjusted so that i also appears where j and the automaton is adjusted so that i also appears where j
appeared. appeared.
- acc_code::unit_propagation() is a new method for performing unit
propagation in acceptance condition. E.g. Fin(0) | (Inf(0) &
Inf(1)) becomes Fin(0) | Inf(1). This is now called by
simplify_acceptance_here().
- propagate_marks_vector() and propagate_marks_here() are helper - propagate_marks_vector() and propagate_marks_here() are helper
functions for propagatings marks on the automaton: ignoring functions for propagating marks on the automaton: ignoring
self-loops and out-of-SCC transitions, marks common to all the self-loops and out-of-SCC transitions, marks common to all the
input transitions of a state can be pushed to all its outgoing input transitions of a state can be pushed to all its outgoing
transitions, and vice-versa. This is repeated until a fix point transitions, and vice-versa. This is repeated until a fix point
@ -112,20 +117,23 @@ New in spot 2.8.7.dev (not yet released)
same transition structure (where the ..._maybe() variant would same transition structure (where the ..._maybe() variant would
modify the Rabin automaton if needed). modify the Rabin automaton if needed).
- to_parity() has been rewritten now combines several strategies for - to_parity() has been rewritten. It now combines several strategies
paritizing automata with any acceptance condition. for paritizing automata with any acceptance condition.
- relabel_bse(), used by ltlfilt --relabel-bool, is now better at - relabel_bse(), used by ltlfilt --relabel-bool, is now better at
dealing with n-ary operators and isolating subsets of operands dealing with n-ary operators and isolating subsets of operands
that can be relabeled as a single term. that can be relabeled as a single term.
- print_dot() default was changed to use circles for automata with - print_dot()'s default was changed to use circles for automata with
fewer than 10 unamed states, ellipses for automata with up to 1000 fewer than 10 unamed states, ellipses for automata with up to 1000
unamed states (or named states with up to 4 characters), and unamed states (or named states with up to 4 characters), and
rounded rectangles otherwise. Rectangles are also used for rounded rectangles otherwise. Rectangles are also used for
automata with acceptance bullets on states. The new "E" option automata with acceptance bullets on states. The new "E" option
can be used to force rectangles in all situations. can be used to force rectangles in all situations.
- The generic emptiness check has been slightly improved (doing
fewer recursive calls in the worst case).
Backward-incompatible changes: Backward-incompatible changes:
- iar() and iar_maybe() have been moved from - iar() and iar_maybe() have been moved from

2
configure.ac
View file

@ -21,7 +21,7 @@
# along with this program. If not, see <http://www.gnu.org/licenses/>. # along with this program. If not, see <http://www.gnu.org/licenses/>.
AC_PREREQ([2.63]) AC_PREREQ([2.63])
AC_INIT([spot], [2.8.7.dev], [spot@lrde.epita.fr]) AC_INIT([spot], [2.9], [spot@lrde.epita.fr])
AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_AUX_DIR([tools])
AC_CONFIG_MACRO_DIR([m4]) AC_CONFIG_MACRO_DIR([m4])
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])

10
doc/org/setup.org
View file

@ -1,11 +1,11 @@
#+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil #+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil
#+EMAIL: spot@lrde.epita.fr #+EMAIL: spot@lrde.epita.fr
#+HTML_LINK_HOME: index.html #+HTML_LINK_HOME: index.html
#+MACRO: SPOTVERSION 2.8.7 #+MACRO: SPOTVERSION 2.9
#+MACRO: LASTRELEASE 2.8.7 #+MACRO: LASTRELEASE 2.9
#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.7.tar.gz][=spot-2.8.7.tar.gz=]] #+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.tar.gz][=spot-2.9.tar.gz=]]
#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-7/NEWS][summary of the changes]] #+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9/NEWS][summary of the changes]]
#+MACRO: LASTDATE 2020-03-13 #+MACRO: LASTDATE 2020-04-30
#+ATTR_HTML: :id spotlogo #+ATTR_HTML: :id spotlogo
[[file:spot2.svg]] [[file:spot2.svg]]