ChangeLog 10.5 KB
Newer Older
1
2
2004-01-16  Alexandre Duret-Lutz  <adl@src.lip6.fr>

3
4
	* src/TestOperations.cc: Include sys/wait.h.

5
6
7
8
9
10
11
12
13
14
15
16
17
	* 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.

18
19
20
21
2003-12-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* doc/texinfo.tex: New upstream version.

22
23
24
25
26
27
28
29
30
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-13  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
31
32
33
34

	* doc/lbtt.texi: Never use @-commands in @node names, recent Texinfo
	versions are stricter on this.

35
36
37
38
39
40
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.
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
41

42
43
2003-07-09  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

44
45
46
47
48
	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):
49
50
51
52
53
54
55
	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.

56
57
58
59
60
61
2003-07-04  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
2003-07-18  Heikki Tauriainen  <heikki.tauriainen@hut.fi>

	* UserCommands.cc (printAutomatonAnalysisResults): Ensure that
	the states in a witness for the nonemptiness of two Bchi
	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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
94
95
96
97
98
99
100
101
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.
102

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
103
104
105
	* BitArray.cc (BitArray::BitArray): Do not clear the allocated
	array after initialization. All callers updated to reflect the
	changed constructor semantics.
106

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
107
108
109
110
111
	* BitArray.cc (BitArray::bitwiseAnd, BitArray::bitwiseOr)
	(BitArray::bitwiseXor): New functions.

	* BitArray.cc (BitArray::equal, BitArray::subset)
	(BitArray::count): Fix `&' operator precedence in comparisons.
112

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
113
114
115
	* BitArray.cc (BitArray::hammingDistance): Use the `bit_counts'
	array to compute the result instead of scanning the array bit by
	bit.
116

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
	* 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.

140
	* BuchiAutomaton.h (BuchiAutomaton::regularize): Changed
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
	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.
172

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
173
174
175
176
177
178
	* 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.
179

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
	* 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).
236

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
237
238
239
240
241
242
243
244
245
246
247
248
	* 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.
249

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
	* 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.
275

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
276
277
278
279
	* TestRoundInfo.h: Removed redundant inclusion of BitArray.h.

	* translate.cc (main): Use autoconf-generated PACKAGE_VERSION
	macro for displaying program version.
280

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
281
282
283
284
285
286
287
288
289
290
	* 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.
291

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
292
293
294
2001-11-12  Heikki Tauriainen  <heikki.tauriainen@hut.fi>

	* Version 1.0.0 released.