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

Merge branch 'master' into next

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2020-03-13 08:07:16 +01:00
commit e827d3a634
3 changed files with 25 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

21
NEWS
View file

@ -1,4 +1,4 @@
New in spot 2.8.6.dev (not yet released) New in spot 2.8.7.dev (not yet released)
Command-line tools: Command-line tools:
@ -103,10 +103,12 @@ New in spot 2.8.6.dev (not yet released)
- car() is a new variant of LAR algorithm that combines several - car() is a new variant of LAR algorithm that combines several
strategies for paritizing any automaton. strategies for paritizing any automaton.
New in spot 2.8.7 (2019-03-13)
Bugs fixed: Bugs fixed:
- Building a product between two complete automata where one operand - Building a product between two complete automata where one operand
had false acceptance could create a incomplete automaton had false acceptance could create an incomplete automaton
incorrectly tagged as complete, causing the print_hoa() function incorrectly tagged as complete, causing the print_hoa() function
to raise an exception. to raise an exception.
@ -119,6 +121,21 @@ New in spot 2.8.6.dev (not yet released)
wrong. This could in turn cause segfaults or infinite loops while wrong. This could in turn cause segfaults or infinite loops while
running autcross or autfilt --stats=%w. running autcross or autfilt --stats=%w.
- The generic emptiness check used a suboptimal selection of "Fin"
to remove, not matching the correct line in our ATVA'19 paper.
This could cause superfluous recursive calls, however benchmarks
have shown the difference to be insignificant in practice.
- The sl(), and sl2() functions for computing the "self-loopization"
of an automaton, and used for instance in algorithms for computing
proof of stutter-sensitiveness (e.g., in our web application),
were incorrect when applied on automata with "t" acceptance (or
more generaly, any automaton where a cycle without mark is
accepting).
- ltlcross was not diagnosing write errors associated to
options --grind=FILENAME and --save-bogus=FILENAME.
New in spot 2.8.6 (2020-02-19) New in spot 2.8.6 (2020-02-19)
Bugs fixed: Bugs fixed:

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.6.dev], [spot@lrde.epita.fr]) AC_INIT([spot], [2.8.7.dev], [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.6 #+MACRO: SPOTVERSION 2.8.7
#+MACRO: LASTRELEASE 2.8.6 #+MACRO: LASTRELEASE 2.8.7
#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.6.tar.gz][=spot-2.8.6.tar.gz=]] #+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.7.tar.gz][=spot-2.8.7.tar.gz=]]
#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-6/NEWS][summary of the changes]] #+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-7/NEWS][summary of the changes]]
#+MACRO: LASTDATE 2020-02-19 #+MACRO: LASTDATE 2020-03-13
#+ATTR_HTML: :id spotlogo #+ATTR_HTML: :id spotlogo
[[file:spot2.svg]] [[file:spot2.svg]]