345 lines
12 KiB
Text
345 lines
12 KiB
Text
2004-03-08 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||
|
||
* doc/texinfo.tex: New upstream version.
|
||
|
||
2004-02-11 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||
|
||
* src/ExternalTranslator.cc: Include sys/wait.h.
|
||
|
||
* src/SpotWrapper.cc (SpotWrapper::SPOT_AND, SpotWrapper::SPOT_OR):
|
||
Define as && and || as in Spin.
|
||
* src/SpotWrapper.hh: Update by email.
|
||
|
||
2004-01-16 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||
|
||
* src/TestOperations.cc: Include sys/wait.h.
|
||
|
||
2003-07-29 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||
|
||
* src/TestOperations.cc (generateBuchiAutomaton): Forward SIGINT
|
||
and SIGQUIT.
|
||
* src/ExternalTranslator.cc (ExternalTranslator::translate): Likewise.
|
||
* src/main.cc (main): Do not intercept SIGINT in
|
||
non-interactive runs.
|
||
|
||
2003-07-10 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||
|
||
Spot wants `^', not `xor'.
|
||
* src/SpotWrapper.hh (SpotWrapper::SPOT_XOR): Declare.
|
||
* src/SpotWrapper.cc (SpotWrapper::SPOT_XOR): Define.
|
||
(SpotWrapper::translateFormula): Use SPOT_XOR.
|
||
|
||
2003-07-09 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||
|
||
I want $? = 1 whenever some test fails.
|
||
* src/main.cc (testLoop): Return 1 iff an error occured.
|
||
(main): Use testLoop's output as exit status.
|
||
|
||
* src/ExternalTranslator.h (class ExternalTranslator):
|
||
Declare class SpotWrapper as a friend.
|
||
* src/SpotWrapper.h, src/SpotWrapper.cc: New files.
|
||
* src/Makefile.am (lbtt_translate_SOURCES): Add SpotWrapper.cc
|
||
and SpotWrapper.h.
|
||
* src/translate.cc (main): Add the --spot option, and build
|
||
a SpotWrapper if required.
|
||
|
||
2004-02-13 Heikki Tauriainen <heikki.tauriainen@hut.fi>
|
||
|
||
* src/BitArray.{h,cc}, src/BuchiAutomaton.{h,cc},
|
||
src/Configuration.{h,cc}, src/DispUtil.{h,cc},
|
||
src/ExternalTranslator.{h,cc}, src/FormulaRandomizer.{h,cc},
|
||
src/LtlFormula.{h,cc}, src/NeverClaimAutomaton.{h,cc},
|
||
src/PathEvaluator.{h,cc}, src/PathIterator.{h,cc},
|
||
src/ProductAutomaton.{h,cc}, src/SpinWrapper.{h,cc},
|
||
src/StatDisplay.{h,cc}, src/StateSpace.{h,cc},
|
||
src/StateSpaceRandomizer.{h,cc}, src/StringUtil.{h,cc},
|
||
src/TestOperations.{h,cc}, src/TestStatistics.{h,cc},
|
||
src/translate.{h,cc}, src/UserCommandReader.{h,cc},
|
||
src/UserCommands.{h,cc}: Remove all #pragmas.
|
||
|
||
2004-02-12 Heikki Tauriainen <heikki.tauriainen@hut.fi>
|
||
|
||
* doc/texinfo.tex: New upstream version.
|
||
|
||
* doc/lbtt.texi: Update edition to 1.0.2.
|
||
Remove node names with commands to fix dvi file generation.
|
||
Move the node about the lbtt-translate utility to correct menu.
|
||
Reformat the automata file format section to avoid overfull lines
|
||
in dvi generation.
|
||
Fix description of the Algorithm block used with lbtt-translate.
|
||
|
||
* doc/testprocedure.txt, doc/intersectioncheck.txt: Add initial
|
||
newlines.
|
||
|
||
2004-02-11 Heikki Tauriainen <heikki.tauriainen@hut.fi>
|
||
|
||
* src/UserCommandReader.cc [HAVE_ISATTY]: Include the unistd.h
|
||
header.
|
||
(executeUserCommands) Stop waiting for new commands if an EOF is
|
||
detected. [HAVE_ISATTY]: If standard input is not connected to a
|
||
terminal, echo the input line.
|
||
|
||
2004-02-10 Heikki Tauriainen <heikki.tauriainen@hut.fi>
|
||
|
||
* configure.ac: Remove duplicate checks for headers.
|
||
(GLIBC_OBSTACK_WORKAROUND): New config.h macro for checking for a
|
||
version of the obstack.h header that requires a workaround to be
|
||
compiled with g++.
|
||
Add check for the `isatty' library function.
|
||
Include the stdio.h header when testing for readline libraries.
|
||
|
||
* src/Alloc.h: Rename to LbttAlloc.h to avoid a name conflict with
|
||
system header files on Darwin.
|
||
[GLIBC_OBSTACK_WORKAROUND] (__INT_TO_PTR): Redefine macro to
|
||
work around a C++ bug in the obstack.h header file in glibc 2.3.2.
|
||
Thanks to Alexandre Duret-Lutz for the original patch.
|
||
|
||
* src/BuchiAutomaton.h, src/Configuration.h, src/DispUtil.cc,
|
||
src/ExternalTranslator.h, src/FormulaRandomizer.h, src/Graph.h.in,
|
||
src/LtlFormula.h, src/main.cc, src/Makefile.am,
|
||
src/NeverClaimAutomaton.h, src/PathEvaluator.h,
|
||
src/ProductAutomaton.h, src/SccIterator.h, src/SharedTestData.h,
|
||
src/StatDisplay.h, src/StateSpace.h, src/StateSpaceRandomizer.cc,
|
||
src/StringUtil.h, src/TestOperations.h, src/TestRoundInfo.h,
|
||
src/TestStatistics.h, src/UserCommandReader.h,
|
||
src/UserCommands.h: Adjust includes.
|
||
|
||
* Update copyright information in source files.
|
||
|
||
2003-07-04 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||
|
||
* src/Config-parse.yy: Remove stray `,' in %token arguments.
|
||
|
||
2003-07-18 Heikki Tauriainen <heikki.tauriainen@hut.fi>
|
||
|
||
* UserCommands.cc (printAutomatonAnalysisResults): Ensure that
|
||
the states in a witness for the nonemptiness of two B<>chi
|
||
automata are distinct to prevent the truth valuation for the
|
||
atomic propositions from being defined multiple times in any
|
||
state of the witness.
|
||
|
||
* Version 1.0.2 released.
|
||
|
||
2003-07-17 Heikki Tauriainen <heikki.tauriainen@hut.fi>
|
||
|
||
* NeverClaimAutomaton.cc (ParseErrorException::ParseErrorException):
|
||
Fix a string buffer overflow.
|
||
|
||
* ProductAutomaton.cc (findAcceptingExecution): Concatenate
|
||
fragments of an accepting cycle in the correct order. (Thanks to
|
||
Joachim Klein for pointing out an example uncovering the bug
|
||
in previous releases.)
|
||
|
||
2002-11-04 Heikki Tauriainen <heikki.tauriainen@hut.fi>
|
||
|
||
* StatDisplay.cc (printCollectiveStats): If using more than five
|
||
formula operators (but the total number of operators is not
|
||
a multiple of 5), insert an empty line in the output before the
|
||
last row of the operator distribution table.
|
||
|
||
2002-10-21 Heikki Tauriainen <heikki.tauriainen@hut.fi>
|
||
|
||
* BitArray.cc (BitArray::find): Fix bug in testing whether
|
||
all accessed bytes were zero.
|
||
|
||
2002-10-01 Heikki Tauriainen <heikki.tauriainen@hut.fi>
|
||
|
||
* Version 1.0.1 released.
|
||
|
||
2002-01 -- 2002-09-25 Heikki Tauriainen <heikki.tauriainen@hut.fi>
|
||
|
||
* Alloc.h: Use preprocessor macro HAVE_SINGLE_CLIENT_ALLOC
|
||
instead of HAVE_SGI_STL in #ifdef conditionals.
|
||
|
||
* BitArray.cc (BitArray::BitArray): Do not clear the allocated
|
||
array after initialization. All callers updated to reflect the
|
||
changed constructor semantics.
|
||
|
||
* BitArray.cc (BitArray::bitwiseAnd, BitArray::bitwiseOr)
|
||
(BitArray::bitwiseXor): New functions.
|
||
|
||
* BitArray.cc (BitArray::equal, BitArray::subset)
|
||
(BitArray::count): Fix `&' operator precedence in comparisons.
|
||
|
||
* BitArray.cc (BitArray::hammingDistance): Use the `bit_counts'
|
||
array to compute the result instead of scanning the array bit by
|
||
bit.
|
||
|
||
* BitArray.cc: Documentation fixes.
|
||
|
||
* BitArray.h (BitArray::bitwiseAnd, BitArray::bitwiseOr)
|
||
(BitArray::bitwiseXor): New functions.
|
||
|
||
* BitArray.h: Documentation fixes.
|
||
|
||
* Bitset.h (Bitset::Bitset(const BitArray&, const unsigned long))
|
||
(Bitset::Bitset(const Bitset&)): Use `memcpy' instead of
|
||
`BitArray::copy'.
|
||
|
||
* Bitset.h (Bitset::operator=(const Bitset&)): Reallocate memory
|
||
only if necessary.
|
||
|
||
* Bitset.h: Documentation fixes.
|
||
|
||
* BuchiAutomaton.cc (BuchiAutomaton::regularize): Changed
|
||
semantics: instead of modifying the object itself, the function
|
||
now returns a pointer to a newly allocated BuchiAutomaton (the
|
||
regularized automaton).
|
||
|
||
* BuchiAutomaton.cc: Documentation fixes.
|
||
|
||
* BuchiAutomaton.h (BuchiAutomaton::regularize): Changed
|
||
semantics (see above).
|
||
|
||
* BuchiAutomaton.h
|
||
(BuchiAutomaton::BuchiTransition::enabled(const BitArray&,
|
||
const unsigned int)): New function.
|
||
(BuchiAutomaton::BuchiTransition::enabled(const Bitset&)):
|
||
Use the above function internally.
|
||
|
||
* BuchiAutomaton.h
|
||
(BuchiAutomaton::BuchiState::print(ostream&, const int, const
|
||
GraphOutputFormat)): New function.
|
||
|
||
* BuchiAutomaton.h (BuchiAutomaton::BuchiTransition::operator<)
|
||
(BuchiAutomaton::BuchiTransition::operator==): Fix function
|
||
prototypes to match those of the base class. Make functions
|
||
private to prevent external comparison of plain Graph::Edges
|
||
with BuchiAutomaton::BuchiTransitions.
|
||
|
||
* Configuration.cc (Configuration::read): Use autoconf-generated
|
||
PACKAGE_VERSION macro for displaying program version instead of
|
||
including version.h.
|
||
|
||
* configure.in: Renamed to configure.ac. Updated to Autoconf
|
||
2.53 and Automake 1.6. Improved checking for the presence of
|
||
the slist STL extension. Revised checking for the availability of
|
||
the GNU readline library and the libraries to include.
|
||
Replace the old preprocessor macro HAVE_SGI_STL with new macros
|
||
HAVE_SINGLE_CLIENT_ALLOC and HAVE_SLIST. Introduce new
|
||
preprocessor macro SLIST_NAMESPACE.
|
||
|
||
* EdgeContainer.h: Remove uses of redundant preprocessor macros.
|
||
|
||
* Graph.h: Renamed to Graph.h.in to implement the optional
|
||
inclusion of the slist header using an autoconf substitution
|
||
variable.
|
||
|
||
* Graph.h.in: Use HAVE_SLIST macro instead of HAVE_SGI_STL in
|
||
#ifdef conditionals.
|
||
|
||
* Graph.h.in (Graph::Edge, Graph::Node): Make classes public (to
|
||
prevent warnings from Intel C++ Compiler).
|
||
|
||
* Graph.h.in (Graph::operator[], Graph::node, Graph::size)
|
||
(Graph::expand, Graph::stats, Graph::subGraphStats)
|
||
(Graph::Edge::targetNode, Graph::Node::operator=)
|
||
(operator<<(ostream&, const Graph<GraphEdgeContainer>::Edge&)
|
||
(operator<<(ostream&, const Graph<GraphEdgeContainer>::Node&):
|
||
Added explicit `typename' specifiers to parameter and/or return
|
||
types (to prevent warnings from gcc 3.1).
|
||
|
||
* Graph.h.in (Graph::subGraphStats): Make `s' a const variable.
|
||
|
||
* Graph.h.in (Graph::Edge::ptr_equal::ptr_equal): Change
|
||
definition to match that of `Graph::Edge::ptr_less'. All callers
|
||
modified accordingly.
|
||
|
||
* Graph.h.in (Graph::Edge::operator<, Graph::Edge::operator==):
|
||
Make member functions protected.
|
||
Make class Graph::Edge a friend of Graph::Edge::ptr_equal and
|
||
Graph::Edge::ptr_less.
|
||
|
||
* LtlFormula.cc (LtlFormula): New static variable
|
||
`eval_proposition_id_limit' stores the maximum proposition
|
||
id during the evaluation of a strictly propositional formula.
|
||
|
||
* LtlFormula.cc (LtlFormula::sat_eval): Make `max_atom' a const
|
||
variable.
|
||
Access the identifier of a proposition through Atom::getId.
|
||
|
||
* LtlFormula.h
|
||
(LtlFormula::evaluate(const BitArray&, const unsigned long int)):
|
||
New function.
|
||
(LtlFormula::evaluate(const Bitset&)): Use the above function
|
||
internally.
|
||
|
||
* LtlFormula.h (ptr_less): Make class public.
|
||
|
||
* LtlFormula.h (LtlFormula::eval): Use a BitArray instead of a
|
||
Bitset internally.
|
||
|
||
* LtlFormula.h (Atom::eval, Constant::eval, LtlNegation::eval)
|
||
(UnaryFormula::eval, LtlNext::eval, LtlFinally::eval)
|
||
(LtlGlobally::eval, BinaryFormula::eval, LtlDisjunction::eval)
|
||
(LtlConjunction::eval, LtlImplication::eval, LtlEquivalence::eval)
|
||
(LtlXor::eval, LtlUntil::eval, LtlV::eval, LtlWeakUntil::eval)
|
||
(LtlStrongRelease::eval, LtlBefore::eval): Use BitArray instead
|
||
of a Bitset for evaluation. Make subformula parameters (if any)
|
||
`const'.
|
||
|
||
* main.cc (testLoop): Use autoconf-generated PACKAGE_VERSION
|
||
macro for displaying program version instead of including
|
||
version.h.
|
||
|
||
* src/Makefile.am: Remove redundant references to @LEXLIB@ (the
|
||
sources are independent of any external lexer library).
|
||
|
||
* NeverClaimAutomaton.cc (NeverClaimAutomaton::write): Add
|
||
detection for jumps to undefined never claim labels.
|
||
|
||
* NeverClaim-parse.yy (yyerror): Fix computation of the position
|
||
of a parse error.
|
||
|
||
* PathEvaluator.cc (PathEvaluator::eval) Avoid creating a
|
||
temporary Bitset object during evaluation of atomic propositions.
|
||
|
||
* ProductAutomaton.cc (ProductAutomaton::computeProduct):
|
||
Avoid creating a temporary Bitset object when checking the
|
||
enabledness of a product transition.
|
||
|
||
* ProductAutomaton.cc (ProductAutomaton::findAcceptingExecution)
|
||
Use BitArrays instead of Bitsets.
|
||
|
||
* ProductAutomaton.h (ProductAutomaton::operator[])
|
||
(ProductAutomaton::node): Make state id parameter `const'.
|
||
|
||
* ProductAutomaton.h (ProductAutomaton::ProductState::print):
|
||
Change function prototype to match that of the base class.
|
||
|
||
* SccIterator.h: Add `typename' specifiers to prevent warnings
|
||
from gcc 3.1.
|
||
|
||
* SpinWrapper.cc (SpinWrapper::SpinAutomaton::parseAutomaton):
|
||
Remove redundant `try' block.
|
||
|
||
* StateSpace.cc (StateSpace::State::print): Fix typo when
|
||
displaying empty sets of propositions in dot format (the open
|
||
brace was previously missing).
|
||
|
||
* StateSpace.h
|
||
(StateSpace::print(ostream&, const int, const GraphOutputFormat):
|
||
New function.
|
||
|
||
* TestOperations.cc (performEmptinessCheck): Added a colon to
|
||
the end of the "Accepting cycles" message.
|
||
|
||
* TestRoundInfo.h: Removed redundant inclusion of BitArray.h.
|
||
|
||
* translate.cc (main): Use autoconf-generated PACKAGE_VERSION
|
||
macro for displaying program version.
|
||
|
||
* translate.cc (main): Fix bug in checking the number of
|
||
command line arguments.
|
||
|
||
* UserCommands.cc (printCrossComparisonAnalysisResults): Fix
|
||
bug in the construction of the witness path in which the formula
|
||
should be evaluated when the witness path is extracted directly
|
||
from the original state space (i.e., when analyzing results
|
||
against the internal model checking algorithm).
|
||
|
||
* version.h.in: Removed.
|
||
|
||
2001-11-12 Heikki Tauriainen <heikki.tauriainen@hut.fi>
|
||
|
||
* Version 1.0.0 released.
|