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

3
4
	* src/tgbatest/spotlbtt.test: Add notice about long run time.

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

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

28
29
30
31
32
	* 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.

33
34
2003-10-22  Alexandre Duret-Lutz  <adl@src.lip6.fr>

35
36
37
38
	* src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc
	(emptiness_check::seq_counter, emptiness_check::periode): Rename as ...
	(emptiness_check::prefix, emptiness_check::period): ... these.

39
40
41
42
	* src/tgbaalgos/emptinesscheck.cc
	(emptiness_check::tgba_emptiness_check,
	emptiness_check::accepting_path): Simplify BDD operations.

43
44
45
46
47
	* src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh:
	Reindent.
	(emptiness_check::~emptiness_check, emptiness_check::emptiness_check):
	Remove, unused.

48
49
50
51
52
2003-10-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

53
54
55
56
57
2003-10-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>

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

58
59
2003-10-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>

60
61
62
63
64
65
66
67
68
69
70
	* 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.

71
72
73
	* iface/gspn/Makefile.am (XFAIL_TESTS): Remove.

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

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

92
93
2003-10-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>

94
95
96
97
98
99
100
	* 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.

101
102
	* src/ltlparse/ltlscan.ll: Allow doubly quoted atomic propositions.

103
104
2003-10-01  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

110
111
112
113
114
115
116
	* 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.

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

124
125
126
127
128
	* 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.

129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
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.
147

148
149
150
151
152
153
154
155
156
157
158
159
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.

160
161
162
163
2003-09-11  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

164
165
2003-08-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
	* 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.

188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
	* 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.

203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
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>.

221
222
223
224
225
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.

226
227
228
229
230
2003-08-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

231
232
2003-08-22  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

233
234
	* src/tgbaalgos/magic.cc (seen_with_magic, seen_without_magic): Remove.

235
236
237
	* wrap/python/cgi/ltl2tgba.in: Fix display of relations for
	tgba_bdd_concrete automata.

238
239
240
241
242
243
244
245
246
	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.

247
248
2003-08-20  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

249
250
251
252
	* tgba/tgbaproduct.cc, tgba/tgbaproduct.hh:
	(state_bdd_product, tgba_product_succ_iterator): Rename as ...
	(state_product, tgba_succ_iterator_product): ... these.

253
254
255
256
257
258
259
260
	* 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.

261
262
263
264
265
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.

266
267
2003-08-18  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

268
269
	* configure.ac: Bump version to 0.0i.

270
	* configure.ac, NEWS: Bump version to 0.0h.
271

272
273
	* wrap/python/cgi/Makefile.am (CLEANFILES): Clean ltl2tgba.py.

274
275
276
277
	* wrap/python/tests/ltl2tgba.test: Run $srcdir/ltl2tgba.py, not
	ltl2tgba.py.

2003-08-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319

	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.

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

325
326
327
328
329
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.

330
331
2003-08-10  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
	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.

348
349
350
351
	* 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.

352
353
354
	* src/tgbatest/tgbaread.test, src/tgbatest/explicit.test:
	Adjust expected output after 2003-08-07's change.

355
356
	* src/tgba/bdddict.hh: Typo in comments.

357
358
	* src/ltlenv/environment.hh: Typo in comments.

359
360
361
362
363
364
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>
365
366
367
368
369
370

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

371
2003-08-06  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
372

373
374
375
376
377
378
	* 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.

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

383
384
385
	* wrap/python/cgi/ltl2tgba.in: Handle show_formula_dot and
	show_formula_gif.

386
387
388
389
390
	* 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.

391
392
2003-08-05  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

393
394
395
396
397
	* 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().

398
399
	* README: Update layout.

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

405
406
	* wrap/python/spot.i: Add an ostringstream emulation.

407
408
2003-08-04  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

409
410
	* wrap/python/spot.i: Add an ofstream emulation.

411
412
413
414
	* wrap/python/spot.i: Declare spot::tgba::get_init_state,
	spot::tgba::succ_iter, and spot::tgba_succ_iterator::current_state
	as constructors.

415
416
417
418
419
420
421
422
423
424
425
	* 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.

426
427
428
	* 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.
429

430
431
432
	* wrap/python/spot.i: Include headers from tgba/ and tgbaalgos/.
	* wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test:
	New files.
433

434
435
436
437
	* wrap/python/tests/Makefile.am (TESTS): Add ltl2tgba.test.
	(EXTRA_DIST): Add ltl2tgba.py.
	* wrap/python/tests/run.in: Distinguish *.py and *.test.

438
439
440
	* wrap/python/tests/ltlparse.py: New file.
	* wrap/python/tests/Makefile.am (TESTS): Add it.

441
442
2003-08-01  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

443
444
445
446
	* 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
447
	(_buddy_la_SOURCES, _buddy_la_LDFLAGS, $(srcdir)/buddy_wrap.cxx)
448
449
450
451
	($(srcdir)/buddy.py): New.
	* wrap/python/tests/bddnqueen.py: New file.
	* wrap/python/tests/Makefile.am (TESTS): Add it.

452
453
454
455
456
457
458
459
460
461
462
463
464
465
	* 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.

466
	* configure.ac: Bump version to 0.0g.
467

468
	* configure.ac, NEWS: Bump version to 0.0f.
469

470
471
472
473
474
475
476
	* 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.

477
478
479
480
481
	* 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):

482
483
484
	* wrap/python/Makefile.am (spot_wrap.cxx, spot.py): Lookup
	spot.i in $(srcdir).

485
486
2003-07-31  Alexandre Duret-Lutz  <adl@gnu.org>

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

497
498
499
	* wrap/python/ltihooks.py: New file.
	* wrap/python/Makefile.am (EXTRA_DIST): Add ltihooks.py.

500
501
	* wrap/Makefile.am, wrap/spot.i: Move ...
	* wrap/python/Makefile.am, wrap/python/spot.i: ... here.
502

503
504
505
	* wrap/Makefile.am: New file.
	* configure.ac: Output wrap/python/Makefile.

506
507
508
	* src/misc/const_sel.hh: Delete.
	* src/misc/Makefile.am (misc_HEADERS): Remove const_sel.hh.

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

513
514
2003-07-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

515
516
517
	* iface/gspn/gspn.cc (tgba_gspn::format_state): Call gspn's
	print_state.

518
	* iface/gspn/dcswaveltl.test: Check for a false formula too.
519

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

529
530
531
532
533
534
535
536
537
	* 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.

538
539
2003-07-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

540
541
542
	* src/ltlparse/ltlscan.ll: Allow /\, \/, and xor, used in LBTT.
	* src/ltltest/parse.test: Test them.

543
544
545
546
	* src/tgbaalgos/lbtt.cc: Typos.

	* lbtt/: Upgrade to lbtt 1.0.2.

547
548
549
550
551
	* 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.

552
553
554
555
556
557
558
559
560
561
562
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.

563
564
2003-07-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

565
566
567
568
569
570
	* 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.

571
572
573
574
	* 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.

575
576
	* iface/gspn/dcswave.test: Comment state space sizes.

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

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

594
595
2003-07-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

	* iface/gspn/gspn.cc (tgba_gspn_private_::tgba_gspn_private_):
606
607
	Rethrow caught expections.

608
609
610
611
612
613
614
615
616
617
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
618
	its dictionary.
619

620
621
2003-07-17  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
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.

680
681
2003-07-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

682
683
684
	* m4/lbtt.m4 (AX_CHECK_LBTT): Set LBTT and LBTT_TRANSLATE
	when using an already installed lbtt.

685
686
687
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
	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.

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

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

789
790
	* configure.ac: Bump version to 0.0e.

791
792
793
	* configure.ac: Bump version to 0.0d.
	* NEWS, README: New files.

794
795
2003-07-12  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

796
797
	* m4/lbtt.m4: Run lbtt-translate, not lbtt.

798
799
	* iface/gspn/gspn.cc: Include cassert.

800
801
2003-07-10  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

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

812
813
814
815
816
817
818
819
820
821
822
	* 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.

823
824
	* src/tgbatest/spotlbtt.test: Make 100 rounds.

825
826
827
828
829
	* 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].

830
831
2003-07-09  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

849
850
851
852
853
854
855
	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.

856
857
858
	* src/tgbaalgos/lbtt.cc (lbtt_reachable): Do not end transitions
	guards with -1 in output.

859
860
2003-07-08  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

861
862
863
864
865
866
867
	* 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 "!".

868
869
	* src/ltlvisit/dump.cc: Strip useless spot::ltl:: prefixes.

870
871
2003-07-07  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

872
873
874
875
	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.

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

884
885
886
887
	* iface/gspn/gspnlib.h: Fit 80 columns.
	[__cplusplus]: Wrap everything under extern "C".

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

894
895
896
897
898
	* 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.

899
900
	* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::tgba_bdd_core_data,
	tgba_bdd_core_data::translate): Handle all_accepting_conditions.
901
	* src/tgba/tgbabddconcretefactory.cc
902
903
	(tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions.

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

909
910
2003-07-03  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

911
	* src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::first):
912
	Simplify, do not call next_non_false_() if either side is done.
913

914
915
916
917
918
919
920
921
922
923
924
925
926
927
	* 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.

928
929
2003-07-02  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

938
939
940
941
942
943
944
	* 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.

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

962
963
964
965
966
967
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.

968
969
2003-06-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

970
971
	* src/tgbaparse/tgbaparse.yy (lines): Expect at last one line.

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

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

1002
1003
1004
1005
1006
	* 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.
1007
	* src/tgba/tgbabddcoredata.cc: Handle varandnext_set.
1008

1009
1010
1011
1012
	* doc/Doxygen.in: Enable LaTeX output.
	* doc/Makefile.am (spotref.pdf): New rule.
	(EXTRA_DIST): Add spotref.pdf.

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

1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
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.

1033
1034
2003-06-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1035
1036
	* Makefile.am (EXTRA_DIST): Add HACKING.

1037
1038
	* configure.ac: Bump version to 0.0c.

1039
1040
	* configure.ac: Bump version to 0.0b.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1041
1042
	* INSTALL: New file.

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

1051
1052
1053
1054
	* src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments.
	* src/ltlast/formula.hh: More Doxygen comments.
	* src/tgba/tgba.hh: Use <tt> in Doxygen comments.

1055
1056
1057
1058
	* doc/mainpage.dox: New file.
	* doc/Makefile.am (EXTRA_DIST): Add mainpage.dox.
	* doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox

1059
1060
1061
1062
1063
1064
1065
	* 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.

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

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

1098
1099
	* doc/Makefile.am (stamp): Prefix $(srcdir) explicitely.

1100
1101
1102
	* m4/buddy.m4 (BUDDY_LDFLAGS): Use $(top_builddir), not $(top_srcdir).
	* src/tgbaparse/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS).

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

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

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

1125
1126
2003-06-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1127
1128
1129
1130
1131
1132
1133
1134
	* 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.

1135
1136
1137
	* src/tgba/bddprint.hh, src/tgba/tgbabddconcretefactory.hh,
	src/tgba/tgbaproduct.hh: Fix Doxygen comments.

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

1156
1157
	* src/tgbatest/ltl2tgba.cc: Support -v.

1158
1159
2003-06-24  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1160
1161
	* src/tgbatest/ltl2tgba.cc (syntax): Fix usage message.

1162
1163
1164
	* src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort
	accepting conditions.

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

1172
1173
2003-06-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
1174
1175
1176
1177
1178
	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.
1179
1180
1181
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

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

1248
1249
1250
1251
1252
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.

1253
1254
2003-06-19  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

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

1276
	* src/tgbatest/ltl2tgba.cc: Handle the -o and -r options.
1277

1278
1279
1280
1281
	* src/tgbatest/tripprod.test, src/tgbatest/explprod.test,
	src/tgbatest/readsave.test: Adjust to reflect yesterday's
	bddprint.cc change.

1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
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.

1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
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.

1305
1306
2003-06-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
	* 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.

1321
	Make sure we can multiply two tgba_explicit.
1322

1323
1324
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
	* 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.
1353
	* tgbatest/explprod.cc, tgbatest/explprod.test: New files.
1354
1355
1356
1357
1358
	* tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
	(explprod_SOURCES): New variable.
	(TESTS): Add explprod.test.
	(CLEANFILES): Add input1 and input2.

1359
1360
1361
1362
1363
1364
1365
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.

1366
1367
1368
1369
1370
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.

1371
1372
2003-06-06  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1373
1374
1375
1376
1377
1378
	* 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.

1379
1380
1381
1382
1383
1384
1385
	* 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.

1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
	* 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.

1402
1403
1404
	* src/ltltest/equals.cc, src/ltltest/readltl.cc,
	src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include <cassert>.

1405
1406
2003-06-05  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
	* 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.

1437
1438
	* src/ltlparse/ltlparse.yy: Typo in comment.

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

1447
1448
2003-06-04  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1449
1450
	* src/ltlparse/ltlparse.yy (result): Suppress unused definition.

1451
1452
	* src/Makefile.am (SUBDIRS): Build `ltltest' after `.'.

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

	* 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
1464
1465
1466
1467
1468
1469
1470
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.

1471
1472
1473
1474
1475
1476
1477
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.

1478
1479
2003-05-27  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

1488
1489
	* src/tgba/bddfactory.hh, src/tgba/statebdd.hh,
	src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh,
1490
1491
1492
	src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add
	Doxygen comments.

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

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

1531
1532
2003-05-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1533
1534
1535
1536
	* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files.
	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.

	* src/tgba/tgbabddtranslatefactory.cc
1537
1538
	(tgba_bdd_translate_factory::compute_pairs): Be quiet.

1539
1540
1541
1542
1543
	* src/Makefile.am (SUBDIRS): Add tgbaalgos.
	(libspot_la_LIBADD): Add tgba/libtgbaalgos.
	* src/tgbaalgos/Makefile.am: New file.
	* configure.ac: Output src/tgbaalgos/Makefile.

1544
1545
1546
1547
	* 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.

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

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

1581
1582
1583
1584
1585
1586
1587
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>.

1588
1589
2003-05-16  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

1590
1591
1592
	* src/ltlvisit/dotty.cc: Rewrite to display formulae as
	graphs rather than trees, to show how nodes are shared.

1593
1594
1595
1596
1597
1598
1599
	* 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.

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

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

1614
1615
1616
1617
1618
1619
1620
1621
1622
1623
1624
1625
1626
	* 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.

1627
1628
2003-05-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

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

1654
1655
1656
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
	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.

1695
1696
1697
	* src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to
	remove a warning with newer versions of Flex.

1698
1699
1700
1701
1702
1703
	* 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.

1704
1705
1706
1707
1708
1709
1710
1711
1712
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.

1713
1714
1715
1716
1717
1718
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.

1719
2003-04-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1720

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

1729
1730
1731
1732
1733
1734
	* 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.

1735
2003-04-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1736

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

1742
1743
1744
	* src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here...
	* src/ltlenv/defaultenv.cc: ... but here.

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

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

1756
2003-04-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
1757
1758
1759
1760
1761

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

1762
2003-04-24  Rachid REBIHA  <rebiha@src.lip6.fr>
1763
1764
1765
1766
1767
1768

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