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

Release Spot 2.11

Browse source 
* NEWS, configure.ac, doc/org/setup.org: Update version.
This commit is contained in:
Alexandre Duret-Lutz 2022-10-08 20:59:27 +02:00
parent 1a5b5602db
commit 8131fae1a6
3 changed files with 31 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

47
NEWS
View file

@ -1,26 +1,26 @@
New in spot 2.10.6.dev (not yet released) New in spot 2.11 (2022-10-08)
Build: Build:
- configure will now diagnose situation where Python bindings will - configure will now diagnose situations where Python bindings will
be installed in a directory that is not part of Python's search be installed in a directory that is not part of Python's search
path. A new configure option --with-pythondir can be used to path. A new configure option --with-pythondir can be used to
modify this installation path. modify this installation path.
- A new configure option --enable-pthread enable the compilation of - A new configure option --enable-pthread enables the compilation of
Spot with -pthread, and activate the parallel version of some Spot with -pthread, and render available the parallel version of
algorithms. If Spot is compiled with -pthread enabled, any user some algorithms. If Spot is compiled with -pthread enabled, any
linking with Spot should also link with the pthread library. In user linking with Spot should also link with the pthread library.
order to not break existing build setups using Spot, this option In order to not break existing build setups using Spot, this
is currently disabled by default in this release. We plan to turn option is currently disabled by default in this release. We plan
it on by default in some future release. Third-party project to turn it on by default in some future release. Third-party
using Spot may want to start linking with -pthread in prevision project using Spot may want to start linking with -pthread in
for this change. prevision for this change.
Command-line tools: Command-line tools:
- autfilt has a new options --aliases=drop|keep to specify - autfilt has a new options --aliases=drop|keep to specify
if the output code should attempt to preserve aliases if the HOA printer should attempt to preserve aliases
present in the HOA input. This defaults to "keep". present in the HOA input. This defaults to "keep".
- autfilt has a new --to-finite option, illustrated on - autfilt has a new --to-finite option, illustrated on
@ -79,11 +79,11 @@ New in spot 2.10.6.dev (not yet released)
- tgba_determinize() learned to fill the "original-classes" property. - tgba_determinize() learned to fill the "original-classes" property.
States of the determinized automaton that correspond to the same States of the determinized automaton that correspond to the same
subset of states of the original automaton belong to the same subset of states of the original automaton belong to the same
class. Filling this property is only done on demand has it inccurs class. Filling this property is only done on demand as it inccurs
on small overhead. a small overhead.
- sbacc() learned to take the "original-classes" property into - sbacc() learned to take the "original-classes" property into
account and preserve it. account and to preserve it.
- The HOA parser and printer learned to map the synthesis-outputs - The HOA parser and printer learned to map the synthesis-outputs
property of Spot to the controllable-AP header for the Extended property of Spot to the controllable-AP header for the Extended
@ -148,10 +148,10 @@ New in spot 2.10.6.dev (not yet released)
is a co-Büchi automaton. And product_or() learned that the is a co-Büchi automaton. And product_or() learned that the
"or"-product of two Büchi automata is a Büchi automaton. "or"-product of two Büchi automata is a Büchi automaton.
- spot::postprocessor has a new extra option merge-states-min that - spot::postprocessor has a new extra option "merge-states-min" that
indicate above how many states twa_graph::merge_states(), which indicates above how many states twa_graph::merge_states() (which
perform a very cheap pass to fuse states with identicall perform a very cheap pass to fuse states with identicall
succesors, should be called before running simulation-based succesors) should be called before running simulation-based
reductions. reductions.
- A new function delay_branching_here(aut) can be used to simplify - A new function delay_branching_here(aut) can be used to simplify
@ -164,15 +164,18 @@ New in spot 2.10.6.dev (not yet released)
further simplification. This was introduced to help with automata further simplification. This was introduced to help with automata
produced from formulas output by "genltl --eil-gsi" (see above). produced from formulas output by "genltl --eil-gsi" (see above).
- spot::postprocessor has new configuration variable branch-post that - spot::postprocessor has new configuration variable branch-post
can be used to control the use of branching-postponement (diabled that can be used to control the use of branching-postponement
by default) or delayed-branching (see above, enabled by default). (disabled by default) or delayed-branching (see above, enabled by
See the spot-x(7) man page for details. default). See the spot-x(7) man page for details.
- spot::postprocessor is now using acd_transform() by default when - spot::postprocessor is now using acd_transform() by default when
building parity automata. Setting option "acd=0" will revert building parity automata. Setting option "acd=0" will revert
to using "to_parity()" instead. to using "to_parity()" instead.
- to_parity() has been almost entirely rewritten and is a bit
faster.
- When asked to build parity automata, spot::translator is now more - When asked to build parity automata, spot::translator is now more
aggressively using LTL decomposition, as done in the Generic aggressively using LTL decomposition, as done in the Generic
acceptance case before paritizing the result. This results in acceptance case before paritizing the result. This results in

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.69]) AC_PREREQ([2.69])
AC_INIT([spot], [2.10.6.dev], [spot@lrde.epita.fr]) AC_INIT([spot], [2.11], [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.10.6 #+MACRO: SPOTVERSION 2.11
#+MACRO: LASTRELEASE 2.10.6 #+MACRO: LASTRELEASE 2.11
#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.10.6.tar.gz][=spot-2.10.6.tar.gz=]] #+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.11.tar.gz][=spot-2.11.tar.gz=]]
#+MACRO: LASTNEWS [[https://gitlab.lre.epita.fr/spot/spot/blob/spot-2-10-6/NEWS][summary of the changes]] #+MACRO: LASTNEWS [[https://gitlab.lre.epita.fr/spot/spot/blob/spot-2-11/NEWS][summary of the changes]]
#+MACRO: LASTDATE 2022-05-18 #+MACRO: LASTDATE 2022-10-08
#+ATTR_HTML: :id spotlogo #+ATTR_HTML: :id spotlogo
[[file:spot2.svg]] [[file:spot2.svg]]