191 lines
7.9 KiB
Text
191 lines
7.9 KiB
Text
lbtt NEWS -- history of user-visible changes. 01 Oct 2002
|
|
Copyright (C) 2002 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@hut.fi>.
|
|
|
|
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/>.
|