ChangeLog 60.4 KB
Newer Older
1
2
2003-08-01  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

3
4
5
6
7
8
9
10
11
12
13
14
15
16
	* src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: Merge the
	two unabbreviate_logic definitions (const and non-const) into a
	function that takes a const formula* and return a non-const
	formula*.  Since formula* is convertible to const formula*, and
	the const version of the function just called the non-onst one, it
	makes no sense to keep both.  Also, it confused Swig.
	* src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh: Likewise
	for negative_normal_form.
	* src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: Likewise
	for unabbreviate_ltl.
	* src/ltlvisit/clone.cc, src/ltlvisit/clone.hh: Likewise for clone.
	* src/ltlvisit/destroy.cc, src/ltlvisit/destroy.hh: Likewise
	for destroy.

17
	* configure.ac: Bump version to 0.0g.
18

19
	* configure.ac, NEWS: Bump version to 0.0f.
20

21
22
23
24
25
26
27
	* iface/gspn/simple.test, iface/gspn/dcswave.test,
	iface/gspn/dcswaveltl.test: Make sure the example directory
	is writable.
	* m4/lbtt.m4, m4/buddy.m4: Always configure buddy/ and lbtt/,
	regardless of the --with-included-buddy and --with-included-lbtt
	settings.

28
29
30
31
32
	* wrap/python/Makefile.am (python_PYTHON, _spot_la_SOURCES):
	Explicitely refer to spot_wrap.cxx and spot.py as
	$(srcdir)/spot_wrap.cxx and $(srcdir)/spot.py.
	(spot_wrap.cxx, spot.py):

33
34
35
	* wrap/python/Makefile.am (spot_wrap.cxx, spot.py): Lookup
	spot.i in $(srcdir).

36
37
2003-07-31  Alexandre Duret-Lutz  <adl@gnu.org>

38
39
40
41
42
43
44
45
46
47
	* configure.ac: Output wrap/python/tests/Makefile
	and wrap/python/tests/run.
	* wrap/python/Makefile.am (SUBDIRS): New variable.
	* wrap/python/spot.i: Include all formulae headers from ltlast/,
	as well as ltlvisit/destroy.hh.
	(spot::ltl::formula::__cmp__, spot::ltl::formula::__str__): New
	functions.
	* wrap/python/tests/Makefile.am, wrap/python/tests/ltlsimple.py,
	wrap/python/tests/run.in: New files.

48
49
50
	* wrap/python/ltihooks.py: New file.
	* wrap/python/Makefile.am (EXTRA_DIST): Add ltihooks.py.

51
52
	* wrap/Makefile.am, wrap/spot.i: Move ...
	* wrap/python/Makefile.am, wrap/python/spot.i: ... here.
53

54
55
56
	* wrap/Makefile.am: New file.
	* configure.ac: Output wrap/python/Makefile.

57
58
59
	* src/misc/const_sel.hh: Delete.
	* src/misc/Makefile.am (misc_HEADERS): Remove const_sel.hh.

60
61
62
63
	* src/tgbaalgos/magic.cc, src/tgbaalgos/reachiter.cc: Include cassert.
	* iface/Makefile.am (SUBDIRS): Recurse in gspn only if condition
	WITH_GSPN.

64
65
2003-07-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

66
67
68
	* iface/gspn/gspn.cc (tgba_gspn::format_state): Call gspn's
	print_state.

69
	* iface/gspn/dcswaveltl.test: Check for a false formula too.
70

71
	* iface/gspn/dcswaveltl.test, iface/gspn/ltlgspn.cc: New files.
72
73
74
75
76
77
78
79
	* iface/gspn/Makefile.am (TESTS): Add dcswaveltl.test.
	(ltlgspn_rg_LDADD, ltlgspn_srg_LDADD, ltlgspn_rg_SOURCES)
	(ltlgspn_srg_SOURCES): New variables.
	(check_PROGRAMS): Add ltlgspn-rg and ltlgspn-srg.

	* iface/gspn/Makefile.am (gspn_HEADERS, gspndir): Install
	gspn.hh.

80
81
82
83
84
85
86
87
88
	* src/tgba/tgba.hh, src/tgba/tgba.cc
	(tgba::project_state): New method.
	* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
	(tgba_product::project_state): New method.
	* src/tgba/tgbabta.hh, src/tgba/tgbabta.cc
	(tgba_bta_proxy::project_state): New method.
	* src/tgbaalgos/magic.cc (magic_search::print_result): Take
	a restrict argument.

89
90
2003-07-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

91
92
93
	* src/ltlparse/ltlscan.ll: Allow /\, \/, and xor, used in LBTT.
	* src/ltltest/parse.test: Test them.

94
95
96
97
	* src/tgbaalgos/lbtt.cc: Typos.

	* lbtt/: Upgrade to lbtt 1.0.2.

98
99
100
101
102
	* src/tgbatest/Makefile.am (check_PROGRAMS): Add tbalbtt.
	(tbalbtt_SOURCES, tbalbtt_CXXFLAGS): New variables.
	* src/tgbatest/spotlbtt.cc [TBA]: Build tba proxies conditionally.
	* src/tgbatest/spotlbtt.test: Include tbalbtt in the tests.

103
104
105
106
107
108
109
110
111
112
113
2003-07-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/tgbatba.hh, src/tgba/tgbatba.cc
	(tgba_tba_proxy::state_is_accepting): New method.
	* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc: New files.
	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES,
	tgbaalgos_HEADERS): Add them.
	* src/tgbatest/ltlmagic.cc, src/tgbatest/ltlmagic.test: New files.
	* src/tgbatest/Makefile.am (TESTS, ltlmagic_SOURCES,
	check_PROGRAMS): Add them.

114
115
2003-07-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

116
117
118
119
120
121
	* src/tgba/tgba.hh (tgba::~tgba): Make it public.
	* src/tgba/tgbatba.cc, src/tgba/tgbatba.hh: New files.
	* src/tgba/Makefile.am (tgba_HEADERS): Add tgbatba.hh.
	(libtgba_la_SOURCES): Add tgbatba.cc.
	* src/tgbatest/ltl2tgba.cc: Add option -D.

122
123
124
125
	* 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.

126
127
	* iface/gspn/dcswave.test: Comment state space sizes.

128
129
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh.
	(libtgbaalgos_la_SOURCES): Add reachiters.cc.
130
	* src/tgbaalgos/dotty.cc, src/tgbaalgos/save.cc: Rewrite using
131
132
133
134
	spot::tgba_reachable_iterator_breadth_first.
	* src/tgbatest/explicit.test, src/tgbatest/tgbaread.test,
	src/tgbatest/tripprod.test: Adjust expected output.

135
136
137
138
139
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.
140
	* iface/gspn/dcswave.test, iface/gspn/simple.test,
141
142
143
144
	iface/gspn/defs.in: New files.
	* iface/gspn/dottygspn.cc (main): Take the list of properties
	of interest in argument.

145
146
2003-07-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

147
148
149
150
151
	* 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,
152
	iface/gspn/examples/simple/simple.tobs: New files, from
153
154
155
156
	Yann Thierry-Mieg.
	* iface/gspn/Makefile.am (EXTRA_DIST): New variables.

	* iface/gspn/gspn.cc (tgba_gspn_private_::tgba_gspn_private_):
157
158
	Rethrow caught expections.

159
160
161
162
163
164
165
166
167
168
169
170
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.

171
172
2003-07-17  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
	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.
195
	* src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
	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.
213
214
	(tgba_gspn::succ_iter): Fix usage of cube.

215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
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.

231
232
2003-07-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

233
234
235
	* m4/lbtt.m4 (AX_CHECK_LBTT): Set LBTT and LBTT_TRANSLATE
	when using an already installed lbtt.

236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
	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.

265
266
267
268
269
270
271
272
273
274
275
276
277
278
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.
279
	This huge change removes more code than it adds.
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
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338

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

340
341
	* configure.ac: Bump version to 0.0e.

342
343
344
	* configure.ac: Bump version to 0.0d.
	* NEWS, README: New files.

345
346
2003-07-12  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

347
348
	* m4/lbtt.m4: Run lbtt-translate, not lbtt.

349
350
	* iface/gspn/gspn.cc: Include cassert.

351
352
2003-07-10  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

353
	* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(multop)):
354
355
356
	Forward root_ to children of And.
	(ltl_trad_visitor::recurse): Take a root argument.

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

363
364
365
366
367
368
369
370
371
372
373
	* 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.

374
375
	* src/tgbatest/spotlbtt.test: Make 100 rounds.

376
377
378
379
380
	* 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].

381
382
2003-07-09  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
	* 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):
398
	Fix computation of states sharing the same accepting set.
399

400
401
402
403
404
405
406
	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.

407
408
409
	* src/tgbaalgos/lbtt.cc (lbtt_reachable): Do not end transitions
	guards with -1 in output.

410
411
2003-07-08  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

412
413
414
415
416
417
418
	* 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 "!".

419
420
	* src/ltlvisit/dump.cc: Strip useless spot::ltl:: prefixes.

421
422
2003-07-07  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

423
424
425
426
	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.

427
428
	* src/tgba/succiter.hh (current_state, current_conditions
	current_accepting_conditions): Mark as const.
429
430
431
	* src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
	src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
	src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
432
433
434
	src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh:
	Likewise.

435
436
437
438
	* iface/gspn/gspnlib.h: Fit 80 columns.
	[__cplusplus]: Wrap everything under extern "C".

	* src/tgba/succiterconcrete.hh
439
	(tgba_succ_iterator_concrete::current_acc_): New attribute.
440
	* src/tgba/succiterconcrete.cc
441
	(tgba_succ_iterator_concrete::next): Set current_acc_.
442
	(tgba_succ_iterator_concrete::current_accepting_conditions):
443
444
	Simply return it.

445
446
447
448
449
	* 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.

450
451
	* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::tgba_bdd_core_data,
	tgba_bdd_core_data::translate): Handle all_accepting_conditions.
452
	* src/tgba/tgbabddconcretefactory.cc
453
454
	(tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions.

455
456
457
458
459
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.

460
461
2003-07-03  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

462
	* src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::first):
463
	Simplify, do not call next_non_false_() if either side is done.
464

465
466
467
468
469
470
471
472
473
474
475
476
477
478
	* 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.

479
480
2003-07-02  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

481
482
483
	* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New
	function.
	* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate):
484
	Likewise.
485
486
	* src/tgba/tgbabddtranslatefactory.cc
	(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
487
488
	tgba_bdd_core_data::translate.

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

496
497
498
499
500
501
502
503
504
505
506
507
508
509
	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.
510
	* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc:
511
512
	Handle acc_set.

513
514
515
516
517
518
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.

519
520
2003-06-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

521
522
	* src/tgbaparse/tgbaparse.yy (lines): Expect at last one line.

523
524
525
526
527
528
529
530
531
532
	* 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.
533

534
535
	* src/tgba/succiter.hh (tgba_bdd_succ_iterator::done):
	Mark as const.
536
	* src/tgba/succiterconcrete.cc
537
538
539
	(tgba_succ_iterator_concrete::done): Likewise.
	* src/tgba/succiterconcrete.hh
	(tgba_succ_iterator_concrete::done): Likewise.
540
	* src/tgba/tgbaexplicit.cc
541
542
543
544
545
546
547
548
549
550
551
	(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.
552

553
554
555
556
557
	* 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.
558
	* src/tgba/tgbabddcoredata.cc: Handle varandnext_set.
559

560
561
562
563
	* doc/Doxygen.in: Enable LaTeX output.
	* doc/Makefile.am (spotref.pdf): New rule.
	(EXTRA_DIST): Add spotref.pdf.

564
	* src/tgba/tgbabddconcretefactory.cc:
565
566
567
568
	(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.
569
	* src/tgba/tgbabddconcretefactory.hh
570
571
	(tgba_bdd_concrete_factory::now_to_next_): New variable.

572
573
574
575
576
577
578
579
580
581
582
583
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.

584
585
2003-06-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

586
587
	* Makefile.am (EXTRA_DIST): Add HACKING.

588
589
	* configure.ac: Bump version to 0.0c.

590
591
	* configure.ac: Bump version to 0.0b.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
592
593
	* INSTALL: New file.

594
595
596
597
	* 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
598
599
	* src/tgbatests/explprod.cc, src/tgbatests/ltl2tgba.cc,
	src/tgbatests/ltlprod.cc, src/tgbatests/mixprod.cc,
600
601
	src/tgbatests/reach.cc, src/tgbatests/tripprod.cc: Adjust inclusions.

602
603
604
605
	* src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments.
	* src/ltlast/formula.hh: More Doxygen comments.
	* src/tgba/tgba.hh: Use <tt> in Doxygen comments.

606
607
608
609
	* doc/mainpage.dox: New file.
	* doc/Makefile.am (EXTRA_DIST): Add mainpage.dox.
	* doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox

610
611
612
613
614
615
616
	* 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.

617
618
619
	* doc/Makefile.am (doc): Typo.
	* src/ltlvisit/tostring.hh (to_string): Add doxygen comments.
	* src/ltlast/multop.hh (multop::paircmp): Add doxygen comments.
620
621
	* src/tgba/tgbaexplicit.hh (tgba_explicit::transtion,
	state_explicit, tgba_explicit_succ_iterator): Add doxygen comments.
622
623
	* src/ltlvisit/postfix.hh: Typo.

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

649
650
	* doc/Makefile.am (stamp): Prefix $(srcdir) explicitely.

651
652
653
	* m4/buddy.m4 (BUDDY_LDFLAGS): Use $(top_builddir), not $(top_srcdir).
	* src/tgbaparse/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS).

654
655
656
657
658
659
	* 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.

660
	Distribute BuDDy.  Compile and link with the included version if
661
662
663
	explicitely requested (--with-included-buddy) or if there is now
	stuitable version already installed.

664
665
666
667
668
669
670
671
672
673
	* 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.
674
	* src/tgbatest/Makefile.am (AM_CPPFLAGS): Likewise.
675

676
677
2003-06-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

686
687
688
	* src/tgba/bddprint.hh, src/tgba/tgbabddconcretefactory.hh,
	src/tgba/tgbaproduct.hh: Fix Doxygen comments.

689
690
691
692
693
694
695
696
697
698
	* 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.
699
	* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state):
700
701
702
703
704
705
706
	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.

707
708
	* src/tgbatest/ltl2tgba.cc: Support -v.

709
710
2003-06-24  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

711
712
	* src/tgbatest/ltl2tgba.cc (syntax): Fix usage message.

713
714
715
	* src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort
	accepting conditions.

716
717
718
719
720
721
722
	* 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.

723
724
2003-06-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
725
726
727
728
729
	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.
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
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
785
786
787
788
789
790
791
792
793
794
795
796
797
798

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

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

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

806
807
	* src/tgba/tgbabddconcretefactory.cc
	(tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the
808
809
	formulae used as keys in prom_.
	(tgba_bdd_concrete_factory::create_promise): Delete.
810
	(tgba_bdd_concrete_factory::declare_promise,
811
	tgba_bdd_concrete_factory::finish): New functions.
812
	* src/tgba/tgbabddconcretefactory.hh
813
	(tgba_bdd_concrete_factory::create_promise): Delete.
814
	(tgba_bdd_concrete_factory::declare_promise,
815
816
817
818
819
820
821
	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().

822
	* src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter):
823
	Revert the change from 2003-06-12, it needs more work (the
824
825
826
	automaton generated on Xa&(b U !a) was bogus, with that
	patch).

827
	* src/tgbatest/ltl2tgba.cc: Handle the -o and -r options.
828

829
830
831
832
	* src/tgbatest/tripprod.test, src/tgbatest/explprod.test,
	src/tgbatest/readsave.test: Adjust to reflect yesterday's
	bddprint.cc change.

833
834
835
836
837
838
839
840
841
842
843
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.

844
845
846
847
848
849
850
851
852
853
854
855
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.

856
857
2003-06-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

858
859
860
861
862
863
864
865
866
867
868
869
870
871
	* 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.

872
	Make sure we can multiply two tgba_explicit.
873

874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
	* 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.
904
	* tgbatest/explprod.cc, tgbatest/explprod.test: New files.
905
906
907
908
909
	* tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
	(explprod_SOURCES): New variable.
	(TESTS): Add explprod.test.
	(CLEANFILES): Add input1 and input2.

910
911
912
913
914
915
916
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.

917
918
919
920
921
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.

922
923
2003-06-06  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

924
925
926
927
928
929
	* 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.

930
931
932
933
934
935
936
	* 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.

937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
	* 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.

953
954
955
	* src/ltltest/equals.cc, src/ltltest/readltl.cc,
	src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include <cassert>.

956
957
2003-06-05  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

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

988
989
	* src/ltlparse/ltlparse.yy: Typo in comment.

990
991
992
993
994
	* 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.
995
	* src/tgbatest/Makefile.am, src/tgbatest/defs.in,
996
997
	src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files.

998
999
2003-06-04  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1000
1001
	* src/ltlparse/ltlparse.yy (result): Suppress unused definition.

1002
1003
	* src/Makefile.am (SUBDIRS): Build `ltltest' after `.'.

1004
1005
1006
1007
	* 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
1008
2003-06-03  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
1009
1010
1011
1012
1013
1014

	* 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
1015
1016
1017
1018
1019
1020
1021
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.

1022
1023
1024
1025
1026
1027
1028
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.

1029
1030
2003-05-27  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1031
1032
1033
1034
1035
1036
1037
1038
	* 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.

1039
1040
	* src/tgba/bddfactory.hh, src/tgba/statebdd.hh,
	src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh,
1041
1042
1043
	src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add
	Doxygen comments.

1044
1045
1046
1047
1048
	* 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.
1049
	* src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
	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.

1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
	* 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.)

1082
1083
2003-05-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1084
1085
1086
1087
	* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files.
	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.

	* src/tgba/tgbabddtranslatefactory.cc
1088
1089
	(tgba_bdd_translate_factory::compute_pairs): Be quiet.

1090
1091
1092
1093
1094
	* src/Makefile.am (SUBDIRS): Add tgbaalgos.
	(libspot_la_LIBADD): Add tgba/libtgbaalgos.
	* src/tgbaalgos/Makefile.am: New file.
	* configure.ac: Output src/tgbaalgos/Makefile.

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

1099
1100
1101
1102
1103
1104
	* 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.
1105
	(tgba_bdd_concrete::succ_iter): Take a state_bdd as argument,
1106
1107
1108
	not a bdd.
	* src/tgba/tgbabddconcrete.cc: Likewise.

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
1109
	Initial code for TGBA (Transition Generalized Bchi Automata).
1110
1111
1112
1113
1114
	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.
1115
	* configure.ac: Output src/tgba/Makefile.
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
	* 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.

1132
1133
1134
1135
1136
1137
1138
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>.

1139
1140
2003-05-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1141
1142
1143
	* src/ltlvisit/dotty.cc: Rewrite to display formulae as
	graphs rather than trees, to show how nodes are shared.

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

1151
1152
1153
1154
1155
1156
1157
	* 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.
1158
	* src/ltltest/readltl.cc, src/ltltest/equals.cc,
1159
1160
	src/ltltest/tostring.cc: Adjust usage.

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

1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
	* 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.

1178
1179
2003-05-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
1180
	Implement spot::ltl::destroy() and exercise it.
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204

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

1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
	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.

1246
1247
1248
	* src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to
	remove a warning with newer versions of Flex.

1249
1250
1251
1252
1253
1254
	* 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.

1255
1256
1257
1258
1259
1260
1261
1262
1263
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.

1264
1265
1266
1267
1268
1269
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.

1270
2003-04-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1271

1272
1273
	* src/ltlvisit/Makefile.am (lib_LTLIBRARIES): Rename as ...
	(noinst_LTLIBRARIES): ... this.
1274
	* src/ltlenv/Makefile.am, src/ltlast/Makefile.am,
1275
	src/ltlparse/Makefile.am: Likewise.
1276
	* src/Makefile.am (lib_LTLIBRARIES, libspot_la_SOURCES,
1277
1278
1279
	libspot_la_LIBADD): New variable.   Build a libspot.la library
	from all the sub-libraries.

1280
1281
1282
1283
1284
1285
	* 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.

1286
2003-04-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1287

1288
	* configure.ac: Call AC_PROG_LIBTOOL.
1289
	* src/ltlast/Makefile.am, src/ltlenv/Makefile.am,
1290
1291
1292
	src/ltlparse/Makefile.am, src/ltltest/Makefile.am,
	src/ltlvisit/Makefile.am: Adust to build libtool libraries.

1293
1294
1295
	* src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here...
	* src/ltlenv/defaultenv.cc: ... but here.

1296
1297
1298
	* src/ltltest/tostring.test: Simplify with set -e.  Move the
	description of the test ...
	* src/ltltest/tostring.cc: ... here, where it is actually coded.
1299
1300
	* src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test,
	src/ltltest/nenoform.test,  src/ltltest/tunenoform.test:
1301
1302
	Simplify with set -e.

1303
	* configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make
1304
	sure we always use paths relative to src/ in src/'s
1305
1306
	subdirectories.

1307
2003-04-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1308
1309
1310
1311
1312

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

1313
1314
1315
1316
1317
1318
1319
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.

1320
2003-04-18  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1321

1322
1323
1324
	* src/ltlparse/Makefile.am (EXTRA_DIST): Distribute ltlparse.yy.
	* src/ltlast/Makefile.am (libltlast_a_SOURCES): Add visitor.hh.

1325
1326
1327
1328
1329
1330
1331
	* 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,
1332
	src/ltlvisit/nenoform.hh, src/ltlvisit/tunabbrev.hh: Add
1333
	Doxygen comments.
1334
	* src/visitor.hh: Do not use const_sel.  This clarifies
1335
1336
	the code and helps Doxygen.

1337
1338
1339
	* configure.ac: Output doc/Doxyfile and doc/Makefile.
	* doc/Makefile.am, doc/Doxyfile.in: New files.
	* Makefile.am (SUBDIRS): Add doc.
1340

1341
	* src/ltlparse/ltlscan.ll: Recognize && and ||.
1342
	* src/ltltest/parse.test, src/ltltest/parseerr.test,
1343
1344
	src/ltltest/equals.test: Use these operators..

1345
2003-04-17  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1346

1347
1348
	* src/ltltest/readltl.cc, src/ltltest/equals.cc: Cosmetics.

1349
1350
1351
1352
1353
1354
1355
1356
	* 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.
1357
	* src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy
1358
1359
	the environment.
	* src/ltlvisit/nenoform.cc (visit(const atomic_prop*)): Likewise.
1360

1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
	* 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.

1371
1372
1373
1374
1375
	* 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).

1376
1377
1378
1379
1380
1381
	* 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.
1382
	(nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES,
1383
1384
1385
	tunenoform_CPPFLAGS): New variables.
	(TESTS): Add nenoform.test and tunenoform.test.

1386
1387
	* src/ltlvisit/lunabbrev.hh: Fix include guard.

1388
2003-04-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1389

1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
	* 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.
1402
	(unabbreviate_logic_visitor::visit): Use it instead of calling
1403
1404
	unabbreviate_logic directly.

1405
1406
	* src/ltlvisit/lunabbrev.hh: Add missing include guard.

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

1417
1418
1419
	* src/ltltest/equals.test (check0, check1): Remove. Use check 0, and
	check 1 instead.

1420
1421
1422
1423
1424
1425
	* 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.
1426

1427
1428
1429
1430
1431
1432
	* 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.

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

1441
	* src/ltlast/multop.cc (multop::multop): Use multop::add.
1442
	(multop::add): If the formulae we add is itself a multop for the
1443
1444
1445
	same operator, merge its children with ours.
	* src/ltltest/parseerr.test: Add two tests for multop merging.

1446
2003-04-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1447

1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
	* 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.

1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
	* 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,
1473
1474
	src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc,
	src/ltltest/parse.test, src/ltltest/parseerr.test,
1475
	src/misc/Makefile.am, src/misc/const_sel.hh: New files.