alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/lbtt/NEWS
Alexandre Duret-Lutz 6c2bdf4512 Update to LBTT 1.2.1
2008-04-10 10:20:40 +02:00

370 lines
15 KiB
Text
Raw Blame History

lbtt NEWS -- history of user-visible changes. 9 Apr 2008
Copyright (C) 2008 Heikki Tauriainen
Permission is granted to anyone to make or distribute verbatim copies
of this document as received, in any medium, provided that the
copyright notice and this permission notice are preserved.
Permission is granted to distribute modified versions
of this document, or of portions of it, under the above conditions,
provided also that they carry prominent notices stating who last
changed them.
Please send bug reports to <heikki.tauriainen@tkk.fi>.
Version 1.2.1
* Fix compilation and warnings on GCC 4.3 (thanks to Alexandre Duret-Lutz
for the patch).
Version 1.2.0
* This release adds direct support (contributed by Alexandre Duret-Lutz)
for the LTL-to-Büchi translator distributed with the Spot model
checking library (available at <http://spot.lip6.fr/>).
lbtt 1.2.0 also supports reading input formulas from standard input
(by using the command-line option `--formulafile=-'; when reading input
formulas from an actual file, the filename needs to be different from
"-").
Version 1.1.3
* This release fixes build problems with GCC 4 and more job control
problems.
Version 1.1.2
* Another bug fix release that fixes memory access and job control
problems.
Version 1.1.1
* This release includes fixes to build problems with non-GNU
compilers on GNU libc systems and a few minor bug fixes.
Version 1.1.0
* File formats
- The file format for automata description files has changed to
accommodate automata with acceptance conditions on both states
and transitions. The old format for automata remains supported
with the restriction that each guard formula of a transition
should be followed by a newline (with optional preceding white
space).
- In addition to the prefix format for LTL formulas, the input
files used with the `--formulafile' command line option may now
contain formulas in a variety of other formats, such as in the
infix format used by lbtt for log messages, together with formats
used by some LTL-to-Büchi translator implementations (Spin,
LTL2BA, LTL2AUT, Temporal Massage Parlor, Wring, Spot, LBT).
These formats can also be used for guard formulas in automaton
description files (however, lbtt still uses the prefix format in
the input files for the translators).
Thanks to Alexandre Duret-Lutz for useful suggestions for
enhancements.
* Support for symbolic names of implementations
- Beside the numeric identifiers of implementations, lbtt now
accepts also the symbolic names of implementations (as defined in
a configuration file) as parameters for command line options and
internal commands. Consequently, the names of implementations
defined in the configuration file have to be unique.
- The name `lbtt' is now reserved for lbtt's internal model checking
algorithm and cannot be used as a name for an implementation in
the configuration file.
* User commands
- For consistency, numeric intervals in state or implementation
identifier lists can now be specified using either - or ... as a
separator between the bounds of the interval.
- The user command `formula' now accepts an additional parameter
(`normal' or `nnf') for choosing whether to display a formula in
the form in which it was generated or in negation normal form.
- The internal model checking algorithm is now referred to with the
keyword "lbtt" instead of "p" as was the case with previous
versions of lbtt. The internal model checking algorithm can now be
enabled or disabled similarly to the external translators.
- The `consistencyanalysis' and `buchianalysis' commands now show
more information about the accepting runs of Büchi automata to
help examining the runs. (Because of this change, the runs and
witnesses may be longer than in previous versions of lbtt.)
- The `implementations' and `translators' commands are now recognized
as synonyms of the `algorithms' command.
* Configuration files
- Quotes are no longer required for enclosing string values
containing no white space.
- Numeric intervals in formula or state space sizes can now be
specified using either - or ... as a separator between the bounds
of the interval.
- The keywords "Implementation" and "Translator" are now recognized
as synonyms of the "Algorithm" block identifier.
* User interrupts
Keyboard interrupt handling is now enabled only at explicit request
(if not enabled, lbtt simply aborts on keyboard interrupts). The
interrupt handler is enabled by combining the keyword `onbreak' with
any of the three standard interactivity modes (`always', `never', or
`onerror') in the arguments for the `GlobalOptions.Interactive'
configuration file option or the `--interactive' command line option.
For example, use the command line option
`--interactive=onerror,onbreak' to pause testing in case of an error
or on a user interrupt.
* Command line options
- The `--pause' command line option now works identically to the
`--interactive' option.
- The command-line options `--nopause' and `--pauseonerror' are no
longer supported. Use the `--interactive' or the `--pause'
option instead with an optional argument of a comma-separated list
of interactivity modes (`always', `never', `onerror', `onbreak').
* Timeouts
lbtt now supports specifying a time (in wall-clock time) after
which the execution of a translator is aborted if it has not yet
produced a result. The timeout can be set using either the new
configuration file option `GlobalOptions.TranslatorTimeout' or the
equivalent command line option `--translatortimeout'. Both options
require a parameter of the form [hours]h[minutes]min[seconds]s; for
example, use the command line option `--translatortimeout=1h30min'
to set the timeout at one hour and thirty minutes.
* Reporting
- lbtt now reports test statistics also in verbosity modes 1 and 2.
The output of the user command `results' also reflects the active
verbosity mode more accurately.
- lbtt now exits with status 0 only if no test failures were
detected; otherwise the exit status is either 1 (at least
one failure occurred), 2 (error in program configuration or
command line parameters) or 3 (lbtt exited due to an internal
error).
* Internal changes
Due to the changes in the supported file formats, this version
includes a rewrite of the product computation and emptiness checking
algorithms. As this is a major internal change, any information about
unexpected changes in the stability (*) of the tool is welcomed at the
e-mail address given above.
(*) Unfortunately, the above changes in the source code are known to
cause build problems with GCC 2.95. Therefore, this compiler is no
longer officially supported for building the tool.
---------------------------------------------------------------------------
Version 1.0.3
* This release fixes several compilation issues with GNU libc 2.3.2
and Darwin, and documentation generation in dvi format. A problem
with reading user commands from a source that is not a terminal was
also fixed. Many thanks to Alexandre Duret-Lutz for patches and
useful suggestions.
Version 1.0.2
* Bug fix release.
* The official WWW home page of the tool is now located at
<http://www.tcs.hut.fi/Software/lbtt/>. From there you can also
access the FormulaOptions block generator for lbtt configuration
files. The generator has limited support for specifying relative
(instead of absolute) priorities for the LTL operators.
Version 1.0.1
* This release does not add new functionality to the program apart from
some bug fixes and changes to sources to make them more compatible
with versions 3.1.x and 3.2 of gcc.
Version 1.0.0
* lbtt is now packaged using GNU Autotools.
* The distribution includes sources for documentation that can be
built in `info', `dvi' and `html' formats using GNU texinfo. The
documentation is also available at the program's home page at
<http://www.tcs.hut.fi/%7Ehtauriai/lbtt/>.
* lbtt now has direct support for the following binary LTL formula
operators:
---------------------------------------------------------------
operator symbol used in input symbol used in
files for LTL-to-Büchi messages
translators
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
logical "exclusive or"
^ xor
temporal "weak until"
W W
temporal "strong release" (dual of "weak until")
M M
temporal "before"
B B
The ^ operator is also accepted in the transition guard formulas of the
Büchi automata that are given to lbtt as input.
Please see the included documentation for a reference on the exact
semantics of these operators.
* Changes in program behavior:
- The default priority for LTL formula operators is now 0 (instead of
10 as in previous versions).
- The default interval for changing state spaces is now one test round
(instead of 10 as in previous versions).
- The sequences of random formulas and state spaces generated by lbtt
should now be independent of each other, i.e., changing the formula
generation parameters does not affect the sequence of generated state
spaces and vice versa. Unfortunately, the changes required to
implement this functionality make the test sequences obtained using
previous versions of the tool irreproducible with version 1.0.0. In
addition, the random seed must now be set separately for the formula
and state space generation algorithms.
* Changes in program configuration:
- lbtt supports the following new configuration file and command line
options (`O' -- command line option, `C' -- equivalent configuration
file option (SectionName.OptionName), `D' -- description):
O: --[no]comparisontest
C: GlobalOptions.ComparisonTest = Yes | No
D: Enable or disable the model checking result cross-comparison
test
O: --[no]consistencytest
C: GlobalOptions.ConsistencyTest = Yes | No
D: Enable or disable the model checking result consistency test
O: --[no]intersectiontest
C: GlobalOptions.IntersectionTest = Yes | No
D: Enable or disable the Büchi automata intersection emptiness
test
O: --profile
D: Disable all of the above automata correctness tests
O: --skip=N
D: Skip the first N test rounds
O: --nogeneratennf
C: FormulaOptions.GenerateMode = Normal
D: Do not force random formulas to be generated in negation
normal form
O: --nooutputnnf
C: FormulaOptions.OutputMode = Normal
D: Do not rewrite LTL formulas into negation normal form before
passing them to LTL-to Büchi translators
O: --quiet, --silent
D: Run all tests silently without interruption
O: --showconfig
D: Display program configuration and exit
O: --showoperatordistribution
D: Compute the expected distribution of random formula operators
and display the distribution with other configuration
information
O: --xorpriority=PRIORITY
C: FormulaOptions.XorPriority = PRIORITY
D: Set priority for the logical "exclusive or" operator
O: --weakuntilpriority=PRIORITY
C: FormulaOptions.WeakUntilPriority = PRIORITY
D: Set priority for the temporal "weak until" operator
O: --strongreleasepriority=PRIORITY
C: FormulaOptions.StrongReleasePriority = PRIORITY
D: Set priority for the temporal "strong release" operator
O: --beforepriority=PRIORITY
C: FormulaOptions.BeforePriority = PRIORITY
D: Set priority for the temporal "before" operator
- The following configuration file and command line options have been
renamed in lbtt version 1.0.0:
Command line options:
--synchronousproduct => --modelcheck
--localproduct => --localmodelcheck
--globalproduct => --globalmodelcheck
--randomseed => --formularandomseed,
--statespacerandomseed
--formulalength => --formulasize
--vpriority => --releasepriority
Configuration file options:
GlobalOptions.FormulaChangeInterval
=> FormulaOptions.ChangeInterval
GlobalOptions.StateSpaceChangeInterval
=> StateSpaceOptions.ChangeInterval
GlobalOptions.SynchronousProduct
=> GlobalOptions.ModelCheck
GlobalOptions.RandomSeed => FormulaOptions.RandomSeed
StateSpaceOptions.RandomSeed
FormulaOptions.Length => FormulaOptions.Size
FormulaOptions.VPriority => FormulaOptions.ReleasePriority
Please see the included documentation for more information on these
options.
* Changes in the user command interface:
- lbtt's internal command interface now supports redirecting the
output of some internal commands to a pipe to be processed by an
external program. This can be achieved by ending the command line
with `| <command>'.
- If using random or enumerated paths as state spaces for the tests,
the user commands `resultanalysis' and `eval' now support referring
to results computed using lbtt's internal model checking algorithm.
- The tool includes a new user command `consistencyanalysis' that can
be used for analyzing failures in the model checking result
consistency check.
- The user command `resultanalysis' now accepts an optional state
space identifier which can be used to force the analysis to be
performed in a certain state of the state space.
- The user command `pathinconsistencies' has been removed. (The `eval'
command provides equivalent functionality.)
- lbtt now supports the GNU readline library that provides command
line editing enhancements when using the user commands. The support
can be optionally disabled by running the `configure' script with
the parameter `--without-readline'.
* The additional programs `aasa_lbt' and `spin_lbt' have been replaced with
a common `lbtt-translate' utility. This program does not implement an
LTL-to-Büchi translation algorithm, however; a free LTL-to-Büchi
translator that provides similar functionality to the `aasa_lbt' tool
included in previous lbtt releases can be obtained via
<http://www.tcs.hut.fi/Software/maria/tools/lbt/>.
Reference in a new issue View git blame Copy permalink