ChangeLog 36.8 KB
Newer Older
1
2
2003-06-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

3
4
5
6
	* src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments.
	* src/ltlast/formula.hh: More Doxygen comments.
	* src/tgba/tgba.hh: Use <tt> in Doxygen comments.

7
8
9
10
	* doc/mainpage.dox: New file.
	* doc/Makefile.am (EXTRA_DIST): Add mainpage.dox.
	* doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox

11
12
13
14
15
16
17
	* src/tgba/succiter.hh: Adjust comments about promises to
	refer to accepting conditions.
	* src/tgba/tgbabddconcretefactory.hh: Likewise.
	* src/tgba/tgbabddcoredata.hh: Likewise.
	* src/tgba/dictunion.cc: Likewise.
	* src/tgba/tgba.hh: Likewise.

18
19
20
	* doc/Makefile.am (doc): Typo.
	* src/ltlvisit/tostring.hh (to_string): Add doxygen comments.
	* src/ltlast/multop.hh (multop::paircmp): Add doxygen comments.
21
22
	* src/tgba/tgbaexplicit.hh (tgba_explicit::transtion,
	state_explicit, tgba_explicit_succ_iterator): Add doxygen comments.
23
24
	* src/ltlvisit/postfix.hh: Typo.

25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
	* src/ltlast/Makefile.am (ltlastdir, ltlast_HEADERS): New variables.
	(libltlast_la_SOURCES): Move all headers to ltlast_HEADERS.
	* src/ltlenv/Makefile.am (ltlenvdir, ltlenv_HEADERS): New variables.
	(libltlenv_la_SOURCES): Move all headers to ltlenv_HEADERS.
	* src/ltlparse/Makefile.am (ltlparsedir, ltlparse_HEADERS): New
	variables.
	(libltlparse_la_SOURCES): Move all public headers to ltlparse_HEADERS.
	* src/ltlvisit/Makefile.am (ltlvisitdir, ltlvisit_HEADERS): New
	variables.
	(libltlvisit_la_SOURCES): Move all headers to ltlparse_HEADERS.
	* src/misc/Makefile.am (include_HEADERS): Rename as ..
	(misc_HEADERS): ... this.
	(miscdir): New variable.
	* src/tgba/Makefile.am (tgbadir, tgba_HEADERS): New variables.
	(libtgba_la_SOURCES): Move all headers to tgba_HEADERS.
	* src/tgbaalgos/Makefile.am (tgbaalgosdir, tgbaalgos_HEADERS):
	New variables.
	(libtgbaalgos_la_SOURCES): Move all headers to tgbaalgos_HEADERS.
	* src/tgbaparse/Makefile.am (tgbaparsedir, tgbaparse_HEADERS): New
	variables.
	(libtgbaparse_la_SOURCES): Move all public headers to
	tgbaparse_HEADERS.
	* src/tgbaparse/public.hh: Include ltlparse/location.hh, not
	location.hh.

50
51
	* doc/Makefile.am (stamp): Prefix $(srcdir) explicitely.

52
53
54
	* m4/buddy.m4 (BUDDY_LDFLAGS): Use $(top_builddir), not $(top_srcdir).
	* src/tgbaparse/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS).

55
56
57
58
59
60
	* doc/Makefile.am: Rewrite to run Doxygen whenever Doxyfile.in
	or configure.ac changes.  Distribute the html doc.
	* doc/Doxyfile.in (EXCLUDE_PATTERNS): Complete with
	useless Bison classes.
	(FILE_PATTERNS): Remove *.cc files.

61
	Distribute BuDDy.  Compile and link with the included version if
62
63
64
	explicitely requested (--with-included-buddy) or if there is now
	stuitable version already installed.

65
66
67
68
69
70
71
72
73
74
	* buddy/: New directory.  Contains a patched version of BuDDy 2.2.
	* m4/buddy.m4: Make sure the installed BuDDy supports bdd_mergepairs.
	Honor --with-included-buddy and --without-included-buddy.  Define
	the BUDDY_LDFLAGS and BUDDY_CPPFLAGS output variables, and the
	WITH_INCLUDED_BUDDY Automake conditional
	* Makefile.am [WITH_INCLUDED_BUDDY] (MAYBE_SUBDIRS): New variable.
	(SUBDIRS): Prepend $(MAYBE_SUBDIRS).
	* src/Makefile.am (libspot_LDFLAGS): New variable.
	* src/tgba/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS).
	* src/tgbaalgos/Makefile.am (AM_CPPFLAGS): Likewise.
75
	* src/tgbatest/Makefile.am (AM_CPPFLAGS): Likewise.
76

77
78
2003-06-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

79
80
81
82
83
84
85
86
	* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next):
	Rewrite using bdd_satoneset.  This time it's for real.  (I hope.)
	* src/tgba/succiterconcrete.hh (current_base_,
	current_base_left_): Delete.
	* tgba/tgbabddcoredata.hh (next_set): New variable.
	* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust
	to update next_set.

87
88
89
	* src/tgba/bddprint.hh, src/tgba/tgbabddconcretefactory.hh,
	src/tgba/tgbaproduct.hh: Fix Doxygen comments.

90
91
92
93
94
95
96
97
98
99
	* src/tgba/succiterconcrete.hh (next_succ_set_): Rename as ...
	(succ_set_left_): ... this.
	(current_base_, current_base_left_): New variables.
	* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::first):
	Reset current_.
	(tgba_succ_iterator_concrete::next): Rewrite.
	(tgba_succ_iterator_concrete::current_state): Simplify.
	(tgba_succ_iterator_concrete::current_accepting_conditions): Remove
	atomic proposition with universal quantification.
	* src/tgba/ltl2tgba.cc (ltl_to_tgba): Normalize the formula.
100
	* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state):
101
102
103
104
105
106
107
	Complete the initial state.
	(tgba_bdd_concrete::succ_iter): Do not remove Now variable
	from the BDD passed to the iterator.
	* tgba/tgbabddcoredata.hh (notnow_set, var_set): New variables.
	* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust
	to update notnow_set and var_set.

108
109
	* src/tgbatest/ltl2tgba.cc: Support -v.

110
111
2003-06-24  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

112
113
	* src/tgbatest/ltl2tgba.cc (syntax): Fix usage message.

114
115
116
	* src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort
	accepting conditions.

117
118
119
120
121
122
123
	* src/ltlvisit/nenoform.cc (negative_normal_form): New const variant.
	* src/ltlvisit/nenoform.hh (negative_normal_form): New const variant.
	* src/ltlvisit/lunabbrev.cc (unabbreviate_logic): New const variant.
	* src/ltlvisit/lunabbrev.hh (unabbreviate_logic): New const variant.
	* src/ltlvisit/tunabbrev.cc (unabbreviate_ltl): New const variant.
	* src/ltlvisit/tunabbrev.hh (unabbreviate_ltl): New const variant.

124
125
2003-06-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
126
127
128
129
130
	Switch from "promises" to "accepting sets".  Fix the definitions
	of these accepting sets so that they are really useful.  Provide
	an all_accepting_conditions() method for use in the emptyness
	check, and a neg_accepting_conditions() for products.  Predeclare
	TGBA accepting conditions in the i/o.
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199

	* src/tgba/bddprint.cc (want_prom): Rename as ...
	(want_prom): ... this.
	(print_handler): Adjust to display Acc[].
	(print_acc_handler, bdd_print_acc): New functions.
	* src/tgba/bddprint.hh (print_acc_handler, bdd_print_acc):
	New functions.
	* src/tgba/succiter.hh (current_promise): Rename as ...
	(current_accepting_conditions): ... this.
	* src/tgba/succiterconcrete.cc (current_state):
	Rename next to now.
	(current_promise): Rename as ...
	(current_accepting_conditions): ... this, and compute
	the accepting conditions.
	* src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc,
	src/tgba/succiterconcrete.hh,
	src/tgba/tgbabddconcretefactory.cc,
	src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
	src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
	src/tgba/tgbabddtranslatefactory.cc,
	src/tgbaalgos/dotty.cc: Adjust to new names.
	* src/tgba/tgba.hh (all_accepting_conditions,
	neg_accepting_conditions): New functions.
	* src/tgba/tgbabddconcretefactory.cc: Adjust to new
	names, and record accepting conditions instead of promises.
	* src/tgba/tgbabddcoredata.hh (accepting_conditions,
	all_accepting_conditions, negacc_set): New variables.
	(notnow_set, notprom_set, declare_promise): Rename as ...
	(notnext_set, notacc_set, declare_accepting_condition): ... these.
	* src/tgba/tgbaexplicit.hh
	(tgba_explicit_succ_iterator::current_promise): Rename as ...
	(tgba_explicit_succ_iterator::current_accepting_conditions): ... this.
	(tgba_explicit::add_promise): Rename as ...
	(tgba_explicit::add_accepting_condition): ... this.
	(tgba_explicit::declare_accepting_condition,
	tgba_explicit::has_accepting_condition): New variables.
	(tgba_explicit::get_promise): Rename as ...
	(tgba_explicit::get_accepting_condition): ... this.
	(tgba_explicit::all_accepting_conditions,
	tgba_explicit::neg_accepting_conditions): Implement them.
	(all_accepting_conditions, neg_accepting_conditions,
	all_accepting_conditions): New variables.
	(tgba_explicit_succ_iterator): Embed all_accepting_conditions_.
	* src/tgba/tgbaexplicit.cc: Likewise.
	* src/tgba/tgbaproduct.hh
	(tgba_product_succ_uterator): Embed left_neg_ and right_neg_.
	(tgba_product::all_accepting_conditions,
	tgba_product::neg_accepting_conditions): Implement them.
	* src/tgba/tgbatranslateproxy.hh:
	(tgba_translate_proxy::all_accepting_conditions,
	tgba_translate_proxy::neg_accepting_conditions): Implement them.
	* src/tgba/tgbatranslateproxy.cc: Likewise.
	* src/tgbaalgos/save.cc (save_rec): Call bdd_print
	(tgba_save_reachable): Output the `acc =' line.
	* src/tgbaparse/tgbaparse.yy: Support the for
	accepting conditions definitions using an "acc =" line
	at the start.  Later, use has_accepting_condition while
	parsing	accepting conditions to ensure they were declared.
	Disallow !cond in accepting conditions.
	* src/tgbaparse/tgbascan.ll (ACC_DEF): New token.
	* src/tgbatest/explicit.cc (main): Declare accepting conditions.
	* src/tgbatest/ltl2tgba.cc (main): Add support for the -a, -A,
	and -R new options.
	* src/tgbatest/tgbaread.cc (main): Really exit on parse error.
	* src/tgbatest/explicit.test, src/tgbatest/explprod.test,
	src/tgbatest/mixprod.test, src/tgbatest/readsave.test,
	src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Reflect
	recent changes.

200
201
202
203
204
2003-06-22  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgbatest/tripprod.test, src/tgbatest/explprod.test:
	Sort out some possible inversions in the output.

205
206
2003-06-19  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

207
208
	* src/tgba/tgbabddconcretefactory.cc
	(tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the
209
210
	formulae used as keys in prom_.
	(tgba_bdd_concrete_factory::create_promise): Delete.
211
	(tgba_bdd_concrete_factory::declare_promise,
212
	tgba_bdd_concrete_factory::finish): New functions.
213
	* src/tgba/tgbabddconcretefactory.hh
214
	(tgba_bdd_concrete_factory::create_promise): Delete.
215
	(tgba_bdd_concrete_factory::declare_promise,
216
217
218
219
220
221
222
	tgba_bdd_concrete_factory::finish): New functions.
	(tgba_bdd_concrete_factory::prom_): New map.
	* src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Adjust
	the Fx and aUb cases to register promises with
	tgba_bdd_concrete_factory::declare_promise().
	(ltl2tgba): Call tgba_bdd_concrete_factory::finish().

223
	* src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter):
224
	Revert the change from 2003-06-12, it needs more work (the
225
226
227
	automaton generated on Xa&(b U !a) was bogus, with that
	patch).

228
	* src/tgbatest/ltl2tgba.cc: Handle the -o and -r options.
229

230
231
232
233
	* src/tgbatest/tripprod.test, src/tgbatest/explprod.test,
	src/tgbatest/readsave.test: Adjust to reflect yesterday's
	bddprint.cc change.

234
235
236
237
238
239
240
241
242
243
244
2003-06-18  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/bddprint.cc (print_handler): Quote promises
	when !want_prom.
	* src/tgbaparse/tgbaparse.yy (prop_list): Accept strings or
	identifiers.  Discard empty strings.
	* src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: New file.
	* src/tgbatest/Makefile.am (check_PROGRAMS): Add mixprod.
	(mixprod_SOURCES): New variable.
	(TESTS): Add mixprod.test.

245
246
247
248
249
250
251
252
253
254
255
256
2003-06-17  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product):
	New constructor.
	* src/tgba/tgbaproduct.hh (state_bdd_product::state_bdd_product):
	New constructor.
	* tgbatest/tripprod.cc, tgbatest/tripprod.test: New files.
	* src/tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
	(tripprod_SOURCES): New variable.
	(CLEANFILES): Add input3.
	(TESTS): Add tripprod.test.

257
258
2003-06-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

259
260
261
262
263
264
265
266
267
268
269
270
271
272
	* src/tgba/tgbabddprod.cc, src/tgba/tgbabddprod.hh: Rename as ...
	* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: ... these.
	(tgba_bdd_product, tgba_bdd_product_succ_iterator): Rename as ...
	(tgba_product, tgba_product_succ_iterator): ... these, and adjust
	all uses.
	* src/tgba/tgbabddtranslateproxy.cc,
	src/tgba/tgbabddtranslateproxy.hh: Rename as ...
	* src/tgba/tgbatranslateproxy.cc,
	src/tgba/tgbatranslateproxy.hh: ... these.
	(tgba_bdd_translate_proxy, tgba_bdd_translate_proxy_succ_iterator):
	Rename as ...
	(tgba_translate_proxy, tgba_translate_proxy_succ_iterator): ... these,
	and adjust all uses.

273
	Make sure we can multiply two tgba_explicit.
274

275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
	* tgba/state.hh (state::translate, state::clone, state::as_bdd):
	New virtual methods.
	* tgba/stataebdd.cc (state::translate, state::clone): New methods.
	* tgba/stataebdd.hh (state::translate, state::clone): New methods.
	* tgba/tgbabddprod.cc (state_bdd_product::clone,
	tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator):
	New methods.
	(tgba_bdd_product_succ_iterator::first): Reset right_
	if any of left_ or right_ is already done (i.e., is empty).
	(tgba_bdd_product_succ_iterator::done): Return true
	if right_ is NULL.
	(tgba_bdd_product_succ_iterator::current_state,
	tgba_bdd_product::get_init_state): Work	directory with `state's.
	* tgba/tgbabddprod.hh (state_bdd_product::clone,
	tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator):
	New methods.
	* tgba/tgbabddtranslateproxy.cc
	(tgba_bdd_translate_proxy_succ_iterator::
	tgba_bdd_translate_proxy_succ_iterator): Work on any kind of iteraator.
	(tgba_bdd_translate_proxy_succ_iterator::
	~tgba_bdd_translate_proxy_succ_iterator): New method.
	(tgba_bdd_translate_proxy_succ_iterator::current_state,
	tgba_bdd_translate_proxy::get_init_state,
	tgba_bdd_translate_proxy::succ_iter): Work on `state's and
	`tgba_succ_iterator's directlry.
	(tgba_bdd_translate_proxy::format_state): Delegate formating
	to the proxied automata.
	* tgba/tgbaexplicit.cc (state_explicit::clone): New method.
	* src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition,
	tgba_explicit::get_promise): Call ltl::destroy on existing formulae.
305
	* tgbatest/explprod.cc, tgbatest/explprod.test: New files.
306
307
308
309
310
	* tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
	(explprod_SOURCES): New variable.
	(TESTS): Add explprod.test.
	(CLEANFILES): Add input1 and input2.

311
312
313
314
315
316
317
2003-06-12  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Make
	sure to compute the status of the most Now variables possible.
	This helps to identify equivalant states.
	(tgba_bdd_concrete): Call set_init_state.

318
319
320
321
322
2003-06-10  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Handle F and G.
	* src/tgbatest/ltl2tgba.test: Use F and G.

323
324
2003-06-06  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

325
326
327
328
329
330
	* src/tgbatest/bddprod.test: New file.
	* src/tgbatest/Makefile.am (check_PROGRAMS): Add bddprod.
	(bddprod_SOURCES, bddprod_CXXFLAGS): New variables.
	(TESTS): Add bddprod.test.
	* src/tgbatest/ltlprod.c: Handle BDD_CONCRETE_PRODUCT.

331
332
333
334
335
336
337
	* src/tgba/dictunion.cc (tgba_bdd_dict_union): Clone formulae
	while building new dictionary.
	* src/tgbatest/ltlprod.test, src/tgbatest/ltlprod.cc: New files.
	* src/tgbatest/Makefile.am (check_PROGRAMS): Add ltlprod.
	(ltlprod_SOURCES): New variable.
	(TESTS): Add ltlprod.test.

338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
	* src/ltlvisit/clone.cc (clone): New const version.
	* src/ltlvisit/clone.hh (clone): Likewise.
	* src/ltlvisit/destroy.cc (destroy): New const version.
	* src/ltlvisit/destroy.hh (destroy): Likewise.
	* src/tgba/tgbabddconcretefactory.cc
	(tgba_bdd_concrete_factory::create_state,
	tgba_bdd_concrete_factory::create_atomic_prop,
	tgba_bdd_concrete_factory::promise): Clone new formulae.
	* src/tgba/tgbabdddict.cc (tgba_bdd_dict::tgba_bdd_dict,
	tgba_bdd_dict::~tgba_bdd_dict, tgba_bdd_dict::operator=): New methods
	that clone and destroy formulae.
	* src/tgbatest/ltl2tgba.test, src/tgbatest/ltl2tgba.cc: New files.
	* src/tgbatest/Makefile.am (check_PROGRAMS): Add ltl2tgba.
	(ltl2tgba_SOURCES): New variable.
	(TESTS): Add ltl2tgba.test.

354
355
356
	* src/ltltest/equals.cc, src/ltltest/readltl.cc,
	src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include <cassert>.

357
358
2003-06-05  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

359
360
361
362
363
364
365
366
367
368
369
370
371
372
	* src/tgba/bddprint.cc (dict): Make this variable static.
	(want_prom): New global static variable.
	(print_handle): Honor want_prom.
	(print_sat_handler, bdd_print_sat, bdd_format_sat): New functions.
	(bdd_print_set, bdd_print_dot, bdd_print_table): Set want_prom.
	* src/tgba/bddprint.hh (bdd_print_sat, bdd_format_sat): New functions.
	* src/tgbaalgos/save.cc, src/tgbaalgos/save.hh,
	src/tgbatest/readsave.cc, src/tgbatest/readsave.test: New files.
	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add
	save.cc and save.hh.
	* src/tgbatest/Makefile.am (check_PROGRAMS): Add readsave.
	(readsave_SOURCES): New variable.
	(TESTS): Add readsave.test.

373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
	* configure.ac: Output src/tgbaparse/Makefile.
	* src/Makefile.am (SUBDIRS): Add tgbaparse.
	(libspot_la_LDADD): Add tgbaparse/libtgbaparse.la.
	* src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition,
	tgba_explicit::get_promise, tgba_explicit::add_neg_condition,
	tgba_explicit::add_neg_promise): New methods.
	* src/tgba/tgbaexplicit.hh: Declare them.
	* src/tgbaparse/Makefile.am, src/tgbaparse/fmterror.cc,
	src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh,
	src/tgbaparse/tgbaparse.yy, src/tgbaparse/tgbascan.ll,
	src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test: New files.
	* src/tgbatest/Makefile.am (check_PROGRAMS): Add tgbaread.
	(TESTS): Add tgbaread.cc.
	(CLEANFILES): Add input.
	(tgbaread_SOURCES): New variable.

389
390
	* src/ltlparse/ltlparse.yy: Typo in comment.

391
392
393
394
395
	* configure.ac: Output src/tgbatest/Makefile and src/tgbatest/defs.
	* src/Makefile.am (SUBDIRS): Add tgbatest.
	* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: New file.
	* src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgbaexplicit.cc
	and tgbaexplicit.hh.
396
	* src/tgbatest/Makefile.am, src/tgbatest/defs.in,
397
398
	src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files.

399
400
2003-06-04  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

401
402
	* src/ltlparse/ltlparse.yy (result): Suppress unused definition.

403
404
	* src/Makefile.am (SUBDIRS): Build `ltltest' after `.'.

405
406
407
408
	* src/ltlparse/ltlscan.ll: Use ltlyy as %prefix.
	* src/ltlparse/parsedecl.hh (YY_DECL): Rename yylex to ltlyylex.
	* src/ltlparse/ltlparse.yy: Define yylex as ltlyylex.

Alexandre Duret-Lutz's avatar
.    
Alexandre Duret-Lutz committed
409
2003-06-03  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
410
411
412
413
414
415

	* src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc,
	src/tgba/succiterconcrete.cc, src/tgba/tgbabddconcrete.cc,
	src/tgba/tgbabddprod.cc, src/tgba/tgbabddtranslatefactory.cc,
	src/tgba/tgbabddtranslateproxy.cc: Include <cassert>.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
416
417
418
419
420
421
422
2003-06-02  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/tgbabdddict.cc, src/tgba/tgbabdddict.hh: New files.
	* src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.
	* src/tgba/tgbabdddict.cc (tgba_bdd_dict::contains): New function.
	* src/tgba/tgbabdddict.hh (tgba_bdd_dict::contains): Likewise.

423
424
425
426
427
428
429
2003-05-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/statebdd.hh (state_bdd::as_bdd): Add non-const variant.
	* src/tgba/tgbabddtranslateproxy.cc,
	src/tgba/tgbabddtranslateproxy.hh: New files.
	* src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.

430
431
2003-05-27  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

432
433
434
435
436
437
438
439
	* src/tgba/bddprint.cc, src/tgba/bddprint.hh,
	src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh,
	src/tgba/tgbabddconcretefactory.hh,
	src/tgba/tgbabddconcreteproduct.cc,
	src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddfactory.hh,
	src/tgba/tgbabddtranslatefactory.hh, src/tgbaalgos/dotty.cc:
	Add Doxygen comments.

440
441
	* src/tgba/bddfactory.hh, src/tgba/statebdd.hh,
	src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh,
442
443
444
	src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add
	Doxygen comments.

445
446
447
448
449
	* src/tgba/bddprint.hh (bdd_format_set): New function.
	* src/tgba/bddprint.cc (bdd_format_set): Likewise.
	* src/tgba/state.hh: Add Doxygen comments.
	(state::compare): Take a state*, not a state&.
	(state_ptr_less_than): New functor.
450
	* src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a
451
452
453
454
455
456
457
458
459
460
461
462
	state&.
	* src/tgba/statebdd.cc (state_bdd::compare): Likewise.
	* src/tgba/succiter.hh: Add Doxygen comments.
	* src/tgba/tgba.hh: Mention promises.
	(tgba::formate_state): New pure virtual method.
	* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::formate_state):
	New method.
	* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::formate_state):
	Likewise.
	* src/tgbaalgos/dotty.cc: Adjust to use state_ptr_less_than
	and tgba::formate_state.

463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
	* src/tgba/succiter.hh (tgba_succ_iterator::current_state):
	Return a state*, not a state_bdd.
	* src/tgba/succiterconcrete.hh
	(tgba_succ_iterator_concrete::current_state): Return a state_bdd*,
	not a state_bdd.
	* src/tgba/tgba.hh: Add Doxygen comments.
	(tgba::succ_iter, tgba::get_init_state): Use state*, not state_bdd.
	* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::get_init_state):
	Return a state_bdd*, not a state_bdd.
	(tgba_bdd_concrete::get_init_bdd): New method.
	(tgba_bdd_concrete::succ_uter): Take a state* as argument.
	* src/tgba/tgbabddconcrete.cc: Likewise.
	* src/tgba/tgbabddtranslatefactory.cc
	(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
	tgba_bdd_concrete::get_init_bdd.
	* src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty): Adjust
	to use state* instead of state_bdd.
	* src/tgba/succlist.hh: Delete.  (Leftover from a previous
	draft.)

483
484
2003-05-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

485
486
487
488
	* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files.
	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.

	* src/tgba/tgbabddtranslatefactory.cc
489
490
	(tgba_bdd_translate_factory::compute_pairs): Be quiet.

491
492
493
494
495
	* src/Makefile.am (SUBDIRS): Add tgbaalgos.
	(libspot_la_LIBADD): Add tgba/libtgbaalgos.
	* src/tgbaalgos/Makefile.am: New file.
	* configure.ac: Output src/tgbaalgos/Makefile.

496
497
498
499
	* src/tgba/bddprint.hh, src/tgba/bddprint.cc: New files.
	* src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.
	* src/tgba/public.hh: Include bddprint.hh.

500
501
502
503
504
505
	* src/tgba/tgba.hh: Rename as ...
	* src/tgba/public.hh: .. this.
	* src/tgba/tgba.hh: New file.
	* src/tgba/Makefile.am (libtgba_la_SOURCES): Add public.hh.
	* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Inherit from tgba.
	(tgba_bdd_concrete::init_iter): Delete.
506
	(tgba_bdd_concrete::succ_iter): Take a state_bdd as argument,
507
508
509
	not a bdd.
	* src/tgba/tgbabddconcrete.cc: Likewise.

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
510
	Initial code for TGBA (Transition Generalized Bchi Automata).
511
512
513
514
515
	Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba,
	a LTL-to-TGBA translator using Couvreur's algorithm.

	* src/Makefile.am (SUBDIRS): Add tgba.
	(libspot_la_LIBADD): Add tgba/libtgba.la.
516
	* configure.ac: Output src/tgba/Makefile.
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
	* src/tgba/Makefile.am, src/tgba/bddfactory.cc,
	src/tgba/bddfactory.hh, src/tgba/dictunion.cc,
	src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh,
	src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh,
	src/tgba/succiter.hh, src/tgba/succiterconcrete.cc,
	src/tgba/succiterconcrete.hh, src/tgba/succlist.hh,
	src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc,
	src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc,
	src/tgba/tgbabddconcretefactory.hh,
	src/tgba/tgbabddconcreteproduct.cc,
	src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
	src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.cc,
	src/tgba/tgbabdddict.hh, src/tgba/tgbabddfactory.hh,
	src/tgba/tgbabddtranslatefactory.cc,
	src/tgba/tgbabddtranslatefactory.hh: New files.

533
534
535
536
537
538
539
2003-05-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* m4/gccwarn.m4: Do not use -Winline, this is inappropriate
	with STL.
	* src/ltlast/atomic_prop.cc, src/ltlvisit/lunabbrev.cc,
	src/ltlvisit/nenoform.cc: Include <cassert>.

540
541
2003-05-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

542
543
544
	* src/ltlvisit/dotty.cc: Rewrite to display formulae as
	graphs rather than trees, to show how nodes are shared.

545
546
547
548
549
550
551
	* src/ltlvisit/dump.hh (dump): Return the passed ostream.
	* src/ltlvisit/dump.cc (dump): Likewise.
	* src/ltlvisit/dotty.hh (dotty): Likewise.
	* src/ltlvisit/dotty.cc (dotty): Likewise.
	* src/ltlvisit/tostring.hh (to_string): Likewise.
	* src/ltlvisit/tostring.cc (to_string): Likewise.

552
553
554
555
556
557
558
	* src/ltlvisit/dump.hh (dump): Take a formula* as argument,
	not a formula&.  This is more homogeneous.
	* src/ltlvisit/dump.cc (dump): Likewise.
	* src/ltlvisit/dotty.hh (dotty): Likewise.
	* src/ltlvisit/dotty.cc (dotty): Likewise.
	* src/ltlvisit/tostring.hh (to_string): Likewise.
	* src/ltlvisit/tostring.cc (to_string): Likewise.
559
	* src/ltltest/readltl.cc, src/ltltest/equals.cc,
560
561
	src/ltltest/tostring.cc: Adjust usage.

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
562
563
564
	Check trivial multop equality at build time.  This makes the equal
	visitor useless, since two equals formulae will now share the same
	address.
565

566
567
568
569
570
571
572
573
574
575
576
577
578
	* src/ltlast/multop.hh (add_sorted): New function.
	(paircmp): New comparison functor.
	(map): Use paircmp, we want to compare the vectors' contents,
	not their addresses.
	* src/ltlast/multop.cc (add_sorted): New function.
	(add): Use it.
	* src/ltltest/equals.cc, src/ltltest/tostring.cc: Compare
	pointers instead of calling equal.
	* src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: Delete.
	* src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Remove
	equals.cc and equals.hh.
	* wrap/spot.i: Do not include equals.hh.

579
580
2003-05-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
581
	Implement spot::ltl::destroy() and exercise it.
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605

	* src/ltlast/atomic_prop.hh: Declare instance_count().
	* src/ltlast/binop.hh, src/ltlast/unop.hh, src/ltlast/multop.hh:
	Likewise.  Also, really inherit for ref_formula this time.
	* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
	src/ltlast/unop.cc, src/ltlast/multop.cc: On destruction, suppress
	the instance from the instance map.  Implement instance_count().
	* src/ltlast/formula.cc, src/ltlast/formula.hh,
	src/ltlast/ref_formula.cc, src/ltlast/ref_formula.hh: Add virtual
	destructors.
	* src/ltlparse/ltlparse.yy: Recover from binary operators with
	missing right hand operand (the point is just to destroy the
	the left hand operand).
	* src/ltltest/equals.cc, src/ltltest/readltl.cc,
	src/ltltest/tostring.cc: Destroy used formulae.  Make sure
	instance_count()s are null are the end.
	* src/ltltest/parseerr.test: Adjust expected result, now
	that the parser lnows about missing right hand operands.
	* src/ltlvisit/destroy.hh, src/ltlvisit/destroy.cc,
	src/ltlvisit/postfix.hh, src/ltlvisit/postfix.cc: New files.
	* src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Add them.
	* src/ltlvisit/lunabbrev.cc (Xor, Equiv): Clone formulae
	occurring twice in the rewritten expression.

606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
	Massage the AST so that identical sub-formula share the same
	reference-counted formula*.  One can't call constructors for AST
	items anymore, everything need to be acquired through instance()
	class methods.

	* src/ltlast/formula.cc, src/ltlast/refformula.cc,
	src/ltlast/refformula.hh: New files.
	* src/ltlast/Makefile.am (libltlast_la_SOURCES): Add them.
	* src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
	src/ltlast/unop.cc, src/ltlast/unop.hh,
	src/ltlast/binop.cc, src/ltlast/binop.hh: Make the constructor
	and destructor protected.  Define a static function `instance()'
	to get an instance with specific argument.  Use a map called
	`instances' to store all known instances.  Inherit from
	ref_formula.
	* src/ltlast/constant.hh, src/ltlast/constant.cc: Protect
	the constructor and destructor.  Provide the false_instance()
	and true_instance() functions instead.
	* src/formula.hh (ref, unref, ref_, unref_): New methods.
	* src/ltlast/multop.cc, src/ltlast/multop.hh: Protect
	the constructor, destructor, as well as the add() method.
	Provides the instance(), and add() class methods instead.
	Store children_ as a pointer.
	* src/ltlenv/defaultenv.cc (require): Adjust to
	call atomic_prop::instance.
	* src/ltlparse/ltlparse.yy: Adjust to call instance() functions
	instead of constructors.
	* src/ltltest/Makefile.am (LDADD): Tweak library ordering.
	* src/ltlvisit/clone.hh (clone_visitor): Inherit from visitor,
	not const_visitor, and adjust all prototypes appropriately.
	* src/ltlvisit/clone.cc (clone_visitor): Likewise.
	Call ref() or instance() methods instead of copy constructors.
	* src/ltlvisit/equals.cc: Simplify atomic_prop and constant
	cases.
	* src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc,
	src/ltlvisit/tunabbrev.hh, src/ltlvisit/tunabbrev.cc,
	src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: Use instance()
	methods instead of constructor.  Make these children of visitor, not
	const_visitor.
	* src/ltltest/readltl.c (main): Do not delete the formula.

647
648
649
	* src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to
	remove a warning with newer versions of Flex.

650
651
652
653
654
655
	* src/ltlparse/ltlparse.yy (error_list, parse_environment, result):
	CVS Bison now supports %parse-param for the C++ skeleton; pass these
	variables as arguments to the Parser::Parser constructor instead of
	using globals.
	(parse): Adjust Parser::Parser call.

656
657
658
659
660
661
662
663
664
2003-05-12  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/ltlvisit/tostring.cc: Reindent and strip out superfluous
	spot::ltl:: prefixes.
	(to_string(formula)): New function.
	* src/ltlvisit/tostring.hh (to_string(formula)): Likewise.
	* src/ltltest/tostring.cc: Use this new to_string function to
	simplify.

665
666
667
668
669
670
2003-05-05  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* m4/buddy.m4: New file.
	* Makefile.am (EXTRA_DIST): Add m4/buddy.m4.
	* configure.ac: Call AX_CHECK_BUDDY.

671
2003-04-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
672

673
674
	* src/ltlvisit/Makefile.am (lib_LTLIBRARIES): Rename as ...
	(noinst_LTLIBRARIES): ... this.
675
	* src/ltlenv/Makefile.am, src/ltlast/Makefile.am,
676
	src/ltlparse/Makefile.am: Likewise.
677
	* src/Makefile.am (lib_LTLIBRARIES, libspot_la_SOURCES,
678
679
680
	libspot_la_LIBADD): New variable.   Build a libspot.la library
	from all the sub-libraries.

681
682
683
684
685
686
	* m4/pypath.m4: New file.
	* Makefile.am (SUBDIRS): Add wrap.
	* wrap/Makefile.am: New file.
	* wrap/spot.i: New file.  Preliminary bindings for Python.
	* configure.ac: Call adl_CHECK_PYTHON and output wrap/Makefile.

687
2003-04-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
688

689
	* configure.ac: Call AC_PROG_LIBTOOL.
690
	* src/ltlast/Makefile.am, src/ltlenv/Makefile.am,
691
692
693
	src/ltlparse/Makefile.am, src/ltltest/Makefile.am,
	src/ltlvisit/Makefile.am: Adust to build libtool libraries.

694
695
696
	* src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here...
	* src/ltlenv/defaultenv.cc: ... but here.

697
698
699
	* src/ltltest/tostring.test: Simplify with set -e.  Move the
	description of the test ...
	* src/ltltest/tostring.cc: ... here, where it is actually coded.
700
701
	* src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test,
	src/ltltest/nenoform.test,  src/ltltest/tunenoform.test:
702
703
	Simplify with set -e.

704
	* configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make
705
	sure we always use paths relative to src/ in src/'s
706
707
	subdirectories.

708
2003-04-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
709
710
711
712
713

	* src/ltlparse/Makefile.am (CXXFLAGS): Turn on GCC warnings
	now that CVS Bison is fixed.
	* src/ltlparse/ltlscan.ll: Use yyunput to shut up a GCC warning.

714
715
716
717
718
719
720
2003-04-24  Rachid REBIHA  <rebiha@nyx>

	* src/ltltest/tostring.test: New file.
	* src/ltltest/tostring.cc: New files.
	* src/ltlvisit/tostring.hh: From ast to string New files.
	* src/ltlvisit/tostring.cc: From ast to string New files.

721
2003-04-18  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
722

723
724
725
	* src/ltlparse/Makefile.am (EXTRA_DIST): Distribute ltlparse.yy.
	* src/ltlast/Makefile.am (libltlast_a_SOURCES): Add visitor.hh.

726
727
728
729
730
731
732
	* src/ltlast/atomic_prop.hh, src/ltlast/binop.hh,
	src/ltlast/constant.hh, src/ltlast/formula.hh,
	src/ltlast/multop.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh,
	src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh,
	src/ltlparse/public.hh, src/ltlvisit/clone.hh,
	src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh,
	src/ltlvisit/equals.hh, src/ltlvisit/lunabbrev.hh,
733
	src/ltlvisit/nenoform.hh, src/ltlvisit/tunabbrev.hh: Add
734
	Doxygen comments.
735
	* src/visitor.hh: Do not use const_sel.  This clarifies
736
737
	the code and helps Doxygen.

738
739
740
	* configure.ac: Output doc/Doxyfile and doc/Makefile.
	* doc/Makefile.am, doc/Doxyfile.in: New files.
	* Makefile.am (SUBDIRS): Add doc.
741

742
	* src/ltlparse/ltlscan.ll: Recognize && and ||.
743
	* src/ltltest/parse.test, src/ltltest/parseerr.test,
744
745
	src/ltltest/equals.test: Use these operators..

746
2003-04-17  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
747

748
749
	* src/ltltest/readltl.cc, src/ltltest/equals.cc: Cosmetics.

750
751
752
753
754
755
756
757
	* src/ltlenv/environment.hh (require): Return a formula, not
	an atomic_prop.
	* src/ltlast/atomic_prop.hh (atomic_prop): New argument env.
	(environment_): New member.
	(env): New method.
	* src/ltlast/atomic_prop.cc (atomic_prop, env): Likewise.
	* src/ltlenv/defaultenv.cc (require): Pass *this as the
	environment argument to atomic_prop.
758
	* src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy
759
760
	the environment.
	* src/ltlvisit/nenoform.cc (visit(const atomic_prop*)): Likewise.
761

762
763
764
765
766
767
768
769
770
771
	* configure.ac: Output src/ltlenv/Makefile.
	* src/ltlenv/Makefile.am, src/ltlenv/defaultenv.cc,
	src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh: New files.
	* src/ltlparse/public.hh (parse): Take an environment as third
	argument.
	* src/ltlparse/ltlparse.yy (ATOMIC_PROP, parse): Require the
	atomic proposition via the environment.
	* src/ltltest/readltl.cc (main): Adjust the call to parse().
	* src/ltltest/Makefile.am (LDADD): Add ../ltlenv/libltlenv.a.

772
773
774
775
776
	* src/ltlvisit/clone.hh, src/ltlvisit/clone.cc: New files.
	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
	* src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Inherit
	from clone_visitor and remove all useless methods (now inherited).

777
778
779
780
781
782
	* src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: New files.
	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
	* src/ltltest/equals.cc (main) [NENOFORM]: Call negative_normal_form.
	* src/ltltest/nenoform.test, src/ltltest/tunenoform.test: New files.
	* src/ltltest/Makefile.am (check_PROGRAMS): Add nenoform and
	tunenoform.
783
	(nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES,
784
785
786
	tunenoform_CPPFLAGS): New variables.
	(TESTS): Add nenoform.test and tunenoform.test.

787
788
	* src/ltlvisit/lunabbrev.hh: Fix include guard.

789
2003-04-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
790

791
792
793
794
795
796
797
798
799
800
801
802
	* src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: New files.
	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
	* src/ltltest/tunabbrev.test: New file.
	* src/ltltest/lunabbrev.test: Fix comment.
	* src/ltltest/Makefile.am (TESTS): Add tunabbrev.test.
	(check_PROGRAMS): Add tunabbrev.
	(tunabbrev_SOURCES, tunabbrev_CPPFLAGS): New variables.
	* src/ltltest/equals.cc (main) [TUNABBREV]: Call unabbreviate_ltl.
	* src/ltlvisit/lunabbrev.hh (unabbreviate_logic_visitor::recurse):
	New virtual function.
	* src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::recurse):
	Likewise.
803
	(unabbreviate_logic_visitor::visit): Use it instead of calling
804
805
	unabbreviate_logic directly.

806
807
	* src/ltlvisit/lunabbrev.hh: Add missing include guard.

808
809
810
811
812
813
814
815
816
817
	* src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: New files.
	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
	* src/ltlast/multop.cc (multop::multop(type)): New constructor.
	* src/ltlast/multop.hh (multop::multop(type)): New constructor.
	* src/ltltest/lunabbrev.test: New file.
	* src/ltltest/Makefile.am (TESTS): Add lunabbrev.test.
	(check_PROGRAMS): Add lunabbrev.
	(lunabbrev_SOURCES, lunabbrev_CPPFLAGS): New variables.
	* src/ltltest/equals.cc (main) [LUNABBREV]: Call unabbreviate_logic.

818
819
820
	* src/ltltest/equals.test (check0, check1): Remove. Use check 0, and
	check 1 instead.

821
822
823
824
825
826
	* src/ltlast/formulae.hh: Rename as ...
	* src/ltlast/formula.hh: ... this.
	* src/ltlast/Makefile.am (libltlast_a_SOURCES): Adjust.
	* src/ltlast/formula.hh (formulae): Rename as ...
	(formula): ... this.
	Adjust all uses.
827

828
829
830
831
832
833
	* src/ltlparse/public.hh (format_parse_errors): New function.
	* src/ltlparse/fmterror.cc: New file.
	* src/ltlparse/Makefile.am (libltlparse_a_SOURCES): Add fmterror.cc.
	* src/ltltests/equals.cc, src/ltltests/readltl.cc: Simplify using
	format_parse_errors.

834
835
836
837
838
839
840
841
	* src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: New files.
	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add equals.hh
	and equals.cc.
	* src/ltltest/equals.cc, src/ltltest/equals.test: New files.
	* src/ltltest/Makefile.am (check_PROGRAMS): Add equals.
	(equals_SOURCES): New variable.
	(TESTS): Add equals.test.

842
	* src/ltlast/multop.cc (multop::multop): Use multop::add.
843
	(multop::add): If the formulae we add is itself a multop for the
844
845
846
	same operator, merge its children with ours.
	* src/ltltest/parseerr.test: Add two tests for multop merging.

847
2003-04-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
848

849
850
851
852
853
854
855
856
857
858
859
860
	* src/ltlast/formulae.hh (formulae::equals): Remove.
	* src/ltlast/unop.hh (unop::equals): Remove.
	* src/ltlast/unop.cc (unop::equals): Remove.
	* src/ltlast/binop.hh (binop::equals): Remove.
	* src/ltlast/binop.cc (binop::equals): Remove.
	* src/ltlast/multop.hh (multop::equals): Remove.
	* src/ltlast/multop.cc (multop::equals): Remove.
	* src/ltlast/atomic_prop.hh (atomic_prop::equals): Remove.
	* src/ltlast/atomic_prop.cc (atomic_prop::equals): Remove.
	* src/ltlast/constant.hh (constant::equals): Remove.
	* src/ltlast/constant.cc (constant::equals): Remove.

861
862
863
864
865
866
867
868
869
870
871
872
873
	* HACKING, Makefile.am, configure.ac, m4/gccwarn.m4,
	src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
	src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
	src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
	src/ltlast/constant.hh, src/ltlast/formulae.hh,
	src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/predecl.hh,
	src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/visitor.hh,
	src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy,
	src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
	src/ltlparse/public.hh, src/ltlvisit/Makefile.am,
	src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
	src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
	src/ltlvisit/rewrite.cc, src/ltlvisit/rewrite.hh,
874
875
	src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc,
	src/ltltest/parse.test, src/ltltest/parseerr.test,
876
	src/misc/Makefile.am, src/misc/const_sel.hh: New files.