ChangeLog 398 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
2012-03-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	python: fix return value of emptiness_check_instantiator

	* wrap/python/spot.i: Fix typemap for
	emptiness_check_instantiator::construct.  The previous code used
	to turn (None, "error") into simply ("error").
	* wrap/python/ajax/spot.in: Fix handling or errors when
	instantiating emptiness checks.

11
12
13
14
2012-02-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Summarize recent changes.

15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
2012-02-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Make all python code compatible with Python 2.x and Python 3.x.

	* wrap/python/buddy.i (__le__, __lt__, __eq__, __ne__, __ge__
	__gt__): New operators for bdd.
	* wrap/python/spot.i (__le__, __lt__, __eq__, __ne__, __ge__
	__gt__, __hash__): New operators for formula.
	(nl_cout, nl_cerr): New functions.
	* wrap/python/tests/bddnqueen.py,
	wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py,
	wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py,
	wrap/python/tests/minato.py, wrap/python/tests/modgray.py: Adjust
	to the new print syntax by using sys.output.write() or nl_cout()
	instead.
	* wrap/python/tests/optionmap.py: Remove all print calls.
	* wrap/python/ajax/spot.in: Massive adjustments in order to work
	with both Python 2 and 3.  In python 3, reopening stdout as
	unbuffered requires it to be open as binary, which in turns
	requires any string output to be encoded manually.  BaseHTTPServer
	and CGIHTTPServer have been merged into http.server, so we have
	to try two different import syntaxes.  execfile no longer exists,
	so it has to be emulated.
	This also fixes two bugs where the script would segfault on
	empty input, or when calling Tau03 on automata with less then
	one acceptance conditions.

42
43
44
45
46
47
48
2012-02-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix computation of PYTHONINC for Python 3.

	* m4/pypath.m4: The print syntax changed in Python 3, so use
	sys.stdout.write for compatibility with all versions.

49
50
51
52
2012-02-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* HACKING: Minor updates and corrections.

53
54
55
56
57
58
59
60
61
62
2012-02-15  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix a race condition on the CGI script.

	* wrap/python/ajax/spot.in: Create all cache files in a temporary
	directory, and only rename this directory at the end.  This way if
	two processes are processing the same request, they won't attempt
	to populate the same directory (and only one of the first of two
	renames will succeed, but that is OK).

63
64
65
66
67
68
69
70
71
2012-01-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix a segfault reported by Etienne Renault using dve2check.

	* src/misc/intvcmp2.cc (stream_compression_base::run): Fix a case
	where the "id" of the compression to use would be miscalculated,
	causing wrong values to be encoded.
	* src/tgbatest/intvcmp2.cc: Add this particular test case.

72
73
74
75
2012-01-20  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Add missing dates.

76
77
78
79
2012-01-19  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
80
81
82
83
84
85
2012-01-19  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Release Spot 0.8.2.

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

86
87
88
89
90
91
92
2012-01-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Small speedup in safra_tree::compare().

	* src/tgba/tgbasafracomplement.cc (safra_tree::compare): Improve
	the order of the tests.

93
94
95
96
2012-01-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Mention the last two changes.

97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
2012-01-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Implement a unicity table for states created by tgba_tba_proxy.

	Suggested by Nikos Gorogiannis.

	* src/tgba/tgbatba.hh (tgba_tba_proxy::create_state): New method.
	(tgba_tba_proxy::uniq_map_): New attribute.
	* src/tgba/tgbatba.cc (state_tba_proxy): Use the default
	copy constructor.  Empty the destructor.  Implement an empty
	destroy() method.  Use addresses for comparison.  Make clone()
	a no-op.
	(tgba_tba_proxy): Allocate and deallocate the unicity table.
	Implement create_sates().
	(tgba_tba_proxy, tgba_sba_proxy, tgba_tba_proxy_succ_iterator):
	Adjust state construction to call create_state().

114
115
116
117
118
119
120
121
122
2012-01-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Minor speedups in tgba_safra_complement().

	* src/tgba/tgbasafracomplement.cc (safra_tree:succ_create): Do not
	lookup *i twice, and do not copy it->second.
	(safra_tree::normalize_siblings): Do not lookup *node_it before
	insertion.

123
124
125
126
127
2012-01-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* src/eltlparse/eltlparse.yy (realias): Add a useless return to
	fix a g++ warning.

128
129
130
131
2012-01-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* bench/ltlclasses/run: Typo in comment.

132
133
134
135
136
137
138
139
140
2012-01-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Make it possible not to build Python bindings.

	* configure.ac: Add a --disable-python option tied to
	a USE_PYTHON conditional.
	* README: Document the option.
	* wrap/Makefile.am: Use the conditional.

141
142
143
144
145
146
147
148
2012-01-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix position of the Send button with WebKit.

	* wrap/python/ajax/css/ltl2tgba.css: Fix position of the "Send"
	button with WebKit.  The folding arrow icon had a vertical border
	that overlapped with the next line.

149
150
151
152
153
2012-01-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* wrap/python/ajax/spot.py: Add a required "None" second
	argument to utime().

154
155
156
157
158
159
160
161
162
163
164
2012-01-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	minimize_wdba() failed to fully minimize some automata.

	* src/tgbaalgos/minimize.cc (minimize_wdba): Fix the Löding
	algorithm to use colors.  The previous implementation was an
	incorrect approximation.
	* src/tgbatest/wdba2.test: New file showing two equivalent
	formulas that were minimized in automata with different sizes.
	* src/tgbatest/Makefile.am: Add it.

165
166
167
168
2012-01-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Update with recent fixes.

169
170
171
172
173
174
175
176
177
2012-01-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix a 'make check' failure when valgrind is not installed.

	* src/kripketest/defs.in (run2): Remove this function.  It was
	incorrectly trying to run valgrind even when valgrind is not
	installed.
	* src/kripketest/kripke.test: Simplify and use run().

178
179
180
181
182
183
184
2012-01-12  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Do use of tr1::unordered_map with G++ 4.0.0.

	* m4/stl.m4 (AC_HEADER_TR1_UNORDERED_MAP): Add some code so
	we don't pick a broken tr1::unordered_map.

185
186
187
188
2012-01-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* lrde-upload.sh: Retrieve the package version from configure.ac.

189
190
191
192
193
194
195
196
197
2012-01-05  Ala-Eddine Ben-Salem  <ala@lrde.epita.fr>

	Fix detection of the last iteration of minimize_dfa().

	* src/tgbaalgos/minimize.cc (minimize_dfa): Fix detection of the
	last iteration.  An extra iteration case could be missed in case
	where a split generates only singletons, and yet predecessor
	classes need to be refined.

198
199
200
201
202
203
204
205
206
207
208
209
2012-01-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix computation of length of LTL formulas.

	* src/ltlvisit/length.cc: Fix computation for ltl::multop
	operator. "a&b&c" was reported with length 3, ignoring the
	"&" operators, because of a typo.
	* src/ltlvisit/length.hh: Fix description to correctly
	reflect this change intended since 2010-01-22.
	* src/ltltest/length.test, src/ltltest/length.cc: New files.
	* src/ltltest/Makefile.am: Add them.

210
211
212
213
2011-12-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
214
215
216
217
218
219
2011-12-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Release Spot 0.8.1.

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

220
221
222
223
2011-12-18  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Summarize recent fixes.

224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
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.

243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
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.

260
261
262
263
264
265
266
267
268
269
270
271
272
273
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.

274
275
276
277
278
279
280
281
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
282
283
284
285
286
287
288
289
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.

290
291
292
293
2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* AUTHORS: Sort alphabetically.

294
295
296
297
298
299
300
301
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.

302
303
304
305
306
307
308
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.

309
310
311
312
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
313
314
315
316
317
318
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
319
320
321
322
323
324
325
326
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.

327
328
329
330
331
332
333
2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Fix some Doxygen errors.

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

334
335
336
337
338
339
340
341
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.

342
343
344
345
2011-11-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Mention the Kripke I/O.

346
347
348
349
350
351
352
353
354
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.

355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
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.

376
377
378
379
2011-11-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* AUTHORS: Add Thomas Badie.

380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
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.

405
406
407
408
409
410
411
412
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.

413
414
415
416
417
418
419
420
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
421
422
423
424
425
426
427
428
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.

429
430
431
432
433
434
435
436
437
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.

438
439
440
441
2011-11-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Add an entry for the previous fix.

442
443
444
445
446
447
448
449
450
451
452
453
454
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.

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

463
464
465
466
467
468
469
470
471
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.

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

479
480
481
482
2011-10-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

483
484
485
486
2011-10-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Update with recent fixes.

487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
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.

507
508
509
510
2011-10-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

511
512
513
514
515
516
517
518
519
520
521
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.

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

537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
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.

560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
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.

575
576
577
578
579
580
581
582
583
584
585
586
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.

587
588
589
590
591
592
593
594
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.

595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
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
613
614
615
616
617
618
619
2011-08-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	Please GCC 4.6.

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

620
621
622
623
624
625
626
627
628
629
630
631
632
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.

633
634
635
636
2011-08-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

637
638
639
640
2011-07-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

641
642
643
644
645
646
647
648
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.

649
650
651
652
653
654
655
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.

656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
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.

673
674
675
676
2011-06-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

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

685
686
687
688
689
2011-06-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

690
691
692
693
2011-06-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* NEWS: Update with recent changes.

694
695
696
697
698
699
700
701
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.

702
703
704
705
706
707
708
709
710
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.

711
712
713
714
715
716
717
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.

718
719
720
721
722
723
724
725
726
727
728
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.

729
730
731
732
2011-06-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

733
734
735
736
2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

737
738
739
740
2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

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

753
754
755
756
757
758
759
760
761
762
763
764
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.

765
766
767
768
769
770
771
772
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".

773
774
775
776
777
778
779
780
781
782
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.

783
784
785
786
787
788
789
790
791
792
793
794
795
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.

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

803
804
805
806
2011-06-02  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* iface/dve2/README: Document state compression.

807
808
809
810
811
812
813
814
815
816
817
818
819
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.

820
821
822
823
2011-05-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

824
825
826
827
2011-05-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* bench/wdba/README: Typos.

828
829
830
831
832
833
834
835
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.

836
837
838
839
840
2011-05-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

841
842
843
844
2011-05-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

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

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

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

868
869
870
871
872
873
874
875
876
877
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.

878
879
880
881
2011-04-15  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

882
883
884
885
886
887
888
889
890
891
892
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.

893
894
895
896
897
898
899
900
901
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.

902
903
904
905
2011-04-11  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

906
907
908
909
910
911
912
913
914
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.

915
916
917
918
919
2011-04-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

920
921
922
923
924
925
926
927
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

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

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

945
946
947
948
2011-04-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

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

949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
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.

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

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

984
985
986
987
2011-04-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	* HACKING: Add an example for using callgrind.

988
989
990
991
992
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.

993
994
995
996
997
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.

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

	* iface/dve2/dve2.cc: Use a fixed-size memory pool for dve2_state
For faster browsing, not all history is shown. View entire blame