ChangeLog 56.1 KB
Newer Older
1
2
2003-07-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

3
4
5
6
	* src/tgbaalgos/lbtt.cc (bdd_less_than): Move ...
	* src/misc/bddlt.hh: ... in this new file.
	* src/misc/Makefile.am (misc_HEADERS): Add bddlt.hh.

7
8
	* iface/gspn/dcswave.test: Comment state space sizes.

9
10
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh.
	(libtgbaalgos_la_SOURCES): Add reachiters.cc.
11
	* src/tgbaalgos/dotty.cc, src/tgbaalgos/save.cc: Rewrite using
12
13
14
15
	spot::tgba_reachable_iterator_breadth_first.
	* src/tgbatest/explicit.test, src/tgbatest/tgbaread.test,
	src/tgbatest/tripprod.test: Adjust expected output.

16
17
18
19
20
2003-07-24  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* configure.ac: Output iface/gspn/defs.
	* iface/gspn/Makefile.am (EXTRA_DIST): Add $(TESTS).
	(TESTS, check_SCRIPTS, distclean-local): New.
21
	* iface/gspn/dcswave.test, iface/gspn/simple.test,
22
23
24
25
	iface/gspn/defs.in: New files.
	* iface/gspn/dottygspn.cc (main): Take the list of properties
	of interest in argument.

26
27
2003-07-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

28
29
30
31
32
	* iface/gspn/examples/DCSwave/DCSWave.def,
	iface/gspn/examples/DCSwave/DCSWave.net
	iface/gspn/examples/DCSwave/DCSWave.tobs,
	iface/gspn/examples/simple/simple.def,
	iface/gspn/examples/simple/simple.net,
33
	iface/gspn/examples/simple/simple.tobs: New files, from
34
35
36
37
	Yann Thierry-Mieg.
	* iface/gspn/Makefile.am (EXTRA_DIST): New variables.

	* iface/gspn/gspn.cc (tgba_gspn_private_::tgba_gspn_private_):
38
39
	Rethrow caught expections.

40
41
42
43
44
45
46
47
48
49
50
51
2003-07-22  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* m4/gspnlib.m4: Check for libgspnRG.a and libgspnSRG.a.
	Define LIBGSPNRG_LDFLAGS and LIBGSPNSRG_LDFLAGS, not
	LIBGSPN_LDFLAGS.
	* iface/gspn/Makefile.am: Adjust, build dottygspn-rg and
	dottygspn-srg instead of dottygspn.
	* iface/gspn/gspn.cc (EVENT_TRUE): Undefine.
	(tgba_gspn_private_::~tgba_gspn_private_): Free all_indexes.
	* iface/gspn/dottygspn.cc (main): Destroy the automaton before
	its dictionnary.

52
53
2003-07-17  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
	Now succ_iter() can fetch extra information from
	the root of a product to reduce its number of successors.
	* src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgba.cc.
	* src/tgba/tgba.hh (tgba::succ_iter): Add the global_state and
	global_automaton arguments.
	(tgba::support_conditions, tgba::support_variables,
	tgba::compute_support_conditions, tgba::compute_support_variables):
	New functions.
	(tgba::last_support_conditions_input_,
	tgba::last_support_conditions_output_,
	tgba::last_support_variables_input_,
	tgba::last_support_variables_output_): New attributes.
	* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::succ_iter):
	Handle the two new arguments.
	(tgba_bdd_concrete::compute_support_conditions,
	tgba_bdd_concrete::compute_support_variables): Implement them.
	* src/tgba/tgbabddconcrete.hh: Adjust.
	* src/tgba/tgbaexplicit.cc (tgba_explicit::succ_iter):	Ignore
	the two new arguments.
	(tgba_explicit::compute_support_conditions,
	tgba_explicit::compute_support_variables): Implement them.
	* src/tgba/tgbaexplicit.hh: Adjust.
76
	* src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
	two new arguments.
	(tgba_product::compute_support_conditions,
	tgba_product::compute_support_variables): Implement them.
	* src/tgba/tgbaproduct.hh: Adjust.
	* iface/gspn/gspn.cc (tgba_gspn_private_::last_state_cond_input,
	tgba_gspn_private_::last_state_cond_output,
	(tgba_gspn_private_::tgba_gspn_private_): Set last_state_cond_input.
	(tgba_gspn_private_::~tgba_gspn_private_): Delete
	last_state_cond_input.
	(tgba_gspn_private_::state_conds): New function, eved out
	from tgba_gspn::succ_iter.
	(tgba_gspn::succ_iter): Use it.  Use the two new arguments.
	(tgba_gspn::compute_support_conditions,
	tgba_gspn::compute_support_variables): New functions.
	* iface/gspn/gspn.hh: Adjust.

	* iface/gspn/gspn.cc (EVENT_TRUE): Override temporarily.
94
95
	(tgba_gspn::succ_iter): Fix usage of cube.

96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
2003-07-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* m4/gspnlib.m4: New file.
	* configure.ac: Call AX_CHECK_GSPNLIB.
	* Makefile.am (EXTRA_DIST): Add m4/gspnlib.m4.
	* iface/gspn/Makefile.am (AM_CPPFLAGS): Add $(LIBGSPN_CPPFLAGS).
	(libspotgspn_la_LIBADD, check_PROGRAMS, dottygspn_SOURCES,
	dottygspn_LDADD): New variables.
	* iface/gspn/gspn.hh (gspn_interface): New class.
	(gspn_exeption): Take a string argument and adjust all callers.
	(operator<<): Define for gspn_exeption.
	* iface/gspn/gspn.cc (gspn_interface::gspn_interface,
	gspn_interface::~gspn_interface): New.
	* iface/gspn/gspnlib.h: Delete, it belongs to GSPN.
	* iface/gspn/dottygspn.cc: New file.

112
113
2003-07-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

114
115
116
	* m4/lbtt.m4 (AX_CHECK_LBTT): Set LBTT and LBTT_TRANSLATE
	when using an already installed lbtt.

117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
	Homogenize passing of automata as pointers, not references.
	Disallow copy for security.

	* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Disallow copy.
	* src/tgba/tgbaexplicit.hh (tgba_explicit): Likewise.
	* src/tgba/tgbaexplicit.cc (tgba_explicit::operator=,
	tgba_explicit::tgba_explicit(tgba_explicit)): Remove.
	* src/tgba/tgbabddconcreteproduct.cc
	(tgba_bdd_concrete_product_factory::tgba_bdd_concrete_product_factory,
	product): Take operand automata as pointers.
	* src/tgba/tgbabddconcreteproduct.hh (product): Likewise.
	* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh:
	(tgba_product): Disallow copy.
	(tgba_product::tgba_product): Take operand automata as pointers.
	* src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty_reachable):
	Take tgba arguments as pointer.
	* src/tgbaalgos/dotty.hh (dotty_reachable): Likewise.
	* src/tgbaalgos/lbtt.cc (fill_todo, lbtt_reachable): Likewise.
	* src/tgbaalgos/lbtt.hh (lbtt_reachable): Likewise.
	* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh (ltl_to_tgba):
	Likewise.
	* src/tgbaalgos/save.cc (save_rec, tgba_save_reachable): Likewise.
	* src/tgbaalgos/save.hh (save): Likewise.
	* src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
	src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
	src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc,
	src/tgbatest/spotlbtt.cc, src/tgbatest/tgbaread.cc,
	src/tgbatest/tripprod.cc: Likewise.

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
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
2003-07-14  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	Before this change, all automata would construct their own
	dictionaries (map of BDD variables to LTL formulae).  This was
	cumbersome, because to multiply two automata we had to build a
	common dictionary (the union of the two LTL formula spaces), and
	install wrappers to translate each automaton's BDD answers into
	the common dictionary.  This translation, that had to be repeated
	when several products were nested, was time consuming and was a
	hindrance for some optimizations.
	In the new scheme, all automata involved in a product must
	share the same dictionary.  An empty dictionary should be
	constructed by the user and passed to the automaton' constructors
	as necessary.
	This huge change removes most code than it adds.

	* src/Makefile.am (libspot_la_LIBADD): Add misc/libmisc.la.
	* src/misc/bddalloc.hh, src/misc/bddalloc.cc: New files.  These
	partly replace src/tgba/bddfactory.hh and src/tgba/bddfactory.cc.
	* src/misc/Makefile.am: Adjust to build bddalloc.hh and bddalloc.cc.
	* src/tgba/bddfactory.hh, src/tgba/bddfactory.cc,
	src/tgba/dictunion.hh, src/tgba/dictunion.cc,
	src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
	src/tgba/tgbabddtranslatefactory.hh,
	src/tgba/tgbabddtranslatefactory.cc,
	src/tgba/tgbatranslateproxy.hh, src/tgba/tgbatranslateproxy.cc:
	Delete.
	* src/tgba/bdddict.hh, src/tgba/bdddict.cc: New files.  These
	replaces tgbabdddict.hh and tgbabdddict.cc, and also part of
	bddfactory.hh and bddfactory.cc.
	* src/tgba/bddprint.cc, src/tgba/bddprint.hh: Adjust to
	use bdd_dict* instead of tgba_bdd_dict&.
	* src/tgba/succiterconcrete.cc (succ_iter_concrete::next()):
	Get next_to_now from the dictionary.
	* src/tgba/tgba.hh (tgba::get_dict): Return a bdd_dict*,
	not a const tgba_bdd_dict*.
	* src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh:
	Adjust to use the new dictionary, stored in data_.
	* src/tgba/tgbabddconcretefactory.cc,
	src/tgba/tgbabddconcretefactory.hh: Likewise.  Plus
	now_to_next_ is now also stored in the dictionary.
	* src/tgba/tgbabddconcreteproduct.cc: Likewise.  Now
	that both operand share the same product, there is not
	point in using tgba_bdd_translate_factory.
	* src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh:
	Store a bdd_dict (taken as constructor argument).
	(tgba_bdd_core_data::~tgba_bdd_core_data): Remove.
	(tgba_bdd_core_data::translate): Remove.
	(tgba_bdd_core_data::next_to_now): Remove (now in dict).
	(tgba_bdd_core_data::dict): New pointer.
	* src/tgba/tgbabddfactory.hh: (tgba_bdd_factory::get_dict): Remove.
	* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
	Adjust to use the new dictionary.
	* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Likewise.  Do
	not use tgba_bdd_dict_union and tgba_bdd_translate_proxy anymore.
	* src/tgbaalgos/lbtt.cc, src/tgbaalgos/save.cc: Adjust to
	use bdd_dict* instead of tgba_bdd_dict&.
	* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.cc: Likewise.
	(ltl_to_tgba): Take a dict argument.
	* src/tgbaparse/public.hh (tgba_parse): Take a dict argument.
	* src/tgbaparse/tgbaparse.yy (tgba_parse): Take a dict argument.
	* src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
	src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
	src/tgbatest/readsave.cc, src/tgbatest/spotlbtt.cc,
	src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Instantiate
	a dictionary, and pass it to the automata' constructors.
	* src/tgbatest/ltl2tgba.cc: Likewise, and remove the -o (defrag)
	option.
	* iface/gspn/gspn.hh (tgba_gspn::tgba_gspn): Take a bdd_dict argument.
	(tgba_gspn::get_dict): Adjust return type.
	* iface/gspn/gspn.cc: Do not use bdd_factory, adjust to
	use the new dictionary instead.

2003-07-13  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
220

221
222
	* configure.ac: Bump version to 0.0e.

223
224
225
	* configure.ac: Bump version to 0.0d.
	* NEWS, README: New files.

226
227
2003-07-12  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

228
229
	* m4/lbtt.m4: Run lbtt-translate, not lbtt.

230
231
	* iface/gspn/gspn.cc: Include cassert.

232
233
2003-07-10  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

234
	* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(multop)):
235
236
237
	Forward root_ to children of And.
	(ltl_trad_visitor::recurse): Take a root argument.

238
239
240
241
242
243
	* src/tgba/tgbabddconcretefactory.hh
	(tgba_bdd_concrete_factory::add_relation): Rename as ...
	(tgba_bdd_concrete_factory::constrain_relation): ... this.
	* src/tgba/tgbabddconcretefactory.cc, src/tgbaalgos/ltl2tgba.cc:
	Adjust.

244
245
246
247
248
249
250
251
252
253
254
	* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::G)): Do
	not create Now/Next variable when G is the root of the formula.
	(ltl_trad_visitor::ltl_trad_visitor): Take a root argument.
	(ltl_trad_visitor::recurse): Create a new visitor, do not copy
	the current one.
	(ltl_to_tgba): Build ltl_trad_visitor with root = true.

	* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::X)):
	Remove FIXME about handling X(a U b) and X(a R b) better, it's
	done naturally.

255
256
	* src/tgbatest/spotlbtt.test: Make 100 rounds.

257
258
259
260
261
	* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next):
	Fix so that !p.!Acc[g].Acc[f] + p.!Acc[g].Acc[f] + p.Acc[g].!Acc[f]
	is factored as !p.!Acc[g].Acc[f] + p.(!Acc[g].Acc[f] + Acc[g].!Acc[f]),
	not !Acc[g].Acc[f] + p.Acc[g].!Acc[f].

262
263
2003-07-09  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
	* lbtt/: New directory.  Contains a patched version of lbtt 1.0.1.
	* Makefile.am (MAYBE_LBTT): New variables.
	(SUBDIRS): Add $(MAYBE_LBTT).
	(EXTRA_DIST): Add m4/lbtt.m4.
	* configure.ac: Call AX_CHECK_LBTT.
	* m4/lbtt.m4: New file.
	* src/tgbatest/Makefile.am (check_PROGRAMS): Add spotlbtt.
	(spotlbtt_SOURCES): New variables.
	(TESTS): Add spotlbtt.test.
	(CLEANFILE): Add config.
	* src/tgbatest/defs.in (top_builddir, LBTT, LBTT_TRANSLATE): New
	substitutions.
	* src/tgbatest/spotlbtt.cc, src/tgbatest/spotlbtt.test: New files.

	* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next):
279
	Fix computation of states sharing the same accepting set.
280

281
282
283
284
285
286
287
	Make sure we only output one initial state in LBTT's output.
	* src/tgbaalgos/lbtt.cc (fill_todo): Add the 'first' argument
	to designate initial states.
	(lbtt_reachable): Adjust calls to fill_todo.  Handle the
	fake initial state accepting conditions specially.
	* src/tgbaalgos/lbtt.hh: Update comments.

288
289
290
	* src/tgbaalgos/lbtt.cc (lbtt_reachable): Do not end transitions
	guards with -1 in output.

291
292
2003-07-08  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

293
294
295
296
297
298
299
	* src/tgbatest/ltl2tgba.cc: Add option -t to output the LBTT automata.
	* src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh: New files.
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add lbtt.hh.
	(libtgbaalgos_la_SOURCES): Add lbtt.cc.
	* src/tgba/bddprint.cc (print_sat_handler): Put a space after "!".
	* src/tgbatest/readsave.test: Adjust spaces after "!".

300
301
	* src/ltlvisit/dump.cc: Strip useless spot::ltl:: prefixes.

302
303
2003-07-07  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

304
305
306
307
	First sketch of the GSPN wrapper objects.
	* iface/gspn/gspn.cc, iface/gspn/gspn.hh: New files.
	* iface/gspn/Makefile.am (libspotgspn_la_SOURCES): Add them.

308
309
	* src/tgba/succiter.hh (current_state, current_conditions
	current_accepting_conditions): Mark as const.
310
311
312
	* src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
	src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
	src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
313
314
315
	src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh:
	Likewise.

316
317
318
319
	* iface/gspn/gspnlib.h: Fit 80 columns.
	[__cplusplus]: Wrap everything under extern "C".

	* src/tgba/succiterconcrete.hh
320
	(tgba_succ_iterator_concrete::current_acc_): New attribute.
321
	* src/tgba/succiterconcrete.cc
322
	(tgba_succ_iterator_concrete::next): Set current_acc_.
323
	(tgba_succ_iterator_concrete::current_accepting_conditions):
324
325
	Simply return it.

326
327
328
329
330
	* configure.ac: Output iface/Makefile and iface/gspn/Makefile.
	* iface/Makefile.am, iface/gspn/Makefile.am: New files.
	* Makefile.am (SUBDIRS): Add iface.
	* iface/gspn/gspnlib.h: New file, from Yann and Souheib.

331
332
	* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::tgba_bdd_core_data,
	tgba_bdd_core_data::translate): Handle all_accepting_conditions.
333
	* src/tgba/tgbabddconcretefactory.cc
334
335
	(tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions.

336
337
338
339
340
2003-07-04  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit): Declare
	accepting conditions w.r.t. to Now variables, not Next.

341
342
2003-07-03  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

343
	* src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::first):
344
	Simplify, do not call next_non_false_() if either side is done.
345

346
347
348
349
350
351
352
353
354
355
356
357
358
359
	* src/tgba/succiter.hh (tgba_succ_iterator::current_condition):
	State that this is a boolean function.
	* src/tgba/succiterconcrete.hh
	(tgba_succ_iterator_concrete::trans_dest_,
	tgba_succ_iterator_concrete::trans_set_,
	tgba_succ_iterator_concrete::trans_set_left_,
	tgba_succ_iterator_concrete::neg_trans_set_): Remove.
	* src/tgba/succiterconcrete.cc
	(tgba_succ_iterator_concrete::tgba_succ_iterator_concrete,
	tgba_succ_iterator_concrete::first): Adjust to removed members.
	(tgba_succ_iterator_concrete::next): Simplify, transitions
	are no labelled by boolean functions, not only conjunctions.
	Suggested by Denis Poitrenaud.

360
361
2003-07-02  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

362
363
364
	* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New
	function.
	* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate):
365
	Likewise.
366
367
	* src/tgba/tgbabddtranslatefactory.cc
	(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
368
369
	tgba_bdd_core_data::translate.

370
371
372
373
374
375
376
	* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::nownext_set):
	New attribute.
	* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc:
	Handle nownext_set.
	* src/tgba/succiterconcrete.cc
	(tgba_succ_iterator_concrete::next): Use nownext_set to simplify.

377
378
379
380
381
382
383
384
385
386
387
388
389
390
	Rewrite tgba_succ_iterator_concrete::next for the fourth time
	(or is it the fifth?).

	* src/tgba/succiterconcrete.hh
	(tgba_succ_iterator_concrete::trans_dest_,
	tgba_succ_iterator_concrete::trans_set_,
	tgba_succ_iterator_concrete::trans_set_left_,
	tgba_succ_iterator_concrete::neg_trans_set_): New attributes.
	* src/tgba/succiterconcrete.cc
	(tgba_succ_iterator_concrete::tgba_succ_iterator_concrete): Initialize
	new members.
	(tgba_succ_iterator_concrete::first): Likewise.
	(tgba_succ_iterator_concrete::next): Rewrite.
	* tgba/tgbabddcoredata.hh (tgba_bdd_core_data::acc_set): New attribute.
391
	* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc:
392
393
	Handle acc_set.

394
395
396
397
398
399
2003-07-01  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/tgbabddtranslatefactory.cc
	(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Translate
	varandnext_set.

400
401
2003-06-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

402
403
	* src/tgbaparse/tgbaparse.yy (lines): Expect at last one line.

404
405
406
407
408
409
410
411
412
413
	* doc/Doxyfile.in (HAVE_DOT): Set to YES to output
	collaboration diagrams.
	* doc/mainpage.dox: Typo.

	* src/tgba/state.hh (state::as_bdd): Delete.
	* src/tgba/tgbaproduct.hh (state_bdd_product): Inherit from state,
	not state_bdd.
	(state_bdd_product::state_bdd_product): Adjust.
	* src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product):
	Adjust.
414

415
416
	* src/tgba/succiter.hh (tgba_bdd_succ_iterator::done):
	Mark as const.
417
	* src/tgba/succiterconcrete.cc
418
419
420
	(tgba_succ_iterator_concrete::done): Likewise.
	* src/tgba/succiterconcrete.hh
	(tgba_succ_iterator_concrete::done): Likewise.
421
	* src/tgba/tgbaexplicit.cc
422
423
424
425
426
427
428
429
430
431
432
	(tgba_explicit_succ_iterator::done): Likewise.
	* src/tgba/tgbaexplicit.hh
	(tgba_explicit_succ_iterator::done): Likewise.
	* src/tgba/tgbaproduct.cc
	(tgba_product_succ_iterator::done): Likewise.
	* src/tgba/tgbaproduct.hh
	(tgba_product_succ_iterator::done): Likewise.
	* src/tgba/tgbatranslateproxy.hh
	(tgba_translate_proxy_succ_iterator::done): Likewise.
	* src/tgba/tgbatranslateproxy.cc
	(tgba_translate_proxy_succ_iterator::done): Likewise.
433

434
435
436
437
438
	* src/tgba/succiterconcrete.cc
	(tgba_succ_iterator_concrete::next): Call bdd_satoneset
	on data_.varandnext_set.  The previous implementation
	was wrong for GFa.
	* src/tgba/tgbabddcoredata.hh: Declare varandnext_set.
439
	* src/tgba/tgbabddcoredata.cc: Handle varandnext_set.
440

441
442
443
444
	* doc/Doxygen.in: Enable LaTeX output.
	* doc/Makefile.am (spotref.pdf): New rule.
	(EXTRA_DIST): Add spotref.pdf.

445
	* src/tgba/tgbabddconcretefactory.cc:
446
447
448
449
	(tgba_bdd_concrete_factory::tgba_bdd_concrete_factory): New.
	(tgba_bdd_concrete_factory::create_state): Update now_to_next_.
	(tgba_bdd_concrete_factory::finish): Constraint Next variables
	in the relation.
450
	* src/tgba/tgbabddconcretefactory.hh
451
452
	(tgba_bdd_concrete_factory::now_to_next_): New variable.

453
454
455
456
457
458
459
460
461
462
463
464
2003-06-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	Fix errors reported by ICC.

	* src/tgba/state.hh (state_ptr_less_than::operator()): Make it const.
	* src/tgba/tgbaproduct.cc: Include string.hh.
	* src/ltlast/multop.hh (multop::add, multop::add_sorted): Do
	not use qualified names in declarations.
	* m4/gccwarn.m4 (CF_GXX_WARNINGS): Fix GXX test.
	* src/ltlenv/defaultenv.hh, src/ltlenv/defaultenv.cc,
	src/ltlenv/environment.hh: Add virtual destructors.

465
466
2003-06-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

467
468
	* Makefile.am (EXTRA_DIST): Add HACKING.

469
470
	* configure.ac: Bump version to 0.0c.

471
472
	* configure.ac: Bump version to 0.0b.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
473
474
	* INSTALL: New file.

475
476
477
478
	* src/tgba/ltl2tgba.hh, src/tgba/ltl2tgba.cc: Move ...
	* src/tgbaalgos/ltl2tgba.hh, src/tgbaalgos/ltl2tgba.cc: ... here.
	* src/tgba/Makefile.am, src/tgbaalgos/Makefile.am: Adjust.
	* src/tgba/public.hh: Do not include ltl2tgba.hh.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
479
480
	* src/tgbatests/explprod.cc, src/tgbatests/ltl2tgba.cc,
	src/tgbatests/ltlprod.cc, src/tgbatests/mixprod.cc,
481
482
	src/tgbatests/reach.cc, src/tgbatests/tripprod.cc: Adjust inclusions.

483
484
485
486
	* src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments.
	* src/ltlast/formula.hh: More Doxygen comments.
	* src/tgba/tgba.hh: Use <tt> in Doxygen comments.

487
488
489
490
	* doc/mainpage.dox: New file.
	* doc/Makefile.am (EXTRA_DIST): Add mainpage.dox.
	* doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox

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

498
499
500
	* doc/Makefile.am (doc): Typo.
	* src/ltlvisit/tostring.hh (to_string): Add doxygen comments.
	* src/ltlast/multop.hh (multop::paircmp): Add doxygen comments.
501
502
	* src/tgba/tgbaexplicit.hh (tgba_explicit::transtion,
	state_explicit, tgba_explicit_succ_iterator): Add doxygen comments.
503
504
	* src/ltlvisit/postfix.hh: Typo.

505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
	* 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.

530
531
	* doc/Makefile.am (stamp): Prefix $(srcdir) explicitely.

532
533
534
	* m4/buddy.m4 (BUDDY_LDFLAGS): Use $(top_builddir), not $(top_srcdir).
	* src/tgbaparse/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS).

535
536
537
538
539
540
	* 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.

541
	Distribute BuDDy.  Compile and link with the included version if
542
543
544
	explicitely requested (--with-included-buddy) or if there is now
	stuitable version already installed.

545
546
547
548
549
550
551
552
553
554
	* 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.
555
	* src/tgbatest/Makefile.am (AM_CPPFLAGS): Likewise.
556

557
558
2003-06-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

559
560
561
562
563
564
565
566
	* 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.

567
568
569
	* src/tgba/bddprint.hh, src/tgba/tgbabddconcretefactory.hh,
	src/tgba/tgbaproduct.hh: Fix Doxygen comments.

570
571
572
573
574
575
576
577
578
579
	* 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.
580
	* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state):
581
582
583
584
585
586
587
	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.

588
589
	* src/tgbatest/ltl2tgba.cc: Support -v.

590
591
2003-06-24  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

592
593
	* src/tgbatest/ltl2tgba.cc (syntax): Fix usage message.

594
595
596
	* src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort
	accepting conditions.

597
598
599
600
601
602
603
	* 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.

604
605
2003-06-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
606
607
608
609
610
	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.
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
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679

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

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

685
686
2003-06-19  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

687
688
	* src/tgba/tgbabddconcretefactory.cc
	(tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the
689
690
	formulae used as keys in prom_.
	(tgba_bdd_concrete_factory::create_promise): Delete.
691
	(tgba_bdd_concrete_factory::declare_promise,
692
	tgba_bdd_concrete_factory::finish): New functions.
693
	* src/tgba/tgbabddconcretefactory.hh
694
	(tgba_bdd_concrete_factory::create_promise): Delete.
695
	(tgba_bdd_concrete_factory::declare_promise,
696
697
698
699
700
701
702
	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().

703
	* src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter):
704
	Revert the change from 2003-06-12, it needs more work (the
705
706
707
	automaton generated on Xa&(b U !a) was bogus, with that
	patch).

708
	* src/tgbatest/ltl2tgba.cc: Handle the -o and -r options.
709

710
711
712
713
	* src/tgbatest/tripprod.test, src/tgbatest/explprod.test,
	src/tgbatest/readsave.test: Adjust to reflect yesterday's
	bddprint.cc change.

714
715
716
717
718
719
720
721
722
723
724
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.

725
726
727
728
729
730
731
732
733
734
735
736
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.

737
738
2003-06-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

739
740
741
742
743
744
745
746
747
748
749
750
751
752
	* 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.

753
	Make sure we can multiply two tgba_explicit.
754

755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
	* 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.
785
	* tgbatest/explprod.cc, tgbatest/explprod.test: New files.
786
787
788
789
790
	* tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
	(explprod_SOURCES): New variable.
	(TESTS): Add explprod.test.
	(CLEANFILES): Add input1 and input2.

791
792
793
794
795
796
797
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.

798
799
800
801
802
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.

803
804
2003-06-06  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

805
806
807
808
809
810
	* 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.

811
812
813
814
815
816
817
	* 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.

818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
	* 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.

834
835
836
	* src/ltltest/equals.cc, src/ltltest/readltl.cc,
	src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include <cassert>.

837
838
2003-06-05  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

839
840
841
842
843
844
845
846
847
848
849
850
851
852
	* 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.

853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
	* 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.

869
870
	* src/ltlparse/ltlparse.yy: Typo in comment.

871
872
873
874
875
	* 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.
876
	* src/tgbatest/Makefile.am, src/tgbatest/defs.in,
877
878
	src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files.

879
880
2003-06-04  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

881
882
	* src/ltlparse/ltlparse.yy (result): Suppress unused definition.

883
884
	* src/Makefile.am (SUBDIRS): Build `ltltest' after `.'.

885
886
887
888
	* 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
889
2003-06-03  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
890
891
892
893
894
895

	* 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
896
897
898
899
900
901
902
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.

903
904
905
906
907
908
909
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.

910
911
2003-05-27  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

912
913
914
915
916
917
918
919
	* 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.

920
921
	* src/tgba/bddfactory.hh, src/tgba/statebdd.hh,
	src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh,
922
923
924
	src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add
	Doxygen comments.

925
926
927
928
929
	* 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.
930
	* src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a
931
932
933
934
935
936
937
938
939
940
941
942
	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.

943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
	* 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.)

963
964
2003-05-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

965
966
967
968
	* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files.
	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.

	* src/tgba/tgbabddtranslatefactory.cc
969
970
	(tgba_bdd_translate_factory::compute_pairs): Be quiet.

971
972
973
974
975
	* src/Makefile.am (SUBDIRS): Add tgbaalgos.
	(libspot_la_LIBADD): Add tgba/libtgbaalgos.
	* src/tgbaalgos/Makefile.am: New file.
	* configure.ac: Output src/tgbaalgos/Makefile.

976
977
978
979
	* 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.

980
981
982
983
984
985
	* 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.
986
	(tgba_bdd_concrete::succ_iter): Take a state_bdd as argument,
987
988
989
	not a bdd.
	* src/tgba/tgbabddconcrete.cc: Likewise.

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
990
	Initial code for TGBA (Transition Generalized Bchi Automata).
991
992
993
994
995
	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.
996
	* configure.ac: Output src/tgba/Makefile.
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
	* 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.

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

1020
1021
2003-05-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1022
1023
1024
	* src/ltlvisit/dotty.cc: Rewrite to display formulae as
	graphs rather than trees, to show how nodes are shared.

1025
1026
1027
1028
1029
1030
1031
	* 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.

1032
1033
1034
1035
1036
1037
1038
	* 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.
1039
	* src/ltltest/readltl.cc, src/ltltest/equals.cc,
1040
1041
	src/ltltest/tostring.cc: Adjust usage.

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

1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
	* 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.

1059
1060
2003-05-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
1061
	Implement spot::ltl::destroy() and exercise it.
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085

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

1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
	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.

1127
1128
1129
	* src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to
	remove a warning with newer versions of Flex.

1130
1131
1132
1133
1134
1135
	* 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.

1136
1137
1138
1139
1140
1141
1142
1143
1144
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.

1145
1146
1147
1148
1149
1150
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.

1151
2003-04-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1152

1153
1154
	* src/ltlvisit/Makefile.am (lib_LTLIBRARIES): Rename as ...
	(noinst_LTLIBRARIES): ... this.
1155
	* src/ltlenv/Makefile.am, src/ltlast/Makefile.am,
1156
	src/ltlparse/Makefile.am: Likewise.
1157
	* src/Makefile.am (lib_LTLIBRARIES, libspot_la_SOURCES,
1158
1159
1160
	libspot_la_LIBADD): New variable.   Build a libspot.la library
	from all the sub-libraries.

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

1167
2003-04-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1168

1169
	* configure.ac: Call AC_PROG_LIBTOOL.
1170
	* src/ltlast/Makefile.am, src/ltlenv/Makefile.am,
1171
1172
1173
	src/ltlparse/Makefile.am, src/ltltest/Makefile.am,
	src/ltlvisit/Makefile.am: Adust to build libtool libraries.

1174
1175
1176
	* src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here...
	* src/ltlenv/defaultenv.cc: ... but here.

1177
1178
1179
	* src/ltltest/tostring.test: Simplify with set -e.  Move the
	description of the test ...
	* src/ltltest/tostring.cc: ... here, where it is actually coded.
1180
1181
	* src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test,
	src/ltltest/nenoform.test,  src/ltltest/tunenoform.test:
1182
1183
	Simplify with set -e.

1184
	* configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make
1185
	sure we always use paths relative to src/ in src/'s
1186
1187
	subdirectories.

1188
2003-04-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1189
1190
1191
1192
1193

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

1194
1195
1196
1197
1198
1199
1200
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.

1201
2003-04-18  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1202

1203
1204
1205
	* src/ltlparse/Makefile.am (EXTRA_DIST): Distribute ltlparse.yy.
	* src/ltlast/Makefile.am (libltlast_a_SOURCES): Add visitor.hh.

1206
1207
1208
1209
1210
1211
1212
	* 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,
1213
	src/ltlvisit/nenoform.hh, src/ltlvisit/tunabbrev.hh: Add
1214
	Doxygen comments.
1215
	* src/visitor.hh: Do not use const_sel.  This clarifies
1216
1217
	the code and helps Doxygen.

1218
1219
1220
	* configure.ac: Output doc/Doxyfile and doc/Makefile.
	* doc/Makefile.am, doc/Doxyfile.in: New files.
	* Makefile.am (SUBDIRS): Add doc.
1221

1222
	* src/ltlparse/ltlscan.ll: Recognize && and ||.
1223
	* src/ltltest/parse.test, src/ltltest/parseerr.test,
1224
1225
	src/ltltest/equals.test: Use these operators..

1226
2003-04-17  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1227

1228
1229
	* src/ltltest/readltl.cc, src/ltltest/equals.cc: Cosmetics.

1230
1231
1232
1233
1234
1235
1236
1237
	* 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.
1238
	* src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy
1239
1240
	the environment.
	* src/ltlvisit/nenoform.cc (visit(const atomic_prop*)): Likewise.
1241

1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
	* 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.

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

1257
1258
1259
1260
1261
1262
	* 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.
1263
	(nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES,
1264
1265
1266
	tunenoform_CPPFLAGS): New variables.
	(TESTS): Add nenoform.test and tunenoform.test.

1267
1268
	* src/ltlvisit/lunabbrev.hh: Fix include guard.

1269
2003-04-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1270

1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
	* 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.
1283
	(unabbreviate_logic_visitor::visit): Use it instead of calling
1284
1285
	unabbreviate_logic directly.

1286
1287
	* src/ltlvisit/lunabbrev.hh: Add missing include guard.

1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
	* 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.

1298
1299
1300
	* src/ltltest/equals.test (check0, check1): Remove. Use check 0, and
	check 1 instead.

1301
1302
1303
1304
1305
1306
	* 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.
1307

1308
1309
1310
1311
1312
1313
	* 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.

1314
1315
1316
1317
1318
1319
1320
1321
	* 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.

1322
	* src/ltlast/multop.cc (multop::multop): Use multop::add.
1323
	(multop::add): If the formulae we add is itself a multop for the
1324
1325
1326
	same operator, merge its children with ours.
	* src/ltltest/parseerr.test: Add two tests for multop merging.

1327
2003-04-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1328

1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
	* 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.

1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
	* 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,
1354
1355
	src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc,
	src/ltltest/parse.test, src/ltltest/parseerr.test,
1356
	src/misc/Makefile.am, src/misc/const_sel.hh: New files.