[lbtt] Make it clearer this is not LBTT 1.2.1.
* configure.ac: Bump the version number to 1.2.1a. * NEWS: Summarize all changes since 1.2.1. * README: Warn this is not 1.2.1, and add pointers to NEWS and ChangeLog.
This commit is contained in:
Alexandre Duret-Lutz
parent
faed4e8be2
commit
a8fd9e8b14
4 changed files with 51 additions and 12 deletions
|
|
@ -1,3 +1,12 @@
|
||||||
|
2012-05-21 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
|
Make it clearer this is not LBTT 1.2.1.
|
||||||
|
|
||||||
|
* configure.ac: Bump the version number to 1.2.1a.
|
||||||
|
* NEWS: Summarize all changes since 1.2.1.
|
||||||
|
* README: Warn this is not 1.2.1, and add pointers to NEWS and
|
||||||
|
ChangeLog.
|
||||||
|
|
||||||
2012-05-21 Tomáš Babiak <xbabiak@fi.muni.cz>
|
2012-05-21 Tomáš Babiak <xbabiak@fi.muni.cz>
|
||||||
|
|
||||||
Count deterministic automata and deterministic states.
|
Count deterministic automata and deterministic states.
|
||||||
|
|
|
||||||
43
lbtt/NEWS
43
lbtt/NEWS
|
|
@ -1,4 +1,4 @@
|
||||||
lbtt NEWS -- history of user-visible changes. 9 Apr 2008
|
lbtt NEWS -- history of user-visible changes.
|
||||||
Copyright (C) 2008 Heikki Tauriainen
|
Copyright (C) 2008 Heikki Tauriainen
|
||||||
|
|
||||||
Permission is granted to anyone to make or distribute verbatim copies
|
Permission is granted to anyone to make or distribute verbatim copies
|
||||||
|
|
@ -10,9 +10,30 @@ Copyright (C) 2008 Heikki Tauriainen
|
||||||
provided also that they carry prominent notices stating who last
|
provided also that they carry prominent notices stating who last
|
||||||
changed them.
|
changed them.
|
||||||
|
|
||||||
Please send bug reports to <heikki.tauriainen@tkk.fi>.
|
+-----------------------------------------------------------------------+
|
||||||
|
| This version of LBTT, distributed with Spot, contains several changes |
|
||||||
|
| that are not in the original version 1.2.1 released in 2008. |
|
||||||
|
| Unfortunately Heikki Tiaurainen left the TCS lab of TKK and nobody is |
|
||||||
|
| maintaining LBTT at TKK currently. Please report any issue with this |
|
||||||
|
| modified version, named 1.2.1a, to <spot@lrde.epita.fr>. The list of |
|
||||||
|
| changes follows (see ChangeLog for details). |
|
||||||
|
+-----------------------------------------------------------------------+
|
||||||
|
|
||||||
Version 1.2.1
|
Version 1.2.1a
|
||||||
|
|
||||||
|
* Fix compilation with newer versions of Bison.
|
||||||
|
* Fix compilation on Intel's icpc, and with recent version of G++.
|
||||||
|
* Fix construction of manual ("make dvi" and "make pdf") for recent
|
||||||
|
version of texinfo.
|
||||||
|
* Fix generation of random formulae on 64bit machines. (They were
|
||||||
|
all identical.)
|
||||||
|
* Do not complain about missing path to algorithm that are disabled in
|
||||||
|
the config file.
|
||||||
|
* Don't rewrite W and M operators for Spot.
|
||||||
|
* Count the number of nondeterministic states, and the number of
|
||||||
|
deterministic automata (thanks to Tomáš Babiak)
|
||||||
|
|
||||||
|
Version 1.2.1 (9 Apr 2008)
|
||||||
|
|
||||||
* Fix compilation and warnings on GCC 4.3 (thanks to Alexandre Duret-Lutz
|
* Fix compilation and warnings on GCC 4.3 (thanks to Alexandre Duret-Lutz
|
||||||
for the patch).
|
for the patch).
|
||||||
|
|
@ -20,7 +41,7 @@ Version 1.2.1
|
||||||
Version 1.2.0
|
Version 1.2.0
|
||||||
|
|
||||||
* This release adds direct support (contributed by Alexandre Duret-Lutz)
|
* This release adds direct support (contributed by Alexandre Duret-Lutz)
|
||||||
for the LTL-to-Büchi translator distributed with the Spot model
|
for the LTL-to-Büchi translator distributed with the Spot model
|
||||||
checking library (available at <http://spot.lip6.fr/>).
|
checking library (available at <http://spot.lip6.fr/>).
|
||||||
|
|
||||||
lbtt 1.2.0 also supports reading input formulas from standard input
|
lbtt 1.2.0 also supports reading input formulas from standard input
|
||||||
|
|
@ -58,7 +79,7 @@ Version 1.1.0
|
||||||
files used with the `--formulafile' command line option may now
|
files used with the `--formulafile' command line option may now
|
||||||
contain formulas in a variety of other formats, such as in the
|
contain formulas in a variety of other formats, such as in the
|
||||||
infix format used by lbtt for log messages, together with formats
|
infix format used by lbtt for log messages, together with formats
|
||||||
used by some LTL-to-Büchi translator implementations (Spin,
|
used by some LTL-to-Büchi translator implementations (Spin,
|
||||||
LTL2BA, LTL2AUT, Temporal Massage Parlor, Wring, Spot, LBT).
|
LTL2BA, LTL2AUT, Temporal Massage Parlor, Wring, Spot, LBT).
|
||||||
These formats can also be used for guard formulas in automaton
|
These formats can also be used for guard formulas in automaton
|
||||||
description files (however, lbtt still uses the prefix format in
|
description files (however, lbtt still uses the prefix format in
|
||||||
|
|
@ -95,7 +116,7 @@ Version 1.1.0
|
||||||
enabled or disabled similarly to the external translators.
|
enabled or disabled similarly to the external translators.
|
||||||
|
|
||||||
- The `consistencyanalysis' and `buchianalysis' commands now show
|
- The `consistencyanalysis' and `buchianalysis' commands now show
|
||||||
more information about the accepting runs of Büchi automata to
|
more information about the accepting runs of Büchi automata to
|
||||||
help examining the runs. (Because of this change, the runs and
|
help examining the runs. (Because of this change, the runs and
|
||||||
witnesses may be longer than in previous versions of lbtt.)
|
witnesses may be longer than in previous versions of lbtt.)
|
||||||
|
|
||||||
|
|
@ -210,7 +231,7 @@ Version 1.0.0
|
||||||
operators:
|
operators:
|
||||||
---------------------------------------------------------------
|
---------------------------------------------------------------
|
||||||
operator symbol used in input symbol used in
|
operator symbol used in input symbol used in
|
||||||
files for LTL-to-Büchi messages
|
files for LTL-to-Büchi messages
|
||||||
translators
|
translators
|
||||||
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
|
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
|
||||||
logical "exclusive or"
|
logical "exclusive or"
|
||||||
|
|
@ -223,7 +244,7 @@ Version 1.0.0
|
||||||
B B
|
B B
|
||||||
|
|
||||||
The ^ operator is also accepted in the transition guard formulas of the
|
The ^ operator is also accepted in the transition guard formulas of the
|
||||||
Büchi automata that are given to lbtt as input.
|
Büchi automata that are given to lbtt as input.
|
||||||
|
|
||||||
Please see the included documentation for a reference on the exact
|
Please see the included documentation for a reference on the exact
|
||||||
semantics of these operators.
|
semantics of these operators.
|
||||||
|
|
@ -262,7 +283,7 @@ Version 1.0.0
|
||||||
|
|
||||||
O: --[no]intersectiontest
|
O: --[no]intersectiontest
|
||||||
C: GlobalOptions.IntersectionTest = Yes | No
|
C: GlobalOptions.IntersectionTest = Yes | No
|
||||||
D: Enable or disable the Büchi automata intersection emptiness
|
D: Enable or disable the Büchi automata intersection emptiness
|
||||||
test
|
test
|
||||||
|
|
||||||
O: --profile
|
O: --profile
|
||||||
|
|
@ -279,7 +300,7 @@ Version 1.0.0
|
||||||
O: --nooutputnnf
|
O: --nooutputnnf
|
||||||
C: FormulaOptions.OutputMode = Normal
|
C: FormulaOptions.OutputMode = Normal
|
||||||
D: Do not rewrite LTL formulas into negation normal form before
|
D: Do not rewrite LTL formulas into negation normal form before
|
||||||
passing them to LTL-to Büchi translators
|
passing them to LTL-to Büchi translators
|
||||||
|
|
||||||
O: --quiet, --silent
|
O: --quiet, --silent
|
||||||
D: Run all tests silently without interruption
|
D: Run all tests silently without interruption
|
||||||
|
|
@ -364,7 +385,7 @@ Version 1.0.0
|
||||||
|
|
||||||
* The additional programs `aasa_lbt' and `spin_lbt' have been replaced with
|
* The additional programs `aasa_lbt' and `spin_lbt' have been replaced with
|
||||||
a common `lbtt-translate' utility. This program does not implement an
|
a common `lbtt-translate' utility. This program does not implement an
|
||||||
LTL-to-Büchi translation algorithm, however; a free LTL-to-Büchi
|
LTL-to-Büchi translation algorithm, however; a free LTL-to-Büchi
|
||||||
translator that provides similar functionality to the `aasa_lbt' tool
|
translator that provides similar functionality to the `aasa_lbt' tool
|
||||||
included in previous lbtt releases can be obtained via
|
included in previous lbtt releases can be obtained via
|
||||||
<http://www.tcs.hut.fi/Software/maria/tools/lbt/>.
|
<http://www.tcs.hut.fi/Software/maria/tools/lbt/>.
|
||||||
|
|
|
||||||
|
|
@ -1,3 +1,12 @@
|
||||||
|
+-----------------------------------------------------------------------+
|
||||||
|
| This version of LBTT, distributed with Spot, contains several changes |
|
||||||
|
| that are not in the original version 1.2.1 released in 2008. |
|
||||||
|
| Unfortunately Heikki Tiaurainen left the TCS lab of TKK and nobody is |
|
||||||
|
| maintaining LBTT at TKK currently. Please report any issue with this |
|
||||||
|
| modified version, named 1.2.1a, to <spot@lrde.epita.fr>. See NEWS |
|
||||||
|
| and ChangeLog for the list of changes. |
|
||||||
|
+-----------------------------------------------------------------------+
|
||||||
|
|
||||||
lbtt version 1.2.1
|
lbtt version 1.2.1
|
||||||
------------------
|
------------------
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
# Process this file with autoconf to produce a configure script.
|
# Process this file with autoconf to produce a configure script.
|
||||||
|
|
||||||
AC_PREREQ([2.59])
|
AC_PREREQ([2.59])
|
||||||
AC_INIT([lbtt], [1.2.1], [heikki.tauriainen@tkk.fi])
|
AC_INIT([lbtt], [1.2.1a], [heikki.tauriainen@tkk.fi])
|
||||||
AC_REVISION([Revision: 1.9])
|
AC_REVISION([Revision: 1.9])
|
||||||
AC_CONFIG_SRCDIR([src/main.cc])
|
AC_CONFIG_SRCDIR([src/main.cc])
|
||||||
AC_CONFIG_HEADERS([config.h])
|
AC_CONFIG_HEADERS([config.h])
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue