From b81d7e5839deb0a203c42ad7e970888622352df1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 9 Mar 2017 15:04:58 +0100 Subject: [PATCH] python: add python bindings for declarative_environment * python/spot/impl.i: Here. * tests/python/declenv.py: New file. * tests/Makefile.am: Add it. --- python/spot/impl.i | 2 ++ tests/Makefile.am | 9 +++--- tests/python/declenv.py | 71 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 78 insertions(+), 4 deletions(-) create mode 100644 tests/python/declenv.py diff --git a/python/spot/impl.i b/python/spot/impl.i index 2df9f8f53..9667aed9d 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 c1b37ddeb..aedabe53d 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 000000000..647f4d5e1 --- /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 -- GitLab