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 2017-05-11 10:18:00 +02:00
commit 7dfa0ec15d
4 changed files with 39 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

42
NEWS
View file

@ -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:

2
configure.ac
View file

@ -21,7 +21,7 @@
# along with this program. If not, see <http://www.gnu.org/licenses/>.
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])

23
doc/org/concepts.org
View file

@ -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

10
doc/org/setup.org
View file

@ -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