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 . 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 . * 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 `| '. - 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 .