ChangeLog 12.6 KB
Newer Older
1
2
2003-05-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
	Implements spot::ltl::destroy() and exercise it.

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

28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
	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.

69
70
71
	* src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to
	remove a warning with newer versions of Flex.

72
73
74
75
76
77
	* 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.

78
79
80
81
82
83
84
85
86
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.

87
88
89
90
91
92
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.

93
94
2003-04-30  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

95
96
	* src/ltlvisit/Makefile.am (lib_LTLIBRARIES): Rename as ...
	(noinst_LTLIBRARIES): ... this.
97
	* src/ltlenv/Makefile.am, src/ltlast/Makefile.am,
98
	src/ltlparse/Makefile.am: Likewise.
99
	* src/Makefile.am (lib_LTLIBRARIES, libspot_la_SOURCES,
100
101
102
	libspot_la_LIBADD): New variable.   Build a libspot.la library
	from all the sub-libraries.

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

109
110
2003-04-29  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

111
	* configure.ac: Call AC_PROG_LIBTOOL.
112
	* src/ltlast/Makefile.am, src/ltlenv/Makefile.am,
113
114
115
	src/ltlparse/Makefile.am, src/ltltest/Makefile.am,
	src/ltlvisit/Makefile.am: Adust to build libtool libraries.

116
117
118
	* src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here...
	* src/ltlenv/defaultenv.cc: ... but here.

119
120
121
	* src/ltltest/tostring.test: Simplify with set -e.  Move the
	description of the test ...
	* src/ltltest/tostring.cc: ... here, where it is actually coded.
122
123
	* src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test,
	src/ltltest/nenoform.test,  src/ltltest/tunenoform.test:
124
125
	Simplify with set -e.

126
	* configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make
127
	sure we always use paths relative to src/ in src/'s
128
129
	subdirectories.

130
131
132
133
134
135
2003-04-28  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

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

136
137
138
139
140
141
142
2003-04-24  Rachid REBIHA  <rebiha@nyx>

	* src/ltltest/tostring.test: New file.
	* src/ltltest/tostring.cc: New files.
	* src/ltlvisit/tostring.hh: From ast to string New files.
	* src/ltlvisit/tostring.cc: From ast to string New files.

143
144
2003-04-18  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

145
146
147
	* src/ltlparse/Makefile.am (EXTRA_DIST): Distribute ltlparse.yy.
	* src/ltlast/Makefile.am (libltlast_a_SOURCES): Add visitor.hh.

148
149
150
151
152
153
154
	* src/ltlast/atomic_prop.hh, src/ltlast/binop.hh,
	src/ltlast/constant.hh, src/ltlast/formula.hh,
	src/ltlast/multop.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh,
	src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh,
	src/ltlparse/public.hh, src/ltlvisit/clone.hh,
	src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh,
	src/ltlvisit/equals.hh, src/ltlvisit/lunabbrev.hh,
155
	src/ltlvisit/nenoform.hh, src/ltlvisit/tunabbrev.hh: Add
156
	Doxygen comments.
157
	* src/visitor.hh: Do not use const_sel.  This clarifies
158
159
	the code and helps Doxygen.

160
161
162
	* configure.ac: Output doc/Doxyfile and doc/Makefile.
	* doc/Makefile.am, doc/Doxyfile.in: New files.
	* Makefile.am (SUBDIRS): Add doc.
163

164
	* src/ltlparse/ltlscan.ll: Recognize && and ||.
165
	* src/ltltest/parse.test, src/ltltest/parseerr.test,
166
167
	src/ltltest/equals.test: Use these operators..

168
169
2003-04-17  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

170
171
	* src/ltltest/readltl.cc, src/ltltest/equals.cc: Cosmetics.

172
173
174
175
176
177
178
179
	* src/ltlenv/environment.hh (require): Return a formula, not
	an atomic_prop.
	* src/ltlast/atomic_prop.hh (atomic_prop): New argument env.
	(environment_): New member.
	(env): New method.
	* src/ltlast/atomic_prop.cc (atomic_prop, env): Likewise.
	* src/ltlenv/defaultenv.cc (require): Pass *this as the
	environment argument to atomic_prop.
180
	* src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy
181
182
	the environment.
	* src/ltlvisit/nenoform.cc (visit(const atomic_prop*)): Likewise.
183

184
185
186
187
188
189
190
191
192
193
	* configure.ac: Output src/ltlenv/Makefile.
	* src/ltlenv/Makefile.am, src/ltlenv/defaultenv.cc,
	src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh: New files.
	* src/ltlparse/public.hh (parse): Take an environment as third
	argument.
	* src/ltlparse/ltlparse.yy (ATOMIC_PROP, parse): Require the
	atomic proposition via the environment.
	* src/ltltest/readltl.cc (main): Adjust the call to parse().
	* src/ltltest/Makefile.am (LDADD): Add ../ltlenv/libltlenv.a.

194
195
196
197
198
	* src/ltlvisit/clone.hh, src/ltlvisit/clone.cc: New files.
	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
	* src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Inherit
	from clone_visitor and remove all useless methods (now inherited).

199
200
201
202
203
204
	* src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: New files.
	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
	* src/ltltest/equals.cc (main) [NENOFORM]: Call negative_normal_form.
	* src/ltltest/nenoform.test, src/ltltest/tunenoform.test: New files.
	* src/ltltest/Makefile.am (check_PROGRAMS): Add nenoform and
	tunenoform.
205
	(nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES,
206
207
208
	tunenoform_CPPFLAGS): New variables.
	(TESTS): Add nenoform.test and tunenoform.test.

209
210
	* src/ltlvisit/lunabbrev.hh: Fix include guard.

211
2003-04-16  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
212

213
214
215
216
217
218
219
220
221
222
223
224
	* src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: New files.
	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
	* src/ltltest/tunabbrev.test: New file.
	* src/ltltest/lunabbrev.test: Fix comment.
	* src/ltltest/Makefile.am (TESTS): Add tunabbrev.test.
	(check_PROGRAMS): Add tunabbrev.
	(tunabbrev_SOURCES, tunabbrev_CPPFLAGS): New variables.
	* src/ltltest/equals.cc (main) [TUNABBREV]: Call unabbreviate_ltl.
	* src/ltlvisit/lunabbrev.hh (unabbreviate_logic_visitor::recurse):
	New virtual function.
	* src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::recurse):
	Likewise.
225
	(unabbreviate_logic_visitor::visit): Use it instead of calling
226
227
	unabbreviate_logic directly.

228
229
	* src/ltlvisit/lunabbrev.hh: Add missing include guard.

230
231
232
233
234
235
236
237
238
239
	* src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: New files.
	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
	* src/ltlast/multop.cc (multop::multop(type)): New constructor.
	* src/ltlast/multop.hh (multop::multop(type)): New constructor.
	* src/ltltest/lunabbrev.test: New file.
	* src/ltltest/Makefile.am (TESTS): Add lunabbrev.test.
	(check_PROGRAMS): Add lunabbrev.
	(lunabbrev_SOURCES, lunabbrev_CPPFLAGS): New variables.
	* src/ltltest/equals.cc (main) [LUNABBREV]: Call unabbreviate_logic.

240
241
242
	* src/ltltest/equals.test (check0, check1): Remove. Use check 0, and
	check 1 instead.

243
244
245
246
247
248
	* src/ltlast/formulae.hh: Rename as ...
	* src/ltlast/formula.hh: ... this.
	* src/ltlast/Makefile.am (libltlast_a_SOURCES): Adjust.
	* src/ltlast/formula.hh (formulae): Rename as ...
	(formula): ... this.
	Adjust all uses.
249

250
251
252
253
254
255
	* src/ltlparse/public.hh (format_parse_errors): New function.
	* src/ltlparse/fmterror.cc: New file.
	* src/ltlparse/Makefile.am (libltlparse_a_SOURCES): Add fmterror.cc.
	* src/ltltests/equals.cc, src/ltltests/readltl.cc: Simplify using
	format_parse_errors.

256
257
258
259
260
261
262
263
	* src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: New files.
	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add equals.hh
	and equals.cc.
	* src/ltltest/equals.cc, src/ltltest/equals.test: New files.
	* src/ltltest/Makefile.am (check_PROGRAMS): Add equals.
	(equals_SOURCES): New variable.
	(TESTS): Add equals.test.

264
	* src/ltlast/multop.cc (multop::multop): Use multop::add.
265
	(multop::add): If the formulae we add is itself a multop for the
266
267
268
	same operator, merge its children with ours.
	* src/ltltest/parseerr.test: Add two tests for multop merging.

269
270
2003-04-15  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

271
272
273
274
275
276
277
278
279
280
281
282
	* src/ltlast/formulae.hh (formulae::equals): Remove.
	* src/ltlast/unop.hh (unop::equals): Remove.
	* src/ltlast/unop.cc (unop::equals): Remove.
	* src/ltlast/binop.hh (binop::equals): Remove.
	* src/ltlast/binop.cc (binop::equals): Remove.
	* src/ltlast/multop.hh (multop::equals): Remove.
	* src/ltlast/multop.cc (multop::equals): Remove.
	* src/ltlast/atomic_prop.hh (atomic_prop::equals): Remove.
	* src/ltlast/atomic_prop.cc (atomic_prop::equals): Remove.
	* src/ltlast/constant.hh (constant::equals): Remove.
	* src/ltlast/constant.cc (constant::equals): Remove.

283
284
285
286
287
288
289
290
291
292
293
294
295
	* HACKING, Makefile.am, configure.ac, m4/gccwarn.m4,
	src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
	src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
	src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
	src/ltlast/constant.hh, src/ltlast/formulae.hh,
	src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/predecl.hh,
	src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/visitor.hh,
	src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy,
	src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
	src/ltlparse/public.hh, src/ltlvisit/Makefile.am,
	src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
	src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
	src/ltlvisit/rewrite.cc, src/ltlvisit/rewrite.hh,
296
297
	src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc,
	src/ltltest/parse.test, src/ltltest/parseerr.test,
298
	src/misc/Makefile.am, src/misc/const_sel.hh: New files.