201 lines
7.2 KiB
Text
201 lines
7.2 KiB
Text
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.
|