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

Release Spot 2.10

Browse source 
* NEWS, configure.ac, doc/org/setup.org: Bump version.
This commit is contained in:
Alexandre Duret-Lutz 2021-11-13 11:47:28 +01:00
parent 0706887e62
commit 37de3470b8
3 changed files with 30 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

47
NEWS
View file

@ -1,4 +1,4 @@
New in spot 2.9.8.dev (not yet released) New in spot 2.10 (2021-11-13)
Build: Build:
@ -16,7 +16,7 @@ New in spot 2.9.8.dev (not yet released)
are discussed on https://spot-dev.lrde.epita.fr/ltlsynt.html are discussed on https://spot-dev.lrde.epita.fr/ltlsynt.html
+ ltlsynt now accepts only one of the --ins or --outs options to + ltlsynt now accepts only one of the --ins or --outs options to
be given and will deduce the value of this other one. be given and will deduce the value of the other one.
+ ltlsynt learned --print-game-hoa to output its internal parity + ltlsynt learned --print-game-hoa to output its internal parity
game in the HOA format (with an extension described below). game in the HOA format (with an extension described below).
@ -40,8 +40,9 @@ New in spot 2.9.8.dev (not yet released)
+ ltlsynt now has a --decompose=yes|no option to specify if + ltlsynt now has a --decompose=yes|no option to specify if
the specification should be decomposed into independent the specification should be decomposed into independent
sub-specifications, the controller of which can then be glued sub-specifications, the controllers of which can then be glued
together to satisfy the input specification. together to satisfy the input specification.
(cf. [finkbeiner.21.nfm] in doc/spot.bib)
+ ltlsynt learned --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat + ltlsynt learned --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat
to specifies how to simplify the synthesized controler. to specifies how to simplify the synthesized controler.
@ -69,10 +70,9 @@ New in spot 2.9.8.dev (not yet released)
Library: Library:
- Spot now provides convenient function to create and solve games. - Spot now provides convenient functions to create and solve games.
The functions are located in twaalgos/game.hh. Additional (twaalgos/game.hh) and some additional functions for reactive
functions related to the application to reactive synthesis are in synthesis (twaalgos/synthesis.hh, twaalgos/mealy_machine.hh).
twaalgos/synthesis.hh.
- A new class called aig represent an and-inverter-graphs, and is - A new class called aig represent an and-inverter-graphs, and is
currently used during synthesis. (twaalgos/aiger.hh) currently used during synthesis. (twaalgos/aiger.hh)
@ -154,8 +154,7 @@ New in spot 2.9.8.dev (not yet released)
well. (Issue #418.) well. (Issue #418.)
- The parity_game class has been removed, now any twa_graph_ptr that - The parity_game class has been removed, now any twa_graph_ptr that
has a parity max odd acceptance and a "state-player" property is has a "state-player" property is considered to be a game.
considered to be a parity game.
- the "state-player" property is output by the HOA printer, and read - the "state-player" property is output by the HOA printer, and read
back by the automaton parser, which means that games can be saved back by the automaton parser, which means that games can be saved
@ -244,7 +243,7 @@ New in spot 2.9.8.dev (not yet released)
"dba-simul", "dpa-simul", and "det-simul" at once. "dba-simul", "dpa-simul", and "det-simul" at once.
- tgba_powerset() now takes an extra optional argument to specify a - tgba_powerset() now takes an extra optional argument to specify a
list of accepting sinks states if some arex known. Doing so can list of accepting sinks states if some are known. Doing so can
cut the size of the powerset automaton by 2^|sinks| in favorable cut the size of the powerset automaton by 2^|sinks| in favorable
cases. cases.
@ -255,14 +254,16 @@ New in spot 2.9.8.dev (not yet released)
outgoing edge of some state. It can be used together with outgoing edge of some state. It can be used together with
purge_dead_states() to remove selected states. purge_dead_states() to remove selected states.
- Add reduce_direct_sim(), reduce_direct_cosim() and reduce_iterated() - The new functions reduce_direct_sim(), reduce_direct_cosim() and
(and their state based acceptance version, reduce_direct_sim_sba(), reduce_iterated() (and their state based acceptance version,
reduce_direct_cosim_sba() and reduce_iterated_sba()), a new reduction reduce_direct_sim_sba(), reduce_direct_cosim_sba() and
based simulation using a matrix-based implementation. This new version reduce_iterated_sba()), are matrix-based implementation of
should be faster than the signature-based BDD implementation in most simulation-based reductions. This new version is faster
cases. By default, the old one is used. This behavior can be changed by than the signature-based BDD implementation in most cases,
setting SPOT_SIMULATION_REDUCTION environment variable or using the however there are some cases it does not capture yet.. By
"-x simul-method=..." option (see spot-x(7)). default, the old one is used. This behavior can be changed by
setting SPOT_SIMULATION_REDUCTION environment variable or using
the "-x simul-method=..." option (see spot-x(7)).
- The automaton parser will now recognize lines of the form - The automaton parser will now recognize lines of the form
#line 10 "filename" #line 10 "filename"
@ -270,11 +271,11 @@ New in spot 2.9.8.dev (not yet released)
that error messages should be emitted as if the next automaton that error messages should be emitted as if the next automaton
was read from "filename" starting on line 10. (Issue #232) was read from "filename" starting on line 10. (Issue #232)
- The automaton parser for HOA will now be faster at parsing files - The automaton parser for HOA is now faster at parsing files where
where a label is used multiple times (i.e., most automata): it a label is used multiple times (i.e., most automata): it uses a
uses a hash table to avoid reconstructing BDDs corresponding to hash table to avoid reconstructing BDDs corresponding to label
label that have already been parsed. This trick was already used that have already been parsed. This trick was already used in the
in the never claim parser. never claim parser.
- spot::twa_graph::merge_states() will now sort the vector of edges - spot::twa_graph::merge_states() will now sort the vector of edges
before attempting to detect mergeable states. When merging states before attempting to detect mergeable states. When merging states

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.9.8.dev], [spot@lrde.epita.fr]) AC_INIT([spot], [2.10], [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.9.8 #+MACRO: SPOTVERSION 2.10
#+MACRO: LASTRELEASE 2.9.8 #+MACRO: LASTRELEASE 2.10
#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.8.tar.gz][=spot-2.9.8.tar.gz=]] #+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.10.tar.gz][=spot-2.10.tar.gz=]]
#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-8/NEWS][summary of the changes]] #+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-10/NEWS][summary of the changes]]
#+MACRO: LASTDATE 2021-08-10 #+MACRO: LASTDATE 2021-11-13
#+ATTR_HTML: :id spotlogo #+ATTR_HTML: :id spotlogo
[[file:spot2.svg]] [[file:spot2.svg]]