diff --git a/python/spot/impl.i b/python/spot/impl.i index 2df9f8f530274d93e9061bacbae39e69e8dfd082..9667aed9d4408d135dbe5a6410cbc1a958247903 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -87,6 +87,7 @@ #include #include +#include #include #include @@ -425,6 +426,7 @@ namespace std { } %include +%include %include %include diff --git a/tests/Makefile.am b/tests/Makefile.am index c1b37ddebeff69ccd6fbf3186fbe7d9ba6e18046..aedabe53d06ce9ab76983614dc9358732acc5773 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -322,15 +322,15 @@ TESTS_ipython = \ # do not consider part of the documentation: those have to start # with a _. TESTS_python = \ - python/_aux.ipynb \ python/_altscc.ipynb \ + python/_aux.ipynb \ python/accparse2.py \ python/alarm.py \ python/alternating.py \ - python/bddnqueen.py \ python/bdditer.py \ + python/bddnqueen.py \ python/bugdet.py \ - python/sccinfo.py \ + python/declenv.py \ python/decompose_scc.py \ python/implies.py \ python/interdep.py \ @@ -347,8 +347,9 @@ TESTS_python = \ python/relabel.py \ python/remfin.py \ python/satmin.py \ - python/setacc.py \ python/sccfilter.py \ + python/sccinfo.py \ + python/setacc.py \ python/setxor.py \ python/sum.py \ python/trival.py \ diff --git a/tests/python/declenv.py b/tests/python/declenv.py new file mode 100644 index 0000000000000000000000000000000000000000..647f4d5e1a55140cc881a8fa4793bee9a0346872 --- /dev/null +++ b/tests/python/declenv.py @@ -0,0 +1,71 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# 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 +# the Free Software Foundation; either version 3 of the License, or +# (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 +# along with this program. If not, see . + + +# This file tests various error conditions on the twa API + +import spot + +env = spot.declarative_environment() +env.declare("a") +env.declare("b") + +f1a = spot.parse_infix_psl("a U b") +f1b = spot.parse_infix_psl("a U b", env) +assert not f1a.errors +assert not f1b.errors +# In the past, atomic propositions requires via different environments were +# never equal, but this feature was never used and we changed that in Spot 2.0 +# for the sake of simplicity. +assert f1a.f == f1b.f + +f2 = spot.parse_infix_psl("(a U b) U c", env) +assert f2.errors +ostr = spot.ostringstream() +f2.format_errors(ostr) +err = ostr.str() +assert "unknown atomic proposition `c'" in err + +f3 = spot.parse_prefix_ltl("R a d", env) +assert f3.errors +ostr = spot.ostringstream() +f3.format_errors(ostr) +err = ostr.str() +assert "unknown atomic proposition `d'" in err + +f4 = spot.parse_prefix_ltl("R a b", env) +assert not f4.errors + +for (x, op) in [('a* <-> b*', "`<->'"), + ('a* -> b', "`->'"), + ('a ^ b*', "`^'"), + ('!(b*)', "`!'"), + ('a*[=2]', "[=...]"), + ('a*[->2]', "[->...]")]: + f5 = spot.parse_infix_sere(x) + assert f5.errors + ostr = spot.ostringstream() + f5.format_errors(ostr) + err = ostr.str() + assert "not a Boolean expression" in err + assert op in err + assert "SERE" in err + +f6 = spot.parse_infix_sere('(a <-> b -> c ^ b)[=2] & c[->2]') +assert not f6.errors