ChangeLog 181 KB
Newer Older
1
2
3
4
5
6
2004-11-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbatest/emptchkr.test: Try degeneralized automata.
	* src/tgbatest/randtgba.cc (main): Pass the correct automaton to
	minimize_run().

7
8
2004-11-28  Alexandre Duret-Lutz  <adl@src.lip6.fr>

9
10
11
12
13
	* src/ltltest/equals.cc (main): Add option -E.
	* src/ltltest/parseerr.test: Use `equals -E' instead of `readltl'
	to check the parsing of erroneous strings without being sensible
	to the ordering for formulae in memory.

14
15
16
	* src/tgbatest/randtgba.cc (to_float): Use strtod() instead of
	strtof() to please Solaris 9.

17
18
19
	* configure.ac (AM_INIT_AUTOMAKE): Use option tar-ustar, we have
	filenames longer than 99 bytes.

20
21
22
23
	* wrap/python/tests/run.in: Do not override PYTHONPATH, just add
	to it.
	Report from Akim Demaille.

24
25
26
	* src/sanity/style.test: Make sure grep supports the options put
	into GREP_OPTIONS.

27
28
29
30
	* wrap/python/tests/run.in: Define DYLD_LIBRARY_PATH so that
	Darwin finds non-installed libraries.
	Report from Akim Demaille.

31
32
	* src/tgbatest/ltl2tgba.cc (syntax): Mention gv04 in help text.

33
34
35
36
37
2004-11-27  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/minimizerun.cc: Shut up a GCC warning when assert
	are disabled.

38
39
40
41
42
43
44
45
46
47
2004-11-27  Alexandre Duret-Lutz  <adl@src.lip6.fr>
	    Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>

	* src/tgbaalgos/minimizerun.hh, src/tgbaalgos/minimizerun.cc: New
	files.
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
	libtgbaalgos_la_SOURCES): Add them/
	* src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add option -m.
	* src/tgbatest/emptchkr.test: Use -m.

48
49
50
51
52
53
54
55
56
2004-11-25  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>

	* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
	src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
	src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.hh,
	src/tgbaalgos/tau03opt.cc: Fix comments and debug traces

	* src/tgbatest/randtgba.cc: Adjust names of algorithms.

57
58
2004-11-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>

59
60
	* src/tgbatest/randtgba.cc: Add option -D.

61
62
63
64
65
66
67
68
	* src/tgbaalgos/emptiness.hh (emptiness_check, emptiness_check_result):
	Add the TGBA considered as a protected attribute, and provide an
	automaton() accessor.
	* src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc,
	src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc,
	src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/gtec.cc: Adjust to follow
	this new interface.

69
70
2004-11-24  Alexandre Duret-Lutz  <adl@src.lip6.fr>

71
72
73
74
	* src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: Revert
	previous change (bfs_steps_with_path_conditions turned up
	useless), and document bfs_step.

75
76
77
78
	* src/tgbaalgos/bfssteps.hh (bfs_steps_with_path_conditions): New
	class.
	* src/tgbaalgos/bfssteps.cc: Remove includes that are now superfluous.

79
80
81
82
	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run,
	couvreur99_check_result::accepting_cycle): Rewrite the BFSs using
	the bfs_steps class.

83
84
85
86
87
88
	* src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: New files.
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
	libtgbaalgos_la_SOURCES): Add them.
	* src/tgbaalgos/gv04.cc (gv04::result::accepting_run): Use
	the new bfs_steps class.

89
90
91
92
93
94
95
2004-11-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/gv04.cc (gv04::result): New struct to compute
	counter examples.
	(gv04:check): Return a gv04::result.

2004-11-23  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
96
97
98

	* src/tgbaalgos/tau03opt.cc: Fix a warning.

99
100
2004-11-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

101
102
103
104
105
	* src/tgbaalgos/gv04.cc (gv04): Inherit from ec_statistics.
	(gv04::check, gv04::push, gv04::pop): Update the statistics for
	randtgba.
	(gv04::print_stats): Print them here too.

106
107
108
109
110
	* src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check,
	couvreur99_check_shy::check): Compute more statistics for
	randtgba.
	(couvreur99_check::print_stats): Print these here too.

111
112
	* src/sanity/style.test: Allow "'" after ",".

113
114
115
116
117
118
119
120
121
	* src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh: New files, partly
	based on Thomas Martinez's src/tgbaalgos/tarjan_on_fly.cc and
	src/tgbaalgos/tarjan_on_fly.hh former implementation.
	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES,
	tgbaalgos_HEADERS): Add them.
	* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Bind the
	new algorithm.
	* src/tgbatest/emptchk.test: Test it.

122
2004-11-22  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
123
124
125
126
127
128
129
130
131
132
133
134
135
136

	* src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/weight.cc,
	src/tgbaalgos/weight.hh: New files.
	* src/tgbaalgos/Makefile.am: Add them.
	* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc,
	src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc,
	src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/status.cc,
	src/tgbaalgos/gtec/status.hh, : Add emptiness check statistics
	capability.
	* src/tgbatest/randtgba.cc: Print these statistics.
	* src/tgbatest/ltl2tgba.cc: tau03opt search can deal without acceptance
	condition.
	* src/tgbatest/emptchk.test: Test tau03opt search.

137
138
139
140
141
142
143
144
145
2004-11-19  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc,
	src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc,
	src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03.cc,
	src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: Fix
	copyright year, and do not include <iterator>.

2004-11-18  Alexandre Duret-Lutz  <adl@src.lip6.fr>
146
147
148
149

	* src/tgbatest/randtgba.cc (main): Add options -z and -Z for statistics.
	(ce_stat): New struct.

150
2004-11-17  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
151
152
153
154
155
156
157
158
159
160

	* src/tgbaalgos/se05.hh, src/tgbaalgos/tau03.hh: Typo.
	* src/tgbaalgos/tau03.cc: Suppress optimisations, the algorithm is now
	the original one.
	* src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: New files
	implementing most of all the optimisations of tau03.
	* src/tgbaalgos/Makefile.am: Add them.
	* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Make them public.
	* src/tgbatest/tba_samples_from_spin.test: Test them.

161
162
2004-11-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>

163
164
165
	* src/tgba/tgba.hh, src/tgbaalgos/ltl2tgba_fm.hh,
	src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/stats.hh: Typos.

166
167
168
169
170
171
	* src/tgbatest/Makefile.am (EXTRA_DIST): Distribute the files
	from tba_samples_from_spin.
	* src/tgbatest/tba_samples_from_spin.test: Get these example files
	from $srcdir, for the sake of VPATH builds.
	(light_run): Remove, not needed.

172
173
174
175
176
177
	* src/misc/bareword.hh, src/misc/bddalloc.hh, src/misc/bddlt.hh,
	src/misc/escape.hh, src/misc/freelist.hh, src/misc/hash.hh,
	src/misc/hashfunc.hh, src/misc/minato.hh, src/misc/modgray.hh,
	src/misc/random.hh, src/misc/version.hh, src/tgba/state.hh: More
	Doxygen groups.

178
2004-11-17  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
179
180
181
182
183
184
185
186
187
188

	* src/tgbaalgos/magic.hh: Fix a comment and remove se05 interface.
	* src/tgbaalgos/magic.cc: Fix a comment.
	* src/tgbaalgos/se05.hh: New file.
	* src/tgbaalgos/se05.cc: Fix a comment.
	* src/tgbaalgos/tau03.hh: New file.
	* src/tgbaalgos/tau03.cc: New file.
	* src/tgbaalgos/Makefile.am: Add it.
	* src/tgbatest/ltl2tgba.cc: Add tau03 new emptiness check.
	* src/tgbatest/randtgba.cc: Add tau03 new emptiness check.
189
	* src/tgbatest/emptchkr.test: Fix a comment.
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
	* src/tgbatest/tba_samples_from_spin/explicit1_1.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_2.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_3.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_4.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_5.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_6.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_7.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_8.tba,
	src/tgbatest/tba_samples_from_spin/explicit1_9.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_1.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_2.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_3.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_4.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_5.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_6.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_7.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_8.tba,
	src/tgbatest/tba_samples_from_spin/explicit2_9.tba: New files
	* src/tgbatest/tba_samples_from_spin.test : New test.
	* src/tgbatest/Makefile.am: Add it.

211
212
2004-11-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>

213
214
215
216
217
218
219
220
221
222
223
	* src/tgba/tgba.hh, src/tgbaalgos/dotty.hh,
	src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
	src/tgbaalgos/emptiness.hh, src/tgbaalgos/lbtt.hh,
	src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh,
	src/tgbaalgos/neverclaim.hh, src/tgbaalgos/powerset.hh,
	src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh,
	src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.hh,
	src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh
	src/tgbaalgos/save.hh, src/tgbaalgos/stats.hh,
	src/tgbaparse/public.hh: Add Doxygen groups for TGBA algorithms.

224
225
226
227
228
229
230
231
232
233
234
235
236
	* src/ltlast/atomic_prop.hh, src/ltlast/binop.hh,
	src/ltlast/constant.hh, src/ltlast/formula.hh,
	src/ltlast/multop.hh, src/ltlast/refformula.hh,
	src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.hh,
	src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh,
	src/ltlparse/public.hh, src/ltlvisit/apcollect.hh,
	src/ltlvisit/basicreduce.hh, src/ltlvisit/clone.hh,
	src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh,
	src/ltlvisit/dump.hh, src/ltlvisit/length.hh,
	src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh: Add Doxygen
	groups for LTL algorithms and types.
	* doc/Makefile.am (fast-doc): New target.

237
238
239
	* src/misc/hashfunc.hh: Include cstddef to define size_t, and guard
	the file for multiple inclusions.

240
241
242
243
244
245
246
247
248
249
250
251
252
	* src/tgba/bdddict.hh, src/tgba/state.hh, src/tgba/statebdd.hh,
	src/tgba/succiter.hh, src/tgba/succiterconcrete.hh,
	src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
	src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbaexplicit.hh,
	src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh,
	src/tgba/tgbatba.hh, src/tgbaalgos/emptiness.hh,
	src/tgbaalgos/magic.hh, src/tgbaalgos/replayrun.hh,
	src/tgbaalgos/gtec/gtec.hh, iface/gspn/ssp.hh: Introduce Doxygen
	groups in the documentation.  Presently this only covers the
	tgba/ directory, and the emptiness-check algorithms.
	* doc/Doxyfile.in (EXCLUDE_PATTERNS): Skip Bison-generated files
	in src/evtgbaparse/.

253
254
2004-11-16  Alexandre Duret-Lutz  <adl@src.lip6.fr>

255
256
257
258
259
260
261
262
263
264
265
266
267
	* src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the
	functionality of the old tgba_tba_proxy.
	* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator,
	tgba_tba_proxy): Rewrite to produce TBA with at most N copies of
	each state, skipping the `bddtrue' stage now used only in
	tgba_sba_proxy.  Doing so removes approximately 6% of states in
	the degeneralized tests of spotlbtt.test.
	(tgba_sba_proxy): Implement it.
	* src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: Adjust
	to take a tgba_sba_proxy.
	* src/tgbatest/ltl2tgba.cc: Add option -DS and adjust call to
	never_claim_reachable().

268
269
270
	* src/tgba/tgbatba.cc (state_tba_proxy::hash): Use wang32_hash.
	* src/tgba/tgbaproduct.cc (state_product::hash): Likewise.

271
272
273
274
275
	* src/misc/hashfunc.hh (wang32_hash): New file and function,
	extracted from...
	* src/evtgba/product.cc (evtgba_product_state::hash): ... here.
	* src/misc/Makefile.am (misc_HEADERS): Add hashfunc.hh.

276
2004-11-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>
277
278
279
280
281
282
283

	* src/tgbatest/ltl2tgba.cc (main): For non-generalized emptiness
	check, degeneralize the automaton only if it has too much
	acceptance conditions.  This makes it easier to reproduce runs
	of randtgba.
	* src/tgbatest/emptchk.test: Adjust.

284
2004-11-15  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
285
286
287
288
289

	* src/tgbaalgos/magic.cc: Fix a stupid bug.
	* src/tgbaalgos/se05.cc: Fix the same bug.
	* src/tgbatest/Makefile.am: Signify that emptchkr.test pass.

290
291
2004-11-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>

292
293
294
295
	* tgbatest/randtgba.cc: Add options -e and -r.
	* tgbatest/emptchkr.test: New file.
	* src/tgbatest/Makefile.am (TESTS, XFAIL_TESTS): Add emptchkr.test.

296
297
298
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix a memory leak
	if debug==false.

299
300
301
302
	* src/tgbaalgos/randomgraph.cc (random_graph): Do declare all the
	acceptance conditions in the produced automaton, in case they are
	not actually used.

303
304
305
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Write to the
	supplied stream, not std::cout.

306
2004-11-15  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
307
308
309
310
311
312
313
314

	* src/tgbaalgos/magic.cc: Add a bit state hashing version.
	* src/tgbaalgos/se05.cc: Add a bit state hashing version.
	* src/tgbaalgos/magic.hh: Make them public.
	* src/tgbatest/ltl2tgba.cc: Add the two new emptiness checks.
	* src/tgbatest/emptchk.test: Incorporate tests of src/tgbatest/dfs.test.
	* src/tgbatest/dfs.test: Introduce new characteristic explicit tests.

315
316
317
318
319
320
321
2004-11-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* wrap/python/cgi/ltl2tgba.in: Add options to check the produced
	automata for emptiness, using the existing algorithms.
	* wrap/python/spot.i: Declare spot::explicit_magic_search,
	and spot::explicit_se05_search as allocating their output.

322
323
2004-11-12  Alexandre Duret-Lutz  <adl@src.lip6.fr>

324
325
326
327
	* configure.ac: Check for srand48 and drand48.
	* src/misc/random.cc (srand, drand): Use srand48 and drand48 if
	available.

328
329
330
331
332
333
334
335
	* src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: New files.
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS)
	(libtgbaalgos_la_SOURCES): Add them.
	* src/tgba/tgbaexplicit.hh (tgba_explicit::add_state): Make it public.
	* src/tgbatest/randtgba.cc: New file.
	* src/tgbatest/Makefile.am (noinst_PROGRAMS, readsave_SOURCES): Add it.
	* src/tgbatest/readsave.test: Check a random graph.

336
337
338
	* misc/random.cc, misc/random.hh: New files.
	* src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.

339
340
2004-11-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>

341
342
343
	* src/evtgbaparse/public.hh (evtgba_parse): Fix doxygen comments.
	* src/tgbaalgos/projrun.hh (project_tgba_run): Likewise.

344
345
	* src/tgbaalgos/emptiness.hh (print_tgba_run): Document it.

346
347
348
349
350
351
352
	* src/tgbaalgos/replayrun.hh,
	src/tgbaalgos/replayrun.cc (replay_tgba_run): Take a `debug'
	option to decide whether the output should look like that of
	print_tgba_run() or a complete debug trace.
	* src/tgbatest/ltl2tgba.cc (main): Call replay_tgba_run() with
	debug=true.

353
354
355
356
357
	* iface/gspn/ltlgspn.cc (main): Adjust to recent changes to
	src/tgbaalgos/magic.cc, call explicit_magic_search() instead of
	building a spot::magic_search.
	* iface/gspn/udcseltl.test: Adjust to new output of print_tgba_run().

358
359
2004-11-09  Alexandre Duret-Lutz  <adl@src.lip6.fr>

360
361
362
	* src/tgbatest/Makefile.am (TESTS): Remove non-existing magic.test
	and se05.test.

363
364
365
	* src/tgbatest/ltl2tgba.cc (syntax): Fix old typos and reword
	some help strings.

366
2004-11-09  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
367
368
369
370
371
372
373
374
375
376
377
378

	* src/tgbaalgos/magic.cc: rewrite to externalize the heap and
	prepare it to a bit state hashing version.
	* src/tgbaalgos/magic.hh: adapt to the new interface of
	magic_search and se05_search.
	* src/tgbaalgos/se05.cc: new file.
	* src/tgbaalgos/Makefile.am: Add it.
	* src/tgbatest/ltl2tgba.cc: Add new emptiness check.
	* src/tgbatest/emptchk.test: more tests.
	* src/tgbatest/dfs.test: new file.
	* src/tgbatest/Makefile.am: Add it.

379
380
381
382
383
2004-11-09  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/emptiness.cc (print_tgba_run): Output the
	labels as formulae rather than bdd sets.

384
385
2004-11-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>

386
387
388
389
390
391
392
	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_path):
	Rewrite as ...
	(couvreur99_check_result::accepting_cycle): ... this less complex
	implementation.
	(couvreur99_check_result::complete_cycle): Delete.
	* src/tgbatest/emptchke.test: More explicit examples.

393
394
395
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Do not leak
	the initial state when no valid outgoing transition is found.

396
397
398
399
400
	* src/tgbaparse/tgbaparse.yy: Add `%destructor's so the parser
	does not leak on errors.
	* src/tgbatest/ltl2tgba.cc: Free the automata if it could not be
	fully parsed.

401
402
403
	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run):
	Remove spurious FIXME.

404
405
2004-11-05  Alexandre Duret-Lutz  <adl@src.lip6.fr>

406
407
408
409
	* src/evtgbaalgos/save.cc (save_bfs::output_acc_set): Sort
	acceptance conditions in the output.
	* src/evtgbatest/readsave.test, src/evtgbatest/product.test: Adjust.

410
411
412
	* src/tgbaalgos/rundotdec.cc (tgba_run_dotty_decorator::link_decl):
	Typo.

413
414
2004-11-04  Alexandre Duret-Lutz  <adl@src.lip6.fr>

415
416
417
	* src/tgbaalgos/neverclaim.cc (never_claim_bfs::process_link):
	Adjust prototype.

418
419
420
421
	* src/tgba/tgba.hh, src/tgba/tgba.cc
	(tgba::number_of_acceptance_conditions): New method.
	* src/tgbaalgos/lbtt.cc (lbtt_bfs::lbtt_bfs): Use it.

422
423
424
425
	* wrap/python/spot.i: Generate bindings for tgbaalgos/dottydec.hh,
	tgbaalgos/emptiness.hh, tgbaalgos/gtec/gtec.hh, and
	tgbaalgos/rundotdec.hh.

426
427
	* src/tgbaalgos/lbtt.cc (lbtt_bfs::process_link): Adjust prototype.

428
429
2004-11-03  Alexandre Duret-Lutz  <adl@src.lip6.fr>

430
431
432
433
434
435
436
437
438
439
	* src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh,
	src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: New files.
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
	libtgbaalgos_la_SOURCES): Add them.
	* src/tgbaalgos/dotty.hh (dotty_reachable): Take a dotty_decorator
	as third parameter.
	* src/tgbaalgos/dotty.cc (dotty_bfs::process_state,
	dotty_bfs::process_link): Use the decorator.
	* src/tgbatest/ltl2tgba.cc: Graph the accepting run if the -g option
	is given.
440
	* src/tgbatest/emptchk.test: Exercise -g.
441

442
443
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Add missing std::endl.

444
445
446
447
448
449
450
451
452
453
454
455
456
457
	* tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc
	(tgba_reachable_iterator::process_link): Take the state* as arguments
	in addition to the state numbers.
	* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
	(tgba_explicit::copy_acceptance_conditions_of): New method.
	* tgbaalgos/dupexp.cc (dupexp_iter::dupexp_iter): Call
	copy_acceptance_conditions_of.
	(dupexp_iter::process_state, duplex_iter::declare_state,
	dupexp_iter::name_): Remove.
	(dupexp_iter::process_link): Adjust prototype, and format
	the state here rather than in process_state.
	* tgbaalgos/stats.cc, tgbaalgos/dotty.cc: Adjust prototype
	of process_link.

458
459
2004-11-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>

460
461
	* src/ltlvisit/reduce.hh (is_eventual, is_universal): More doc.

462
463
464
465
466
	* src/tgbaalgos/projrun.hh, src/tgbaalgos/projrun.cc: New files.
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
	libtgbaalgos_la_SOURCES): Add them.
	* iface/gspn/ltlgspn.cc (main): Call project_tgba_run if -P.

467
468
469
470
471
472
473
	* src/tgbaalgos/emptiness.cc,
	src/tgbaalgos/emptiness.hh (print_tgba_run): Take the tgba*
	argument before the tgba_run* argument (for consistency with
	replay_tgba_run).
	* src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust
	calls to print_tgba_run().

474
475
	* src/ltlast/formula.hh (ltl::formula::~formula): Make it protected.

476
477
2004-10-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>

478
479
480
481
482
483
484
485
486
487
488
489
	A tgba can now annotate a transition (i.e., the position of a
	tgba_succ_iterator) with some string.  This comes handy to
	associate that transition to its high-level name.
	* src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::transition_annotation):
	New method.
	* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
	(tgba_product::transition_annotation): Implement it.
	* src/tgba/tgbatba.hh, src/tgba/tgbatba.cc
	(tgba_tba_proxy::transition_annotation): Likewise.
	* src/tgbaalgos/replayrun.cc (print_annotation): New function.
	(replay_tgba_run): Use it.

490
491
492
493
	* src/tgbaalgos/gtec/gtec.cc,
	src/tgbaalgos/gtec/gtec.hh (couvreur99_check::print_stats): New.
	* src/tgbatest/ltl2tgba.cc: Print emptiness-check statistics.

494
495
496
497
498
499
	* src/sanity/style.test: Diagnose superfluous constructs such
	as `if (x) delete x;'.
	* iface/gspn/gspn.cc, iface/gspn/ssp.cc, src/ltlvisit/basicreduce.cc,
	src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgbaalgos/magic.cc,
	src/tgbatest/ltl2tgba.cc: Remove such constructs.

500
501
502
503
	* src/tgbatest/ltl2tgba.cc: Replace -e, -E, -m, -M, and -n by
	-eALGO and -EALGO to ease the addition of new algorithms.
	* src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust.

504
505
506
	* src/misc/version.cc: Fix trailing whitespace.
	* src/sanity/style.test: Diagnose trailing whitespace.

507
508
509
510
	* src/tgbatest/ltl2tgba.cc: Fix lines longer than 80 chars.
	* src/sanity/80columns.test: Use expand to untabify, the previous
	recipe was incomplete.

511
512
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Note duplicate states.

513
514
515
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Verify the run is
	accepting.

516
517
518
	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_path):
	Initialize best_end to remove a spurious warning.

519
520
521
522
523
524
525
526
527
528
	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run,
	couvreur99_check_result::complete_cycle,
	couvreur99_check_result::accepting_path): Record conditions and
	acceptance conditions in the accepting run.  Simplify the
	todo BFS stack for accepting_run and complete_cycle.
	* src/tgbatest/ltl2tgba.cc (main): Do use replay_tgba_run
	now everything works.
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Be more verbose
	when an outgoing transition is not found.

529
530
2004-10-28  Alexandre Duret-Lutz  <adl@src.lip6.fr>

531
532
533
534
	* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc (magic_search):
	Record the acceptance conditions in the accepting run.
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix logic.

535
536
537
538
539
540
541
542
543
	* src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh: New files.
	Cannot test them because the run returned by the emptiness checks
	are currently incomplete (they lack the acceptance conditions, and
	sometimes even the labels in the prefix).
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
	libtgbaalgos_la_SOURCES): Add them.
	* src/tgbatest/ltl2tgba.cc (main): Prepare to use replay_tgba_run
	when the emptiness checks are fixed.

544
545
2004-10-27  Alexandre Duret-Lutz  <adl@src.lip6.fr>

546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
	Introduce an emptiness-check interface, and modify the existing
	algorithms to conform to it, uniformly.  This will unfortunately
	break third-party code that were using these algorithms.
	* src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: New files.
	* src/tgbaalgos/Makefile.am: New files.
	* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh: Adjust to
	conform to the new emptiness-check interface.
	* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
	src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
	src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh:
	Likewise.  The classes have been renamed are as following
	  emptiness_check -> couvreur99_check
	  emptiness_check_shy -> couvreur99_check_shy
          emptiness_check_status -> couvreur99_check_status
	  counter_example -> couvreur99_check_result
	* src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh,
	iface/gspn/ssp.cc: Adjust to renaming and new interface.

564
565
566
567
568
569
570
571
572
	* src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh:
	New files.
	* src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS,
	libevtgbaalgos_la_SOURCES): Add them.
	* src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/ltl2evtgba.test:
	New files.
	* src/evtgbatest/Makefile.am (check_PROGRAMS, TESTS): Add them.
	(ltl2evtgba_SOURCES): New variable.

573
574
575
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Do not assert
	that the true state has only one link when unobs is used.

576
577
578
579
2004-10-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/evtgbatest/Makefile.am (CLEANFILES): New variable.

580
581
2004-10-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
	Preliminary support for Event-based GBA.
	* src/evtgba/Makefile.am, src/evtgba/evtgba.cc,
	src/evtgba/evtgba.hh, src/evtgba/evtgbaiter.hh,
	src/evtgba/explicit.cc, src/evtgba/explicit.hh,
	src/evtgba/product.cc, src/evtgba/product.hh,
	src/evtgba/symbol.cc, src/evtgba/symbol.hh,
	src/evtgbaalgos/Makefile.am, src/evtgbaalgos/dotty.cc,
	src/evtgbaalgos/dotty.hh, src/evtgbaalgos/reachiter.cc,
	src/evtgbaalgos/reachiter.hh, src/evtgbaalgos/save.cc,
	src/evtgbaalgos/save.hh, src/evtgbaparse/Makefile.am,
	src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll,
	src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh,
	src/evtgbaparse/public.hh, src/evtgbatest/Makefile.am,
	src/evtgbatest/defs.in, src/evtgbatest/explicit.cc,
	src/evtgbatest/explicit.test, src/evtgbatest/product.cc,
	src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
	src/evtgbatest/readsave.test: New files.
	* configure.ac: Create the Makefiles in these new subdirectories.
	* src/Makefile.am: Recurse them.

602
603
604
	* src/misc/bareword.hh, src/misc/bareword.cc (quote_unless_bare_word):
	New function.

605
606
607
	* src/ltlvisit/tostring.cc (to_spin_string_visitor): Move to
	anonymous namespace.

608
609
610
611
2004-10-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* wrap/python/Makefile.am (_spot_la_SOURCES): Add spot_wrap.h.

612
613
2004-10-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>

614
615
616
	* src/misc/modgray.hh (loopless_modular_mixed_radix_gray_code::done,
	loopless_modular_mixed_radix_gray_code::last): Declare as const.

617
618
619
	* src/misc/bareword.hh, src/misc/bareword.cc: New files.
	* src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them.

620
621
622
623
624
625
	* src/misc/modgray.hh, src/misc/modgray.cc: New files.
	* src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them.
	* wrap/python/spot.i: Activate directors, and interface modgray.hh.
	* wrap/python/tests/modgray.py: New file.
	* wrap/python/tests/Makefile.am (TESTS): Add it.

626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
2004-10-18  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* iface/gspn/gspn.cc, src/ltlvisit/basicreduce.cc,
	src/ltlvisit/destroy.cc, src/ltlvisit/dotty.cc,
	src/ltlvisit/dump.cc, src/ltlvisit/length.cc,
	src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
	src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
	src/tgba/formula2bdd.cc, src/tgba/tgbabddconcreteproduct.cc,
	src/tgba/tgbatba.cc, src/tgbaalgos/dotty.cc,
	src/tgbaalgos/dupexp.cc, src/tgbaalgos/lbtt.cc,
	src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc,
	src/tgbaalgos/save.cc, src/tgbaalgos/stats.cc,
	src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh:
	Declare private classes and helper function in anonymous namespaces.
	* HACKING, src/sanity/style.test: Document and check this.
	Also check for trailing { after namespace or class.
	* src/ltlast/predecl.hh, src/ltlast/visitor.hh,
	src/tgba/tgbareduc.hh: Fix trailing {.

645
646
2004-10-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>

647
648
	* src/tgbaalgos/gtec/ce.cc: Reinstall change from 2004-09-21.

649
650
651
652
653
654
655
656
657
658
659
660
661
662
	Back out all Thomas's changes on emptiness checks since
	2004-08-23.  Some of these will need to be reintegrated more
	slowly and cleanly.

	* src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/ce.cc,
	src/tgbaalgos/gtec/ce.hh, src/tgbatest/Makefile.am,
	src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc: Revert.
	* src/tgbaalgos/colordfs.cc, src/tgbaalgos/colordfs.hh,
	src/tgbaalgos/minimalce.cc, src/tgbaalgos/minimalce.hh,
	src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/nesteddfs.hh,
	src/tgbaalgos/nesteddfsgen.cc, src/tgbaalgos/nesteddfsgen.hh,
	src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh:
	Delete.

663
664
2004-10-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

665
666
667
	* src/ltltest/reduc.test: Do source ./defs.  Revert mistaken
	change from 2004-09-13.

668
669
	* src/tgbatest/explicit.test: Typo.

670
671
2004-10-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

672
673
674
675
676
677
678
679
680
681
682
	The computation of the counter example fails the valgrind tests
	and is wrong into two ways: the search stack is generally not a
	path, and does not run until the end of the STL container.
	Remove it.
	* src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh
	(tarjan_on_fly): Do not inherit from the emptiness_search class,
	because the check method will no longer return a counter example.
	(tarjan_on_fly::check): Return only a boolean.
	(tarjan_on_fly::build_counter): Delete.
	* src/tgbatest/ltl2tgba.cc: Adjust.

683
684
685
686
687
	* src/tgba/tgbaexplicit.cc (tgba_explicit_succ_iterator::current_state,
	tgba_explicit_succ_iterator::current_condition,
	tgba_explicit_succ_iterator::current_accepting_conditions): Assert
	the iteration is not finished.

688
689
690
691
2004-10-12  Alexandre Duret-Lutz  <adl@gnu.org>

	* wrap/python/tests/run.in: Typo.  From Akim Demaille.

692
693
694
695
696
2004-10-11  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* configure.ac: Empty CFLAGS and CXXFLAGS.
	* m4/debug.m4: Update CXXFLAGS too.

697
698
699
700
2004-10-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* doc/Doxyfile.in: Upgrade to Doxygen 1.3.9.

701
702
703
704
705
2004-09-27  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/sanity/style.test: Suggest using "x->y", not "(*x).y".
	* src/tgbaalgos/tarjan_on_fly.cc: Fix.

706
707
2004-09-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

708
709
710
711
712
713
	* src/sanity/style.test: Suggest ++i over i++ when it does not
	matter, for consistency.
	* src/tgbaalgos/tarjan_on_fly.cc, iface/gspn/ssp.cc,
	src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc,
	src/tgbaalgos/minimalce.cc, src/tgba/tgbareduc.cc: Adjust.

714
715
716
717
	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): New unobs argument.
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Handle unobs.
	* src/tgbatest/ltl2tgba.cc (syntax, main): New -U option.

718
719
2004-09-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

720
721
722
723
724
	* src/tgbaalgos/colordfs.hh, src/tgbaalgos/minimalce.cc,
	src/tgbaalgos/minimalce.hh, src/tgbaalgos/nesteddfs.hh,
	src/tgbaalgos/tarjan_on_fly.hh, src/tgbatest/ltl2tgba.cc: Rename
	emptyness_search to emptiness_search.

725
726
727
728
729
730
731
732
733
734
	* src/sanity/style.test: Warn about places where size() is used
	instead of empty().
	* src/misc/bddalloc.cc (bdd_allocator::extend): Use empty() rather
	than size() when checking emptiness of lists.
	* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/minimalce.cc,
	src/ltlvisit/basicreduce.cc, src/ltlvisit/reduce.cc,
	src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/ltl2tgba_fm.cc,
	src/misc/minato.cc: Likewise.
	* src/ltlast/multop.cc (multop::instance): Call ->size() only once.

735
736
2004-09-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
737
738
739
740
741
742
	Update to SWIG 1.3.22.
	* wrap/python/libpy.c: Delete.
	* wrap/python/swigpy.i: New file.
	* wrap/python/Makefile.am (swigpy_wrap.c): Build this from swigpy.i
	and use it instead of libpy.c.

743
744
	* INSTALL, lbtt/INSTALL: New upstream version.

745
746
2004-09-14  Thomas Martinez  <martinez@src.lip6.fr>

martinez's avatar
martinez committed
747
748
749
750
751
752
753
754
	* src/tgbatest/emptchk.test
	src/tgbaalgos/tarjan_on_fly.hh,
	src/tgbaalgos/tarjan_on_fly.cc,
	src/tgbaalgos/nesteddfs.hh,
	src/tgbaalgos/nesteddfs.cc,
	src/tgbaalgos/minimalce.hh,
	src/tgbaalgos/minimalce.cc: To correct a bug.

755
756
	* src/ltltest/reduc.test (FICH): bad file name.

martinez's avatar
martinez committed
757
758
2004-09-13  Thomas Martinez  <martinez@src.lip6.fr>

759
760
761
	* src/tgbaalgos/nesteddfsgen.hh src/tgbaalgos/nesteddfsgen.cc:
	New algorithm for emptiness check.

martinez's avatar
martinez committed
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
	* src/tgbatest/spotlbtt.test,
	src/tgbatest/reductgba.cc,
	src/tgbatest/ltl2tgba.cc:
	Add option for reduction of TGBA.

	* src/tgbatest/emptchk.test, src/tgbaalgos/Makefile.am,
	src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc,
	src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc,
	src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc,
	src/tgbaalgos/colordfs.hh, src/tgbaalgos/colordfs.cc:
	Remove some bugs.

	src/tgbaalgos/gtec/ce.cc:
	Modification of construction of counter example.

	* src/tgbaalgos/reductgba_sim.hh src/tgbaalgos/reductgba_sim.cc,
	src/tgbaalgos/reductgba_sim_del.cc,
	src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc:
	Modification for delayed simulation.


martinez's avatar
martinez committed
783
784
785
786
787
788
789
790
791
2004-08-23  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbaalgos/tarjan_on_fly.hh,
	src/tgbaalgos/tarjan_on_fly.cc,
	src/tgbaalgos/nesteddfs.hh,
	src/tgbaalgos/nesteddfs.cc,
	src/tgbaalgos/minimalce.hh,
	src/tgbaalgos/minimalce.cc,
	src/tgbaalgos/colordfs.hh,
792
	src/tgbaalgos/colordfs.cc: four new algorithms for emptiness check.
martinez's avatar
martinez committed
793

martinez's avatar
martinez committed
794
	* src/tgbaalgos/gtec/ce.hh,
martinez's avatar
martinez committed
795
796
797
	src/tgbaalgos/gtec/ce.cc: Adapt the counter exemple for the ce
	object in minimalce.hh.

martinez's avatar
martinez committed
798
	* src/tgbatest/ltl2tgba.cc,
martinez's avatar
martinez committed
799
	src/tgbatest/emptchk.test,
800
	src/tgbaalgos/Makefile.am: Add files for emptiness-check.
martinez's avatar
martinez committed
801
802
803
804
805
806
807

2004-08-23  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbaalgos/reductgba_sim_del.cc: Restrict to degeneralize automata.
	* src/tgba/tgbareduc.hh: src/tgba/tgbareduc.cc: Merge transition
	for scc reduce.

808
809
2004-08-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

810
811
	* configure.ac, NEWS: Bump version to 0.0y.

812
813
	* configure.ac, NEWS: Bump version to 0.0x.

814
815
2004-08-12  Alexandre Duret-Lutz  <adl@src.lip6.fr>

816
817
818
	* doc/Doxyfile.in (GENERATE_TAGFILE): Build spot.tag.
	* doc/Makefile.am (dist_pkgdata_DATA): Add spot.tag.

819
820
	* src/tgbatest/ltl2tgba.cc (syntax): Typo.

821
822
823
	* doc/Doxyfile.in (STRIP_FROM_PATH): Strip @srcdir@ so its
	does not appear when listing mainpage.dox.

824
825
826
827
828
2004-08-11  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh:
	Typos in Doxygen comments.

829
830
2004-08-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>

831
832
833
834
	* src/ltlvisit/apcollect.hh: Fix include guard.  Report from Denis.
	* src/sanity/includes.test: Include files twice to check include
	guards.

835
836
837
	* src/tgbatest/ltl2tgba.cc (main): Fix another gcc warning in case
	assert() is disabled.

838
839
840
	* src/Makefile.am (nodist_EXTRA_libspot_la_SOURCES): New variable,
	to force C++ linking.

841
842
843
	* iface/gspn/ltlgspn.cc: Fix a gcc warning in case assert() is
	disabled.

844
845
2004-08-09  Alexandre Duret-Lutz  <adl@src.lip6.fr>

846
847
848
849
850
	* src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh: New files,
	based on code from <Denis.Poitrenaud@lip6.fr>.
	* src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES, ltlvisit_HEADERS):
	Add them.

851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
	* iface/gspn/common.cc, iface/gspn/common.hh,
	src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
	src/ltlparse/fmterror.cc, src/ltlparse/public.hh,
	src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
	src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
	src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
	src/misc/escape.cc, src/misc/escape.hh, src/tgba/bdddict.cc,
	src/tgba/bdddict.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh,
	src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh,
	src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
	src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
	src/tgbaalgos/save.cc, src/tgbaalgos/save.hh,
	src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh,
	src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh: Include <iosfwd>
	in headers, and prefer <ostream> in the body whenever possible.
	* src/sanity/style.test, HACKING: Check and document this.

868
869
870
871
872
873
874
	* src/ltlast/allnodes.hh, src/ltlast/atomic_prop.hh,
	src/ltlast/binop.hh, src/ltlast/constant.hh,
	src/ltlast/formula.hh, src/ltlast/multop.hh,
	src/ltlast/predecl.hh, src/ltlast/refformula.hh,
	src/ltlast/unop.hh, src/ltlast/visitor.hh: Use \file to introduce
	each file.

875
876
877
	* doc/Doxyfile.in (STRIP_FROM_INC_PATH): Define, so that the
	`#include' references are correct.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
878
879
	* README: Update.

880
881
	* m4/gccoptim.m4: Compute optimization flags for CXX too.

882
883
	* m4/ndebug.m4: Update CPPFLAGS, not CFLAGS.

884
885
886
887
	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Document all
	parameters.
	* src/tgbaalgos/ltl2tgba_lacim.hh (ltl_to_tgba_lacim): Likewise.

888
889
890
891
892
893
2004-08-07  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* configure.ac: Call AC_PROG_CC and AM_PROG_CC_C_O.
	* wrap/python/Makefile.am (_buddy_la_LDFLAGS): Move libspotswigpy.la ...
	(_buddy_la_LIBADD): ... here.

894
895
896
897
2004-08-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* lbtt/: Merge lbtt 1.1.2.

898
899
900
901
2004-07-30  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* lbtt/: Merge lbtt 1.1.1.

902
903
904
905
2004-07-26  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* doc/Doxyfile.in: Update for Doxygen 1.3.8.

906
907
908
909
910
2004-07-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* configure.ac: Call AC_LIBTOOL_WIN32_DLL
	* src/Makefile.am (libspot_la_LDFLAGS): Add -no-undefined.

911
912
2004-07-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

913
914
915
	* src/tgbatest/explicit.test: Do not use `-i', it's not needed
	and it is wrong to put it after `-e'.  Caught by Denis too.

916
917
918
	* src/ltltest/reduc.test: Use `test a = b' not `test a == b'.
	Reported by <Denis.Poitrenaud@lip6.fr> (failure on Cygwin).

919
920
921
922
923
924
2004-07-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbatest/defs.in (VALGRIND): Specify --tool=memcheck for
	compatibility with valgrind 2.1.x.
	* src/ltltest/defs.in (VALGRIND): Likewise.

925
926
2004-07-16  Alexandre Duret-Lutz  <adl@src.lip6.fr>

927
928
929
	* m4/gccwarn.m4: Do not check nor use -Wstrict-prototypes.
	g++-3.4 complains it makes no sense in C++.

930
931
	* iface/gspn/ssp.cc: Typos.

932
933
934
935
	* iface/gspn/gspn.cc (tgba_succ_iterator_gspn::tgba_succ_iterator_gspn):
	Set size_ to 1 when stuttering is needed, so that done() does not
	return true immediately.

936
937
938
939
2004-07-12  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/gtec/gtec.hh: Typos in comments.

940
941
2004-07-09  Alexandre Duret-Lutz  <adl@src.lip6.fr>

942
943
944
	* src/tgba/state.hh (state_ptr_equal, state_ptr_hash): Fix Doxygen
	example.

945
946
947
948
	* src/tgbaalgos/reductgba_sim.hh (parity_game_graph_delayed,
	reduc_tgba_sim): Fix warnings about Doxygen comment.
	* src/ltlvisit/reduce.hh (reduce): Likewise.

949
950
951
952
	* doc/footer.html: New file, link to RefDocComments on the wiki.
	* doc/Doxyfile.in (HTML_FOOTER): Use footer.html.
	* doc/Makefile.am (EXTRA_DIST): Add footer.html.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
953
954
	* THANKS: Fill in.

955
956
	* src/tgbatest/ltl2baw.pl: Do not use -T anymore.  Fix comments.

957
958
2004-07-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>

959
960
961
962
963
964
965
966
967
968
969
970
	lbtt 1.1.0 supports TGBAs, use that and remove old workarounds.
	* src/tgbaalgos/lbtt.cc (state_acc_pair, state_acc_pair_equal,
	state_acc_pair_hash, acp_seen_map, todo_set, seen_map, fill_todo
	lbtt_reachable): Remove.
	(nonacceptant_lbtt_bfs): Rename as ...
	(lbtt_bfs): ... this, and adjust to output acceptance conditions
	on transitions.
	(nonacceptant_lbtt_reachable): Rename as ...
	(lbtt_reachable): ... this.
	* src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): Delete.
	* src/tgbatest/ltl2tgba.cc: Suppress option "-T".

971
972
973
974
975
	Patch from Heikki Tauriainen <heikki.tauriainen@hut.fi>.
	* src/tgbaalgos/gtec/ce.cc (counter_example::counter_example): Do
	not parenthesize the type after the new operator (g++ 3.4 complains).
	* src/tgbaalgos/dupexp.cc (dupexp_iter::process_state,
	dupexp_iter::declare_state): Use this->automata_instead of
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
976
977
	automata_.  Local protected member automata_ inherited from
	template base class must be prefixed or g++ 3.4 will not look it
978
979
	up (conforming to 14.6.2.3).

980
981
2004-07-07  Alexandre Duret-Lutz  <adl@src.lip6.fr>

982
983
984
985
	* lbtt/: Merge lbtt 1.1.0.
	* src/tgbatest/spotlbtt.test: Adjust config file syntax to
	please lbtt 1.1.0.

986
987
988
989
990
	* src/tgbaalgos/gtec/gtec.hh (emptiness_check_shy::find_state): Add
	comments.
	* iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Likewise.
	Soheib and I had a hard time figuring why we did this...

991
992
993
994
995
996
997
998
999
2004-07-02  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
	src/tgbaalgos/reductgba_sim.cc,	src/tgbaalgos/reductgba_sim.hh,
	src/tgbaalgos/reductgba_sim_del.cc: Remove some comments.

	* src/tgbatest/ltl2tgba.cc, src/tgbatest/reductgba.cc: Adjust ...
	* src/tgbatest/spotlbtt.test: More test (delayed simulation)

1000
1001
2004-06-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1002
1003
	* configure.ac, NEWS: Bump version to 0.0w.

1004
1005
	* configure.ac, NEWS: Bump version to 0.0v.

martinez's avatar
martinez committed
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
2004-06-28  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/reduccmp.test: Bug.

	* src/tgbatest/reductgba.test: More Test.

	* src/tgbatest/ltl2tgba.cc: Adjust ...
	* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.hh,
	src/tgbaalgos/reductgba_sim.cc: try to optimize.

	* src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc: Scc reduction
	and we remove some acceptance condition in scc which are not accepting.
	* src/ltlvisit/syntimpl.cc : Some case wasn't detect.
	* src/ltlvisit/basicreduce.cc: Case FGa || FGb = F(Ga | Gb) added.
	* src/ltltest/syntimpl.test: More Test.
	* src/ltltest/syntimpl.cc: Put the formula in negative normal form.

1023
1024
1025
1026
2004-06-28  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* buddy/: Merge buddy-2-3.

1027
1028
1029
1030
1031
2004-06-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbatest/ltl2tgba.cc (main): Degeneralize before
	the simulations.

1032
1033
1034
1035
1036
1037
1038
1039
2004-06-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/ltlvisit/tostring.cc (is_bare_word): New function.
	(to_string_visitor::visitor(const atomic_prop*)): Use is_bare_word
	to better check which atomic proposition need to be quoted.
	* src/ltlparse/ltlscan.ll: Do not allow identifiers starting with F_
	or G_.
	* src/ltltest/equals.test, src/ltltest/tostring.test: More tests.
1040

1041
1042
1043
1044
	* src/tgba/tgbatba.cc (tgba_tba_proxy::format_state): Use
	bdd_format_accset to print the acceptance condition part of the state.
	That produces more readable output.

1045
	* wrap/python/cgi/ltl2tgba.in: Add "Formula Simplications" options.
1046
	* wrap/python/spot.i: Wrap src/ltlvisit/reduce.hh.
1047

1048
1049
1050
1051
1052
1053
1054
1055
1056
	* src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh: New files,
	extracted from ...
	* src/ltlvisit/lunabbrev.cc: ... this one, which now work as documented
	again.
	* src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc: Adjust to call
	simplify_f_g() in addition to unabbreviate_logic().
	* src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES):
	Add simpfg.cc and simpfg.hh.

1057
1058
1059
1060
1061
1062
	* src/ltlvisit/reducform.hh, src/ltlvisit/reducform.cc: Rename to ...
	* src/ltlvisit/reduce.hh, src/ltlvisit/reduce.cc: ... this, to match
	the function name.
	* ltltest/equals.cc, ltltest/reduc.cc, ltlvisit/Makefile.am,
	tgbatest/ltl2tgba.cc, tgbatest/reductgba.cc: Adjust filenames.

1063
1064
1065
	* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit(binop*)):
	Factorize.

1066
1067
1068
1069
1070
1071
1072
1073
	* src/ltlvisit/basicreduce.hh: New file, extracted from ...
	* src/ltlvisit/reducform.hh: ... here.
	* src/ltlvisit/basereduc.cc: Rename as ...
	* src/ltlvisit/basicreduce.cc: ... this, to match the function name.
	* src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES):
	Adjust filenames.
	* src/ltlvisit/reducform.cc: Adjust includes.

1074
1075
1076
	* src/ltlvisit/lunabbrev.hh: Revert superfluous change from
	2004-05-10.

1077
1078
1079
1080
1081
1082
1083
2004-06-22  Thomas Martinez  <martinez@src.lip6.fr>

	* src/ltlvisit/reducform.cc, src/tgba/tgbareduc.cc,
	src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh
	src/tgbaalgos/reductgba_sim_del.cc, src/tgbatest/reduccmp.test,
	src/tgbatest/reductgba.cc: 80 columns and style.

1084
1085
1086
1087
2004-06-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/sanity/style.test: Typo.

1088
1089
1090
1091
1092
1093
1094
1095
1096
2004-06-22  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/ltl2tgba.cc, src/tgbaalgos/reductgba_sim_del.cc,
	src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
	bug in delayed simulation.

	* src/tgbatest/reduccmp.test, src/tgbatest/reductgba.test,
	src/tgba/tgbareduc.cc: bug in scc reduction.

1097
1098
1099
1100
1101
1102
2004-06-21  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/reductgba.test, src/tgba/tgbareduc.cc:
	There is bug in reduction with scc.
	* src/tgbatest/reduccmp.test: More test.

1103
1104
2004-06-17  Thomas Martinez  <martinez@src.lip6.fr>

1105
	* src/tgbatest/reductgba.test: Wrong test are removed.
1106

1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
2004-06-17  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/spotlbtt.test: We don't check the post-reduction
	with scc and delayed simulation.

	* src/tgbatest/ltl2tgba.cc: Adjust parameters.
	* src/tgbatest/reductgba.cc, src/tgbatest/Makefile.am: More Test.
	* src/tgbaalgos/reductgba_sim_del.cc: Not finish, lot of bugs.
	* src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
	Remove some useless comments.
	* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: Bug in SCC.

	* src/ltlvisit/reducform.cc: Correct some bug for multop.
	* src/ltltest/reduc.cc: Thinko
	* src/ltltest/equals.cc: Reduction compare

1123
1124
1125
1126
1127
2004-06-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Free s.
	This fixes a memory leak observed by Soheib Baarir.

1128
1129
1130
1131
1132
2004-06-16  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/reductgba.cc, src/tgbatest/reductgba.test: Test for
	reduction of tgba.

1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
2004-06-15  Thomas Martinez  <martinez@src.lip6.fr>

	* src/tgbatest/ltl2tgba.cc: Add some option for the reduction of
	automata.
	* src/tgbatest/spotlbtt.test, src/tgbatest/Makefile.am: Add some
	test for reduction of automata.
	* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc,
	src/tgbaalgos/reductgba_sim.hh: Compute some simulation relation
	to reduce a tgba.
	* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: A implementation
	of tgba for the reduction.
	* src/tgbaalgos/Makefile.am, src/tgba/Makefile.am:
	Add the reduction of automata.
	* src/ltlvisit/syntimpl.cc, src/ltlvisit/basereduc.cc:
	Lot of mistake are corrected.
	* src/ltlvisit/syntimpl.hh, src/ltlvisit/reducform.cc,
	src/ltlvisit/reducform.hh, src/ltltest/reduc.cc: Adjust.
	* src/ltltest/equals.cc, src/ltltest/reduccmp.test,
	src/ltltest/Makefile.am: Add a test for reduction.

1153
1154
2004-06-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
	* iface/gspn/common.cc, iface/gspn/common.hh: Remove the
	class gspn_environment, and move it to ...
	* src/ltlenv/declenv.cc, src/ltlenv/declenv.hh: .. this new file
	as class declarative_environment.
	* src/ltlenv/Makefile.am (ltlenv_HEADERS): Add declenv.hh.
	(libltlenv_la_SOURCES): Add declenv.cc.
	* iface/gspn/dottygspn.cc, iface/gspn/dottyssp.cc,
	iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc,
	iface/gspn/ssp.cc, iface/gspn/ssp.hh: Adjust references
	to declarative_environment.

1166
1167
1168
1169
1170
1171
	* HACKING, src/sanity/style.test: NULL is not portable, prohibit it.
	* iface/gspn/ssp.cc, src/ltltest/reduc.cc, src/ltltest/syntimpl.cc,
	src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc,
	src/ltlvisit/syntimpl.cc: Use 0 instead of NULL.

2004-06-01  Alexandre Duret-Lutz  <adl@src.lip6.fr>
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183

	* src/ltltest/inf.cc, src/ltltest/inf.test: Rename as ...
	* src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test: ... these.
	* src/ltltest/Makefile.am: Adjust.
	* src/ltlvisit/forminf.cc: Rename as...
	* src/ltlvisit/syntimpl.cc: ... this.
	* src/ltlvisit/syntimpl.hh: New file with definitions extracted
	from ...
	* src/ltlvisit/reducform.hh: ... this one.
	* src/ltlvisit/Makefile.am, src/ltlvisit/reducform.cc: Adjust.

2004-05-30  Alexandre Duret-Lutz  <adl@src.lip6.fr>
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199

	* src/ltlvisit/forminf.cc (form_eventual_universal_visitor,
	inf_form_right_recurse_visitor, inf_form_left_recurse_visitor): Rename
	as ...
	(eventual_universal_visitor, inf_right_recurse_visitor,
	inf_left_recurse_visitor): ... these.
	(is_GF, is_FG): Move ...
	* src/ltlvisit/basereduc.cc (is_GF, is_FG): ... here, since they
	are only used here.
	(basic_reduce_form, basic_reduce_form_visitor): Rename as ...
	(basic_reduce, basic_reduce_visitor): ... these.
	* src/ltlvisit/reducform.cc (reduce_form_visitor): Rename as ...
	(reduce_visitor): ... this.
	* src/ltltest/inf.cc: Adjust calls.
	* src/sanity/style.test: Improve missing-space after coma detection.

1200
1201
2004-05-26  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1202
1203
1204
	* src/ltlvisit/reducform.cc (reduce_form_visitor::visit(constant)):
	Simplify.

1205
1206
1207
1208
1209
1210
1211
	* src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc: Use
	dynamic_cast instead of node_type_form_visitor, this is usually
	smaller.
	* src/ltlvisit/reducform.hh,
	src/ltlvisit/forminf.cc (node_type_form_visitor): Delete.
	* src/sanity/style.test: Two more checks.

1212
1213
2004-05-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1214
1215
1216
1217
1218
1219
1220
1221
	* src/ltlvisit/formlength.cc: Rename as ...
	* src/ltlvisit/length.cc: ... this.
	* src/ltlvisit/length.hh: New file, extracted from ...
	* src/ltlvisit/reducform.hh: ... here.
	* src/ltlvisit/Makefile.am (ltlvisit_HEADERS): Add length.hh.
	(libltlvisit_la_SOURCES): Rename formlength.cc as length.cc.
	* src/ltltest/reduc.cc: Include length.hh.

1222
1223
1224
1225
1226
1227
1228
1229
	* src/ltlvisit/formlength.cc (length_form_vistor): Rename as ..
	(length_visitor): ... this.
	(form_length): Rename as ...
	(length): ... this.
	* src/ltlvisit/reducform.hh (form_length): Rename as ...
	(length): ... this.
	* src/ltltest/reduc.cc: Adjust.

1230
1231
1232
	* src/ltlvisit/basereduc.cc, src/ltlvisit/formlength.cc: Remove
	useless includes.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1233
1234
	* AUTHORS: Update.

1235
1236
1237
	* src/ltlvisit/reducform.hh: Update Doxygen comments for
	previous change.

1238
1239
1240
1241
1242
1243
1244
1245
	* src/ltlvisit/reducform.hh (option): Rename as ...
	(reduce_options): ... this, and use it as a bit field so
	option can be combined easily.
	(reduce): Adjust argument.
	(reduce_form): Remove, not needed anymore.
	* src/ltlvisit/reducform.cc, src/ltltest/reduc.cc,
	src/tgbatest/ltl2tgba.cc: Adjust.

1246
1247
1248
1249
	* src/sanity/style.test: Catch {.*{ and }.*}.
	* src/sanity/80columns.test: Untabify files.
	* iface/gspn/ltlgspn.cc, src/ltlvisit/basereduc.cc: Fix long lines.

1250
1251
1252
	* src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc,
	src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes.

1253
1254
	* wrap/python/cgi/ltl2tgba.in: Typos.

1255
1256
2004-05-24  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1257
1258
1259
	* src/sanity/style.test: Catch `;'-not-followed-by-space.
	* src/ltlvisit/reducform.cc, src/ltlvisit/forminf.cc: Fix style.

1260
1261
	* src/ltlvisit/reducform.hh: Fix some Doxygen comments.

1262
1263
	* src/tgbatest/ltl2tgba.cc (syntax): Keep options sorted.

1264
1265
1266
	* src/sanity/Makefile.am (EXTRA_DIST): Distribute 80columns.test
	and style.test.

1267
	* src/ltltest/Makefile.am (EXTRA_DIST): Distribute formulae.txt.
1268
	* src/ltltest/formulae.txt: New file (2200 LTL formulea generated
1269
1270
1271
1272
	by Wring).
	* src/ltltest/formules.ltl: Delete.
	* src/reduc.test: Read formulae.txt.

1273
1274
1275
1276
1277
1278
1279
1280
1281
2004-05-24  Soheib Baarir  <Souheib.Baarir@lip6.fr>

	* iface/gspn/ssp.hh (gspn_ssp_interface::gspn_ssp_interface): Add
	the `inclusion' flag.
	* iface/gspn/ssp.cc (gspn_ssp_interface::gspn_ssp_interface): Call
	inclusion_version when inclusion is set.
	* iface/gspn/ltlgspn.cc (main) [SSP]: Turn on inclusion for -e3,
	-e4, and -e5.

1282
1283
2004-05-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
	* iface/gspn/gspn.cc (tgba_gspn_private_): Define alive_prop,
	and dead_prop from the dead argument passed to the constructor.
	(tgba_succ_iterator_gspn): Stutter on dead transitions.
	(tgba_gspn::tgba_gspn): Hand dead to tgba_gspn_private_.
	(gspn_interface::gspn_interface): Hand dead to tgba_gspn.
	* iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take a
	dead argument.
	* iface/gspn/ltlgspn.cc [!SSP]: Add a option -d to specify the
	dead property.
	* iface/gspn/udcseltl.test: Try option -d.

1295
1296
1297
	* src/sanity/style.test: Check the iface/ tree too.
	* iface/gspn/gspn.cc, iface/gspn/ssp.cc: Fix style.

1298
1299
1300
1301
1302
1303
	* src/sanity/80columns.test: Check the iface/ tree too.
	* iface/gspn/dcswaveltl.test, iface/gspn/dcswavefm.test,
	iface/gspn/dcswaveeltl.test, iface/gspn/udcsltl.test,
	iface/gspn/udcseltl.test, iface/gspn/udcsfm.test,
	iface/gspn/udcsefm.test: Wrap to fit 80 columns.

1304
1305
1306
1307
1308
1309
2004-05-18  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* doc/Makefile.am (EXTRA_DIST, spot.html): Built the html
	documentation in $(srcdir) since it is distributed.
	* doc/Doxyfile.in (HTML_OUTPUT): Likewise.  Upgrade to Doxygen 1.3.7.

1310
1311
2004-05-17  Thomas Martinez  <martinez@src.lip6.fr>

1312
1313
	* src/ltlvisit/basereduc.cc, src/ltltest/inf.cc (main): Style.

1314
1315
1316
1317
1318
1319
	* src/ltlvisit/basereduc.cc (spot): 80 columns.
	* src/ltlvisit/reducform.cc (spot), src/ltltest/inf.cc,
	src/ltltest/reduc.cc (main), src/ltlvisit/reducform.hh,
	src/tgbatest/ltl2tgba.cc (main): More option.
	* src/ltltest/inf.test: More test.

1320
1321
2004-05-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1322
1323
1324
	* wrap/python/buddy.i: Define typemap for input_buf and use it
	for fdd_extdomain.  Define const_int_ptr and use it for fdd_vars.

1325
1326
1327
1328
1329
1330
1331
	* src/misc/bddalloc.cc (bdd_allocator::varnum): Suppress.
	(bdd_allocator::bdd_allocator): Adjust.
	(bdd_allocator::extvarnum): Always call bdd_varnum(), so that
	it doesn't matter if the number of variable has been augmented
	externally.
	* src/misc/bddalloc.hh (bdd_allocator::varnum): Suppress.

1332
1333
	* src/ltlvisit/formlength.cc: Fix style to please sanity checks.

1334
1335
	* src/ltlvisit/lunabbrev.cc: Fix style to please sanity checks.

1336
1337
1338
	* src/tgbaalgos/neverclaim.cc: Fix them.
	* sanity/style.test: Diagnose semicolons with leading spaces.

1339
1340
1341
	* src/ltlvisit/forminf.cc: Fix style to please sanity checks.
	Also avoid node_type_form_visitor where a dynamic_cast is done.

1342
1343
2004-05-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1344
1345
	* wrap/python/buddy.i: Preliminary bindings for FDD and BVEC.

1346
1347
1348
	* ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style.
	* sanity/style.test: More tests.

1349
1350
1351
	* src/tgbatest/ltl2tgba.cc (main): Fix style.
	* HACKING: Mention `else if'.

1352
1353
1354
1355
	* src/tgbaalgos/neverclaim.cc (never_claim_bfs): Do not output
	space before colon, and do not output the top-level formula using
	Spin's syntax.

1356
1357
2004-05-14  Thomas Martinez  <martinez@src.lip6.fr>

1358
1359
	* src/tgbatest/ltl2tgba.cc (main): Thinko.

1360
1361
1362
1363
1364
1365
	* src/ltlvisit/basereduc.cc (spot): Correct some mistakes.
	* src/ltlvisit/lunabbrev.cc (spot): Nothing change.
	* src/tgbatest/ltl2tgba.cc (main): More option to reduce
	formula.
	* src/tgbatest/spotlbtt.test: One more test.

1366
1367
2004-05-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1368
1369
1370
1371
1372
1373
1374
1375
1376
	* src/ltlvisit/tostring.cc (to_spin_string_visitor,
	to_string_visitor): Do not parenthesize the top-level formula.
	* tgbatest/explicit.test, tgbatest/explpro2.test,
	tgbatest/explpro3.test, tgbatest/explprod.test,
	tgbatest/readsave.test, tgbatest/tgbaread.test,
	tgbatest/tripprod.test: Adjust expected output.
	* sanity/style.test: Fix regexes to catch an error seen in
	tostring.cc.

1377
1378
1379
1380
	* src/tgbaalgos/gtec/gtec.cc (emptiness_check::remove_component):
	Do not try to erase state that are not found in H.
	Report from Soheib Baarir.

1381
1382
1383
	* src/ltltest/reduc.test: Use ./defs and clean result.data.
	* src/ltltest/Makefile.am (CLEANFILES): Clean result.data.

1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
2004-05-13  Thomas Martinez  <martinez@src.lip6.fr>

	* src/ltlvisit/Makefile.am: Copyright 2004.
	* src/ltltest/inf.test: More test.
	* src/ltlvisit/basereduc.cc, src/ltlvisit/forminf.cc (spot):
	Use dynamic_cast.
	* src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh,
	src/ltltest/reduc.test, src/ltltest/reduc.cc: Add an option
	to choose which rules applies to simplify the formula.

1394
1395
2004-05-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1396
1397
	* src/ltltest/reduc.test: Typo.

1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
	* src/ltlparse/ltlparse.yy (OP_POST_NEG, OP_POST_POS): New tokens.
	(subformula): Recognize `ATOMIC_PROP OP_POST_POS' and
	`ATOMIC_PROP OP_POST_NEG'.
	* src/ltlparse/ltlscan.ll: Introduce the not_prop start condition,
	to restrict the set of atomic propositions allowed in places
	where they are not expected.  Make `true' and `false' case insensitive.
	* src/ltltest/parse.test, src/ltltest/tostring.test: More cases.
	* src/ltlvisit/tostring.cc (to_string_visitor): Quote atomic
	propositions equal to "true" or "false".

1408
1409
2004-05-11  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1410
1411
	* src/ltltest/Makefile.am (TESTS): Run inf.test and reduc.test last.

1412
1413
	* src/ltltest/reduc.test: POSIXify.

1414
1415
2004-05-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
	* src/sanity/style.test: New file.
	* src/sanity/Makefile.am (check-local): Run it.
	* src/ltlvisit/nenoform.cc, src/ltlvisit/tostring.cc,
	src/tgba/bdddict.cc, src/tgba/bddprint.cc, src/tgba/tgba.cc,
	src/tgba/tgbaproduct.cc, src/tgbaalgos/lbtt.cc,
	src/tgbaalgos/magic.cc, src/tgbaalgos/powerset.cc,
	src/tgbaalgos/reachiter.cc, src/tgbaalgos/gtec/ce.cc,
	src/tgbaalgos/gtec/gtec.cc, src/tgbatest/ltl2tgba.cc: Fix style
	issues reported by style.test.

1426
1427
1428
1429
1430
	* src/ltltest/inf.cc, src/ltltest/inf.test, src/ltltest/reduc.test,
	src/ltlvisit/formlength.cc, src/ltlvisit/reducform.cc,
	src/ltlvisit/reducform.hh: Fix copyright year, these files were
	created in 2004.

1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
	* src/sanity/80columns.test: New file.
	* src/sanity/Makefile.am (check-local): Run it.
	* src/ltltest/equals.test, src/ltltest/lunabbrev.test,
	src/ltltest/nenoform.test, src/ltltest/parseerr.test
        src/ltltest/tunabbrev.test, src/ltltest/reduc.cc,
	src/ltltest/tunabbrev.test, src/ltlvisit/forminf.cc,
	src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
	src/tgbatest/explprod.test, src/tgbatest/spotlbtt.test,
	src/tgbatest/tripprod.test: Wrap long lines.

1441
1442
2004-05-10  Thomas MARTINEZ  <martinez@abacus.lip6.fr>

1443
1444
	* src/tgbatest/ltl2tgba.cc (main): Add a option for reduce the formula.

1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
	* src/ltltest/formules.ltl: A pattern of 2000 formulas.
	* src/ltltest/inf.test: Test some case of implies.
	* src/ltltest/inf.cc: Test some case of implies.
	* src/ltltest/reduc.test: Test reduction of a file of formula.
	* src/ltltest/reduc.cc: Test reduction of a formula.

	* src/ltlvisit/formlength.cc: Gives the lenght of a formula.
	* src/ltlvisit/forminf.cc: To know if a formula implies an other.
	* src/ltlvisit/basereduc.cc: Implement only basic reduction.
	* src/ltlvisit/reducform.cc: Implement reduction.
	* src/ltlvisit/reducform.hh: To reduce a formula.

1457
1458
2004-05-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1459
1460
1461
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Refine
	fair_loop_approximation when branching postponement is not used.

1462
1463
1464
1465
1466
1467
	Cache formula translations, and canonize formulae before doing
	branching postponement.
	* src/tgbaalgos/ltl2tgba_fm.cc (formula_canonizer): New class, with
	bits extracted from fill_dests and ltl_to_tgba_fm.
	(fill_dests, ltl_to_tgba_fm): Adjust to use formula_canonizer.

1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument
	fair_loop_approx.
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Implement the
	fair_loop_approx optimization.
	(ltl_promise_visitor, ltl_possible_fair_loop_visitor,
	possible_fair_loop_checker): New classes.
	* src/tgbatest/ltl2tgba.cc: Add the -L option.
	* src/tgbatest/spotlbtt.test: Exercise fair_loop_approx.
	* wrap/python/cgi/ltl2tgba.in: Make it an option.

1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
2004-05-07  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument
	branching_postponement.
	* src/tgbaalgos/ltl2tgba_fm.cc (fill_dests): New function, extracted
	from ltl_to_tgba_fm().
	(ltl_to_tgba_fm): Implement the branching_postponement optimization.
	* src/tgbatest/ltl2tgba.cc: Add the -p option.
	* src/tgbatest/spotlbtt.test: Exercise branching postponement.
	* wrap/python/cgi/ltl2tgba.in: Make it an option.

1489
1490
2004-05-04  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1491
1492
1493
	* src/tgbaalgos/ltl2tgba_fm.cc: Add a superfluous return to pacify
	some GCC version.  Report from Denis Poitrenaud.

1494
1495
	* wrap/python/cgi/ltl2tgba.in: Fix output HTML.

1496
1497
1498
1499
1500
1501
1502
1503
1504
2004-05-03  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Clone and then
	free all formulae entered into canonical_succ, to avoid errors
	when a formula is entered into canonical_succ but not into
	formulae_seen.
	* src/tgbatest/ltl2tgba.test: Add a new test, and check with -f.
	Report from Thomas Martinez.

1505
1506
2004-04-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1507
1508
	* configure.ac, NEWS: Bump version to 0.0u.

1509
1510
1511
1512
	* configure.ac, NEWS: Bump version to 0.0t.
	* HACKING: Update tools requirements.
	* src/sanity/Makefile.am (EXTRA_DIST): Distribute includes.test.

1513
1514
1515
1516
	* src/sanity/Makefile.am, src/sanity/includes.test: New files.
	* src/Makefile.am (SUBDIRS): Add sanity.
	* configure.ac: Output src/sanity/Makefile.in.

1517
1518
1519
1520
1521
	* src/tgbatest/Makefile.am (check_PROGRAMS): Move ltl2tgba ...
	(noinst_PROGRAMS): ... here.
	* iface/gspn/Makefile.am (check_PROGRAMS): Rename as ...
	(noinst_PROGRAMS): ... this.

1522
1523
2004-04-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1524
	* src/tgbatest/explicit.test: Reorder bdd variables in output.
1525
1526
	Report from Denis Poitrenaud.

1527
1528
	* wrap/python/cgi/ltl2tgba.in: Print degeneralized statistics
	when show_never_claim.  Change the title to LTL-to-TGBA.
1529
	Suggested by Denis Poitrenaud.
1530

1531
1532
2004-04-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1533
1534
1535
	* wrap/python/cgi/ltl2tgba.in (print_footer): Make ltl2tgba.py's
	version a separate variable.

1536
1537
1538
	* wrap/python/cgi/ltl2tgba.in: Pass the formula to
	never_claim_reachable, and cgi.escape its output.
	Lighten the color a bit.
1539

1540
1541
1542
	* src/tgbaalgos/gtec/ce.hh, src/misc/freelist.hh,
	src/tgba/bddprint.hh: Fix Doxygen comments.

1543
1544
1545
1546
1547
1548
1549
	* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Document
	arguments.
	* src/tgbaalgos/neverclaim.cc (never_claim_bfs::state_is_accepting):
	New method.
	(never_claim_bfs::get_state_label, never_claim_bfs::process_state):
	Use it.

1550
1551
1552
	* wrap/python/cgi/ltl2tgba.in: Use darker color and introduce
	the new variable dot_bgcolor.

1553
1554
1555
	* wrap/python/cgi/ltl2tgba.in (add_options): Revamp options output
	using this new function.

1556
1557
1558
	* wrap/python/spot.i: Process tgbaalgos/neverclaim.hh.
	* wrap/python/cgi/ltl2tgba.in: Display the never claim on demand.

1559
2004-04-21  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570

	* src/ltlvisit/tostring.hh (to_spin_string): New function.
	Convert a formula into a string parsable by Spin.
	* src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: New files.
	Print the never claim in Spin format of a degeneralized TGBA.
	* src/tgbaalgos/Makefile.am: Add them.
	* src/tgbatest/ltl2tgba.cc: Add the option -N which outputs the
	never claim in Spin format of a degeneralized TGBA.
	* src/tgbatest/ltl2neverclaim.test: New file.
	* src/tgbatest/Makefile.am: Add it.

1571
1572
2004-04-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1573
1574
1575
1576
	* src/ltltest/defs.in, src/tgbatest/defs.in: Correctly set exitcode
	when valgrind is not used.
	Reported by Denis Poitrenaud.

1577
1578
1579
1580
1581
	* src/tgba/tgba.hh (tgba::succ_iter): Doco.
	* src/tgba/tgbatba.hh (tgba_tba_proxy::state_is_accepting): Document
	it.
	Reported by Denis Poitrenaud.

1582
2004-04-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>
1583

1584
1585
1586
	* iface/gspn/ltlgspn.cc (main) [SSP]: Use the standard
	counter-example computation for -e5 too.

1587
1588
1589
1590
	* iface/gspn/ltlgspn.cc (main) [!SSP]: Do not accept -e3, -e4, or -e5.
	(main) [SSP]: Use the standard counter-example computation
	for -e and -e1.

1591
1592
1593
2004-04-15  Soheib Baarir  <Souheib.Baarir@lip6.fr>
	    Alexandre Duret-Lutz  <adl@src.lip6.fr>

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1594
1595
1596
1597
1598
1599
1600
1601
1602
	Rename EESRG as SSP.
	* iface/gspn/eesrg.cc, iface/gspn/eesrg.hh,
	iface/gspn/dottyeesrg.cc: Rename as ...
	* iface/gspn/ssp.cc, iface/gspn/ssp.hh, iface/gspn/dottyssp.cc:
	... these.  Adjust all classes and function names.
	* iface/gspn/ltlgspn.cc, iface/gspn/Makefile.am: Adjust all classes
	filenames and function names.
	* m4/gspnlib.m4: Define WITH_GSPN_SSP and LIBGSPNSSP_LDFLAGS.

1603
1604
1605
1606
1607
1608
1609
1610
1611
1612
1613
1614
1615
1616
	* src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map::find):
	Rewrite.
	(numbered_state_heap_hash_map::index): New functions.
	(numbered_state_heap_hash_map::filter): Delete.
	* src/tgbaalgos/gtec/nsheap.hh
	(numbered_state_heap_hash_map::index): New functions.
	(numbered_state_heap_hash_map::filter): Delete.
	* iface/gspn/eesrg.cc (numbered_state_heap_eesrg_semi::find,
	numbered_state_heap_eesrg_semi::index): Rewrite.
	(numbered_state_heap_eesrg_semi::filter): Remove.
	* src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/ce.cc:
	Adjust to use find() and index() instead of filter()..


1617
1618
1619
1620
1621
1622
1623
1624
1625
1626
1627
	* iface/gspn/eesrg.cc (connected_component_eesrg::has_state):
	Free filtered states.
	(emptiness_check_shy_eesrg): New class.
	(emptiness_check_eesrg_shy): New function.
	* iface/gspn/eesrg.hh (emptiness_check_eesrg_shy): New function.
	* iface/gspn/ltlgspn.cc (main) [EESRG]: Handle -e3, -e4, and -e5.
	* * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc
	(emptiness_check_shy::check): Move arc, num, succ_queue, and todo
	as attributes.
	(emptiness_check_shy::find_state): New virtual function.

1628
1629
1630
1631
1632
1633
1634
1635
1636
1637
1638
1639
1640
1641
2004-04-14  Soheib Baarir  <Souheib.Baarir@lip6.fr>
	    Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* iface/gspn/ltlgspn.cc (connected_component_eesrg,
	connected_component_eesrg_factory, numbered_state_heap_eesrg_semi,
	numbered_state_heap_eesrg_const_iterator,
	numbered_state_heap_eesrg_factory_semi): New classes.
	(emptiness_check_eesrg_semi, emptiness_check_eesrg_shy_semi,
	counter_example_eesrg): New functions.
	* iface/gspn/eesrg.hh (emptiness_check_eesrg_semi,
	emptiness_check_eesrg_shy_semi, counter_example_eesrg): New
	functions.
	* iface/gspn/ltlgspn.cc [EESRG]: Adjust to call these new functions.

1642
1643
1644
1645
1646
1647
1648
1649
2004-04-14  Soheib Baarir  <Souheib.Baarir@lip6.fr>

	* iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg,
	state_gspn_eesrg): Compute the array of all successors of the
	right state beforehand, pass it to Greatspn (left automata) at
	once, let it compute the resulting synchronized arcs, and iterate
	on that result.

1650
1651
2004-04-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1652
1653
1654
1655
1656
1657
1658
1659
1660
1661
1662
1663
1664
	* src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap_factory,
	numbered_state_heap_hash_map_factory): New class.
	* src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map_factory):
	Implement it.
	* src/tgbaalgos/gtec/gtec.hh (emptiness_check::emptiness_check,
	emptiness_check_shy::emptiness_check_shy): Take a
	numbered_state_heap_factory argument.
	* tgbaalgos/gtec/status.hh
	(emptiness_check_status::emptiness_check_status): Likewise.
	(emptiness_check_status::h): Make it a numbered_state_heap*.
	* src/tgbaalgos/gtec/ce.cc, tgbaalgos/gtec/gtec.cc,
	tgbaalgos/gtec/status.cc: Adjust uses of ecs_->h.

1665
1666
1667
1668
1669
1670
1671
1672
1673
1674
1675
1676
1677
1678
1679
1680
1681
1682
	* src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc:
	Delete and split into ...
	* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
	src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh,
	src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
	src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh,
	src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
	src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: ...
	these new files.
	* src/tgbaalgos/gtec/Makefile.am: New file.
	* src/tgbaalgos/Makefile.am (SUBDIRS, libtgbaalgos_la_LIBADD):
	Recurse into gtec and link gtec/libgtec.la.
	(tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Remove emptinesscheck.hh
	and emptinesscheck.cc.
	* configure.ac: Output src/tgbalagos/gtec/Makefile.
	* iface/gspn/ltlgspn.cc, src/tgbatest/ltl2tgba.cc: Update includes.
	* README: Update tree description.

1683
1684
2004-04-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1685
	* src/tgbaalgos/emptinesscheck.hh (numbered_state_heap_const_iterator,
1686
	numbered_state_heap, numbered_state_heap_hash_map): New classes.
1687
	* src/tgbaalgos/emptinesscheck.cc
1688
1689
1690
	(numbered_state_heap_hash_map_const_iterator): New class.
	(numbered_state_heap_hash_map): Implement it.

1691
1692
1693
1694
1695
1696
1697
	* src/tgbaalgos/emptinesscheck.hh
	(explicit_connected_component_factory,
	connected_component_hash_set_factory): New classes.
	(counter_example::counter_example): Take an
	explicit_connected_component_factory factory argument.
	* src/tgbaalgos/emptinesscheck.cc: Adjust.

1698
1699
1700
1701
1702
1703
	* src/tgbaalgos/emptinesscheck.hh (explicit_connected_component):
	New class.
	(counter_example::connected_component_set): Rename as ...
	(connected_component_hash_set): ... this, and inherit from
	explicit_connected_component.
	(counter_example::accepting_path, counter_example::complete_cycle):
1704
1705
1706
	Take an explicit_connected_component argument instead of a
	connected_component_set.
	* src/tgbaalgos/emptinesscheck.cc: Adjust.
1707

1708
1709
1710
1711
1712
	* src/tgbaalgos/emptinesscheck.hh
	(counter_example::connected_component_set::has_state): Return
	a const state* and behave like h_filt.
	* src/tgbaalgos/emptinesscheck.cc: Adjust.

1713
1714
1715
1716
1717
1718
	* src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2): Move
	into ...
	(emptiness_check_shy): This new subclass of emptiness_check.
	* src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
	iface/gspn/ltlgspn.cc: Adjust.