Commit b81d7e58 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

python: add python bindings for declarative_environment

* python/spot/impl.i: Here.
* tests/python/declenv.py: New file.
* tests/Makefile.am: Add it.
parent 2df677d2
......@@ -87,6 +87,7 @@
#include <spot/tl/formula.hh>
#include <spot/tl/environment.hh>
#include <spot/tl/declenv.hh>
#include <spot/tl/defaultenv.hh>
#include <spot/tl/parse.hh>
......@@ -425,6 +426,7 @@ namespace std {
}
%include <spot/tl/environment.hh>
%include <spot/tl/declenv.hh>
%include <spot/tl/defaultenv.hh>
%include <spot/tl/parse.hh>
......
......@@ -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 \
......
# -*- 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 <http://www.gnu.org/licenses/>.
# 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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment