* configure.ac: Output wrap/python/tests/Makefile
and wrap/python/tests/run. * wrap/python/Makefile.am (SUBDIRS): New variable. * wrap/python/spot.i: Include all formulae headers from ltlast/, as well as ltlvisit/destroy.hh. (spot::ltl::formula::__cmp__, spot::ltl::formula::__str__): New functions. * wrap/python/tests/Makefile.am, wrap/python/tests/ltlsimple.py, wrap/python/tests/run.in: New files.
This commit is contained in:
parent
99018935bb
commit
0c50e20ffd
9 changed files with 181 additions and 12 deletions
10
ChangeLog
10
ChangeLog
|
|
@ -1,5 +1,15 @@
|
||||||
2003-07-31 Alexandre Duret-Lutz <adl@gnu.org>
|
2003-07-31 Alexandre Duret-Lutz <adl@gnu.org>
|
||||||
|
|
||||||
|
* configure.ac: Output wrap/python/tests/Makefile
|
||||||
|
and wrap/python/tests/run.
|
||||||
|
* wrap/python/Makefile.am (SUBDIRS): New variable.
|
||||||
|
* wrap/python/spot.i: Include all formulae headers from ltlast/,
|
||||||
|
as well as ltlvisit/destroy.hh.
|
||||||
|
(spot::ltl::formula::__cmp__, spot::ltl::formula::__str__): New
|
||||||
|
functions.
|
||||||
|
* wrap/python/tests/Makefile.am, wrap/python/tests/ltlsimple.py,
|
||||||
|
wrap/python/tests/run.in: New files.
|
||||||
|
|
||||||
* wrap/python/ltihooks.py: New file.
|
* wrap/python/ltihooks.py: New file.
|
||||||
* wrap/python/Makefile.am (EXTRA_DIST): Add ltihooks.py.
|
* wrap/python/Makefile.am (EXTRA_DIST): Add ltihooks.py.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -44,5 +44,7 @@ AC_CONFIG_FILES([
|
||||||
src/misc/Makefile
|
src/misc/Makefile
|
||||||
wrap/Makefile
|
wrap/Makefile
|
||||||
wrap/python/Makefile
|
wrap/python/Makefile
|
||||||
|
wrap/python/tests/Makefile
|
||||||
])
|
])
|
||||||
|
AC_CONFIG_FILES([wrap/python/tests/run], [chmod +x wrap/python/tests/run])
|
||||||
AC_OUTPUT
|
AC_OUTPUT
|
||||||
|
|
|
||||||
|
|
@ -7,3 +7,4 @@ spot.py*
|
||||||
*.lo
|
*.lo
|
||||||
*.loT
|
*.loT
|
||||||
spot_wrap.cxx
|
spot_wrap.cxx
|
||||||
|
*.pyc
|
||||||
|
|
|
||||||
|
|
@ -1,3 +1,4 @@
|
||||||
|
SUBDIRS = tests
|
||||||
|
|
||||||
AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_srcdir)/src
|
AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_srcdir)/src
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -4,59 +4,96 @@
|
||||||
%include "std_list.i"
|
%include "std_list.i"
|
||||||
|
|
||||||
%{
|
%{
|
||||||
#include "ltlenv/environment.hh"
|
|
||||||
#include "ltlenv/defaultenv.hh"
|
|
||||||
#include "ltlast/formula.hh"
|
#include "ltlast/formula.hh"
|
||||||
#include "ltlparse/public.hh"
|
#include "ltlast/refformula.hh"
|
||||||
|
#include "ltlast/atomic_prop.hh"
|
||||||
|
#include "ltlast/binop.hh"
|
||||||
|
#include "ltlast/constant.hh"
|
||||||
|
#include "ltlast/multop.hh"
|
||||||
|
#include "ltlast/unop.hh"
|
||||||
#include "ltlast/visitor.hh"
|
#include "ltlast/visitor.hh"
|
||||||
|
|
||||||
|
#include "ltlenv/environment.hh"
|
||||||
|
#include "ltlenv/defaultenv.hh"
|
||||||
|
|
||||||
|
#include "ltlparse/public.hh"
|
||||||
|
|
||||||
#include "ltlvisit/clone.hh"
|
#include "ltlvisit/clone.hh"
|
||||||
|
#include "ltlvisit/destroy.hh"
|
||||||
#include "ltlvisit/dotty.hh"
|
#include "ltlvisit/dotty.hh"
|
||||||
#include "ltlvisit/dump.hh"
|
#include "ltlvisit/dump.hh"
|
||||||
#include "ltlvisit/lunabbrev.hh"
|
#include "ltlvisit/lunabbrev.hh"
|
||||||
#include "ltlvisit/tunabbrev.hh"
|
|
||||||
#include "ltlvisit/nenoform.hh"
|
#include "ltlvisit/nenoform.hh"
|
||||||
#include "ltlvisit/tostring.hh"
|
#include "ltlvisit/tostring.hh"
|
||||||
|
#include "ltlvisit/tunabbrev.hh"
|
||||||
|
|
||||||
using namespace spot::ltl;
|
using namespace spot::ltl;
|
||||||
%}
|
%}
|
||||||
|
|
||||||
%include "ltlenv/environment.hh"
|
|
||||||
%include "ltlenv/defaultenv.hh"
|
|
||||||
%include "ltlast/formula.hh"
|
%include "ltlast/formula.hh"
|
||||||
%include "ltlparse/public.hh"
|
%include "ltlast/refformula.hh"
|
||||||
|
%include "ltlast/atomic_prop.hh"
|
||||||
|
%include "ltlast/binop.hh"
|
||||||
|
%include "ltlast/constant.hh"
|
||||||
|
%include "ltlast/multop.hh"
|
||||||
|
%include "ltlast/unop.hh"
|
||||||
%include "ltlast/visitor.hh"
|
%include "ltlast/visitor.hh"
|
||||||
|
|
||||||
|
%include "ltlenv/environment.hh"
|
||||||
|
%include "ltlenv/defaultenv.hh"
|
||||||
|
|
||||||
|
%include "ltlparse/public.hh"
|
||||||
|
|
||||||
%include "ltlvisit/clone.hh"
|
%include "ltlvisit/clone.hh"
|
||||||
|
%include "ltlvisit/destroy.hh"
|
||||||
%include "ltlvisit/dotty.hh"
|
%include "ltlvisit/dotty.hh"
|
||||||
%include "ltlvisit/dump.hh"
|
%include "ltlvisit/dump.hh"
|
||||||
%include "ltlvisit/lunabbrev.hh"
|
%include "ltlvisit/lunabbrev.hh"
|
||||||
%include "ltlvisit/tunabbrev.hh"
|
|
||||||
%include "ltlvisit/nenoform.hh"
|
%include "ltlvisit/nenoform.hh"
|
||||||
%include "ltlvisit/tostring.hh"
|
%include "ltlvisit/tostring.hh"
|
||||||
|
%include "ltlvisit/tunabbrev.hh"
|
||||||
|
|
||||||
|
|
||||||
|
%extend spot::ltl::formula {
|
||||||
|
|
||||||
|
// When comparing formula, make sure Python compare our
|
||||||
|
// pointers, not the pointers to its wrappers.
|
||||||
|
int
|
||||||
|
__cmp__(const spot::ltl::formula* b)
|
||||||
|
{
|
||||||
|
return b - self;
|
||||||
|
}
|
||||||
|
|
||||||
|
std::string
|
||||||
|
__str__(void)
|
||||||
|
{
|
||||||
|
return spot::ltl::to_string(self);
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
%inline %{
|
%inline %{
|
||||||
|
|
||||||
spot::ltl::parse_error_list
|
spot::ltl::parse_error_list
|
||||||
empty_parse_error_list()
|
empty_parse_error_list()
|
||||||
{
|
{
|
||||||
parse_error_list l;
|
parse_error_list l;
|
||||||
return l;
|
return l;
|
||||||
}
|
}
|
||||||
|
|
||||||
std::ostream&
|
std::ostream&
|
||||||
get_cout()
|
get_cout()
|
||||||
{
|
{
|
||||||
return std::cout;
|
return std::cout;
|
||||||
}
|
}
|
||||||
|
|
||||||
std::ostream&
|
std::ostream&
|
||||||
get_cerr()
|
get_cerr()
|
||||||
{
|
{
|
||||||
return std::cerr;
|
return std::cerr;
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
print_on(std::ostream& on, const std::string& what)
|
print_on(std::ostream& on, const std::string& what)
|
||||||
{
|
{
|
||||||
on << what;
|
on << what;
|
||||||
|
|
|
||||||
3
wrap/python/tests/.cvsignore
Normal file
3
wrap/python/tests/.cvsignore
Normal file
|
|
@ -0,0 +1,3 @@
|
||||||
|
Makefile
|
||||||
|
Makefile.in
|
||||||
|
run
|
||||||
8
wrap/python/tests/Makefile.am
Normal file
8
wrap/python/tests/Makefile.am
Normal file
|
|
@ -0,0 +1,8 @@
|
||||||
|
EXTRA_DIST = $(TESTS)
|
||||||
|
|
||||||
|
TESTS_ENVIRONMENT = ./run
|
||||||
|
# ensure run is rebuilt before the tests are run.
|
||||||
|
check_SCRIPTS = run
|
||||||
|
|
||||||
|
TESTS = \
|
||||||
|
ltlsimple.py
|
||||||
100
wrap/python/tests/ltlsimple.py
Executable file
100
wrap/python/tests/ltlsimple.py
Executable file
|
|
@ -0,0 +1,100 @@
|
||||||
|
import ltihooks
|
||||||
|
import spot
|
||||||
|
|
||||||
|
clone = spot.clone
|
||||||
|
|
||||||
|
e = spot.default_environment.instance()
|
||||||
|
|
||||||
|
#----------------------------------------------------------------------
|
||||||
|
a = e.require('a')
|
||||||
|
b = e.require('b')
|
||||||
|
c = e.require('c')
|
||||||
|
c2 = e.require('c')
|
||||||
|
|
||||||
|
assert c == c2
|
||||||
|
assert spot.atomic_prop.instance_count() == 3
|
||||||
|
|
||||||
|
op = spot.multop.instance(spot.multop.And, clone(a), clone(b))
|
||||||
|
op2 = spot.multop.instance(spot.multop.And, op, c)
|
||||||
|
|
||||||
|
# The symbol for a subformula which hasn't been cloned is better
|
||||||
|
# suppressed, so we don't attempt to reuse it elsewhere.
|
||||||
|
del op, c
|
||||||
|
|
||||||
|
print 'op2 =', op2
|
||||||
|
|
||||||
|
op3 = spot.multop.instance(spot.multop.And, b,
|
||||||
|
spot.multop.instance(spot.multop.And, c2, a))
|
||||||
|
del a, b, c2
|
||||||
|
|
||||||
|
print 'op3 =', op3
|
||||||
|
assert op2 == op3
|
||||||
|
|
||||||
|
op4 = spot.multop.instance(spot.multop.Or, op2, op3)
|
||||||
|
|
||||||
|
print 'op4 =', op4
|
||||||
|
assert op4.nth(0) == op2
|
||||||
|
|
||||||
|
del op2, op3
|
||||||
|
|
||||||
|
assert spot.atomic_prop.instance_count() == 3
|
||||||
|
assert spot.multop.instance_count() == 2
|
||||||
|
|
||||||
|
spot.destroy(op4)
|
||||||
|
del op4
|
||||||
|
|
||||||
|
assert spot.atomic_prop.instance_count() == 0
|
||||||
|
assert spot.multop.instance_count() == 0
|
||||||
|
|
||||||
|
#----------------------------------------------------------------------
|
||||||
|
a = e.require('a')
|
||||||
|
b = e.require('b')
|
||||||
|
c = e.require('c')
|
||||||
|
T = spot.constant.true_instance()
|
||||||
|
F = spot.constant.false_instance()
|
||||||
|
|
||||||
|
f1 = spot.binop.instance(spot.binop.Equiv, T, clone(a))
|
||||||
|
f2 = spot.binop.instance(spot.binop.Implies, F, clone(b))
|
||||||
|
f3 = spot.binop.instance(spot.binop.Xor, F, clone(c))
|
||||||
|
f4 = spot.unop.instance(spot.unop.Not, f3); del f3
|
||||||
|
|
||||||
|
assert spot.atomic_prop.instance_count() == 3
|
||||||
|
assert spot.binop.instance_count() == 3
|
||||||
|
assert spot.unop.instance_count() == 1
|
||||||
|
assert spot.multop.instance_count() == 0
|
||||||
|
|
||||||
|
spot.destroy(a)
|
||||||
|
del a
|
||||||
|
spot.destroy(b)
|
||||||
|
del b
|
||||||
|
spot.destroy(c)
|
||||||
|
del c
|
||||||
|
|
||||||
|
assert spot.atomic_prop.instance_count() == 3
|
||||||
|
assert spot.binop.instance_count() == 3
|
||||||
|
assert spot.unop.instance_count() == 1
|
||||||
|
assert spot.multop.instance_count() == 0
|
||||||
|
|
||||||
|
spot.destroy(f1)
|
||||||
|
del f1
|
||||||
|
|
||||||
|
assert spot.atomic_prop.instance_count() == 2
|
||||||
|
assert spot.binop.instance_count() == 2
|
||||||
|
assert spot.unop.instance_count() == 1
|
||||||
|
assert spot.multop.instance_count() == 0
|
||||||
|
|
||||||
|
spot.destroy(f4)
|
||||||
|
del f4
|
||||||
|
|
||||||
|
assert spot.atomic_prop.instance_count() == 1
|
||||||
|
assert spot.binop.instance_count() == 1
|
||||||
|
assert spot.unop.instance_count() == 0
|
||||||
|
assert spot.multop.instance_count() == 0
|
||||||
|
|
||||||
|
spot.destroy(f2)
|
||||||
|
del f2
|
||||||
|
|
||||||
|
assert spot.atomic_prop.instance_count() == 0
|
||||||
|
assert spot.binop.instance_count() == 0
|
||||||
|
assert spot.unop.instance_count() == 0
|
||||||
|
assert spot.multop.instance_count() == 0
|
||||||
7
wrap/python/tests/run.in
Normal file
7
wrap/python/tests/run.in
Normal file
|
|
@ -0,0 +1,7 @@
|
||||||
|
#!/bin/sh
|
||||||
|
|
||||||
|
# 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+"$@"}
|
||||||
Loading…
Add table
Add a link
Reference in a new issue