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

3
4
5
	* src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to
	remove a warning with newer versions of Flex.

6
7
8
9
10
11
	* 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.

12
13
14
15
16
17
18
19
20
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.

21
22
23
24
25
26
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.

27
28
2003-04-30  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

29
30
	* src/ltlvisit/Makefile.am (lib_LTLIBRARIES): Rename as ...
	(noinst_LTLIBRARIES): ... this.
31
	* src/ltlenv/Makefile.am, src/ltlast/Makefile.am,
32
	src/ltlparse/Makefile.am: Likewise.
33
	* src/Makefile.am (lib_LTLIBRARIES, libspot_la_SOURCES,
34
35
36
	libspot_la_LIBADD): New variable.   Build a libspot.la library
	from all the sub-libraries.

37
38
39
40
41
42
	* 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.

43
44
2003-04-29  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

45
	* configure.ac: Call AC_PROG_LIBTOOL.
46
	* src/ltlast/Makefile.am, src/ltlenv/Makefile.am,
47
48
49
	src/ltlparse/Makefile.am, src/ltltest/Makefile.am,
	src/ltlvisit/Makefile.am: Adust to build libtool libraries.

50
51
52
	* src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here...
	* src/ltlenv/defaultenv.cc: ... but here.

53
54
55
	* src/ltltest/tostring.test: Simplify with set -e.  Move the
	description of the test ...
	* src/ltltest/tostring.cc: ... here, where it is actually coded.
56
57
	* src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test,
	src/ltltest/nenoform.test,  src/ltltest/tunenoform.test:
58
59
	Simplify with set -e.

60
	* configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make
61
	sure we always use paths relative to src/ in src/'s
62
63
	subdirectories.

64
65
66
67
68
69
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.

70
71
72
73
74
75
76
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.

77
78
2003-04-18  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

79
80
81
	* src/ltlparse/Makefile.am (EXTRA_DIST): Distribute ltlparse.yy.
	* src/ltlast/Makefile.am (libltlast_a_SOURCES): Add visitor.hh.

82
83
84
85
86
87
88
	* 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,
89
	src/ltlvisit/nenoform.hh, src/ltlvisit/tunabbrev.hh: Add
90
	Doxygen comments.
91
	* src/visitor.hh: Do not use const_sel.  This clarifies
92
93
	the code and helps Doxygen.

94
95
96
	* configure.ac: Output doc/Doxyfile and doc/Makefile.
	* doc/Makefile.am, doc/Doxyfile.in: New files.
	* Makefile.am (SUBDIRS): Add doc.
97

98
	* src/ltlparse/ltlscan.ll: Recognize && and ||.
99
	* src/ltltest/parse.test, src/ltltest/parseerr.test,
100
101
	src/ltltest/equals.test: Use these operators..

102
103
2003-04-17  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

104
105
	* src/ltltest/readltl.cc, src/ltltest/equals.cc: Cosmetics.

106
107
108
109
110
111
112
113
	* 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.
114
	* src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy
115
116
	the environment.
	* src/ltlvisit/nenoform.cc (visit(const atomic_prop*)): Likewise.
117

118
119
120
121
122
123
124
125
126
127
	* 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.

128
129
130
131
132
	* 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).

133
134
135
136
137
138
	* 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.
139
	(nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES,
140
141
142
	tunenoform_CPPFLAGS): New variables.
	(TESTS): Add nenoform.test and tunenoform.test.

143
144
	* src/ltlvisit/lunabbrev.hh: Fix include guard.

145
2003-04-16  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
146

147
148
149
150
151
152
153
154
155
156
157
158
	* 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.
159
	(unabbreviate_logic_visitor::visit): Use it instead of calling
160
161
	unabbreviate_logic directly.

162
163
	* src/ltlvisit/lunabbrev.hh: Add missing include guard.

164
165
166
167
168
169
170
171
172
173
	* 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.

174
175
176
	* src/ltltest/equals.test (check0, check1): Remove. Use check 0, and
	check 1 instead.

177
178
179
180
181
182
	* 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.
183

184
185
186
187
188
189
	* 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.

190
191
192
193
194
195
196
197
	* 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.

198
	* src/ltlast/multop.cc (multop::multop): Use multop::add.
199
	(multop::add): If the formulae we add is itself a multop for the
200
201
202
	same operator, merge its children with ours.
	* src/ltltest/parseerr.test: Add two tests for multop merging.

203
204
2003-04-15  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

205
206
207
208
209
210
211
212
213
214
215
216
	* 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.

217
218
219
220
221
222
223
224
225
226
227
228
229
	* 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,
230
231
	src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc,
	src/ltltest/parse.test, src/ltltest/parseerr.test,
232
	src/misc/Makefile.am, src/misc/const_sel.hh: New files.