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

Release Spot 1.0.

Browse source 
* NEWS, configure.ac: Bump version to 1.0.
This commit is contained in:
Alexandre Duret-Lutz 2012-10-27 09:30:56 +02:00
parent f9373e4a9f
commit 213b67e84b
2 changed files with 18 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

32
NEWS
View file

@ -1,4 +1,4 @@
New in spot 0.9.2a: New in spot 1.0 (2012-10-27):
* License change: Spot is now distributed using GPL v3+ instead * License change: Spot is now distributed using GPL v3+ instead
of GPL v2+. This is because we started using some third-party of GPL v2+. This is because we started using some third-party
@ -8,11 +8,11 @@ New in spot 0.9.2a:
Useful command-line tools are now installed in addition to the Useful command-line tools are now installed in addition to the
library. Some of these tools were originally written for our test library. Some of these tools were originally written for our test
suite and had evolved organically into useful programs with crapy suite and had evolved organically into useful programs with crappy
interfaces: they have now been rewritten with better argument interfaces: they have now been rewritten with better argument
parsing, saner defaults, and they come with man pages. parsing, saner defaults, and they come with man pages.
- genltl: Generate LTL formulas from scallable patterns. - genltl: Generate LTL formulas from scalable patterns.
This offers 20 patterns so far. This offers 20 patterns so far.
- randltl: Generate random LTL/PSL formulas. - randltl: Generate random LTL/PSL formulas.
@ -26,7 +26,7 @@ New in spot 0.9.2a:
equivalent, ... equivalent, ...
- ltl2tgba: Translate LTL/PSL formulas into Büchi automata (TGBA, - ltl2tgba: Translate LTL/PSL formulas into Büchi automata (TGBA,
BA, or Monitor). A fondamental change to the BA, or Monitor). A fundamental change to the
interface is that you may now specify the goal of the interface is that you may now specify the goal of the
translation: do you you favor deterministic or smaller translation: do you you favor deterministic or smaller
automata? automata?
@ -39,13 +39,15 @@ New in spot 0.9.2a:
that supports PSL in addition to LTL, and that can that supports PSL in addition to LTL, and that can
output more statistics. output more statistics.
These binaries are built in the src/bin/ directory. The former An introduction to these tools can be found on-line at
test versions of genltl and randltl have been removed from the http://spot.lip6.fr/userdoc/tools.html
source tree. The old version of ltl2tgba with its gazillion
options is still is src/tgbatest/ and is meant to be used for The former test versions of genltl and randltl have been removed
testing only. Although ltlcross is meant to replace LBTT, we from the source tree. The old version of ltl2tgba with its
are still using both tools in this release, but this is likely gazillion options is still is src/tgbatest/ and is meant to be
the last time we redistribute LBTT. used for testing only. Although ltlcross is meant to replace
LBTT, we are still using both tools in this release; however this
is likely to be the last release of Spot that redistributes LBTT.
* New features in the Spot library: * New features in the Spot library:
@ -77,7 +79,7 @@ New in spot 0.9.2a:
A discussion of these automata, part of Ala Eddine BEN SALEM's A discussion of these automata, part of Ala Eddine BEN SALEM's
PhD work, should appear in ToPNoC VI (LNCS 7400). The web-based PhD work, should appear in ToPNoC VI (LNCS 7400). The web-based
interface and the aformentioned ltl2tgta tool can be used interface and the aforementioned ltl2tgta tool can be used
to build testing automata. to build testing automata.
- TGBA can now be reduced by Reverse Simulation (in addition to - TGBA can now be reduced by Reverse Simulation (in addition to
@ -100,7 +102,7 @@ New in spot 0.9.2a:
- to_wring_string() can be used to print an LTL formula into - to_wring_string() can be used to print an LTL formula into
Wring's syntax. Wring's syntax.
- The LTL/PSL parser now has a lenient mode that can be usefull - The LTL/PSL parser now has a lenient mode that can be useful
to interpret atomic proposition with language-specific constructs. to interpret atomic proposition with language-specific constructs.
In lenient mode, any (...) or {...} block that cannot be parsed In lenient mode, any (...) or {...} block that cannot be parsed
as formula will be assumed to be an atomic proposition. as formula will be assumed to be an atomic proposition.
@ -111,14 +113,14 @@ New in spot 0.9.2a:
- minimize_obligation() has a new option to disable WDBA - minimize_obligation() has a new option to disable WDBA
minimization it cases it would produce a deterministic automaton minimization it cases it would produce a deterministic automaton
that is bigger than the original TGBA. This can help that is bigger than the original TGBA. This can help
chosing between less states or more determinism. choosing between less states or more determinism.
- new functions is_deterministic() and count_nondet_states() - new functions is_deterministic() and count_nondet_states()
(The count of nondeterministic states is now displayed on (The count of nondeterministic states is now displayed on
automata generated with the web interface.) automata generated with the web interface.)
- A new class, "postprocessor", makes it easier to apply - A new class, "postprocessor", makes it easier to apply
all availlable simplification algorithms on a TGBA/BA/Monitors. all available simplification algorithms on a TGBA/BA/Monitors.
* Minor changes: * Minor changes:

2
configure.ac
View file

@ -20,7 +20,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.61]) AC_PREREQ([2.61])
AC_INIT([spot], [0.9.2a], [spot@lrde.epita.fr]) AC_INIT([spot], [1.0], [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])