ChangeLog 78.2 KB
Newer Older
1
2
2003-10-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>

3
4
5
	* src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_result):
	Indent output as in the magic search.

6
7
	* src/tgbatest/spotlbtt.test: Add notice about long run time.

8
9
10
11
12
13
14
15
16
17
	Merge emptinesscheckexplicit into ltl2tgba.
	* src/tgbatest/Makefile.am (check_PROGRAMS): Remove
	emptinesscheckexplicit.
	(emptinesscheckexplicit_SOURCES): Remove.
	(TESTS): Replace emptinesscheckexplicit.test by emptchke.test.
	* src/tgbatest/emptinesscheckexplicit.cc,
	src/tgbatest/emptinesscheckexplicit.test: Delete.
	* src/tgbatest/empchke.test: New file.
	* src/tgbatest/ltl2tgba.cc: Add support for -X.

18
19
20
21
22
23
24
25
26
27
28
29
30
	Merge emptiness-checks tests into ltl2tgba.
	* src/tgbatest/Makefile (check_PRORGRAMS): Remove
	emptinesscheck and ltlmagic.
	(emptinesscheck_SOURCES, ltlmagic_SOURCES): Remove.
	(TESTS): Replace emptinesscheck.test and ltlmagic.test by
	emptchk.test.
	* src/tgbatest/emptinesscheck.test, src/tgbatest/ltlmagic.test:
	Delete.
	* src/tgbatest/emptchk.test: New file.
	* src/tgbatest/emptinesscheck.cc, src/tgbatest/ltlmagic.cc:
	Delete.
	* src/tgbatest/ltl2tgba.cc: Add support for -e, -E, -m, -M, and -n.

31
32
33
34
35
	* src/tgbaalgos/emptinesscheck.cc
	(emptiness_check::tgba_emptiness_check): Do not print anything.
	(emptiness_check::counter_example): Assume that tgba_emptiness_check
	has already been called.

36
37
2003-10-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

38
39
40
41
	* src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc
	(emptiness_check::seq_counter, emptiness_check::periode): Rename as ...
	(emptiness_check::prefix, emptiness_check::period): ... these.

42
43
44
45
	* src/tgbaalgos/emptinesscheck.cc
	(emptiness_check::tgba_emptiness_check,
	emptiness_check::accepting_path): Simplify BDD operations.

46
47
48
49
50
	* src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh:
	Reindent.
	(emptiness_check::~emptiness_check, emptiness_check::emptiness_check):
	Remove, unused.

51
52
53
54
55
2003-10-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* iface/gspn/ltlgspn.cc (main): Allow invocations with
	only one atomic proposition.

56
57
58
59
60
2003-10-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

	* src/misc/bddalloc.cc (bdd_allocator::initialize): Augment
	bdd_init()'s arguments.

61
62
2003-10-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>

63
64
65
66
67
68
69
70
71
72
73
	* iface/gspn/ltlgspn.cc: Use command-line options to
	select algorithms, not #defines.
	* iface/gspn/Makefile.am (check_PROGRAMS): Remove eltlgspn-srg,
	efmgspn-srg, fmgspn-rg, and fmgspn-srg and their associated
	source variables.  These are all replaced by
	ltlgspn-rg and ltlgspn-srg.
	* iface/gspn/dcswavefm.test, iface/gspn/dcswaveltl.test,
	iface/gspn/dcswaveeltl.test, iface/gspn/udcsefm.test,
	iface/gspn/udcseltl.test, iface/gspn/udcsfm.test,
	iface/gspn/udcsltl.test: Adjust calls to ltlgspn-srg.

74
75
76
	* iface/gspn/Makefile.am (XFAIL_TESTS): Remove.

2003-10-06  Rachid REBIHA  <rebiha@src.lip6.fr>
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

	* iface/gspn/ltlgspn.cc: We call tgba_emptiness_check before
	counter_example. And we print the prefix and the periode of
	counter_example's result.
	* src/tgbatest/emptinesscheckexplicit.cc (main):
	We call tgba_emptiness_check before counter_example.
	* src/tgbatest/emptinesscheck.cc (main):
	We call tgba_emptiness_check before counter_example.
	* src/tgbaalgos/emptinesscheck.hh (spot):
	(spot::print_result): New methode to print the prefix and the
	periode of counter_example's result.
	* src/tgbaalgos/emptinesscheck.cc (spot): counter_example doesn't
	call tgba_emptiness_check. counter_example must be executed after
	calling tgba_emptiness_check.  Remove tgba_emptiness_check calls.
	(print_result): New methode to print the prefix and the
	periode of counter_example's result.  Remove most of all std::cout
	during execution of emptiness_check's methodes.

95
96
2003-10-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>

97
98
99
100
101
102
103
	* iface/gspn/udcsfm.test, iface/gspn/udcsefm.test: New files.
	* iface/gspn/Makefile.am (TESTS) Add them.
	(check_PROGRAMS): Add emgspn-srg.
	(efmgspn_srg_SOURCES, efmgspn_srg_LDADD, efmgspn_srg_CPPFLAGS): New
	variables.
	* iface/gspn/udcsltl.test, iface/gspn/udcseltl.test: Complete.

104
105
	* src/ltlparse/ltlscan.ll: Allow doubly quoted atomic propositions.

106
107
2003-10-01  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

108
109
110
111
112
	* iface/gspn/udcsltl.test, iface/gspn/udcseltl.test,
	iface/gspn/dcswaveltl.test, iface/gspn/dcswaveeltl.test,
	iface/gspn/dcswavefm.test: Do not accept $? = 0 when
	a failure is expected.

113
114
115
116
117
118
119
	* iface/gspn/udcsltl.test, iface/gspn/udcseltl.test: New files
	* iface/gspn/Makefile.am (TESTS): Add them.
	(XFAIL_TESTS): Add udcseltl.test.
	* iface/gspn/example/udcs/udcs.net, iface/gspn/example/udcs/udcs.def
	iface/gspn/example/udcs/udcs.tobs: New files.
	* iface/gspn/Makefile.am (EXTRA_DIST): Add them.

120
121
122
123
124
125
126
	* iface/gspn/Makefile.am (check_PROGRAMS): Add eltlgspn-srg.
	(eltlgspn_srg_SOURCES, eltlgspn_srg_LDADD, eltlgspn_srg_CPPFLAGS):
	New variables.
	(TESTS): Add dcswaveeltl.test.
	* iface/gspn/dcswaveeltl.test: New file.
	* iface/gspn/ltlgspn.cc [CEC]: Use emptiness_check.

127
128
129
130
131
	* m4/debug.m4, m4/devel.m4, m4/gccoptim.m4, m4/ndebug.m4: New files.
	* Makefile.am (EXTRA_DIST): Add them.
	* configure.ac: Call adl_ENABLE_DEVEL, adl_ENABLE_DEBUG, ad_GCC_OPTIM,
	and adl_NDEBUG.

132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
2003-09-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/state.hh (state_ptr_less_than, state_ptr_equal):
	Declare as std::binary_function.
	(state_ptr_hash): Declare as std::unary_function.
	* src/tgbaalgos/lbtt.cc (state_acc_pair_equal,
	state_acc_pair_hash): Likewise.
	* src/misc/bddlt.hh (bdd_less_than): Likewise.
	* src/misc/hash.hh (ptr_hash, string_hash): Likewise.

2003-09-25  Rachid REBIHA  <rebiha@src.lip6.fr>

	* src/tgbatest/emptinesscheckexplicit.test,
	src/tgbatest/emptinesscheckexplicit.cc
	src/tgbatest/emptinesscheck.test,
	src/tgbatest/emptinesscheck.cc,
	src/tgbaalgos/emptinesscheck.cc,
	src/tgbaalgos/emptinesscheck.hh: New files.
150

151
152
153
154
155
156
157
158
159
160
161
162
2003-09-22  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh: Rename as ...
	* src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.hh:
	... this, and rename ltl_to_tgba() as ltl_to_tgba_lacim as well.
	* iface/gspn/ltlgspn.cc, src/tgbatest/explprod.cc,
	src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlmagic.cc,
	src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
	src/tgbatest/tripprod.cc, wrap/python/spot.i,
	wrap/python/cgi/ltl2tgba.in, wrap/python/tests/interdep.py,
	wrap/python/tests/ltl2tgba.py: Adjust.

163
164
165
166
2003-09-11  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/state.hh: Include cassert.

167
168
2003-08-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
	* src/tgba/state.hh (state::hash): New method.
	(state_ptr_equal, state_ptr_hash): New functors.
	* src/tgba/statebdd.hh, src/tgba/statebdd.cc (state_bdd::hash):
	New method.
	* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
	(state_explicit::hash): New method.
	(ns_map, sn_map): Use Sgi::hash_map instead of std::map.
	* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
	(state_product::hash): New method.
	* src/tgba/tgbatba.cc (state_tba_proxy::hash): New method.
	* src/tgbaalgos/lbtt.cc (acp_seen, todo_set, seen_map): Redefine
	using Sgi::hash_map or Sgi::hash_set.
	(lbtt_reachable): Don't erase a key that is pointed to by an
	iterator.
	* src/tgbaalgos/reachiter.cc
	(tgba_reachable_iterator::~tgba_reachable_iterator): Likewise.
	* src/tgbaalgos/magic.cc (magic_search::~magic_search()): Likewise.
	* src/tgbaalgos/magic.hh (hash_type): Redefine using Sgi::hash_map.
	* src/tgbaalgos/reachiter.hh (seen_map): Redefine using Sgi::hash_map.
	* iface/gspn/gspn.cc (state_gspn::hash): New method.
	* src/misc/hash.hh (string_hash): New functor.

191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
	* src/tgba/tgbaexplicit.cc (tgba_explicit::all_accepting_conditions)
	Compute all_accepting_conditions_ from neg_accepting_conditions_,
	not by browsing the dictionary.  The dictionary also contains
	accepting conditions from other automata...  This bug was a
	consequence of the change from 2003-07-14.
	* src/tgbaalgos/save.cc (save_bfs::start()): Likewise, do not
	browse the dictionary to print accepting conditions.  Call
	->all_accepting_conditions() instead.
	* src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Typo
	from 2003-08-22 in the computation of all_accepting_conditions_.
	* src/tgbatest/explpro3.test: New file.
	* src/tgbatest/Makefile.am (TESTS): Add explpro3.test.
	* src/tgbatest/explprod.test, src/tgbatest/explpro2.test,
	 src/tgbatest/tripprod.test: Sort the output using Perl.

206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
2003-08-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	Rewrite all std::map<const formula*, ...> as
	Sgi::hash_map<const formula*, ...>.

	* src/misc/hash.hh: New file.
	* src/misc/Makefile.am (misc_HEADERS): Add it.
	* src/ltlvisit/dotty.cc (dotty_visitor::map): Use a hash_map instead
	of a map.
	* src/tgba/bdddict.hh (bdd_dict::fv_map, bdd_dict::vf_map,
	bdd_dict::ref_set, bdd_dict::var_map): Define as hash_map or
	hash_set.
	* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::fv_map,
	translate_dict::vf_map): Likewise.
	* src/tgba/tgbabddconcretefactory.hh
	(tgba_bdd_concrete_factory::acc_map_): Likewise.
	* src/tgba/tgbatba.hh, src/tgbaalgos/reachiter.hh: Include <map>.

224
225
226
227
228
2003-08-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/state.hh (state_ptr_less_than): Make sure left is
	non-null.  Suggested by Denis Poitreneaud.

229
230
231
232
233
2003-08-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* wrap/python/Makefile.am (MAINTAINERCLEANFILES): Add
	buddy_wrap.cxx and buddy.py.

234
235
2003-08-22  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

236
237
	* src/tgbaalgos/magic.cc (seen_with_magic, seen_without_magic): Remove.

238
239
240
	* wrap/python/cgi/ltl2tgba.in: Fix display of relations for
	tgba_bdd_concrete automata.

241
242
243
244
245
246
247
248
249
	Fix computation of product acceptance conditions, when the
	two operands share some acceptance conditions.
	* src/tgba/tgbaproduct.hh (tgba_product::left_acc_complement_,
	tgba_product::right_acc_complement_): New attribute.
	* src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Set them.
	(tgba_product::succ_iter): Use them.
	* src/tgba/explpro2.test: New file.
	* src/tgba/Makefile.am (TESTS): Add it.

250
251
2003-08-20  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

252
253
254
255
	* tgba/tgbaproduct.cc, tgba/tgbaproduct.hh:
	(state_bdd_product, tgba_product_succ_iterator): Rename as ...
	(state_product, tgba_succ_iterator_product): ... these.

256
257
258
259
260
261
262
263
	* iface/gspn/dcswavefm.test: New file.
	* iface/gspn/Makefile.am (check_PROGRAMS): Add fmgspn-rg and
	fmgspn-srg.
	(fmgspn_rg_SOURCES, fmgspn_rg_CPPFLAGS, fmgspn_rg_LDADD,
	fmgspn_srg_SOURCES, fmgspn_srg_CPPFLAGS, fmgspn_srg_LDADD):
	New variables.
	(TESTS): Add dcswavefm.test.

264
265
266
267
268
2003-08-19  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/ltlast/formula.hh: Make it clear that ref() and unref()
	deals with one node, not a entire formula.

269
270
2003-08-18  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

271
272
	* configure.ac: Bump version to 0.0i.

273
	* configure.ac, NEWS: Bump version to 0.0h.
274

275
276
	* wrap/python/cgi/Makefile.am (CLEANFILES): Clean ltl2tgba.py.

277
278
279
280
	* wrap/python/tests/ltl2tgba.test: Run $srcdir/ltl2tgba.py, not
	ltl2tgba.py.

2003-08-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
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

	This implements Couvreur's FM'99 ltl2tgba translation.
	* src/tgba/bdddict.cc (bdd_dict::is_registered): Split as ...
	(bdd_dict::is_registered_proposition, bdd_dict::is_registered_state,
	bdd_dict::is_registered_accepting_variable): ... these.
	* src/tgba/bdddict.hh: Likewise.
	* src/tgba/tgbaexplicit.cc (tgba_explicit::set_init_state): New method.
	(tgba_explicit::declare_accepting_condition): Arrange so that this
	function can be called during the construction of the automaton.
	(tgba_explicit::complement_all_accepting_conditions): New method.
	(tgba_explicit::has_accepting_condition): Adjust to call
	bdd_dict::is_registered_accepting_variable.
	* src/tgba/tgbaexplicit.hh (tgba_explicit::set_init_state,
	tgba_explicit::complement_all_accepting_conditions): New methods.
	* src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh:
	New files.
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
	libtgbaalgos_la_SOURCES): Add them.
	* src/tgbaalgos/ltl2tgba.hh: Add bibtex entry in comment.
	* src/tgbatest/Makefile.am (check_PROGRAMS): Remove spotlbtt
	and tbalbtt.
	(tbalbtt_SOURCES, tbalbtt_CXXFLAGS, spotlbtt_SOURCES): Remove.
	* src/tgbatest/spotlbtt.cc: Delete, superseded by "ltl2tgba -F -t".
	* src/tgbatest/ltl2tgba.cc: Implement the -f and -F options.
	* src/tgbatest/spotlbtt.test: Use "ltl2tgba -F -t" instead of
	"spotlbtt", "ltl2tgba -F -t -D" instead of "tbalbtt", and add
	also check the ltl2tgba_fm translator.
	* wrap/python/spot.i: Wrap ltl2tgba_fm.
	* wrap/python/cgi/ltl2tgba.in: Add radio buttons to select
	between ltl2tgba and ltl2tgba_fm.
	* wrap/python/tests/ltl2tgba.py: Add support for the -f option.
	* wrap/python/tests/ltl2tgba.test: Try the -f option.

	varnum can be augmented by other allocator.  Keep track
	of a local varnum (lvarnum) in each allocator.
	* src/misc/bddalloc.cc (bdd_allocator::bdd_allocator): Initialize
	lvarnum.
	(bdd_allocator::extvarnum): New method.
	(bdd_allocator::allocate_variables): Use lvarnum and extvarnum.
	* src/misc/bddalloc.hh (bdd_allocator::extvarnum): New mathod.
	(bdd_allocator::lvarnum): New variable.

323
324
325
326
327
2003-08-14  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/tgba/state.hh, src/tgba/statebdd.hh, src/tgba/statebdd.cc:
	Remove the translate() method.  Useless since 2003-07-14.

328
329
330
331
332
2003-08-11  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* wrap/python/Makefile.am (SUBDIRS): Build `.' first.
	* wrap/python/cgi/Makefile.am (ltl2tgba.py): Depend on Makefile.

333
334
2003-08-10  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
	Revamp the multop interface to allow some basic optimizations like
	not constructing a single-child multop.
	* src/ltlast/multop.hh (multop::instance(type)): Remove.
	(multop::instance(type, formula*, formula*)): Return a formula*.
	(multop::instance(type, vec*)): Make it public and return a formula*.
	(multop::add_sorted, multop::add):
	* src/ltlast/multop.cc (multop::instance(type, vec*)): Rewrite.
	(multop::instance(type)): Delete.
	(multop::instance(type, formula*, formula*)): Adjust.
	(multop::add_sorted, multop::add): Remove.
	* src/ltlvisit/clone.cc (clone_visitor::visit(multop*)) Adjust.
	* src/ltlvisit/nenoform.cc
	(negative_normal_form_visitor::::visit(multop*)) Adjust.
	* src/ltltest/equals.test: Make sure `a & a' and `a' are equals.
	* wrap/python/tests/ltlsimple.py: Adjust.

351
352
353
354
	* src/tgba/succiterconcrete.cc, src/tgba/tgbaexplicit.cc,
	src/tgba/tgbatba.cc, src/tgbaalgos/lbtt.cc: Use `-' instead of `& !'
	between two BDDs.  That's one less call to BuDDy.

355
356
357
	* src/tgbatest/tgbaread.test, src/tgbatest/explicit.test:
	Adjust expected output after 2003-08-07's change.

358
359
	* src/tgba/bdddict.hh: Typo in comments.

360
361
	* src/ltlenv/environment.hh: Typo in comments.

362
363
364
365
366
367
2003-08-08  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

	* src/ltlparse/ltlparse.yy: Handle and diagnose mismatched parentheses.
	* src/ltltest/parseerr.test: Add some examples.

2003-08-07  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
368
369
370
371
372
373

	* wrap/python/cgi/ltl2tgba.in: Convert GIFs to PNGs.  Restrict
	the size of dot's output to 1024x1024.
	* src/tgbaalgos/dotty.cc (dotty_bfs::start): Do not preset
	the size of the graph.  Set height=0 for the invisible state.

374
2003-08-06  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
375

376
377
378
379
380
381
	* src/ltlparse/ltlparse.yy: Fix precedence OP_OR < OP_XOR < OP_AND.
	* src/ltlast/binop.cc (binop::instance): Order operands for
	associative operators, so that e.g. "a xor b" and "b xor a" are
	mapped to the same formula.
	* src/ltltest/equals.test: Check this.

382
	* src/ltlvisit/dotty.cc (draw_node_): s/shabe/shape/.
383
	(visit): Draw rectangular nodes for atomic propositions and
384
385
	constant.  This is an attempt to mimic BuDDy's output.

386
387
388
	* wrap/python/cgi/ltl2tgba.in: Handle show_formula_dot and
	show_formula_gif.

389
390
391
392
393
	* src/ltlvisit/dotty.hh (dotty): Move the ostream argument first.
	* src/ltlvisit/dump.hh (dump): Likewise.
	* src/ltltest/equals.cc, src/ltltest/readltl.cc,
	src/ltlvisit/dotty.cc, src/ltlvisit/dump.cc: Adjust.

394
395
2003-08-05  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

396
397
398
399
400
	* src/misc/version.hh, src/misc/version.cc: New files.
	* src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them.
	* wrap/python/spot.i: Include misc/version.hh.
	* wrap/python/cgi/ltl2tgba.in: Print spot.version().

401
402
	* README: Update layout.

403
404
405
406
407
	* wrap/python/cgi/Makefile.am, wrap/python/cgi/ltl2tgba.in,
	wrap/python/cgi/README: New files.
	* wrap/python/Makefile.am (SUBDIRS): Add cgi.
	* configure.ac: Output wrap/python/cgi/Makefile.

408
409
	* wrap/python/spot.i: Add an ostringstream emulation.

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

412
413
	* wrap/python/spot.i: Add an ofstream emulation.

414
415
416
417
	* wrap/python/spot.i: Declare spot::tgba::get_init_state,
	spot::tgba::succ_iter, and spot::tgba_succ_iterator::current_state
	as constructors.

418
419
420
421
422
423
424
425
426
427
428
	* wrap/python/Makefile.am (lib_LTLIBRARIES)
	(libspotswigpy_la_SOURCES, libspotswigpy_la_CFLAGS)
	(libspotswigpy_la_LDFLAGS): New variables.
	(_spot_la_LIBADD, _buddy_la_LDFLAGS): Link with libspotswigpy.la
	($(srcdir)/spot_wrap.cxx, $(srcdir)/buddy_wrap.cxx): Run
	swig with -c.
	* wrap/python/tests/libpy.c: New file.
	* wrap/python/tests/run.in: Run python if no arguments are given.
	* wrap/python/tests/interdep.py: New file.
	* wrap/python/tests/Makefile.am (TESTS): Add interdep.py.

429
430
431
	* wrap/python/spot.i: Declare spot::ltl_to_tgba as a constructor.
	* wrap/python/tests/ltl2tgba.py: Do not force `thisown=1' on tgba
	objects.
432

433
434
435
	* wrap/python/spot.i: Include headers from tgba/ and tgbaalgos/.
	* wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test:
	New files.
436

437
438
439
440
	* wrap/python/tests/Makefile.am (TESTS): Add ltl2tgba.test.
	(EXTRA_DIST): Add ltl2tgba.py.
	* wrap/python/tests/run.in: Distinguish *.py and *.test.

441
442
443
	* wrap/python/tests/ltlparse.py: New file.
	* wrap/python/tests/Makefile.am (TESTS): Add it.

444
445
2003-08-01  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

446
447
448
449
	* wrap/python/buddy.i: New file.
	* wrap/python/Makefile.am (EXTRA_DIST): Add it.
	(python_PYTHON, MAINTAINERCLEANFILES): Add buddy.py.
	(pyexec_LTLIBRARIES): Add _buddy.la.
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
450
	(_buddy_la_SOURCES, _buddy_la_LDFLAGS, $(srcdir)/buddy_wrap.cxx)
451
452
453
454
	($(srcdir)/buddy.py): New.
	* wrap/python/tests/bddnqueen.py: New file.
	* wrap/python/tests/Makefile.am (TESTS): Add it.

455
456
457
458
459
460
461
462
463
464
465
466
467
468
	* 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.

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

471
	* configure.ac, NEWS: Bump version to 0.0f.
472

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

480
481
482
483
484
	* 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):

485
486
487
	* wrap/python/Makefile.am (spot_wrap.cxx, spot.py): Lookup
	spot.i in $(srcdir).

488
489
2003-07-31  Alexandre Duret-Lutz  <adl@gnu.org>

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

500
501
502
	* wrap/python/ltihooks.py: New file.
	* wrap/python/Makefile.am (EXTRA_DIST): Add ltihooks.py.

503
504
	* wrap/Makefile.am, wrap/spot.i: Move ...
	* wrap/python/Makefile.am, wrap/python/spot.i: ... here.
505

506
507
508
	* wrap/Makefile.am: New file.
	* configure.ac: Output wrap/python/Makefile.

509
510
511
	* src/misc/const_sel.hh: Delete.
	* src/misc/Makefile.am (misc_HEADERS): Remove const_sel.hh.

512
513
514
515
	* src/tgbaalgos/magic.cc, src/tgbaalgos/reachiter.cc: Include cassert.
	* iface/Makefile.am (SUBDIRS): Recurse in gspn only if condition
	WITH_GSPN.

516
517
2003-07-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

518
519
520
	* iface/gspn/gspn.cc (tgba_gspn::format_state): Call gspn's
	print_state.

521
	* iface/gspn/dcswaveltl.test: Check for a false formula too.
522

523
	* iface/gspn/dcswaveltl.test, iface/gspn/ltlgspn.cc: New files.
524
525
526
527
528
529
530
531
	* 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.

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

541
542
2003-07-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

543
544
545
	* src/ltlparse/ltlscan.ll: Allow /\, \/, and xor, used in LBTT.
	* src/ltltest/parse.test: Test them.

546
547
548
549
	* src/tgbaalgos/lbtt.cc: Typos.

	* lbtt/: Upgrade to lbtt 1.0.2.

550
551
552
553
554
	* 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.

555
556
557
558
559
560
561
562
563
564
565
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.

566
567
2003-07-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

568
569
570
571
572
573
	* 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.

574
575
576
577
	* 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.

578
579
	* iface/gspn/dcswave.test: Comment state space sizes.

580
581
	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh.
	(libtgbaalgos_la_SOURCES): Add reachiters.cc.
582
	* src/tgbaalgos/dotty.cc, src/tgbaalgos/save.cc: Rewrite using
583
584
585
586
	spot::tgba_reachable_iterator_breadth_first.
	* src/tgbatest/explicit.test, src/tgbatest/tgbaread.test,
	src/tgbatest/tripprod.test: Adjust expected output.

587
588
589
590
591
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.
592
	* iface/gspn/dcswave.test, iface/gspn/simple.test,
593
594
595
596
	iface/gspn/defs.in: New files.
	* iface/gspn/dottygspn.cc (main): Take the list of properties
	of interest in argument.

597
598
2003-07-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

599
600
601
602
603
	* 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,
604
	iface/gspn/examples/simple/simple.tobs: New files, from
605
606
607
608
	Yann Thierry-Mieg.
	* iface/gspn/Makefile.am (EXTRA_DIST): New variables.

	* iface/gspn/gspn.cc (tgba_gspn_private_::tgba_gspn_private_):
609
610
	Rethrow caught expections.

611
612
613
614
615
616
617
618
619
620
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
621
	its dictionary.
622

623
624
2003-07-17  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
	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.
647
	* src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
	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.
665
666
	(tgba_gspn::succ_iter): Fix usage of cube.

667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
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.

683
684
2003-07-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

685
686
687
	* m4/lbtt.m4 (AX_CHECK_LBTT): Set LBTT and LBTT_TRANSLATE
	when using an already installed lbtt.

688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
	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.

717
718
719
720
721
722
723
724
725
726
727
728
729
730
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.
731
	This huge change removes more code than it adds.
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

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

792
793
	* configure.ac: Bump version to 0.0e.

794
795
796
	* configure.ac: Bump version to 0.0d.
	* NEWS, README: New files.

797
798
2003-07-12  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

799
800
	* m4/lbtt.m4: Run lbtt-translate, not lbtt.

801
802
	* iface/gspn/gspn.cc: Include cassert.

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

805
	* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(multop)):
806
807
808
	Forward root_ to children of And.
	(ltl_trad_visitor::recurse): Take a root argument.

809
810
811
812
813
814
	* 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.

815
816
817
818
819
820
821
822
823
824
825
	* 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.

826
827
	* src/tgbatest/spotlbtt.test: Make 100 rounds.

828
829
830
831
832
	* 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].

833
834
2003-07-09  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
	* 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):
850
	Fix computation of states sharing the same accepting set.
851

852
853
854
855
856
857
858
	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.

859
860
861
	* src/tgbaalgos/lbtt.cc (lbtt_reachable): Do not end transitions
	guards with -1 in output.

862
863
2003-07-08  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

864
865
866
867
868
869
870
	* 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 "!".

871
872
	* src/ltlvisit/dump.cc: Strip useless spot::ltl:: prefixes.

873
874
2003-07-07  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

875
876
877
878
	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.

879
880
	* src/tgba/succiter.hh (current_state, current_conditions
	current_accepting_conditions): Mark as const.
881
882
883
	* src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
	src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
	src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
884
885
886
	src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh:
	Likewise.

887
888
889
890
	* iface/gspn/gspnlib.h: Fit 80 columns.
	[__cplusplus]: Wrap everything under extern "C".

	* src/tgba/succiterconcrete.hh
891
	(tgba_succ_iterator_concrete::current_acc_): New attribute.
892
	* src/tgba/succiterconcrete.cc
893
	(tgba_succ_iterator_concrete::next): Set current_acc_.
894
	(tgba_succ_iterator_concrete::current_accepting_conditions):
895
896
	Simply return it.

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

902
903
	* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::tgba_bdd_core_data,
	tgba_bdd_core_data::translate): Handle all_accepting_conditions.
904
	* src/tgba/tgbabddconcretefactory.cc
905
906
	(tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions.

907
908
909
910
911
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.

912
913
2003-07-03  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

914
	* src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::first):
915
	Simplify, do not call next_non_false_() if either side is done.
916

917
918
919
920
921
922
923
924
925
926
927
928
929
930
	* 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.

931
932
2003-07-02  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

933
934
935
	* src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New
	function.
	* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate):
936
	Likewise.
937
938
	* src/tgba/tgbabddtranslatefactory.cc
	(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
939
940
	tgba_bdd_core_data::translate.

941
942
943
944
945
946
947
	* 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.

948
949
950
951
952
953
954
955
956
957
958
959
960
961
	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.
962
	* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc:
963
964
	Handle acc_set.

965
966
967
968
969
970
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.

971
972
2003-06-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

973
974
	* src/tgbaparse/tgbaparse.yy (lines): Expect at last one line.

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

986
987
	* src/tgba/succiter.hh (tgba_bdd_succ_iterator::done):
	Mark as const.
988
	* src/tgba/succiterconcrete.cc
989
990
991
	(tgba_succ_iterator_concrete::done): Likewise.
	* src/tgba/succiterconcrete.hh
	(tgba_succ_iterator_concrete::done): Likewise.
992
	* src/tgba/tgbaexplicit.cc
993
994
995
996
997
998
999
1000
1001
1002
1003
	(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.
1004

1005
1006
1007
1008
1009
	* 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.
1010
	* src/tgba/tgbabddcoredata.cc: Handle varandnext_set.
1011

1012
1013
1014
1015
	* doc/Doxygen.in: Enable LaTeX output.
	* doc/Makefile.am (spotref.pdf): New rule.
	(EXTRA_DIST): Add spotref.pdf.

1016
	* src/tgba/tgbabddconcretefactory.cc:
1017
1018
1019
1020
	(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.
1021
	* src/tgba/tgbabddconcretefactory.hh
1022
1023
	(tgba_bdd_concrete_factory::now_to_next_): New variable.

1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
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.

1036
1037
2003-06-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1038
1039
	* Makefile.am (EXTRA_DIST): Add HACKING.

1040
1041
	* configure.ac: Bump version to 0.0c.

1042
1043
	* configure.ac: Bump version to 0.0b.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1044
1045
	* INSTALL: New file.

1046
1047
1048
1049
	* 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
1050
1051
	* src/tgbatests/explprod.cc, src/tgbatests/ltl2tgba.cc,
	src/tgbatests/ltlprod.cc, src/tgbatests/mixprod.cc,
1052
1053
	src/tgbatests/reach.cc, src/tgbatests/tripprod.cc: Adjust inclusions.

1054
1055
1056
1057
	* src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments.
	* src/ltlast/formula.hh: More Doxygen comments.
	* src/tgba/tgba.hh: Use <tt> in Doxygen comments.

1058
1059
1060
1061
	* doc/mainpage.dox: New file.
	* doc/Makefile.am (EXTRA_DIST): Add mainpage.dox.
	* doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox

1062
1063
1064
1065
1066
1067
1068
	* 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.

1069
1070
1071
	* doc/Makefile.am (doc): Typo.
	* src/ltlvisit/tostring.hh (to_string): Add doxygen comments.
	* src/ltlast/multop.hh (multop::paircmp): Add doxygen comments.
1072
1073
	* src/tgba/tgbaexplicit.hh (tgba_explicit::transtion,
	state_explicit, tgba_explicit_succ_iterator): Add doxygen comments.
1074
1075
	* src/ltlvisit/postfix.hh: Typo.

1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
	* 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.

1101
1102
	* doc/Makefile.am (stamp): Prefix $(srcdir) explicitely.

1103
1104
1105
	* m4/buddy.m4 (BUDDY_LDFLAGS): Use $(top_builddir), not $(top_srcdir).
	* src/tgbaparse/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS).

1106
1107
1108
1109
1110
1111
	* 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.

1112
	Distribute BuDDy.  Compile and link with the included version if
1113
1114
1115
	explicitely requested (--with-included-buddy) or if there is now
	stuitable version already installed.

1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
	* 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.
1126
	* src/tgbatest/Makefile.am (AM_CPPFLAGS): Likewise.
1127

1128
1129
2003-06-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

1138
1139
1140
	* src/tgba/bddprint.hh, src/tgba/tgbabddconcretefactory.hh,
	src/tgba/tgbaproduct.hh: Fix Doxygen comments.

1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
	* 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.
1151
	* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state):
1152
1153
1154
1155
1156
1157
1158
	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.

1159
1160
	* src/tgbatest/ltl2tgba.cc: Support -v.

1161
1162
2003-06-24  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1163
1164
	* src/tgbatest/ltl2tgba.cc (syntax): Fix usage message.

1165
1166
1167
	* src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort
	accepting conditions.

1168
1169
1170
1171
1172
1173
1174
	* 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.

1175
1176
2003-06-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
1177
1178
1179
1180
1181
	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.
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
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
1246
1247
1248
1249
1250

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

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

1256
1257
2003-06-19  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1258
1259
	* src/tgba/tgbabddconcretefactory.cc
	(tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the
1260
1261
	formulae used as keys in prom_.
	(tgba_bdd_concrete_factory::create_promise): Delete.
1262
	(tgba_bdd_concrete_factory::declare_promise,
1263
	tgba_bdd_concrete_factory::finish): New functions.
1264
	* src/tgba/tgbabddconcretefactory.hh
1265
	(tgba_bdd_concrete_factory::create_promise): Delete.
1266
	(tgba_bdd_concrete_factory::declare_promise,
1267
1268
1269
1270
1271
1272
1273
	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().

1274
	* src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter):
1275
	Revert the change from 2003-06-12, it needs more work (the
1276
1277
1278
	automaton generated on Xa&(b U !a) was bogus, with that
	patch).

1279
	* src/tgbatest/ltl2tgba.cc: Handle the -o and -r options.
1280

1281
1282
1283
1284
	* src/tgbatest/tripprod.test, src/tgbatest/explprod.test,
	src/tgbatest/readsave.test: Adjust to reflect yesterday's
	bddprint.cc change.

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

1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
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.

1308
1309
2003-06-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
	* 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.

1324
	Make sure we can multiply two tgba_explicit.
1325

1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
	* 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.
1356
	* tgbatest/explprod.cc, tgbatest/explprod.test: New files.
1357
1358
1359
1360
1361
	* tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
	(explprod_SOURCES): New variable.
	(TESTS): Add explprod.test.
	(CLEANFILES): Add input1 and input2.

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

1369
1370
1371
1372
1373
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.

1374
1375
2003-06-06  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

1382
1383
1384
1385
1386
1387
1388
	* 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.

1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
	* 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.

1405
1406
1407
	* src/ltltest/equals.cc, src/ltltest/readltl.cc,
	src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include <cassert>.

1408
1409
2003-06-05  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
	* 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.

1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
	* 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.

1440
1441
	* src/ltlparse/ltlparse.yy: Typo in comment.

1442
1443
1444
1445
1446
	* 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.
1447
	* src/tgbatest/Makefile.am, src/tgbatest/defs.in,
1448
1449
	src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files.

1450
1451
2003-06-04  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1452
1453
	* src/ltlparse/ltlparse.yy (result): Suppress unused definition.

1454
1455
	* src/Makefile.am (SUBDIRS): Build `ltltest' after `.'.

1456
1457
1458
1459
	* 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
1460
2003-06-03  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
1461
1462
1463
1464
1465
1466

	* 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
1467
1468
1469
1470
1471
1472
1473
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.

1474
1475
1476
1477
1478
1479
1480
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.

1481
1482
2003-05-27  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1483
1484
1485
1486
1487
1488
1489
1490
	* 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.

1491
1492
	* src/tgba/bddfactory.hh, src/tgba/statebdd.hh,
	src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh,
1493
1494
1495
	src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add
	Doxygen comments.

1496
1497
1498
1499
1500
	* 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.
1501
	* src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
	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.

1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
	* 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.)

1534
1535
2003-05-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1536
1537
1538
1539
	* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files.
	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.

	* src/tgba/tgbabddtranslatefactory.cc
1540
1541
	(tgba_bdd_translate_factory::compute_pairs): Be quiet.

1542
1543
1544
1545
1546
	* src/Makefile.am (SUBDIRS): Add tgbaalgos.
	(libspot_la_LIBADD): Add tgba/libtgbaalgos.
	* src/tgbaalgos/Makefile.am: New file.
	* configure.ac: Output src/tgbaalgos/Makefile.

1547
1548
1549
1550
	* 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.

1551
1552
1553
1554
1555
1556
	* 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.
1557
	(tgba_bdd_concrete::succ_iter): Take a state_bdd as argument,
1558
1559
1560
	not a bdd.
	* src/tgba/tgbabddconcrete.cc: Likewise.

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
1561
	Initial code for TGBA (Transition Generalized Bchi Automata).
1562
1563
1564
1565
1566
	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.
1567
	* configure.ac: Output src/tgba/Makefile.
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
	* 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.

1584
1585
1586
1587
1588
1589
1590
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>.

1591
1592
2003-05-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1593
1594
1595
	* src/ltlvisit/dotty.cc: Rewrite to display formulae as
	graphs rather than trees, to show how nodes are shared.

1596
1597
1598
1599
1600
1601
1602
	* 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.

1603
1604
1605
1606
1607
1608
1609
	* 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.
1610
	* src/ltltest/readltl.cc, src/ltltest/equals.cc,
1611
1612
	src/ltltest/tostring.cc: Adjust usage.

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

1617
1618
1619
1620
1621
1622
1623
1624
1625
1626
1627
1628
1629
	* 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.

1630
1631
2003-05-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
1632
	Implement spot::ltl::destroy() and exercise it.
1633
1634
1635
1636
1637
1638
1639
1640
1641
1642
1643
1644
1645
1646
1647
1648
1649
1650
1651
1652
1653
1654
1655
1656

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

1657
1658
1659
1660
1661
1662
1663
1664
1665
1666
1667
1668
1669
1670
1671
1672
1673
1674
1675
1676
1677
1678
1679
1680
1681
1682
1683
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694
1695
1696
1697
	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.

1698
1699
1700
	* src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to
	remove a warning with newer versions of Flex.

1701
1702
1703
1704
1705
1706
	* 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.

1707
1708
1709
1710
1711
1712
1713
1714
1715
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.

1716
1717
1718
1719
1720
1721
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.

1722
2003-04-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1723

1724
1725
	* src/ltlvisit/Makefile.am (lib_LTLIBRARIES): Rename as ...
	(noinst_LTLIBRARIES): ... this.
1726
	* src/ltlenv/Makefile.am, src/ltlast/Makefile.am,
1727
	src/ltlparse/Makefile.am: Likewise.
1728
	* src/Makefile.am (lib_LTLIBRARIES, libspot_la_SOURCES,
1729
1730
1731
	libspot_la_LIBADD): New variable.   Build a libspot.la library
	from all the sub-libraries.

1732
1733
1734
1735
1736
1737
	* 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.

1738
2003-04-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1739

1740
	* configure.ac: Call AC_PROG_LIBTOOL.
1741
	* src/ltlast/Makefile.am, src/ltlenv/Makefile.am,
1742
1743
1744
	src/ltlparse/Makefile.am, src/ltltest/Makefile.am,
	src/ltlvisit/Makefile.am: Adust to build libtool libraries.

1745
1746
1747
	* src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here...
	* src/ltlenv/defaultenv.cc: ... but here.

1748
1749
1750
	* src/ltltest/tostring.test: Simplify with set -e.  Move the
	description of the test ...
	* src/ltltest/tostring.cc: ... here, where it is actually coded.
1751
1752
	* src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test,
	src/ltltest/nenoform.test,  src/ltltest/tunenoform.test:
1753
1754
	Simplify with set -e.

1755
	* configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make
1756
	sure we always use paths relative to src/ in src/'s
1757
1758
	subdirectories.

1759
2003-04-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1760
1761
1762
1763
1764

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

1765
2003-04-24  Rachid REBIHA  <rebiha@src.lip6.fr>
1766