From 1095dd7533a4a92ac7c957553ccb1ac143d0ddbb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 4 Aug 2003 13:50:59 +0000 Subject: [PATCH] * wrap/python/spot.i: Include headers from tgba/ and tgbaalgos/. * wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test: New files. * wrap/python/tests/Makefile.am (TESTS): Add ltl2tgba.test. (EXTRA_DIST): Add ltl2tgba.py. * wrap/python/tests/run.in: Distinguish *.py and *.test. --- ChangeLog | 7 ++ wrap/python/spot.i | 42 +++++++++++ wrap/python/tests/Makefile.am | 7 +- wrap/python/tests/ltl2tgba.py | 124 ++++++++++++++++++++++++++++++++ wrap/python/tests/ltl2tgba.test | 16 +++++ wrap/python/tests/ltlsimple.py | 2 +- wrap/python/tests/run.in | 17 ++++- 7 files changed, 210 insertions(+), 5 deletions(-) create mode 100755 wrap/python/tests/ltl2tgba.py create mode 100755 wrap/python/tests/ltl2tgba.test diff --git a/ChangeLog b/ChangeLog index be98c9a12..e21069593 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,12 @@ 2003-08-04 Alexandre Duret-Lutz + * wrap/python/spot.i: Include headers from tgba/ and tgbaalgos/. + * wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test: + New files. + * wrap/python/tests/Makefile.am (TESTS): Add ltl2tgba.test. + (EXTRA_DIST): Add ltl2tgba.py. + * wrap/python/tests/run.in: Distinguish *.py and *.test. + * wrap/python/tests/ltlparse.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add it. diff --git a/wrap/python/spot.i b/wrap/python/spot.i index c7f554c08..8379d89f9 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -27,7 +27,27 @@ #include "ltlvisit/tostring.hh" #include "ltlvisit/tunabbrev.hh" +#include "tgba/bdddict.hh" +#include "tgba/bddprint.hh" +#include "tgba/state.hh" +#include "tgba/succiter.hh" +#include "tgba/tgba.hh" +#include "tgba/statebdd.hh" +#include "tgba/tgbabddcoredata.hh" +#include "tgba/succiterconcrete.hh" +#include "tgba/tgbabddconcrete.hh" +#include "tgba/tgbaexplicit.hh" +#include "tgba/tgbaproduct.hh" +#include "tgba/tgbatba.hh" + +#include "tgbaalgos/ltl2tgba.hh" +#include "tgbaalgos/dotty.hh" +#include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/magic.hh" +#include "tgbaalgos/save.hh" + using namespace spot::ltl; +using namespace spot; %} %include "ltlast/formula.hh" @@ -53,6 +73,27 @@ using namespace spot::ltl; %include "ltlvisit/tostring.hh" %include "ltlvisit/tunabbrev.hh" +// Help SWIG with namespace lookups. +#define ltl spot::ltl +%include "tgba/bdddict.hh" +%include "tgba/bddprint.hh" +%include "tgba/state.hh" +%include "tgba/succiter.hh" +%include "tgba/tgba.hh" +%include "tgba/statebdd.hh" +%include "tgba/tgbabddcoredata.hh" +%include "tgba/succiterconcrete.hh" +%include "tgba/tgbabddconcrete.hh" +%include "tgba/tgbaexplicit.hh" +%include "tgba/tgbaproduct.hh" +%include "tgba/tgbatba.hh" + +%include "tgbaalgos/ltl2tgba.hh" +%include "tgbaalgos/dotty.hh" +%include "tgbaalgos/lbtt.hh" +%include "tgbaalgos/magic.hh" +%include "tgbaalgos/save.hh" +#undef ltl %extend spot::ltl::formula { @@ -98,4 +139,5 @@ print_on(std::ostream& on, const std::string& what) { on << what; } + %} diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index b9c1644f4..5f26461ae 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -1,4 +1,6 @@ -EXTRA_DIST = $(TESTS) +EXTRA_DIST = \ + $(TESTS) \ + ltl2tgba.py TESTS_ENVIRONMENT = ./run # ensure run is rebuilt before the tests are run. @@ -7,4 +9,5 @@ check_SCRIPTS = run TESTS = \ ltlsimple.py \ ltlparse.py \ - bddnqueen.py \ No newline at end of file + bddnqueen.py \ + ltl2tgba.test diff --git a/wrap/python/tests/ltl2tgba.py b/wrap/python/tests/ltl2tgba.py new file mode 100755 index 000000000..7590dcd8a --- /dev/null +++ b/wrap/python/tests/ltl2tgba.py @@ -0,0 +1,124 @@ +# This is a python translation of the ltl2tgba C++ test program. +# Compare with src/tgbatest/ltl2tgba.test. + +import sys +import getopt +import ltihooks +import spot + +def usage(prog): + print "Usage: ", prog, """ [OPTIONS...] formula + +Options: + -a display the accepting_conditions BDD, not the reachability graph + -A same as -a, but as a set + -d turn on traces during parsing + -D degeneralize the automaton + -r display the relation BDD, not the reachability graph + -R same as -r, but as a set + -t display reachable states in LBTT's format + -v display the BDD variables used by the automaton""" + sys.exit(2) + + +prog = sys.argv[0] +try: + opts, args = getopt.getopt(sys.argv[1:], 'aAdDrRtv') +except getopt.GetoptError: + usage(prog) + +exit_code = 0 +debug_opt = 0 +degeneralize_opt = None +output = 0 + +for o, a in opts: + if o == '-a': + output = 2 + elif o == '-A': + output = 4 + elif o == '-d': + debug_opt = 1 + elif o == '-D': + degeneralize_opt = 1 + elif o == '-r': + output = 1 + elif o == '-R': + output = 3 + elif o == '-t': + output = 6 + elif o == '-v': + output = 5 + else: + usage(prog) + +if len(args) != 1: + usage(prog) + + +cout = spot.get_cout() +cerr = spot.get_cerr() + +e = spot.default_environment.instance() +p = spot.empty_parse_error_list() + +f = spot.parse(args[0], p, e, debug_opt) +if spot.format_parse_errors(cerr, args[0], p): + exit_code = 1 + +dict = spot.bdd_dict() + +if f: + concrete = spot.ltl_to_tgba(f, dict) + spot.destroy(f) + del f + a = concrete + + degeneralized = None + if degeneralize_opt: + a = degeneralized = spot.tgba_tba_proxy(a) + + if output == 0: + spot.dotty_reachable(cout, a) + elif output == 1: + spot.bdd_print_dot(cout, concrete.get_dict(), + concrete.get_core_data().relation) + elif output == 2: + spot.bdd_print_dot(cout, concrete.get_dict(), + concrete.get_core_data().accepting_conditions) + elif output == 3: + spot.bdd_print_set(cout, concrete.get_dict(), + concrete.get_core_data().relation) + print + elif output == 4: + spot.bdd_print_set(cout, concrete.get_dict(), + concrete.get_core_data().accepting_conditions) + print + elif output == 5: + a.get_dict().dump(cout) + elif output == 6: + spot.lbtt_reachable(cout, a) + else: + assert "unknown output option" + + # Must delete absolutely all references to an automaton + # so that the C++ destructor gets called. + del a + + if degeneralize_opt: + degeneralized.thisown = 1 + del degeneralized + + concrete.thisown = 1 + del concrete + +else: + exit_code = 1 + +del dict; + +assert spot.atomic_prop.instance_count() == 0 +assert spot.unop.instance_count() == 0 +assert spot.binop.instance_count() == 0 +assert spot.multop.instance_count() == 0 + diff --git a/wrap/python/tests/ltl2tgba.test b/wrap/python/tests/ltl2tgba.test new file mode 100755 index 000000000..3400f06cf --- /dev/null +++ b/wrap/python/tests/ltl2tgba.test @@ -0,0 +1,16 @@ +#!/bin/sh + +set -e + +# We don't check the output, but just running these might be enough to +# trigger assertions. + +./run ltl2tgba.py a +./run ltl2tgba.py 'a U b' +./run ltl2tgba.py 'X a' +./run ltl2tgba.py 'a & b & c' +./run ltl2tgba.py 'a | b | (c U (d & (g U (h ^ i))))' +./run ltl2tgba.py 'Xa & (b U !a) & (b U !a)' +./run ltl2tgba.py 'Fa & Xb & GFc & Gd' +./run ltl2tgba.py 'Fa & Xa & GFc & Gc' +./run ltl2tgba.py 'Fc & X(a | Xb) & GF(a | Xb) & Gc' diff --git a/wrap/python/tests/ltlsimple.py b/wrap/python/tests/ltlsimple.py index dbc8199a7..b9c6c4e3f 100755 --- a/wrap/python/tests/ltlsimple.py +++ b/wrap/python/tests/ltlsimple.py @@ -24,7 +24,7 @@ del op, c print 'op2 =', op2 op3 = spot.multop.instance(spot.multop.And, b, - spot.multop.instance(spot.multop.And, c2, a)) + spot.multop.instance(spot.multop.And, c2, a)) del a, b, c2 print 'op3 =', op3 diff --git a/wrap/python/tests/run.in b/wrap/python/tests/run.in index 519b9f0b1..87a1379b8 100644 --- a/wrap/python/tests/run.in +++ b/wrap/python/tests/run.in @@ -1,7 +1,20 @@ #!/bin/sh -# If we are running from make check (srcdir is set), and VERBOSE is +# If we are running from make check (srcdir is set) and VERBOSE is # unset, be quiet. test -n "$srcdir" && test -z "$VERBOSE" && exec >/dev/null 2>&1 -PYTHONPATH=..:@srcdir@/.. exec @PYTHON@ ${1+"$@"} +if test -z "$1"; then + echo "Usage: ./run something" 2>&1 + exit 1 +fi + +case $1 in + *.py) + PYTHONPATH=..:@srcdir@/.. exec @PYTHON@ "$@";; + *.test) + sh -x "$@";; + *) + echo "Unknown extension" 2>&1 + exit 2;; +esac