Makefile.am 10.7 KB
Newer Older
1
## -*- coding: utf-8 -*-
2
3
4

## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
## Laboratoire de Recherche et Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
5
## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
6
7
## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
## Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
8
9
10
11
12
##
## This file is part of Spot, a model checking library.
##
## Spot is free software; you can redistribute it and/or modify it
## under the terms of the GNU General Public License as published by
13
## the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
14
15
16
17
18
19
20
21
## (at your option) any later version.
##
## Spot is distributed in the hope that it will be useful, but WITHOUT
## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
## or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
## License for more details.
##
## You should have received a copy of the GNU General Public License
22
## along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
23

24
AUTOMAKE_OPTIONS = subdir-objects
25
AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
26
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
27
LDADD = $(top_builddir)/spot/libspot.la
28

29
TEST_EXTENTIONS = .test .py .ipynb .pl
30
31
32
33
34

LOG_COMPILER = ./run
TEST_LOG_COMPILER = ./run
LOG_DRIVER = $(TEST_LOG_DRIVER)
# ensure run is rebuilt before the tests are run.
35
36
37
check_SCRIPTS = run

# We try to keep this somehow by strength.  Test basic things first,
38
39
40
41
42
43
44
# because such failures will be easier to diagnose and fix.  The only
# exception is that we keep TESTS_python at the beginning, because if
# these tests are run at the same time as some heavy tests in
# TESTS_twa they can easily fail due to some timeout in the Jupyter
# communications.
TESTS = $(TESTS_sanity) $(TESTS_python) $(TESTS_misc) $(TESTS_tl) \
  $(TESTS_graph) $(TESTS_kripke) $(TESTS_twa) $(TESTS_ltsmin)
45
46

distclean-local:
47
	find . -name '*.dir' -type d -print | xargs rm -rf
48
49
50
51
52
53
## This is crazy: Even if the python test suite passes without
## reporting an error, it can non-deterministically leave a coredump
## behind.  This happens with ipython 4.0.1 on ArchLinux; ipython
## somehow recovers from this so the only annoyance is that it can
## leave a coredump behind.
	rm -f python/core
54
55
56
57
58
59
60
61
62


############################## CORE ##############################

check_SCRIPTS += core/defs

core/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in
	$(top_builddir)/config.status --file core/defs

63
64
# Keep this sorted alphabetically.
check_PROGRAMS = \
65
66
67
68
69
70
71
72
73
74
  core/acc \
  core/bitvect \
  core/checkpsl \
  core/checkta \
  core/consterm \
  core/emptchk \
  core/equals \
  core/graph \
  core/kind \
  core/length \
75
  core/ikwiad \
76
77
  core/intvcomp \
  core/intvcmp2 \
78
  core/kripkecat \
79
80
81
82
83
84
85
86
  core/ltlprod \
  core/ltl2dot \
  core/ltl2text \
  core/ltlrel \
  core/lunabbrev \
  core/nequals \
  core/nenoform \
  core/ngraph \
87
  core/randtgba \
88
89
90
91
92
  core/readsat \
  core/reduc \
  core/reduccmp \
  core/reduceu \
  core/reductaustr \
93
  core/safra \
94
95
  core/syntimpl \
  core/taatgba \
96
  core/trival \
97
98
99
100
  core/tgbagraph \
  core/tostring \
  core/tunabbrev \
  core/tunenoform
101

102
# Keep this sorted alphabetically.
103
104
105
106
107
108
109
110
111
core_acc_SOURCES = core/acc.cc
core_bitvect_SOURCES  = core/bitvect.cc
core_checkpsl_SOURCES = core/checkpsl.cc
core_checkta_SOURCES = core/checkta.cc
core_emptchk_SOURCES  = core/emptchk.cc
core_graph_SOURCES = core/graph.cc
core_ikwiad_SOURCES = core/ikwiad.cc
core_intvcomp_SOURCES = core/intvcomp.cc
core_intvcmp2_SOURCES = core/intvcmp2.cc
112
core_kripkecat_SOURCES = core/kripkecat.cc
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
core_ltlprod_SOURCES  = core/ltlprod.cc
core_ngraph_SOURCES = core/ngraph.cc
core_randtgba_SOURCES = core/randtgba.cc
core_readsat_SOURCES = core/readsat.cc
core_taatgba_SOURCES = core/taatgba.cc
core_tgbagraph_SOURCES = core/twagraph.cc
core_consterm_SOURCES = core/consterm.cc
core_equals_SOURCES = core/equalsf.cc
core_kind_SOURCES = core/kind.cc
core_length_SOURCES = core/length.cc
core_ltl2dot_SOURCES = core/readltl.cc
core_ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
core_ltl2text_SOURCES = core/readltl.cc
core_ltlrel_SOURCES = core/ltlrel.cc
core_lunabbrev_SOURCES = core/equalsf.cc
core_lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ie"'
core_nenoform_SOURCES = core/equalsf.cc
core_nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
core_nequals_SOURCES = core/equalsf.cc
core_nequals_CPPFLAGS = $(AM_CPPFLAGS) -DNEGATE
core_reduc_SOURCES = core/reduc.cc
core_reduccmp_SOURCES = core/equalsf.cc
core_reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC
core_reduceu_SOURCES = core/equalsf.cc
core_reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV
core_reductaustr_SOURCES = core/equalsf.cc
core_reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR
140
core_safra_SOURCES = core/safra.cc
141
142
core_syntimpl_SOURCES = core/syntimpl.cc
core_tostring_SOURCES = core/tostring.cc
143
core_trival_SOURCES = core/trival.cc
144
145
146
147
core_tunabbrev_SOURCES = core/equalsf.cc
core_tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ieFG"'
core_tunenoform_SOURCES = core/equalsf.cc
core_tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DUNABBREV='"^ieFG"'
148

149

150
151
152
153
154
155
156
157
TESTS_tl = \
  core/bare.test \
  core/parse.test \
  core/parseerr.test \
  core/utf8.test \
  core/length.test \
  core/equals.test \
  core/tostring.test \
158
  core/genltl.test \
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
  core/lunabbrev.test \
  core/tunabbrev.test \
  core/nenoform.test \
  core/tunenoform.test \
  core/unabbrevwm.test \
  core/consterm.test \
  core/kind.test \
  core/remove_x.test \
  core/ltlrel.test \
  core/ltlgrind.test \
  core/ltlcrossgrind.test \
  core/ltlfilt.test \
  core/exclusive-ltl.test \
  core/latex.test \
  core/lbt.test \
  core/lenient.test \
  core/rand.test \
  core/isop.test \
  core/syntimpl.test \
  core/reduc.test \
  core/reduc0.test \
  core/reducpsl.test \
  core/reduccmp.test \
  core/uwrm.test \
  core/eventuniv.test \
184
185
  core/stutter-ltl.test \
  core/format.test
186
187

TESTS_graph = \
188
189
190
  core/graph.test \
  core/ngraph.test \
  core/tgbagraph.test
191
192

TESTS_kripke = \
193
  core/kripke.test
Etienne Renault's avatar
Etienne Renault committed
194

195
196
197
TESTS_misc = \
  core/bitvect.test \
  core/intvcomp.test \
198
  core/minusx.test \
199
  core/full.test \
200
201
  core/trival.test

Etienne Renault's avatar
Etienne Renault committed
202
TESTS_twa = \
203
204
  core/acc.test \
  core/acc2.test \
205
  core/alternating.test \
206
207
208
209
210
  core/ltlcross3.test \
  core/taatgba.test \
  core/renault.test \
  core/nondet.test \
  core/det.test \
211
  core/semidet.test \
212
213
214
215
216
217
  core/neverclaimread.test \
  core/parseaut.test \
  core/optba.test \
  core/complete.test \
  core/complement.test \
  core/remfin.test \
218
  core/gragsa.test \
219
220
221
222
223
224
225
226
227
228
229
  core/dstar.test \
  core/readsave.test \
  core/ltldo.test \
  core/ltldo2.test \
  core/maskacc.test \
  core/maskkeep.test \
  core/prodor.test \
  core/simdet.test \
  core/sim2.test \
  core/sim3.test \
  core/ltl2tgba.test \
230
  core/ltl2tgba2.test \
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
  core/ltl2neverclaim.test \
  core/ltl2neverclaim-lbtt.test \
  core/ltlprod.test \
  core/explprod.test \
  core/explpro2.test \
  core/explpro3.test \
  core/explpro4.test \
  core/tripprod.test \
  core/dupexp.test \
  core/exclusive-tgba.test \
  core/remprop.test \
  core/degendet.test \
  core/degenid.test \
  core/degenlskip.test \
  core/randomize.test \
  core/lbttparse.test \
  core/scc.test \
  core/sccdot.test \
  core/sccsimpl.test \
  core/sepsets.test \
  core/dbacomp.test \
  core/obligation.test \
  core/wdba.test \
  core/wdba2.test \
  core/babiak.test \
  core/monitor.test \
  core/dra2dba.test \
  core/unambig.test \
  core/ltlcross4.test \
260
  core/ltl3ba.test \
261
  core/streett.test \
262
263
264
265
266
267
268
269
270
271
  core/ltl3dra.test \
  core/ltl2dstar.test \
  core/ltl2dstar2.test \
  core/ltl2dstar3.test \
  core/ltl2dstar4.test \
  core/ltl2ta.test \
  core/ltl2ta2.test \
  core/randaut.test \
  core/randtgba.test \
  core/isomorph.test \
272
  core/included.test \
273
  core/uniq.test \
274
  core/safra.test \
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
  core/sbacc.test \
  core/stutter-tgba.test \
  core/strength.test \
  core/emptchk.test \
  core/emptchke.test \
  core/dfs.test \
  core/ltlcrossce.test \
  core/ltlcrossce2.test \
  core/emptchkr.test \
  core/ltlcounter.test \
  core/basimul.test \
  core/satmin.test \
  core/satmin2.test \
  core/spotlbtt.test \
  core/ltlcross.test \
  core/spotlbtt2.test \
  core/ltlcross2.test \
  core/complementation.test \
  core/randpsl.test \
294
295
  core/cycles.test \
  core/acc_word.test
296

297
298

############################## PYTHON ##############################
299

300
if USE_PYTHON
301
302
303
304

# TESTS_ipython contains notebooks that we also want to publish as
# part of the documentation.
TESTS_ipython = \
305
306
  python/acc_cond.ipynb \
  python/accparse.ipynb \
307
  python/alternation.ipynb \
308
309
  python/atva16-fig2a.ipynb \
  python/atva16-fig2b.ipynb \
310
  python/automata-io.ipynb \
311
  python/automata.ipynb \
312
313
  python/decompose.ipynb \
  python/formulas.ipynb \
314
  python/highlighting.ipynb \
315
  python/ltsmin-dve.ipynb \
316
  python/ltsmin-pml.ipynb \
317
318
319
320
  python/piperead.ipynb \
  python/product.ipynb \
  python/randaut.ipynb \
  python/randltl.ipynb \
321
322
  python/testingaut.ipynb \
  python/word.ipynb
323
324
325
326
327
328

# TESTS_python contains all tests.  It may includes notebooks we
# do not consider part of the documentation: those have to start
# with a _.
TESTS_python = \
  python/_aux.ipynb \
329
  python/_altscc.ipynb \
330
331
  python/accparse2.py \
  python/alarm.py \
332
  python/alternating.py \
333
  python/bddnqueen.py \
334
  python/bugdet.py \
335
336
337
  python/implies.py \
  python/interdep.py \
  python/ltl2tgba.test \
338
  python/ltlf.py \
339
340
341
342
  python/ltlparse.py \
  python/ltlsimple.py \
  python/minato.py \
  python/optionmap.py \
343
  python/otfcrash.py \
344
  python/parsetgba.py \
345
  python/prodexpt.py \
346
347
348
349
  python/randgen.py \
  python/relabel.py \
  python/remfin.py \
  python/satmin.py \
350
  python/setacc.py \
351
  python/sccfilter.py \
352
  python/setxor.py \
353
  python/trival.py \
354
  $(TESTS_ipython)
355
endif
356

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
357
CLEANFILES = python/test1.dve python/test1.dve2C python/test1.dve.cpp
358

359
360
361
362
363
SUFFIXES = .ipynb .html
.ipynb.html:
	$(IPYTHON) nbconvert $< --to html --stdout >$@

.PHONY: nb-html
364
nb-html: $(TESTS_ipython:.ipynb=.html)
365
366
367
368
369

EXTRA_DIST = \
  $(TESTS) \
  python/ltl2tgba.py \
  python/ipnbdoctest.py
370
371
372
373


############################## LTSMIN ##############################

374
if USE_LTSMIN
375
check_PROGRAMS += ltsmin/modelcheck
376
377
378
379
380
381
382
383

ltsmin_modelcheck_SOURCES = ltsmin/modelcheck.cc
ltsmin_modelcheck_LDADD = $(top_builddir)/spot/ltsmin/libspotltsmin.la

check_SCRIPTS += ltsmin/defs

ltsmin/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in
	$(top_builddir)/config.status --file ltsmin/defs:core/defs.in
384
endif
385

386
if USE_LTSMIN
387
388
TESTS_ltsmin = \
  ltsmin/check.test \
389
390
  ltsmin/check2.test \
  ltsmin/check3.test \
391
392
  ltsmin/finite.test \
  ltsmin/finite2.test \
393
  ltsmin/finite3.test \
394
395
  ltsmin/kripke.test

396
397
EXTRA_DIST += ltsmin/beem-peterson.4.dve ltsmin/beem-peterson.4.gal \
  ltsmin/elevator2.1.pm ltsmin/finite.dve ltsmin/finite.pm ltsmin/finite.gal
398

399
ltlsmin/kripke.log: core/kripkecat$(EXEEXT)
400
endif
401
402
403
404
405
406
407
408
409
410

############################## SANITY ##############################

TESTS_sanity = \
  sanity/80columns.test \
  sanity/includes.test \
  sanity/ipynb.pl \
  sanity/private.test \
  sanity/readme.pl \
  sanity/style.test