ChangeLog 173 KB
Newer Older
1
2
2004-11-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>

3
4
5
6
7
8
9
10
11
12
13
	* 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.

14
15
16
17
18
19
20
21
22
23
24
25
26
	* 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.

27
28
29
	* src/misc/hashfunc.hh: Include cstddef to define size_t, and guard
	the file for multiple inclusions.

30
31
32
33
34
35
36
37
38
39
40
41
42
	* 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/.

43
44
2004-11-16  Alexandre Duret-Lutz  <adl@src.lip6.fr>

45
46
47
48
49
50
51
52
53
54
55
56
57
	* 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().

58
59
60
	* src/tgba/tgbatba.cc (state_tba_proxy::hash): Use wang32_hash.
	* src/tgba/tgbaproduct.cc (state_product::hash): Likewise.

61
62
63
64
65
	* 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.

66
2004-11-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>
67
68
69
70
71
72
73

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

74
75
76
77
78
79
2004-11-15  Poitrenaud Denis  <denis@src.lip6.fr>

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

80
81
2004-11-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>

82
83
84
85
	* tgbatest/randtgba.cc: Add options -e and -r.
	* tgbatest/emptchkr.test: New file.
	* src/tgbatest/Makefile.am (TESTS, XFAIL_TESTS): Add emptchkr.test.

86
87
88
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix a memory leak
	if debug==false.

89
90
91
92
	* src/tgbaalgos/randomgraph.cc (random_graph): Do declare all the
	acceptance conditions in the produced automaton, in case they are
	not actually used.

93
94
95
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Write to the
	supplied stream, not std::cout.

96
97
98
99
100
101
102
103
104
2004-11-15  Poitrenaud Denis  <denis@src.lip6.fr>

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

105
106
107
108
109
110
111
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.

112
113
2004-11-12  Alexandre Duret-Lutz  <adl@src.lip6.fr>

114
115
116
117
	* configure.ac: Check for srand48 and drand48.
	* src/misc/random.cc (srand, drand): Use srand48 and drand48 if
	available.

118
119
120
121
122
123
124
125
	* 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.

126
127
128
	* misc/random.cc, misc/random.hh: New files.
	* src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.

129
130
2004-11-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>

131
132
133
	* src/evtgbaparse/public.hh (evtgba_parse): Fix doxygen comments.
	* src/tgbaalgos/projrun.hh (project_tgba_run): Likewise.

134
135
	* src/tgbaalgos/emptiness.hh (print_tgba_run): Document it.

136
137
138
139
140
141
142
	* 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.

143
144
145
146
147
	* 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().

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

150
151
152
	* src/tgbatest/Makefile.am (TESTS): Remove non-existing magic.test
	and se05.test.

153
154
155
	* src/tgbatest/ltl2tgba.cc (syntax): Fix old typos and reword
	some help strings.

156
157
158
159
160
161
162
163
164
165
166
167
168
2004-11-09  Poitrenaud Denis  <denis@src.lip6.fr>

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

169
170
171
172
173
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.

174
175
2004-11-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>

176
177
178
179
180
181
182
	* 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.

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

186
187
188
189
190
	* 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.

191
192
193
	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run):
	Remove spurious FIXME.

194
195
2004-11-05  Alexandre Duret-Lutz  <adl@src.lip6.fr>

196
197
198
199
	* src/evtgbaalgos/save.cc (save_bfs::output_acc_set): Sort
	acceptance conditions in the output.
	* src/evtgbatest/readsave.test, src/evtgbatest/product.test: Adjust.

200
201
202
	* src/tgbaalgos/rundotdec.cc (tgba_run_dotty_decorator::link_decl):
	Typo.

203
204
2004-11-04  Alexandre Duret-Lutz  <adl@src.lip6.fr>

205
206
207
	* src/tgbaalgos/neverclaim.cc (never_claim_bfs::process_link):
	Adjust prototype.

208
209
210
211
	* 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.

212
213
214
215
	* wrap/python/spot.i: Generate bindings for tgbaalgos/dottydec.hh,
	tgbaalgos/emptiness.hh, tgbaalgos/gtec/gtec.hh, and
	tgbaalgos/rundotdec.hh.

216
217
	* src/tgbaalgos/lbtt.cc (lbtt_bfs::process_link): Adjust prototype.

218
219
2004-11-03  Alexandre Duret-Lutz  <adl@src.lip6.fr>

220
221
222
223
224
225
226
227
228
229
	* 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.
230
	* src/tgbatest/emptchk.test: Exercise -g.
231

232
233
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Add missing std::endl.

234
235
236
237
238
239
240
241
242
243
244
245
246
247
	* 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.

248
249
2004-11-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>

250
251
	* src/ltlvisit/reduce.hh (is_eventual, is_universal): More doc.

252
253
254
255
256
	* 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.

257
258
259
260
261
262
263
	* 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().

264
265
	* src/ltlast/formula.hh (ltl::formula::~formula): Make it protected.

266
267
2004-10-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>

268
269
270
271
272
273
274
275
276
277
278
279
	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.

280
281
282
283
	* src/tgbaalgos/gtec/gtec.cc,
	src/tgbaalgos/gtec/gtec.hh (couvreur99_check::print_stats): New.
	* src/tgbatest/ltl2tgba.cc: Print emptiness-check statistics.

284
285
286
287
288
289
	* 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.

290
291
292
293
	* 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.

294
295
296
	* src/misc/version.cc: Fix trailing whitespace.
	* src/sanity/style.test: Diagnose trailing whitespace.

297
298
299
300
	* src/tgbatest/ltl2tgba.cc: Fix lines longer than 80 chars.
	* src/sanity/80columns.test: Use expand to untabify, the previous
	recipe was incomplete.

301
302
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Note duplicate states.

303
304
305
	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Verify the run is
	accepting.

306
307
308
	* src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_path):
	Initialize best_end to remove a spurious warning.

309
310
311
312
313
314
315
316
317
318
	* 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.

319
320
2004-10-28  Alexandre Duret-Lutz  <adl@src.lip6.fr>

321
322
323
324
	* 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.

325
326
327
328
329
330
331
332
333
	* 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.

334
335
2004-10-27  Alexandre Duret-Lutz  <adl@src.lip6.fr>

336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
	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.

354
355
356
357
358
359
360
361
362
	* 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.

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

366
367
368
369
2004-10-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

370
371
2004-10-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
	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.

392
393
394
	* src/misc/bareword.hh, src/misc/bareword.cc (quote_unless_bare_word):
	New function.

395
396
397
	* src/ltlvisit/tostring.cc (to_spin_string_visitor): Move to
	anonymous namespace.

398
399
400
401
2004-10-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

402
403
2004-10-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>

404
405
406
	* src/misc/modgray.hh (loopless_modular_mixed_radix_gray_code::done,
	loopless_modular_mixed_radix_gray_code::last): Declare as const.

407
408
409
	* src/misc/bareword.hh, src/misc/bareword.cc: New files.
	* src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them.

410
411
412
413
414
415
	* 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.

416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
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 {.

435
436
2004-10-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

439
440
441
442
443
444
445
446
447
448
449
450
451
452
	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.

453
454
2004-10-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

455
456
457
	* src/ltltest/reduc.test: Do source ./defs.  Revert mistaken
	change from 2004-09-13.

458
459
	* src/tgbatest/explicit.test: Typo.

460
461
2004-10-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

462
463
464
465
466
467
468
469
470
471
472
	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.

473
474
475
476
477
	* 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.

478
479
480
481
2004-10-12  Alexandre Duret-Lutz  <adl@gnu.org>

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

482
483
484
485
486
2004-10-11  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

487
488
489
490
2004-10-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

491
492
493
494
495
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.

496
497
2004-09-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

498
499
500
501
502
503
	* 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.

504
505
506
507
	* 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.

508
509
2004-09-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

510
511
512
513
514
	* 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.

515
516
517
518
519
520
521
522
523
524
	* 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.

525
526
2004-09-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
527
528
529
530
531
532
	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.

533
534
	* INSTALL, lbtt/INSTALL: New upstream version.

535
536
2004-09-14  Thomas Martinez  <martinez@src.lip6.fr>

martinez's avatar
martinez committed
537
538
539
540
541
542
543
544
	* 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.

545
546
	* src/ltltest/reduc.test (FICH): bad file name.

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

549
550
551
	* src/tgbaalgos/nesteddfsgen.hh src/tgbaalgos/nesteddfsgen.cc:
	New algorithm for emptiness check.

martinez's avatar
martinez committed
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
	* 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
573
574
575
576
577
578
579
580
581
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,
582
	src/tgbaalgos/colordfs.cc: four new algorithms for emptiness check.
martinez's avatar
martinez committed
583

martinez's avatar
martinez committed
584
	* src/tgbaalgos/gtec/ce.hh,
martinez's avatar
martinez committed
585
586
587
	src/tgbaalgos/gtec/ce.cc: Adapt the counter exemple for the ce
	object in minimalce.hh.

martinez's avatar
martinez committed
588
	* src/tgbatest/ltl2tgba.cc,
martinez's avatar
martinez committed
589
	src/tgbatest/emptchk.test,
590
	src/tgbaalgos/Makefile.am: Add files for emptiness-check.
martinez's avatar
martinez committed
591
592
593
594
595
596
597

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.

598
599
2004-08-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

600
601
	* configure.ac, NEWS: Bump version to 0.0y.

602
603
	* configure.ac, NEWS: Bump version to 0.0x.

604
605
2004-08-12  Alexandre Duret-Lutz  <adl@src.lip6.fr>

606
607
608
	* doc/Doxyfile.in (GENERATE_TAGFILE): Build spot.tag.
	* doc/Makefile.am (dist_pkgdata_DATA): Add spot.tag.

609
610
	* src/tgbatest/ltl2tgba.cc (syntax): Typo.

611
612
613
	* doc/Doxyfile.in (STRIP_FROM_PATH): Strip @srcdir@ so its
	does not appear when listing mainpage.dox.

614
615
616
617
618
2004-08-11  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

619
620
2004-08-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>

621
622
623
624
	* src/ltlvisit/apcollect.hh: Fix include guard.  Report from Denis.
	* src/sanity/includes.test: Include files twice to check include
	guards.

625
626
627
	* src/tgbatest/ltl2tgba.cc (main): Fix another gcc warning in case
	assert() is disabled.

628
629
630
	* src/Makefile.am (nodist_EXTRA_libspot_la_SOURCES): New variable,
	to force C++ linking.

631
632
633
	* iface/gspn/ltlgspn.cc: Fix a gcc warning in case assert() is
	disabled.

634
635
2004-08-09  Alexandre Duret-Lutz  <adl@src.lip6.fr>

636
637
638
639
640
	* 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.

641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
	* 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.

658
659
660
661
662
663
664
	* 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.

665
666
667
	* doc/Doxyfile.in (STRIP_FROM_INC_PATH): Define, so that the
	`#include' references are correct.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
668
669
	* README: Update.

670
671
	* m4/gccoptim.m4: Compute optimization flags for CXX too.

672
673
	* m4/ndebug.m4: Update CPPFLAGS, not CFLAGS.

674
675
676
677
	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Document all
	parameters.
	* src/tgbaalgos/ltl2tgba_lacim.hh (ltl_to_tgba_lacim): Likewise.

678
679
680
681
682
683
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.

684
685
686
687
2004-08-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* lbtt/: Merge lbtt 1.1.2.

688
689
690
691
2004-07-30  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* lbtt/: Merge lbtt 1.1.1.

692
693
694
695
2004-07-26  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

696
697
698
699
700
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.

701
702
2004-07-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

703
704
705
	* 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.

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

709
710
711
712
713
714
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.

715
716
2004-07-16  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

720
721
	* iface/gspn/ssp.cc: Typos.

722
723
724
725
	* 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.

726
727
728
729
2004-07-12  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

730
731
2004-07-09  Alexandre Duret-Lutz  <adl@src.lip6.fr>

732
733
734
	* src/tgba/state.hh (state_ptr_equal, state_ptr_hash): Fix Doxygen
	example.

735
736
737
738
	* src/tgbaalgos/reductgba_sim.hh (parity_game_graph_delayed,
	reduc_tgba_sim): Fix warnings about Doxygen comment.
	* src/ltlvisit/reduce.hh (reduce): Likewise.

739
740
741
742
	* 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
743
744
	* THANKS: Fill in.

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

747
748
2004-07-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>

749
750
751
752
753
754
755
756
757
758
759
760
	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".

761
762
763
764
765
	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
766
767
	automata_.  Local protected member automata_ inherited from
	template base class must be prefixed or g++ 3.4 will not look it
768
769
	up (conforming to 14.6.2.3).

770
771
2004-07-07  Alexandre Duret-Lutz  <adl@src.lip6.fr>

772
773
774
775
	* lbtt/: Merge lbtt 1.1.0.
	* src/tgbatest/spotlbtt.test: Adjust config file syntax to
	please lbtt 1.1.0.

776
777
778
779
780
	* 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...

781
782
783
784
785
786
787
788
789
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)

790
791
2004-06-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>

792
793
	* configure.ac, NEWS: Bump version to 0.0w.

794
795
	* configure.ac, NEWS: Bump version to 0.0v.

martinez's avatar
martinez committed
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
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.

813
814
815
816
2004-06-28  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* buddy/: Merge buddy-2-3.

817
818
819
820
821
2004-06-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

822
823
824
825
826
827
828
829
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.
830

831
832
833
834
	* 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.

835
	* wrap/python/cgi/ltl2tgba.in: Add "Formula Simplications" options.
836
	* wrap/python/spot.i: Wrap src/ltlvisit/reduce.hh.
837

838
839
840
841
842
843
844
845
846
	* 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.

847
848
849
850
851
852
	* 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.

853
854
855
	* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit(binop*)):
	Factorize.

856
857
858
859
860
861
862
863
	* 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.

864
865
866
	* src/ltlvisit/lunabbrev.hh: Revert superfluous change from
	2004-05-10.

867
868
869
870
871
872
873
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.

874
875
876
877
2004-06-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/sanity/style.test: Typo.

878
879
880
881
882
883
884
885
886
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.

887
888
889
890
891
892
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.

893
894
2004-06-17  Thomas Martinez  <martinez@src.lip6.fr>

895
	* src/tgbatest/reductgba.test: Wrong test are removed.
896

897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
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

913
914
915
916
917
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.

918
919
920
921
922
2004-06-16  Thomas Martinez  <martinez@src.lip6.fr>

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

923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
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.

943
944
2004-06-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>

945
946
947
948
949
950
951
952
953
954
955
	* 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.

956
957
958
959
960
961
	* 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>
962
963
964
965
966
967
968
969
970
971
972
973

	* 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>
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989

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

990
991
2004-05-26  Alexandre Duret-Lutz  <adl@src.lip6.fr>

992
993
994
	* src/ltlvisit/reducform.cc (reduce_form_visitor::visit(constant)):
	Simplify.

995
996
997
998
999
1000
1001
	* 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.

1002
1003
2004-05-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1004
1005
1006
1007
1008
1009
1010
1011
	* 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.

1012
1013
1014
1015
1016
1017
1018
1019
	* 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.

1020
1021
1022
	* src/ltlvisit/basereduc.cc, src/ltlvisit/formlength.cc: Remove
	useless includes.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1023
1024
	* AUTHORS: Update.

1025
1026
1027
	* src/ltlvisit/reducform.hh: Update Doxygen comments for
	previous change.

1028
1029
1030
1031
1032
1033
1034
1035
	* 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.

1036
1037
1038
1039
	* src/sanity/style.test: Catch {.*{ and }.*}.
	* src/sanity/80columns.test: Untabify files.
	* iface/gspn/ltlgspn.cc, src/ltlvisit/basereduc.cc: Fix long lines.

1040
1041
1042
	* src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc,
	src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes.

1043
1044
	* wrap/python/cgi/ltl2tgba.in: Typos.

1045
1046
2004-05-24  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1047
1048
1049
	* src/sanity/style.test: Catch `;'-not-followed-by-space.
	* src/ltlvisit/reducform.cc, src/ltlvisit/forminf.cc: Fix style.

1050
1051
	* src/ltlvisit/reducform.hh: Fix some Doxygen comments.

1052
1053
	* src/tgbatest/ltl2tgba.cc (syntax): Keep options sorted.

1054
1055
1056
	* src/sanity/Makefile.am (EXTRA_DIST): Distribute 80columns.test
	and style.test.

1057
	* src/ltltest/Makefile.am (EXTRA_DIST): Distribute formulae.txt.
1058
	* src/ltltest/formulae.txt: New file (2200 LTL formulea generated
1059
1060
1061
1062
	by Wring).
	* src/ltltest/formules.ltl: Delete.
	* src/reduc.test: Read formulae.txt.

1063
1064
1065
1066
1067
1068
1069
1070
1071
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.

1072
1073
2004-05-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
	* 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.

1085
1086
1087
	* src/sanity/style.test: Check the iface/ tree too.
	* iface/gspn/gspn.cc, iface/gspn/ssp.cc: Fix style.

1088
1089
1090
1091
1092
1093
	* 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.

1094
1095
1096
1097
1098
1099
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.

1100
1101
2004-05-17  Thomas Martinez  <martinez@src.lip6.fr>

1102
1103
	* src/ltlvisit/basereduc.cc, src/ltltest/inf.cc (main): Style.

1104
1105
1106
1107
1108
1109
	* 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.

1110
1111
2004-05-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1112
1113
1114
	* 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.

1115
1116
1117
1118
1119
1120
1121
	* 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.

1122
1123
	* src/ltlvisit/formlength.cc: Fix style to please sanity checks.

1124
1125
	* src/ltlvisit/lunabbrev.cc: Fix style to please sanity checks.

1126
1127
1128
	* src/tgbaalgos/neverclaim.cc: Fix them.
	* sanity/style.test: Diagnose semicolons with leading spaces.

1129
1130
1131
	* src/ltlvisit/forminf.cc: Fix style to please sanity checks.
	Also avoid node_type_form_visitor where a dynamic_cast is done.

1132
1133
2004-05-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1134
1135
	* wrap/python/buddy.i: Preliminary bindings for FDD and BVEC.

1136
1137
1138
	* ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style.
	* sanity/style.test: More tests.

1139
1140
1141
	* src/tgbatest/ltl2tgba.cc (main): Fix style.
	* HACKING: Mention `else if'.

1142
1143
1144
1145
	* 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.

1146
1147
2004-05-14  Thomas Martinez  <martinez@src.lip6.fr>

1148
1149
	* src/tgbatest/ltl2tgba.cc (main): Thinko.

1150
1151
1152
1153
1154
1155
	* 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.

1156
1157
2004-05-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1158
1159
1160
1161
1162
1163
1164
1165
1166
	* 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.

1167
1168
1169
1170
	* 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.

1171
1172
1173
	* src/ltltest/reduc.test: Use ./defs and clean result.data.
	* src/ltltest/Makefile.am (CLEANFILES): Clean result.data.

1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
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.

1184
1185
2004-05-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1186
1187
	* src/ltltest/reduc.test: Typo.

1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
	* 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".

1198
1199
2004-05-11  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

1202
1203
	* src/ltltest/reduc.test: POSIXify.

1204
1205
2004-05-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
	* 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.

1216
1217
1218
1219
1220
	* 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.

1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
	* 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.

1231
1232
2004-05-10  Thomas MARTINEZ  <martinez@abacus.lip6.fr>

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

1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
	* 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.

1247
1248
2004-05-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1249
1250
1251
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Refine
	fair_loop_approximation when branching postponement is not used.

1252
1253
1254
1255
1256
1257
	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.

1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
	* 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.

1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
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.

1279
1280
2004-05-04  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1281
1282
1283
	* src/tgbaalgos/ltl2tgba_fm.cc: Add a superfluous return to pacify
	some GCC version.  Report from Denis Poitrenaud.

1284
1285
	* wrap/python/cgi/ltl2tgba.in: Fix output HTML.

1286
1287
1288
1289
1290
1291
1292
1293
1294
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.

1295
1296
2004-04-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1297
1298
	* configure.ac, NEWS: Bump version to 0.0u.

1299
1300
1301
1302
	* configure.ac, NEWS: Bump version to 0.0t.
	* HACKING: Update tools requirements.
	* src/sanity/Makefile.am (EXTRA_DIST): Distribute includes.test.

1303
1304
1305
1306
	* src/sanity/Makefile.am, src/sanity/includes.test: New files.
	* src/Makefile.am (SUBDIRS): Add sanity.
	* configure.ac: Output src/sanity/Makefile.in.

1307
1308
1309
1310
1311
	* src/tgbatest/Makefile.am (check_PROGRAMS): Move ltl2tgba ...
	(noinst_PROGRAMS): ... here.
	* iface/gspn/Makefile.am (check_PROGRAMS): Rename as ...
	(noinst_PROGRAMS): ... this.

1312
1313
2004-04-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1314
	* src/tgbatest/explicit.test: Reorder bdd variables in output.
1315
1316
	Report from Denis Poitrenaud.

1317
1318
	* wrap/python/cgi/ltl2tgba.in: Print degeneralized statistics
	when show_never_claim.  Change the title to LTL-to-TGBA.
1319
	Suggested by Denis Poitrenaud.
1320

1321
1322
2004-04-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1323
1324
1325
	* wrap/python/cgi/ltl2tgba.in (print_footer): Make ltl2tgba.py's
	version a separate variable.

1326
1327
1328
	* wrap/python/cgi/ltl2tgba.in: Pass the formula to
	never_claim_reachable, and cgi.escape its output.
	Lighten the color a bit.
1329

1330
1331
1332
	* src/tgbaalgos/gtec/ce.hh, src/misc/freelist.hh,
	src/tgba/bddprint.hh: Fix Doxygen comments.

1333
1334
1335
1336
1337
1338
1339
	* 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.

1340
1341
1342
	* wrap/python/cgi/ltl2tgba.in: Use darker color and introduce
	the new variable dot_bgcolor.

1343
1344
1345
	* wrap/python/cgi/ltl2tgba.in (add_options): Revamp options output
	using this new function.

1346
1347
1348
	* wrap/python/spot.i: Process tgbaalgos/neverclaim.hh.
	* wrap/python/cgi/ltl2tgba.in: Display the never claim on demand.

1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
2004-04-21  Denis Poitrenaud  <dp@src.lip6.fr>

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

1361
1362
2004-04-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1363
1364
1365
1366
	* src/ltltest/defs.in, src/tgbatest/defs.in: Correctly set exitcode
	when valgrind is not used.
	Reported by Denis Poitrenaud.

1367
1368
1369
1370
1371
	* src/tgba/tgba.hh (tgba::succ_iter): Doco.
	* src/tgba/tgbatba.hh (tgba_tba_proxy::state_is_accepting): Document
	it.
	Reported by Denis Poitrenaud.

1372
2004-04-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>
1373

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

1377
1378
1379
1380
	* 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.

1381
1382
1383
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
1384
1385
1386
1387
1388
1389
1390
1391
1392
	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.

1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
	* 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()..


1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
	* 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.

1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
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.

1432
1433
1434
1435
1436
1437
1438
1439
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.

1440
1441
2004-04-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
	* 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.

1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
	* 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.

1473
1474
2004-04-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1475
	* src/tgbaalgos/emptinesscheck.hh (numbered_state_heap_const_iterator,
1476
	numbered_state_heap, numbered_state_heap_hash_map): New classes.
1477
	* src/tgbaalgos/emptinesscheck.cc
1478
1479
1480
	(numbered_state_heap_hash_map_const_iterator): New class.
	(numbered_state_heap_hash_map): Implement it.

1481
1482
1483
1484
1485
1486
1487
	* 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.

1488
1489
1490
1491
1492
1493
	* 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):
1494
1495
1496
	Take an explicit_connected_component argument instead of a
	connected_component_set.
	* src/tgbaalgos/emptinesscheck.cc: Adjust.
1497

1498
1499
1500
1501
1502
	* 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.

1503
1504
1505
1506
1507
1508
	* 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.

1509
1510
	* src/tgba/bdddict.hh (bdd_dict::annon_free_list): Hide from Swig.

1511
1512
1513
1514
1515
1516
	* src/tgbaalgo/semptinesscheck.hh (counter_example): New class,
	extracted from ...
	(emptiness_check): ... here.
	* src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
	iface/gspn/ltlgspn.cc: Adjust.

1517
1518
1519
	* wrap/python/Makefile.am ($(srcdir)/spot_wrap.cxx)
	($(srcdir)/buddy_wrap.cxx): Use -noruntime instead of -c.

1520
1521
1522
1523
1524
	* src/tgbaalgo/semptinesscheck.hh (emptiness_check_status): New class,
	extracted from ...
	(emptiness_check): ... here.
	* src/tgbaalgos/emptinesscheck.cc: Adjust.

1525
1526
1527
1528
1529
1530
	* src/tgbaalgo/semptinesscheck.hh (scc_stack): New class, extracted
	from ...
	(emptiness_check): ... here.
	(emptiness_check::root): Redefined as a scc_stack object.
	* src/tgbaalgos/emptinesscheck.cc: Adjust.

1531
1532
1533
1534
1535
2004-04-05  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle):
	Do not visit a state more than once.  Report from Soheib Baarir.

1536
1537
2004-03-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
1548
1549
1550
	* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict): Reuse Acc and Var
	variables from a shared bdd_dict.  Register Next variables as
	anonymous variables.
	(translate_dict::translate_dict, translate_dict::~translate_dict,
	translate_dict::register_proposition,
	translate_dict::register_a_variable,
	translate_dict::register_next_variable,
	translate_dict::dump, translate_dict::var_to_formula,
	ltl_to_tgba_fm): Adjust.
	(translate_dict::dict): New attribute.
	(translate_dict::a_map, translate_dict::a_formula_map,
	translate_dict::var_map, translate_dict::var_formula_map): Delete.

1551
1552
1553
1554
1555
1556
1557
	* src/misc/freelist.cc (free_list::remove): Work around
	invalidated iterators.
	* tgba/bdddict.cc (unregister_variable): New methods,
	extracted from ...
	(bdd_dict::unregister_all_my_variables): ... here.
	* tgba/bdddict.hh (unregister_variable): Declare them.

1558
1559
2004-03-23  Alexandre DURET-LUTZ  <adl@src.lip6.fr>

1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
	* src/misc/freelist.hh (free_list::remove, free_list::insert): New
	methods.
	* src/misc/freelist.cc (free_list::register_n,
	free_list::releases_n): Rewrite using free_list::remove and
	free_list::insert.
	(free_list::remove, free_list::insert): New methods.
	* src/tgba/bdddict.hh (bdd_dict::register_anonymous_variables):
	New method.
	(bdd_dict::annon_free_list): New subclass.
	(bdd_dict::free_annonymous_list_of_type_of): New attribute.
	* src/tgba/bdddict.cc (bdd_dict::register_all_variables_of,
	bdd_dict::unregister_all_my_variables): Handle anonymous variables
	too.
	(bdd_dict::register_anonymous_variables,
	bdd_dict::annon_free_list::annon_free_list,
	bdd_dict::annon_free_list::extend): New methods.

1577
1578
1579
	* src/tgbaalgos/emptinesscheck.cc (emptiness_check::accepting_path)
	Fix handling of PATH when backtracking.  Report from Soheib Baarir.

1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595
2004-03-18  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	Move the free_list management into a separate class for reuse.

	* src/misc/freelist.hh, src/misc/freelist.cc: New files.
	* src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.
	* src/misc/bddalloc.hh (bdd_allocator): Inherit from free_list and
	make dump_free_list visible.
	* src/misc/bddalloc.cc (bdd_allocator::allocate_variables): Move
	all the code into free_list::register_n() and
	bdd_allocator::extend(), and call the former.
	(bdd_allocator::release_variables): Move all the code into
	free_list::release_n() and call it.
	(bdd_allocator::extend): New method.
	* src/tgba/bdddict.cc (bdd_dict::dump): Call dump_free_list;

1596
1597
1598
1599
2004-03-09  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* configure.ac, NEWS: Bump version to 0.0s.

1600
1601
2004-03-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1602
1603
	* configure.ac, NEWS: Bump version to 0.0r.

1604
1605
1606
1607
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm) <exprop>: Do not
	blindly enumerate all combinations of atomic properties; initially
	set all_props to the set of all possibly satisfiable combinations.

1608
1609
2004-02-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1610
1611
1612
	* lbtt/src/Makefile.am (lbtt_translate_SOURCES): Fix leftover
	from 1.0.3 merge.

1613
1614
	* wrap/python/cgi/ltl2tgba.in: Process ltl2tgba.opt if it exists.

1615
1616
	* wrap/python/cgi/ltl2tgba.in: Color translators and their options.

1617
1618
2004-02-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1619
1620
	* wrap/python/cgi/ltl2tgba.in: Present the options in a table.

1621
1622
1623
1624
	* wrap/python/cgi/ltl2tgba.in: Remove the "print dot" options,
	add a "dot source" source behind each picture instead.  Do
	not run `dot' on big automata.

1625
1626
1627
1628
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Fix example
	in comment.  Skip false transitions, and do not compute
	sub-formulae reachable only via false transitions.

1629
1630
1631
1632
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Revert
	yesterday's change.  This optimization is NOT covered by exprop.
	In fact it could be generalized.

1633
1634
2004-02-19  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1635
1636
1637
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Remove the
	cond_for_true optimization.  It is covered by exprop.

1638
1639
1640
	* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::current_state):
	Fix reference to Oddoux's thesis.

1641
1642
2004-02-16  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1643
1644
1645
1646
1647
1648
1649
1650
	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add the
	symb_merge argument.
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Likewise.
	* src/tgbatest/ltl2tgba.cc (main): Rename -fx as -x, and add -y
	to unset symb_merge.
	* wrap/python/cgi/ltl2tgba.in: Remove the exprop version
	of the FM translator, make exprop and symb_merge options.

1651
1652
1653
1654
1655
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit) <unop::G>:
	suppress the GFy optimisation introduced on 2003-11-26, it is
	generalized by the identification of states with same symbolic
	rewriting introduced on 2004-02-02.

1656
1657
	* lbtt/: Merge lbtt 1.0.3.

1658
1659
1660
1661
1662
2004-02-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbatest/ltl2baw.pl (END): Ensure LTL2TGBA is always
	closed.

1663
1664
1665
1666
1667
1668
1669
1670
1671
1672
1673
2004-02-11  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/tgbatest/ltl2tgba.cc (syntax): Recognize "-" as input
	filename for the formula.  Merge the transitions of automata
	read with -X.
	* src/tgbatest/spotlbtt.test: Add many disabled algorithms.
	It is convenient to reuse the `config' file created by this
	test when making statistics.
	* src/tgbatest/ltl2baw.pl: New file.
	* src/tgbatest/Makefile.am (EXTRA_DIST): Add ltl2baw.pl.

1674
1675
2004-02-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1676
1677
1678
	* wrap/python/libpy.c: Update from Swig 1.3.21.
	* HACKING: Update versions.

1679
1680
1681
1682
1683
1684
1685
1686
1687
	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Take an exprop
	argument.  Consider all possible combinations of propositions when
	generating arcs.  Suggested by Jean-Michel Couvreur.
	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Adjust.
	* src/tgbatest/ltl2tgba.cc: Honor -fx.
	* src/tgbatest/spotlbtt.test: Exercise -fx.
	* wrap/python/cgi/ltl2tgba.in: Support Couvreur/FM with exploded
	properties.

1688
1689
2004-02-09  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1690
1691
	* src/ltlparse/ltlparse.yy: Typo.

1692
1693
1694
1695
1696
	* wrap/python/cgi/ltl2tgba.in: Use render_dot when
	showing formula.
	* wrap/python/cgi/README: Mention unique_id.

2004-02-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710

	This should help getting accurate statistics (on both the
	formula automaton and the synchronized product) from LBTT.
	Idea from Jean-Michel Couvreur.

	* src/tgbaalgos/lbtt.cc (nonacceptant_lbtt_bfs): New class.
	(nonacceptant_lbtt_reachable): New function.
	* src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): New
	function.
	* src/tgbatest/ltl2tgba.cc (main): Call nonacceptant_lbtt_reachable
	if the -T option is used.
	* src/tgbatest/spotlbtt.test: Setup the -T variants, disabled by
	default.

1711
1712
2004-02-05  Alexandre Duret-Lutz  <adl@src.lip6.fr>

1713
1714
	* src/tgbaalgos/lbtt.hh: Typos.

1715
1716
	* src/tgbatest/spotlbtt.test: Typo.

</