diff --git a/NEWS b/NEWS index 172a76afc..c274f7806 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.3.3.dev (not yet released) +New in spot 2.3.4.dev (not yet released) Tools: @@ -85,25 +85,6 @@ New in spot 2.3.3.dev (not yet released) names from another automaton, honoring "original-states" if present. - Bugs fixed: - - - the transformation to state-based acceptance (spot::sbacc()) was - incorrect on automata where the empty acceptance mark is accepting. - - - the --help output of randaut and ltl2tgba was showing an - unsupported %b stat. - - - ltldo and ltlcross could leave temporary files behind when - aborting on error. - - - The LTL simplifcation rule that turns F(f)|q into F(f|q) - when q is a subformula that is both eventual and universal - was documented but not applied in some forgotten cases. - - - Because of some caching inside of ltl2tgba, translating multiple - formula in single ltl2tgba run could produce automata different - from those produced by individual runs. - Backward-incompatible changes: - spot::acc_cond::mark_t::operator bool() has been marked as @@ -135,6 +116,27 @@ New in spot 2.3.3.dev (not yet released) spot::twa::prop_deterministic() as a deprecated synonym for spot::twa::prop_universal() to help backward compatibility. +New in spot 2.3.4 (2017-05-11) + + Bugs fixed: + + - The transformation to state-based acceptance (spot::sbacc()) was + incorrect on automata where the empty acceptance mark is accepting. + + - The --help output of randaut and ltl2tgba was showing an + unsupported %b stat. + + - ltldo and ltlcross could leave temporary files behind when + aborting on error. + + - The LTL simplifcation rule that turns F(f)|q into F(f|q) + when q is a subformula that is both eventual and universal + was documented but not applied in some forgotten cases. + + - Because of some caching inside of ltl2tgba, translating multiple + formula in single ltl2tgba run could produce automata different + from those produced by individual runs. + New in spot 2.3.3 (2017-04-11) Tools: diff --git a/configure.ac b/configure.ac index bc4957266..3683a3336 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.3.3.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.3.4.dev], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 7b62e1d74..91dbf410b 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1060,18 +1060,17 @@ better choices. There are actually several property flags that are stored into each automaton, and that can be queried or set by algorithms: -| flag name | meaning when =true= | -|----------------------+-------------------------------------------------------------------------------------------------------------------------------------------| -| =state_acc= | automaton should be considered as having state-based acceptance | -| =inherently_weak= | accepting and rejecting cycles cannot be mixed in the same SCC | -| =weak= | transitions of an SCC all belong to the same acceptance sets | -| =very_weak= | weak automaton where all SCCs have size 1 | -| =terminal= | automaton is weak, accepting SCCs are complete, accepting edges may not go to rejecting SCCs | -| =complete= | it is always possible to move the automaton forward, using any letter | -| =universal= | there is no non-determinism branching in the automaton (hence each word is *recognized* by at most one run, but not necessarily accepted) | -| =semi_deterministic= | any nondeterminism occurs before entering an accepting SCC | -| =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) | -| =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] | +| flag name | meaning when =true= | +|----------------------+----------------------------------------------------------------------------------------------| +| =state_acc= | automaton should be considered as having state-based acceptance | +| =inherently_weak= | accepting and rejecting cycles cannot be mixed in the same SCC | +| =weak= | transitions of an SCC all belong to the same acceptance sets | +| =very_weak= | weak automaton where all SCCs have size 1 | +| =terminal= | automaton is weak, accepting SCCs are complete, accepting edges may not go to rejecting SCCs | +| =deterministic= | there is at most one run *recognizing* a word, but not necessarily accepting it | +| =semi_deterministic= | any nondeterminism occurs before entering an accepting SCC | +| =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) | +| =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] | For each flag =flagname=, the =twa= class has a method =prop_flagname()= that returns the value of the flag as an instance of diff --git a/doc/org/setup.org b/doc/org/setup.org index b60d61ef2..9e28e96ca 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,8 +1,8 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.3.3 -#+MACRO: LASTRELEASE 2.3.3 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.3.3.tar.gz][=spot-2.3.3.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-3-3/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2017-04-11 +#+MACRO: SPOTVERSION 2.3.4 +#+MACRO: LASTRELEASE 2.3.4 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.3.4.tar.gz][=spot-2.3.4.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-3-4/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2017-05-11