ChangeLog 391 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
4
5
6
2011-12-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Release Spot 0.8.1.

	* configure.ac, NEWS: Bump version to 0.8.1.

7
8
9
10
2011-12-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Summarize recent fixes.

11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
2011-12-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix VPATH builds, now that hash.hh include _config.h

	* iface/dve2/Makefile.am, src/eltlparse/Makefile.am
	src/eltltest/Makefile.am, src/evtgba/Makefile.am,
	src/evtgbaalgos/Makefile.am, src/evtgbaparse/Makefile.am,
	src/evtgbatest/Makefile.am, src/kripke/Makefile.am,
	src/kripketest/Makefile.am, src/ltlast/Makefile.am,
	src/ltlparse/Makefile.am, src/ltltest/Makefile.am,
	src/ltlvisit/Makefile.am, src/misc/Makefile.am,
	src/neverparse/Makefile.am, src/saba/Makefile.am,
	src/sabaalgos/Makefile.am, src/sabatest/Makefile.am,
	src/sanity/Makefile.am, src/tgba/Makefile.am,
	src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/Makefile.am,
	src/tgbaparse/Makefile.am, src/tgbatest/Makefile.am,
	wrap/python/Makefile.am (AM_CPPFLAGS): Make sure
	$(top_builddir)/src is included.

30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
2011-12-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Perform WDBA minimization before degeneralization.

	There is no point in degeneralizing an automaton if it can be WDBA
	minimized.  Doing so will only augment the number of states and
	slow down the powerset construction used by the WDBA minimization.

	* src/tgbatest/babiak.test: New file.  It includes 5 formulae
	which Tomáš Babiak reported Spot 0.7.1 would take over one hour to
	translate if degeneralization and WDBA minimization were both
	requested.
	* src/tgbatest/Makefile.am (TESTS): Add it.
	* src/tgbatest/ltl2tgba.cc: Do WDBA minimization before
	degeneralization.  The above formulae are now all translated in a
	few seconds.

47
48
49
50
51
52
53
54
55
56
57
58
59
60
2011-12-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Don't rely on the g++ version to include tr1/unordered_map and co.

	The previous setup failed with clang++ 3.0.

	* m4/stl.m4: New file.
	* configure.ac: Call AC_HEADER_UNORDERED_MAP,
	AC_HEADER_TR1_UNORDERED_MAP, and AC_HEADER_EXT_HASH_MAP.
	* src/misc/hash.hh: Include _config.h, and used the
	SPOT_HAVE_UNORDERED_MAP, SPOT_HAVE_TR1_UNORDERED_MAP,
	or SPOT_HAVE_EXT_HASH_MAP defines to decide which
	file to include.

61
62
63
64
65
66
67
68
2011-12-01  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix mkdir error in ajax/spot.in.

	* wrap/python/ajax/spot.in: Do not print an error
	when attempting to create an existing directory.
	Reported by Étienne Renault.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
69
70
71
72
73
74
75
76
2011-11-29  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix build failure during "make check" on MacOS X.

	* src/kripketest/Makefile.am (LDADD): Remove a broken dependency.
	Reported by Yann Thierry-Mieg.
	* src/sanity/style.test: Make sure it does not appear again.

77
78
79
80
2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* AUTHORS: Sort alphabetically.

81
82
83
84
85
86
87
88
2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Remove the old CGI interface.

	* wrap/python/cgi-bin: Remove this directory.
	* wrap/python/Makefile.am (SUBDIRS): Remove it.
	* configure.ac, README, wrap/python/ajax/README: Likewise.

89
90
91
92
93
94
95
2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Undocument `.' from the web interface.

	* wrap/python/ajax/ltl2tgba.html: Remove `.'
	from the list of acceptable symbols for AND.

96
97
98
99
2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS, configure.ac: Bump version to 0.8a.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
100
101
102
103
104
105
2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Release Spot 0.8.

	* NEWS, configure.ac: Bump version to 0.8.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
106
107
108
109
110
111
112
113
2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Remove spotref.pdf.

	* doc/Doxyfile.in: Do not generate LaTeX output.
	* doc/Makefile.am: Do not build spotref.pdf.
	* NEWS, README: Adjust.

114
115
116
117
118
119
120
2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix some Doxygen errors.

	* src/kripke/kripkeexplicit.hh: Reindent, and fix
	some comments.

121
122
123
124
125
126
127
128
2011-11-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add more nodes when resizing BDD table.

	* src/misc/bddalloc.cc (bdd_allocator::initialize): Call
	bdd_setmaxincrease(500000), because the default is 50000,
	which cause garbage collection to occur too often.

129
130
131
132
2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Mention the Kripke I/O.

133
134
135
136
137
138
139
140
141
2011-11-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Don't flush the stream on each new line, when writing automata.

	* src/tgbaalgos/neverclaim.cc, src/tgbaalgos/dotty.cc,
	src/tgbaalgos/save.cc: Prefer '\n' over std::endl to speedup I/O.
	* src/ltltest/genltl.cc (syntax): Use '\n' too, although it won't
	make a big difference.

142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
2011-11-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add an ltl2tgba option to read Kripke structure.

	Also offers two ways to output Kripke structures.

	* src/kripketest/parse_print_test.cc, src/kripke/kripkeexplicit.cc
	: Simplify includes.
	* src/kripke/kripkeprint.hh (kripke_save_reachable,
	kripke_save_reachable_renumbered): New declarations.
	(KripkePrinter): Move and rename...
	* src/kripke/kripkeprint.cc (kripke_printer): ... here.
	(kripke_printer_renumbered): New class.
	(kripke_save_reachable, kripke_save_reachable_renumbered): New
	function.
	* src/tgbatest/ltl2tgba.cc: Add an option to read Kripke
	structures.
	* iface/dve2/dve2check.cc: Use kripke_save_reachable_renumbered.
	* iface/dve2/defs.in (run2): Remove.
	* iface/dve2/kripke.test: Adjust tests.

163
164
165
166
2011-11-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* AUTHORS: Add Thomas Badie.

167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
2011-05-07  Thomas Badie  <badie@lrde.epita.fr>

	Add text I/O for Kripke structures.

	* src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
	src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: New files.
	* src/kripke/Makefile.am: Add them.
	* src/kripkeparse/fmterror.cc, src/kripkeparse/kripkeparse.yy,
	src/kripkeparse/kripkescan.ll, src/kripkeparse/parsedecl.hh,
	src/kripkeparse/public.hh, src/kripkeparse/scankripke.ll: New
	files.
	* src/kripkeparse/Makefile.am: Add them.
	* src/kripketest/bad_parsing.test, src/kripketest/defs.in,
	src/kripketest/kripke.test, src/kripketest/origin,
	src/kripketest/parse_print_test.cc: New files.
	* src/kripketest/Makefile.am: Add them.
	* src/Makefile.am (SUBDIRS): Add kripkeparse and kripketest.
	* README: Document src/kripketest/ and src/kripkeparse/.
	* configure.ac: Generate src/kripkeparse/Makefile,
	src/kripketest/Makefile, src/kripketest/defs.
	* iface/dve2/defs.in (run2): New function.
	* iface/dve2/dve2check.cc (syntax, main): Add option -gK.
	* iface/dve2/kripke.test: New file.
	* iface/dve2/Makefile.am (TESTS): Add kripke.test.

192
193
194
195
196
197
198
199
2011-11-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix bench/emptchk/pml2tgba.pl for more recent Spin version.

	* bench/emptchk/pml2tgba.pl: Stop checking for version start lines
	depending on the Spin version.  This check was never always
	correct.  Reported by Étienne Renault.

200
201
202
203
204
205
206
207
2011-11-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Update formulae.ltl not to use uncommon operators.

	* bench/emptchk/formulae.ltl: Do not use + and * in the list of
	formulas.  Use | and & instead.  The * operator was removed on
	2010-01-30.  Reported by Étienne Renault.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
208
209
210
211
212
213
214
215
2011-11-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	More documentation.

	* src/tgbaalgos/randomgraph.hh: Document the fact that adding
	acceptance conditions to the graph may generate graphs that do not
	have any accepting cycle.

216
217
218
219
220
221
222
223
224
2011-11-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Display transition annotations in dotty output.

	* src/tgbaalgos/dotty.cc (process_link): Call
	transition_annotation().  Reported by Nikos Gorogiannis.
	* src/tgba/tgba.hh (transition_annotation): More documentation.
	* NEWS: Mention this change.

225
226
227
228
2011-11-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Add an entry for the previous fix.

229
230
231
232
233
234
235
236
237
238
239
240
241
2011-11-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fully quote guards used by neverclaims.

	Especially with should write !(p0) and not !p0, because p0 is
	usually #define'd by the user and he may have forgotten to quote
	the value of the macro.  This issue was discovered by Kristin
	Yvonne Rozier and diagnosed by Gerard Holzmann.

	* src/tgbaalgos/neverclaim.cc (process_link): Call
	to_spin_string(..., true) to fully parentheses the string.
	* src/tgbatest/neverclaimread.test: Add a test.

242
243
244
245
246
247
248
249
2011-11-11  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix a g++-4.7 warning about a variable used only in an assert().

	* src/tgbaalgos/weight.cc (inc_weight_handler)
	(dec_weight_handler): Remove these assertions that require the
	loop the be completed, and use break to exit ASAP.

250
251
252
253
254
255
256
257
258
2011-11-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Allow neverclaim guards of the form `!(x)' or `! (x)'.

	* src/neverparse/neverclaimscan.ll: Make the space between `!' and
	`(' optional.  This fixes the patch from 2011-02-07 that made this
	space mandatory...
	* src/tgbatest/neverclaimread.test: Augment test case.

259
260
261
262
263
264
265
2011-10-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Better documentation for print_tgba_run.

	* src/tgbaalgos/emptiness.hh (print_tgba_run): Reword the
	documentation after a report from Nikos Gorogiannis.

266
267
268
269
2011-10-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/finite.test: Swap -e and -E after change from 2011-07-26.

270
271
272
273
2011-10-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Update with recent fixes.

274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
2011-10-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Safra: Fix usage of multiple acceptance conditions and fix text output.

	* src/tgba/tgbasafracomplement.cc
	(tgba_safra_complement::tgba_safra_complement)
	(tgba_safra_complement::succ_iter): Correct the declaration and
	use of multiple acceptance conditions.
	(state_complement::to_string): Output the L set, not U.  The previous
	code caused different states to share the same names, causing issues
	with the text-based output (state with identical names get merged).
	* src/tgba/tgbasafracomplement.hh
	(tgba_safra_complement::acceptance_cond_vec_): Adjust type to
	store BDDs.
	* src/tgbatest/complementation.cc: Implement a new "-b" option
	to output automata in Spot's syntax.
	* src/tgbatest/complementation.test: Add a test-case supplied
	by Martin Dieguez Lodeiro.
	* THANKS: Add Martin.

294
295
296
297
2011-10-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/tgba/tgbasafracomplement.cc: Fix two asserts.

298
299
300
301
302
303
304
305
306
307
308
2011-10-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Improve the print_safra_automaton output.

	* src/tgba/tgbasafracomplement.cc (print_safra_tree): Fix output in
	case of hash collision.  Use the actual states to get a number, not
	their hash value.
	(print_safra_automaton): Output a mapping of values to states names.
	(safra_tree_automaton::get_sba): New method, used by
	print_safra_automaton.

309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
2011-08-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix errors reported by clang++-2.9.

	* src/evtgbaalgos/tgba2evtgba.cc (process_link): Fix prototype
	to match tgba_reachable_iterator::process_link.
	* src/ltlvisit/tunabbrev.hh: Add using super::visit, so that the
	other visit() method are in scope when we overload one.
	* src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc (start, end,
	process_link): Remove these empty methods.  The default
	implementations are empty too, and process_link had the
	wrong prototype.
	* src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc
	(start, end, process_link): Likewise.

324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
2011-08-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Improve SCC simplification by removing implied acceptance conditions.

	Spot 0.7.1 used to need 190 acceptance conditions to translate the
	188 literature formulae.  With this patch we are down to 185.
	That's not an impressive, but there are only ~20 formulae that
	require more than 1 acceptance conditions; hence little room for
	improvement.

	* src/misc/bddlt.hh (bdd_hash): New function.
	* src/misc/accconv.hh, src/misc/accconv.cc: New files.
	* src/misc/Makefile.am: Add them.
	* src/tgbaalgos/scc.cc (scc_map::build_map): Adjust
	to record all combination of acceptance conditions occurring in a SCC.
	* src/tgbaalgos/scc.hh (scc_map::scc::useful_acc): Update description.
	* src/tgbaalgos/sccfilter.cc (scc_filter): Simplify acceptance
	conditions that are always implied by another acceptance
	conditions.  Previously, we only removed acceptance conditions
	that where always present in accepting SCCs.
	* src/tgbatest/sccsimpl.test: New file.
	* src/tgbatest/Makefile.am (TESTS): Add it.

347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
2011-08-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Refine yesterday's change to the degeneralization.

	This avoids a small regression on the size of degeneralized
	automata of our usual list of literature formulae.

	* src/tgba/tgbatba.hh, src/tgba/tgbatba.cc
	(tgba_tba_proxy::union_acceptance_conditions_of_original_state):
	New method.
	* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): In accepting
	states, ignore only the last expected acceptance condition if its
	common to all outgoing transitions AND if it is not used by any
	outgoing transitions of the destination.

362
363
364
365
366
367
368
369
370
371
372
373
2011-08-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Make sure the degeneralization is idempotent (up to renaming of
	states).

	* src/tgbaalgos/tgbatba.cc: When degeneralizing to SBA, remove the
	acceptance conditions that are common to all outgoing transitions
	of this state.  This helps to make the degeneralization
	idempotent.
	* src/tgbatest/degenid.test: New test case.
	* src/tgbatest/Makefile.am: Add it.

374
375
376
377
378
379
380
381
2011-08-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix escaping of state name in save_reachable()'s output.

	* src/tgbaalgos/save.c (process_state): Escape quotes in the
	name of source and destination states.  This fixes a side bug
	in the upcoming degenid.test test case.

382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
2011-08-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Running `ltl2tgba -R1q -R1t -N` would degeneralize before and
	after the simulation-reduction.

	Report from Tomáš Babiak <xbabiak@fi.muni.cz>.

	* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Take
	a tgba as input.
	* src/tgbaalgos/neverclaim.cc (never_claim_bfs): Call
	state_is_accepting() only if this tgba turns out to be
	a tgba_sba_proxy.  Otherwise check the acceptance of one
	outgoing transition as we do in dotty_bfs since 2011-03-05.
	* src/tgbatest/ltl2tgba.cc: Do not redegeneralize before
	calling never_claim_reachable() if we know the automaton is
	degeneralized already.
	* src/tgbatest/ltl2tgba.test: Add a test case.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
400
401
402
403
404
405
406
2011-08-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Please GCC 4.6.

	* src/tgbatest/complementation.cc (check, automaton): Remove
	these unused variables.

407
408
409
410
411
412
413
414
415
416
417
418
419
2011-08-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix a nondeterministic behavior of the degeneralization algorithm.

	Reported by Tomáš Babiak <xbabiak@fi.muni.cz>.

	* src/tgba/tgbatba.cc (tgba_tba_proxy): Replace the std::map used
	to record outgoing transitions by an Sgi::hash_map, and keep the
	order of these transitions in a separate list.
	* src/tgbatest/degendet.test: New file.
	* src/tgbatest/Makefile.am (TESTS): Add it.
	* THANKS: Add Tomáš and convert to utf8.

420
421
422
423
2011-08-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/tgbatest/ltl2tgba.cc (syntax): -N implies -DS, not -D.

424
425
426
427
2011-07-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2check.cc: Add option -W and simplify formulae.

428
429
430
431
432
433
434
435
2011-07-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	-e means we expect an accepting run.

	* iface/dve2/dve2check.cc: Reverse the value of
	expect_counter_example with respect to the -e/-E options.
	* iface/dve2/dve2check.test: Swap -e and -E.

436
437
438
439
440
441
442
2011-06-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add some "drop shadow" in ltl2tgba.html.

	* wrap/python/ajax/ltl2tgba.html: Add shadow to all boxes.
	* wrap/python/ajax/css/ltl2tgba.css (.shadow): New class.

443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
2011-06-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Revamp the ltl2tgba benchmark.

	* bench/ltl2tgba/algorithms: Reduce the number of Spot configuration
	tested.
	* bench/ltl2tgba/Makefile.am (run, small.txt, big.txt, known.txt):
	New rules.
	* bench/ltl2tgba/big, bench/ltl2tgba/small, bench/ltl2tgba/known:
	Add a 15min timeout to the lbtt configuration.
	* bench/ltl2tgba/defs.in: Adjust variable definitions to accept
	variable inderections.
	* bench/ltl2tgba/parseout.pl: Add an option to output the table in
	LaTeX.  Also consider all formulae, not just the positive
	formulae.
	* bench/ltl2tgba/README: Update.

460
461
462
463
2011-06-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/ltlvisit/tostring.cc (to_spin_string_visitor): Add missing break.

464
465
466
467
468
469
470
471
2011-06-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* wrap/python/ajax/spot.in: Touch the directory containing
	the cached result for the requests.  So that it survives
	the browser's cache.
	(finish): Prune the cache only once per hour, and only eraes
	files that are older than 2 hours.

472
473
474
475
476
2011-06-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* wrap/python/ajax/ltl2tgba.html: Add focus on the formula field
	on page load.

477
478
479
480
2011-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Update with recent changes.

481
482
483
484
485
486
487
488
2011-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Implement cache pruning in the CGI script.

	* wrap/python/ajax/spot.in (finish): Prune the cache once in a
	while.  We rely on hardlinks for garbage collecting the pictures
	and dot sources that may be shared by different requests.

489
490
491
492
493
494
495
496
497
2011-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Cache dot sources in the CGI script.

	* wrap/python/ajax/spot.in (render_dot, render_dot_maybe)
	(render_automaton, render_formula): Cache the dot source, so that
	we do not have to regenerate two pictures from the same contents.
	* wrap/python/spot.i: Typo in the ostringstream declaration.

498
499
500
501
502
503
504
2011-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Output a "Cache-Control:" header in the CGI script.

	* wrap/python/ajax/spot.in: Output a cache-control header, so that
	browsers do no even send two identical requests.

505
506
507
508
509
510
511
512
513
514
515
2011-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Cache results of the spot.py CGI script.

	* wrap/python/ajax/spot.in: Use the QUERY_STRING as a hash key to
	cache the result of the script.  Open stdout without buffering and
	redirect it to a file that we can dump later on cache hits.  Parts
	of this change are extracted from code from Pierre Parutto
	<parutto@lrde.epita.fr>.
	* AUTHORS: Add him.

516
517
518
519
2011-06-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/ltltest/genltl.cc (X_n): Fix assertion.

520
521
522
523
2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/ltlvisit/dotty.cc (dotty_visitor): Reorder attributes.

524
525
526
527
2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/ltltest/genltl.cc (fair_response): Typo.

528
529
530
531
532
533
534
535
536
537
538
539
2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	DVE2: Do not display state variables with only one possible value.

	* iface/dve2/dve2.cc (dve2_kripke::dve2_kripke): Fill
	a format_filter_ array with boolean indicating whether each
	variable should be printed.  Ignore variable with only one
	possible value.
	(dve2_kripke::~dve2_kripke): Destroy it.
	(dve2_kripke::format_state): Use it.
	* iface/dve2/finite.test: Adjust.

540
541
542
543
544
545
546
547
548
549
550
551
2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Remove Kristin Rozier's LTLcounter.pl scripts, now that we can
	generate these formulae with "genltl".

	* src/tgbatest/ltlcounter/: Remove this directory.
	* src/tgbatest/Makefile.am: Adjust.
	* src/tgbatest/ltlcounter.test, bench/ltlcounter/run: Use genltl
	to generate the formulae.
	* bench/ltlcounter/README: Do not mention src/tgbatest/ltlcounter/
	anymore.

552
553
554
555
556
557
558
559
2011-06-06  Alexandre Duret-Lutz  <adl@va-et-vient.net>

	Better layout of the LTL formula parse tree.

	* src/ltlvisit/dotty.cc: Display "L" and "R" tail-labels
	for binary operators.  Gather all constants and atomic
	propositions in a sub-graph with "rank=sink".

560
561
562
563
564
565
566
567
568
569
2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add more formula families to genltl.

	* src/ltltest/genltl.cc (fair_response, ltl_counter)
	(ltl_counter_carry): New functions, constructing function from
	gastin.03.cav and rozier.07.cav.  The LTL counter will replace the
	scripts in src/tgbatest/ltlcounter/.
	(X_n): New helper function.

570
571
572
573
574
575
576
577
578
579
580
581
582
2011-06-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Install a misc/_config.h to hide all the defines that clutter the
	built output.

	This is also a step towards better checks for things like
	__attribute__ or std::tr1.

	* m4/ax_prefix_config_h.m4: New file.
	* configure.ac: Call AC_CONFIG_HEADERS and AX_PREFIX_CONFIG_H.
	* src/misc/Makefile.am: Install misc/_config.h.
	* src/misc/random.cc, src/misc/version.cc: Include misc/_config.h.

583
584
585
586
587
588
589
2011-06-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Document the protocol used between ltl2tgba.html and spot.py.

	* wrap/python/ajax/protocol.txt: New file.
	* wrap/python/ajax/Makefile.am (EXTRA_DIST): Add it.

590
591
592
593
2011-06-02  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/README: Document state compression.

594
595
596
597
598
599
600
601
602
603
604
605
606
2011-06-02  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Update jQuery and jQuery-UI.

	* wrap/python/ajax/ltl2tgba.html: Adjust to use
	jQuery 1.6.1 and jQuery-UI 1.8.13.  Remove a useless check
	of $("#autoupdate").attr("checked") since this checkbox no longer
	exists.
	* wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.8.custom.css:
	Replace by ...
	* wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.13.custom.css: This.
	* wrap/python/ajax/Makefile.am (EXTRA_DIST): Adjust.

607
608
609
610
2011-05-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2.cc: Kill a spurious warning.

611
612
613
614
2011-05-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* bench/wdba/README: Typos.

615
616
617
618
619
620
621
622
2011-05-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Some intvcomp2 speedups.

	* src/misc/intvcmp2.cc (stream_compression_base::run):
	Implement a shift-less encoding for the 1-bit and 3-bit cases.
	Also declare offsets as size_t, to help 64-bit compilers.

623
624
625
626
627
2011-05-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/misc/intvcomp.hh, src/misc/intvcmp2.hh: Include stddef.h for
	size_t.

628
629
630
631
2011-05-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/misc/intvcmp2.cc: Cosmetics to please sanity checks.

632
633
634
635
636
637
638
639
2011-05-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix compilation error with g++ <= 4.3.

	* src/misc/intvcmp2.cc (int_array_array_compression): Specify full
	type of stream_compression_base<int_array_array_compression> in
	constructor to please g++ versions <= 4.3.

640
641
642
643
644
645
646
647
2011-05-02  Alexandre Duret-Lutz  <adl@va-et-vient.net>

	DVE2: Minor memory compaction.

	* iface/dve2/dve2.cc (dve2_state, dve2_compressed_state): Store
	size and count on 16 bits, and hash on 32 bits, to limit memory
	wasted.

648
649
650
651
652
653
654
2011-05-01  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	DVE2: Optionally use the new compression.

	* iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc:
	Add a -Z option and pass it through.

655
656
657
658
659
660
661
662
663
664
2011-05-01  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Implement a new compression inspired from simple-9.

	* src/misc/intvcmp2.cc, src/misc/intvcmp2.hh: New files.
	* src/misc/Makefile.am: Add them.
	* src/tgbatest/intvcmp2.cc: New test.
	* src/tgbatest/Makefile.am: Add it.
	* src/tgbatest/intvcomp.test: Call it.

665
666
667
668
2011-04-15  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/misc/intvcomp.cc: Low-level fine-tuning.

669
670
671
672
673
674
675
676
677
678
679
2011-04-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix compression of large repetitions

	* src/misc/intvcomp.cc (stream_compression_base::run): Limit
	repeatitions to 40, not 42.
	(stream_decompression_base::refill): Refill the end of the stream
	with 0.
	(stream_decompression_base::look_n_bits): Add assertion.
	* src/tgbatest/intvcomp.cc: Add a new test case.

680
681
682
683
684
685
686
687
688
2011-04-12  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	More interfaces to the int array compression routines.

	* src/misc/intvcomp.cc, src/misc/intvcomp.cc: Add interfaces to
	compress vector<int> to vector<unsigned>.
	* src/tgbatest/intvcomp.cc: Test them.
	* src/sanity/style.test: Refine check to avoid a spurious report.

689
690
691
692
2011-04-11  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2.cc: Typo when handling dead==true.

693
694
695
696
697
698
699
700
701
2011-04-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Always pass --enable-devel or --disable-devel to BuDDy.

	* configure.ac: Do not add CXXFLAGS and CFLAGS in ac_configure_args,
	it causes problem when using config.cache.  Instead ...
	* m4/devel.m4: Add --enable-devel or --disable-devel on
	ac_configure_args, now that BuDDy understands that.

702
703
704
705
706
2011-04-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/misc/escape.hh: Fix Doxygen documentation.
	* src/misc/intvcomp.hh: Likewise.

707
708
709
710
711
712
713
714
2011-04-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Move the compression routines into their own *.cc file.

	* src/misc/intvcomp.hh: Move all code...
	* src/misc/intvcomp.cc: ... in this new file.
	* src/misc/Makefile.am: Add invcomp.cc

715
716
717
718
719
720
721
722
723
724
2011-04-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	DVE2: Use mspool for compressed states.

	* iface/dve2/dve2.cc: Adjust to use the new mspool allocator,
	and get rid of the std::vector used to store compressed states.
	* src/misc/intvcomp.hh: Add an "int* -> int*" interface
	in addition to the "int* -> vector<unsigned>*" interface.
	* src/tgbatest/intvcomp.cc: Test the two interfaces.

725
726
727
728
729
730
731
2011-04-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add a multiple-size memory pool implementation.

	* src/misc/mspool.hh: New file.
	* src/misc/Makefile.am: Add it.

732
733
734
735
2011-04-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/misc/fixpool.hh: Typo in comment.

736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
2011-04-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	DVE2: preliminary implementation of compressed states.

	* iface/dve2/dve2.cc (dve2_compressed_state): New class.
	(callback_context): Deal with general state*s, not dve2_state*s.
	(transition_callback_compress): New function.
	(dve2_kripke): Take a compress option.
	(get_init_state, compute_state_condition, succ_iter,
	format_state, state_condition): Handle compressed states.
	(get_vars, compute_state_condition_aux): New helper methods.
	* iface/dve2/dve2.hh (load_dve2): Add a compress option.
	* iface/dve2/dve2check.cc: Add a -z option.
	* iface/dve2/finite.test, iface/dve2/dve2check.test: Add more
	tests.

752
753
754
755
756
757
758
759
760
2011-04-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Preliminary implementation of an int array compressor.

	* src/misc/intvcomp.hh: New file.
	* src/misc/Makefile.am: Add it.
	* src/tgbatest/intvcomp.cc, src/tgbatest/intvcomp.test: New files.
	* src/tgbatest/Makefile.am: Add them.

761
762
763
764
765
766
767
768
769
770
2011-04-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix two spurious segfaults in test cases for the Python interface.

	* wrap/python/tests/setxor.py, wrap/python/tests/bddnqueen.py:
	Clean all used bdd variables before calling bdd_done(), so that
	bdd_delref() is never called after bdd_done().  In NDEBUG builds,
	bdd_delref() does not check whether the BuDDy is running or not,
	and calling it after bdd_done() will crash.

771
772
773
774
2011-04-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* HACKING: Add an example for using callgrind.

775
776
777
778
779
2011-04-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2check.cc (main): Catch out-of-memory errors
	during emptiness check or counterexample generation.

780
781
782
783
784
2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc: Use
	a fixed-size memory pool for product_state instances.

785
786
787
788
789
2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2.cc: Use a fixed-size memory pool for dve2_state
	instances and their variables.

790
791
792
793
794
795
796
2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add a fixed-size memory pool implementation.

	* src/misc/fixpool.hh: New file.
	* src/misc/Makefile.am (misc_HEADERS): Add fixpool.hh.

797
798
799
800
2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* HACKING (command): Some notes about link-time optimizations.

801
802
803
804
805
2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* configure.ac: Pass CXXFLAGS/CFLAGS/CPPFLAGS debug/optimization
	settings to sub configure.

806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
2011-03-31  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Introduct a down_cast macro.

	* src/misc/casts.hh: New file.
	* src/misc/Makefile.am: Add it.
	* iface/dve2/dve2.cc, iface/gspn/gspn.cc, iface/gspn/ssp.cc,
	src/evtgba/explicit.cc, src/evtgba/product.cc, src/misc/casts.hh,
	src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/taatgba.cc,
	src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.cc,
	src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
	src/tgba/tgbakvcomplement.cc, src/tgba/tgbaproduct.cc,
	src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc,
	src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc,
	src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reductgba_sim.cc,
	src/tgbaalgos/reductgba_sim_del.cc: Use down_cast when
	appropriate.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
824
825
826
827
828
829
830
831
832
833
2011-03-31  Alexandre Duret-Lutz  <adl@va-et-vient.net>

	Cosmetics.

	* src/sanity/style.test: Catch some binary operators not
	delimited with spaces.
	* src/tgbaalgos/bfssteps.cc, src/tgbaalgos/magic.cc,
	src/tgbaalgos/reducerun.cc, src/tgbaalgos/se05.cc,
	src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Fix these.

834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
2011-03-31  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Make state_explicit instances persistent objects.

	* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Merge
	state_explicit and tgba_explicit::state.  In the past,
	state_explicit was a small object encapsulating a pointer to the
	persistent tgba_explicit::state; and we used to clone() and
	destroy() a lot of state_explicit instance.  Now state_explicit is
	persistent, and clone() and destroy() have no effects.
	* src/tgba/tgbareduce.cc: Adjust, since this inherits from
	tgbaexplicit and uses the internals of state_explicit.
	* src/tgbatest/reductgba.cc: Fix deletion order for automata.
	* src/tgba/tgba.hh (last_support_conditions_input_,
	last_support_variables_input_): Make these protected, so
	they can be zeroed by tgba_explicit.

851
852
853
854
855
856
857
858
2011-03-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Remove tgba_reduc::format_state().

	* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh (format_state):
	Remove this useless copy of the tgba_explicit_string::format_state
	method.

859
860
861
862
863
864
865
866
867
2011-03-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Protect the state destructor.

	Client code should always call the destroy() method instead.  (It
	was introduced in Spot 0.7.)

	* src/tgba/state.hh (state::~state): Make it protected.

868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
2011-03-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Speedup tgba_product when one of the argument is a Kripke structure.

	The gain is not very impressive.  The runtime of the first example
	in iface/dve2/README (also in dve2check.test) is 15% faster.

	* src/tgba/tgbaproduct.hh (tgba_succ_iterator_product): Move ...
	* src/tgba/tgbaproduct.cc (tgba_succ_iterator_product,
	tgba_succ_iterator_product_common): ... in these two classes.
	(tgba_succ_iterator_product_kripke): New class to speedup
	successor computation on Kripke structures.  We can assume that
	all the transitions leaving the same state have the same label.
	(tgba_product::tgba_product, tgba_product::succ_iter): Use
	tgba_succ_iterator_product_kripke when appropriate.
	(tgba_product_init::tgba_product_init): Adjust for the case
	where tgba_product did reverse its operands.

886
887
888
889
2011-03-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2check.cc: Remove stray debug output.

890
891
892
893
2011-03-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/tgba/tgbaproduct.hh: Do not include statebdd.hh.

894
895
896
897
898
899
900
901
902
903
2011-03-29  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Include <cstddef> in python modules to workaround Swig bug.

	* wrap/python/spot.i, wrap/python/buddy.i: Include <cstddef>
	because Swig 2.0.2 uses ptrdiff_t and does not do the include
	itself.  In g++ most libstdc++ standard headers have been changed
	to no longer include <cstddef> as an implementation detail, so
	the difference shows.

904
905
906
907
2011-03-20  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* THANKS: Add Michael Weber for his help on the DiVinE interface.

908
909
910
911
2011-03-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/ltltest/genltl.cc (syntax): Typos in the help text.

912
913
914
915
916
917
918
919
920
2011-03-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Improve a reduction rule for "a M b".

	* src/ltlvisit/reduce.cc (reduce_visitor): Always reduce "a M b"
	to "a & b" if "a" is a pure eventual formula, remove the
	constraint on "b".
	* src/ltltest/reduccmp.test: Add two tests.

921
922
923
924
2011-03-11  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Mention recent changes to dotty_reachable.

925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
2011-03-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add support for finite behaviors in the DVE interface.

	* iface/dve2/dve2.hh (load_dve2): Take a "dead" argument.
	* iface/dve2/dve2.cc (callback_context): Add a destructor
	to simplify...
	(dve2_succ_iterator::~dve2_succ_iterator) ... this one.
	(convert_aps): Skip the dead proposition.
	(dve2_kripke::dve2_kripke): Take a dead argument, and
	setup alive_prop and dead_prop.
	(compute_state_condition, get_succ): Use a cache for the
	conditions and successor of the last state, to share
	some work between these two function.  Add loops on dead
	states.
	(load_dve2): Pass dead to dve2_kripke and convert_aps.
	* iface/dve2/dve2check.cc: Add a -dDEAD option.
	* iface/dve2/finite.test, iface/dve2/finite.dve: New file.
	* iface/dve2/Makefile.am: Declare them.

945
946
947
948
949
2011-03-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2.cc (convert_aps): Fix two typos while
	parsing >= and >, mistakenly registered as <= and <.

950
951
952
953
954
955
956
957
958
2011-03-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Remove the Nips interface.

	* NEWS: Mention it.
	* configure.ac, README: Remove it.
	* iface/Makefile.am (SUBDIRS): Remove nips.
	* iface/nips/: Delete this directory.

959
960
961
962
963
964
965
966
967
2011-03-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Accept "P_0 == CS" as synonym for "P_0.CS" in the dve2 interface.
	Suggested by Yann Thierry-Mieg.

	* iface/dve2/dve2.cc (convert_aps): Allow string on the right
	of operators, and look them up.
	* iface/dve2/dve2check.test: Test this syntax.

968
969
970
971
972
973
974
975
976
2011-03-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Add some tests for the DVE2 interface.

	* iface/dve2/defs.in, iface/dve2/dve2check.test,
	iface/dve2/beem-peterson.4.dve: New files.
	* iface/dve2/Makefile.am: Add them.
	* configure.ac: Generate iface/dve2/defs.

977
978
979
980
981
982
983
2011-03-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Clear the timer map to help valgrind.

	* src/misc/timer.hh (reset_all): New method.
	* iface/dve2/dve2check.cc: Use it to help valgrind.

984
985
986
987
988
989
990
2011-03-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Some documentation of about the dve2 interface.

	* iface/dve2/README: New file.
	* NEWS: Mention it.

991
992
993
994
995
2011-03-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/dve2.cc, iface/dve2/dve2check.cc: Cosmetic changes
	to please sanity checks.

996
997
998
999
1000
2011-03-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Call divine to compile dve models.

	* iface/dve2/dve2.cc (compile_dve2): New function.  Compile