ChangeLog 9.32 KB
Newer Older
1
2
3
4
5
6
7
8
2003-05-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>

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

9
10
11
12
13
14
15
16
17
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.

18
19
20
21
22
23
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.

24
25
2003-04-30  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

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

34
35
36
37
38
39
	* 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.

40
41
2003-04-29  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

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

47
48
49
	* src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here...
	* src/ltlenv/defaultenv.cc: ... but here.

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

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

61
62
63
64
65
66
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.

67
68
69
70
71
72
73
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.

74
75
2003-04-18  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

76
77
78
	* src/ltlparse/Makefile.am (EXTRA_DIST): Distribute ltlparse.yy.
	* src/ltlast/Makefile.am (libltlast_a_SOURCES): Add visitor.hh.

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

91
92
93
	* configure.ac: Output doc/Doxyfile and doc/Makefile.
	* doc/Makefile.am, doc/Doxyfile.in: New files.
	* Makefile.am (SUBDIRS): Add doc.
94

95
	* src/ltlparse/ltlscan.ll: Recognize && and ||.
96
	* src/ltltest/parse.test, src/ltltest/parseerr.test,
97
98
	src/ltltest/equals.test: Use these operators..

99
100
2003-04-17  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

101
102
	* src/ltltest/readltl.cc, src/ltltest/equals.cc: Cosmetics.

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

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

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

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

140
141
	* src/ltlvisit/lunabbrev.hh: Fix include guard.

142
2003-04-16  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
143

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

159
160
	* src/ltlvisit/lunabbrev.hh: Add missing include guard.

161
162
163
164
165
166
167
168
169
170
	* 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.

171
172
173
	* src/ltltest/equals.test (check0, check1): Remove. Use check 0, and
	check 1 instead.

174
175
176
177
178
179
	* 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.
180

181
182
183
184
185
186
	* 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.

187
188
189
190
191
192
193
194
	* 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.

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

200
201
2003-04-15  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

202
203
204
205
206
207
208
209
210
211
212
213
	* 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.

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