Makefile.am 13.1 KB
Newer Older
1
## -*- coding: utf-8 -*-
2
## Copyright (C) 2009-2020 Laboratoire de Recherche et Développement
3 4 5 6
## de l'Epita (LRDE).
## Copyright (C) 2003-2006 Laboratoire d'Informatique de 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
7 8 9 10 11
##
## 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
12
## the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13 14 15 16 17 18 19 20
## (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
21
## along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

23
AUTOMAKE_OPTIONS = subdir-objects
24
AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
25 26
              -I$(top_srcdir)/spot/bricks -I$(top_builddir)/lib \
	      -I$(top_srcdir)/lib
27
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
Etienne Renault's avatar
Etienne Renault committed
28 29 30
LDADD = $(top_builddir)/spot/libspot.la \
       $(top_builddir)/buddy/src/libbddx.la \
       $(LIBLTDL) -lpthread
31

32 33
# Explicitely set it to avoid default value ".test"
TEST_EXTENSIONS =
34 35
LOG_COMPILER = ./run
# ensure run is rebuilt before the tests are run.
36 37 38
check_SCRIPTS = run

# We try to keep this somehow by strength.  Test basic things first,
39 40 41 42 43 44 45
# 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)
46 47

distclean-local:
48
	find . -name '*.dir' -type d -print | xargs rm -rf
49 50 51 52 53 54
## 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
55 56 57 58 59 60 61 62 63


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

check_SCRIPTS += core/defs

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

64 65
# Keep this sorted alphabetically.
check_PROGRAMS = \
66
  core/acc \
67
  core/bdddict \
68 69 70 71
  core/bitvect \
  core/checkpsl \
  core/checkta \
  core/consterm \
72
  core/cube \
73
  core/bricks \
74 75 76 77 78
  core/emptchk \
  core/equals \
  core/graph \
  core/kind \
  core/length \
79
  core/ikwiad \
80 81
  core/intvcomp \
  core/intvcmp2 \
82
  core/kripkecat \
83 84 85 86
  core/ltl2dot \
  core/ltl2text \
  core/ltlrel \
  core/lunabbrev \
87
  core/mempool \
88 89 90
  core/nequals \
  core/nenoform \
  core/ngraph \
Laurent XU's avatar
Laurent XU committed
91
  core/parity \
92
  core/randtgba \
93 94 95 96
  core/reduc \
  core/reduccmp \
  core/reduceu \
  core/reductaustr \
97
  core/safra \
98
  core/sccif \
99 100
  core/syntimpl \
  core/taatgba \
101
  core/trival \
102 103 104
  core/tgbagraph \
  core/tostring \
  core/tunabbrev \
105 106
  core/tunenoform \
  core/twacube
107

108
# Keep this sorted alphabetically.
109
core_acc_SOURCES = core/acc.cc
110
core_bdddict_SOURCES  = core/bdddict.cc
111 112 113 114 115 116 117 118
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
119
core_kripkecat_SOURCES = core/kripkecat.cc
120
core_mempool_SOURCES = core/mempool.cc
121 122 123 124 125
core_ngraph_SOURCES = core/ngraph.cc
core_randtgba_SOURCES = core/randtgba.cc
core_taatgba_SOURCES = core/taatgba.cc
core_tgbagraph_SOURCES = core/twagraph.cc
core_consterm_SOURCES = core/consterm.cc
126
core_cube_SOURCES = core/cube.cc
127
core_bricks_SOURCES = core/bricks.cc
128 129 130 131 132 133 134 135 136 137 138 139 140
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
Laurent XU's avatar
Laurent XU committed
141
core_parity_SOURCES = core/parity.cc
142 143 144 145 146 147 148
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
149
core_safra_SOURCES = core/safra.cc
150
core_sccif_SOURCES = core/sccif.cc
151 152
core_syntimpl_SOURCES = core/syntimpl.cc
core_tostring_SOURCES = core/tostring.cc
153
core_trival_SOURCES = core/trival.cc
154 155 156 157
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"'
158
core_twacube_SOURCES = core/twacube.cc
159

160

161 162
TESTS_tl = \
  core/bare.test \
163
  core/cube.test \
164 165 166 167 168 169
  core/parse.test \
  core/parseerr.test \
  core/utf8.test \
  core/length.test \
  core/equals.test \
  core/tostring.test \
170
  core/genaut.test \
171
  core/genltl.test \
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
  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 \
197
  core/stutter-ltl.test \
198
  core/hierarchy.test \
199
  core/mempool.test \
200
  core/format.test
201 202

TESTS_graph = \
203 204 205
  core/graph.test \
  core/ngraph.test \
  core/tgbagraph.test
206 207

TESTS_kripke = \
208
  core/kripke.test
Etienne Renault's avatar
Etienne Renault committed
209

210
TESTS_misc = \
211
  core/bdd.test \
212 213
  core/bitvect.test \
  core/intvcomp.test \
214
  core/minusx.test \
215
  core/full.test \
216 217
  core/trival.test

Etienne Renault's avatar
Etienne Renault committed
218
TESTS_twa = \
219
  core/385.test \
220 221
  core/acc.test \
  core/acc2.test \
222
  core/bdddict.test \
223
  core/alternating.test \
224
  core/ltlcross3.test \
225
  core/ltlcross5.test \
226 227 228 229
  core/taatgba.test \
  core/renault.test \
  core/nondet.test \
  core/det.test \
230
  core/semidet.test \
231 232 233 234 235 236
  core/neverclaimread.test \
  core/parseaut.test \
  core/optba.test \
  core/complete.test \
  core/complement.test \
  core/remfin.test \
237
  core/gragsa.test \
238 239
  core/dstar.test \
  core/readsave.test \
240
  core/dot2tex.test \
241 242 243 244
  core/ltldo.test \
  core/ltldo2.test \
  core/maskacc.test \
  core/maskkeep.test \
245
  core/prodchain.test \
246 247 248 249 250
  core/prodor.test \
  core/simdet.test \
  core/sim2.test \
  core/sim3.test \
  core/ltl2tgba.test \
251
  core/ltl2tgba2.test \
252 253 254 255 256 257
  core/ltl2neverclaim.test \
  core/ltl2neverclaim-lbtt.test \
  core/explprod.test \
  core/explpro2.test \
  core/explpro3.test \
  core/explpro4.test \
258
  core/explsum.test \
Thomas Medioni's avatar
Thomas Medioni committed
259
  core/dualize.test \
260
  core/accsimpl.test \
261 262 263 264 265 266 267
  core/tripprod.test \
  core/dupexp.test \
  core/exclusive-tgba.test \
  core/remprop.test \
  core/degendet.test \
  core/degenid.test \
  core/degenlskip.test \
268
  core/degenscc.test \
269 270 271 272
  core/randomize.test \
  core/lbttparse.test \
  core/scc.test \
  core/sccdot.test \
273
  core/sccif.test \
274 275
  core/sccsimpl.test \
  core/sepsets.test \
276
  core/split.test \
277
  core/sugar.test \
278 279 280 281 282 283 284 285
  core/dbacomp.test \
  core/obligation.test \
  core/wdba.test \
  core/wdba2.test \
  core/babiak.test \
  core/monitor.test \
  core/dra2dba.test \
  core/unambig.test \
286
  core/unambig2.test \
287
  core/ltlcross4.test \
288
  core/ltl3ba.test \
289
  core/streett.test \
290 291 292 293 294 295 296
  core/ltl3dra.test \
  core/ltl2dstar.test \
  core/ltl2dstar2.test \
  core/ltl2dstar3.test \
  core/ltl2dstar4.test \
  core/ltl2ta.test \
  core/ltl2ta2.test \
297
  core/pdegen.test \
298 299 300
  core/randaut.test \
  core/randtgba.test \
  core/isomorph.test \
301
  core/included.test \
302
  core/uniq.test \
303
  core/safra.test \
304 305 306 307 308 309 310 311 312 313 314 315 316
  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 \
317
  core/satmin3.test \
318 319 320 321
  core/spotlbtt.test \
  core/ltlcross.test \
  core/spotlbtt2.test \
  core/ltlcross2.test \
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
322 323
  core/autcross.test \
  core/autcross2.test \
324
  core/autcross3.test \
325
  core/autcross4.test \
326
  core/autcross5.test \
327 328
  core/complementation.test \
  core/randpsl.test \
329
  core/cycles.test \
330
  core/acc_word.test \
331
  core/dca.test \
332
  core/dca2.test \
Laurent XU's avatar
Laurent XU committed
333
  core/dnfstreett.test \
Maximilien Colange's avatar
Maximilien Colange committed
334
  core/parity.test \
335
  core/parity2.test \
336
  core/ltlsynt.test \
337 338
  core/rabin2parity.test \
  core/twacube.test
339 340

############################## PYTHON ##############################
341

342
if USE_PYTHON
343 344 345 346

# TESTS_ipython contains notebooks that we also want to publish as
# part of the documentation.
TESTS_ipython = \
347 348
  python/acc_cond.ipynb \
  python/accparse.ipynb \
349
  python/alternation.ipynb \
350 351
  python/atva16-fig2a.ipynb \
  python/atva16-fig2b.ipynb \
352
  python/automata-io.ipynb \
353
  python/automata.ipynb \
354
  python/contains.ipynb \
355 356
  python/decompose.ipynb \
  python/formulas.ipynb \
357
  python/gen.ipynb \
358
  python/highlighting.ipynb \
359
  python/ltsmin-dve.ipynb \
360
  python/ltsmin-pml.ipynb \
Laurent XU's avatar
Laurent XU committed
361
  python/parity.ipynb \
362 363 364
  python/product.ipynb \
  python/randaut.ipynb \
  python/randltl.ipynb \
365
  python/satmin.ipynb \
366
  python/stutter-inv.ipynb \
367
  python/testingaut.ipynb \
368
  python/twagraph-internals.ipynb \
369
  python/word.ipynb
370 371 372 373 374

# 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 = \
375
  python/341.py \
376
  python/_altscc.ipynb \
377
  python/_autparserr.ipynb \
378
  python/_aux.ipynb \
379 380
  python/accparse2.py \
  python/alarm.py \
381
  python/alternating.py \
382
  python/bdddict.py \
383
  python/bdditer.py \
384
  python/bddnqueen.py \
385
  python/bugdet.py \
386
  python/complement_semidet.py \
387
  python/declenv.py \
388
  python/decompose_scc.py \
389
  python/dualize.py \
390
  python/ecfalse.py \
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
391
  python/except.py \
392
  python/gen.py \
393
  python/genem.py \
394 395
  python/implies.py \
  python/interdep.py \
396
  python/kripke.py \
397
  python/ltl2tgba.test \
398
  python/ltlf.py \
399 400
  python/ltlparse.py \
  python/ltlsimple.py \
401
  python/merge.py \
402
  python/minato.py \
403
  python/misc-ec.py \
404
  python/optionmap.py \
405
  python/origstate.py \
406
  python/otfcrash.py \
407
  python/parsetgba.py \
408
  python/parity.py \
409
  python/pdegen.py \
410
  python/prodexpt.py \
411
  python/_product_weak.ipynb \
412
  python/_product_susp.ipynb \
413 414 415
  python/randgen.py \
  python/relabel.py \
  python/remfin.py \
416
  python/removeap.py \
417
  python/satmin.py \
418
  python/sbacc.py \
419
  python/sccfilter.py \
420
  python/sccinfo.py \
421
  python/sccsplit.py \
422
  python/semidet.py \
423
  python/setacc.py \
424
  python/setxor.py \
425
  python/simplacc.py \
426
  python/simstate.py \
427
  python/split.py \
428
  python/streett_totgba.py \
429
  python/streett_totgba2.py \
430
  python/stutter.py \
431
  python/rs_like.py \
432
  python/sum.py \
433
  python/toparity.py \
434
  python/trival.py \
435
  python/tra2tba.py \
436
  python/twagraph.py \
437
  python/toweak.py \
438
  python/_word.ipynb \
439
  $(TESTS_ipython)
440
endif
441

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

444 445 446 447 448
SUFFIXES = .ipynb .html
.ipynb.html:
	$(IPYTHON) nbconvert $< --to html --stdout >$@

.PHONY: nb-html
449
nb-html: $(TESTS_ipython:.ipynb=.html)
450 451 452 453 454

EXTRA_DIST = \
  $(TESTS) \
  python/ltl2tgba.py \
  python/ipnbdoctest.py
455 456 457 458


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

459
if USE_LTSMIN
460
check_PROGRAMS += ltsmin/modelcheck
461 462
ltsmin_modelcheck_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
	$(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib
Etienne Renault's avatar
Etienne Renault committed
463
ltsmin_modelcheck_CXXFLAGS = $(CXXFLAGS) -pthread
464
ltsmin_modelcheck_SOURCES = ltsmin/modelcheck.cc
465 466 467 468 469
ltsmin_modelcheck_LDADD =  \
  $(top_builddir)/bin/libcommon.a		\
  $(top_builddir)/lib/libgnu.la			\
  $(top_builddir)/spot/libspot.la              \
  $(top_builddir)/spot/ltsmin/libspotltsmin.la
470 471 472 473 474 475 476 477

check_SCRIPTS += ltsmin/defs

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

TESTS_ltsmin = \
  ltsmin/check.test \
478 479
  ltsmin/check2.test \
  ltsmin/check3.test \
480 481
  ltsmin/finite.test \
  ltsmin/finite2.test \
482
  ltsmin/finite3.test \
483 484
  ltsmin/kripke.test

485 486
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
487

488
ltlsmin/kripke.log: core/kripkecat$(EXEEXT)
489
endif
490 491 492 493 494

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

TESTS_sanity = \
  sanity/80columns.test \
495
  sanity/bin.test \
496
  sanity/getenv.test \
497 498
  sanity/includes.test \
  sanity/ipynb.pl \
499
  sanity/namedprop.test \
500 501 502
  sanity/private.test \
  sanity/readme.pl \
  sanity/style.test