do not build ikwiad, randtgba, and modelcheck by default
Fix #128. * tests/Makefile.am: Make these check_PROGRAMS. * bench/emptchk/Makefile.am: Adjust. * bench/emptchk/README, bench/emptchk/defs.in: Fix paths.
This commit is contained in:
parent
8880578e0d
commit
d5bf95c5cb
4 changed files with 19 additions and 10 deletions
|
|
@ -20,6 +20,17 @@
|
||||||
|
|
||||||
PML2TGBA = $(PERL) $(srcdir)/pml2tgba.pl
|
PML2TGBA = $(PERL) $(srcdir)/pml2tgba.pl
|
||||||
|
|
||||||
|
all-local: $(top_builddir)/tests/core/ikwiad$(EXEEXT) \
|
||||||
|
$(top_builddir)/tests/core/randtgba$(EXEEXT)
|
||||||
|
|
||||||
|
$(top_builddir)/tests/core/ikwiad$(EXEEXT):
|
||||||
|
cd $(top_builddir)/tests/ && \
|
||||||
|
$(MAKE) $(AM_MAKEFLAGS) core/ikwiad$(EXEEXT)
|
||||||
|
|
||||||
|
$(top_builddir)/tests/core/randtgba$(EXEEXT):
|
||||||
|
cd $(top_builddir)/tests/ && \
|
||||||
|
$(MAKE) $(AM_MAKEFLAGS) core/randtgba$(EXEEXT)
|
||||||
|
|
||||||
noinst_SCRIPTS = defs
|
noinst_SCRIPTS = defs
|
||||||
dist_noinst_SCRIPTS = \
|
dist_noinst_SCRIPTS = \
|
||||||
pml2tgba.pl \
|
pml2tgba.pl \
|
||||||
|
|
|
||||||
|
|
@ -264,7 +264,7 @@ This directory contains:
|
||||||
MORE STATISTICS
|
MORE STATISTICS
|
||||||
=================
|
=================
|
||||||
|
|
||||||
The ltl-*.sh tests use src/tgbatest/randtgba to output statistics,
|
The ltl-*.sh tests use spot/tests/randtgba to output statistics,
|
||||||
but randtgba is able to output a lot more data than what we have
|
but randtgba is able to output a lot more data than what we have
|
||||||
shown above. Try removing the `-1' option from the script, or toying
|
shown above. Try removing the `-1' option from the script, or toying
|
||||||
with randtgba itself.
|
with randtgba itself.
|
||||||
|
|
@ -275,5 +275,5 @@ This directory contains:
|
||||||
(The `bsh=' argument gives the hash table size in bytes; see also
|
(The `bsh=' argument gives the hash table size in bytes; see also
|
||||||
http://spot.lip6.fr/wiki/EmptinessCheckOptions)
|
http://spot.lip6.fr/wiki/EmptinessCheckOptions)
|
||||||
|
|
||||||
Besides randtgba, two other tools that you might find handy we
|
Besides randtgba, two other tools that you might find handy when
|
||||||
experimenting are src/bin/randltl and src/tests/ikwiad.
|
experimenting are bin/randltl and tests/core/ikwiad.
|
||||||
|
|
|
||||||
|
|
@ -32,7 +32,7 @@ test -f "$srcdir/defs.in" || {
|
||||||
exit 1
|
exit 1
|
||||||
}
|
}
|
||||||
|
|
||||||
RANDTGBA='@top_builddir@/src/tgbatest/randtgba@EXEEXT@'
|
RANDTGBA='@top_builddir@/tests/core/randtgba@EXEEXT@'
|
||||||
LTL2TGBA='@top_builddir@/src/tests/ikwiad@EXEEXT@'
|
LTL2TGBA='@top_builddir@/tests/core/ikwiad@EXEEXT@'
|
||||||
FORMULAE=$srcdir/formulae.ltl
|
FORMULAE=$srcdir/formulae.ltl
|
||||||
ALGORITHMS=$srcdir/algorithms
|
ALGORITHMS=$srcdir/algorithms
|
||||||
|
|
|
||||||
|
|
@ -56,10 +56,6 @@ check_SCRIPTS += core/defs
|
||||||
core/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in
|
core/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in
|
||||||
$(top_builddir)/config.status --file core/defs
|
$(top_builddir)/config.status --file core/defs
|
||||||
|
|
||||||
# These are the most used test programs, and they are also useful
|
|
||||||
# to run manually outside the test suite. Always build them.
|
|
||||||
noinst_PROGRAMS = core/ikwiad core/randtgba
|
|
||||||
|
|
||||||
# Keep this sorted alphabetically.
|
# Keep this sorted alphabetically.
|
||||||
check_PROGRAMS = \
|
check_PROGRAMS = \
|
||||||
core/acc \
|
core/acc \
|
||||||
|
|
@ -73,6 +69,7 @@ check_PROGRAMS = \
|
||||||
core/graph \
|
core/graph \
|
||||||
core/kind \
|
core/kind \
|
||||||
core/length \
|
core/length \
|
||||||
|
core/ikwiad \
|
||||||
core/intvcomp \
|
core/intvcomp \
|
||||||
core/intvcmp2 \
|
core/intvcmp2 \
|
||||||
core/kripkecat \
|
core/kripkecat \
|
||||||
|
|
@ -84,6 +81,7 @@ check_PROGRAMS = \
|
||||||
core/nequals \
|
core/nequals \
|
||||||
core/nenoform \
|
core/nenoform \
|
||||||
core/ngraph \
|
core/ngraph \
|
||||||
|
core/randtgba \
|
||||||
core/readsat \
|
core/readsat \
|
||||||
core/reduc \
|
core/reduc \
|
||||||
core/reduccmp \
|
core/reduccmp \
|
||||||
|
|
@ -334,7 +332,7 @@ EXTRA_DIST = \
|
||||||
|
|
||||||
############################## LTSMIN ##############################
|
############################## LTSMIN ##############################
|
||||||
|
|
||||||
noinst_PROGRAMS += ltsmin/modelcheck
|
check_PROGRAMS += ltsmin/modelcheck
|
||||||
|
|
||||||
ltsmin_modelcheck_SOURCES = ltsmin/modelcheck.cc
|
ltsmin_modelcheck_SOURCES = ltsmin/modelcheck.cc
|
||||||
ltsmin_modelcheck_LDADD = $(top_builddir)/spot/ltsmin/libspotltsmin.la
|
ltsmin_modelcheck_LDADD = $(top_builddir)/spot/ltsmin/libspotltsmin.la
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue