2004-02-11 Alexandre Duret-Lutz * 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 * src/TestOperations.cc: Include sys/wait.h. * src/Alloc.h: Rename as ... * src/ObstackAlloc.h: ... this. The problem is that alloc.h is a system header in g++ < 3.0, and Darwin has a case-insensitive filesystem. System headers that include alloc.h pick the local Alloc.h version. * BuchiAutomaton.h, Configuration.h, DispUtil.cc, ExternalTranslator.h, FormulaRandomizer.h, Graph.h.in, LtlFormula.h, Makefile.am, NeverClaimAutomaton.h, PathEvaluator.h, ProductAutomaton.h, SccIterator.h, SharedTestData.h, StatDisplay.h, StateSpace.h, StateSpaceRandomizer.cc, StringUtil.h, TestOperations.h, TestRoundInfo.h, TestStatistics.h, UserCommandReader.h, UserCommands.h, main.cc: Adjust includes. 2003-12-29 Alexandre Duret-Lutz * doc/texinfo.tex: New upstream version. 2003-07-29 Alexandre Duret-Lutz * 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-13 Alexandre Duret-Lutz * doc/lbtt.texi: Never use @-commands in @node names, recent Texinfo versions are stricter on this. 2003-07-10 Alexandre Duret-Lutz 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 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 of required. 2003-07-04 Alexandre Duret-Lutz * src/Config-parse.yy: Remove stray `,' in %token arguments. * src/Alloc.h (__INT_TO_PTR): Redefine to work around glibc 2.3. * doc/texinfo.tex: New upstream version. 2003-07-18 Heikki Tauriainen * 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 * 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 * 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 * BitArray.cc (BitArray::find): Fix bug in testing whether all accessed bytes were zero. 2002-10-01 Heikki Tauriainen * Version 1.0.1 released. 2002-01 -- 2002-09-25 Heikki Tauriainen * 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::Edge&) (operator<<(ostream&, const Graph::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 * Version 1.0.0 released.