7a65bdf6bc
This is adapted from a proposition in a paper by J. Esparza, J. Křentínský, and S. Sickert, submitted to LICS'18. We should add proper references to the code and documentation once that paper is accepted. * spot/twaalgos/gfguarantee.cc, spot/twaalgos/gfguarantee.hh: New files. * spot/twaalgos/Makefile.am, python/spot/impl.i: Add them. * spot/twa/fwd.hh: Add a forward declaration of bdd_dict_ptr. * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Make it possible to call finalize() from the translator subclass. Constify all the do_* functions while we are there. * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add a "gf-guarantee" option to decide whether to use the new translation. * bin/spot-x.cc: Document it. * tests/core/dca2.test, tests/core/genltl.test, tests/core/ltl2tgba2.test, tests/core/parity2.test, tests/core/satmin.test, tests/python/automata.ipynb, tests/python/sbacc.py: Adjust test cases. * tests/python/except.py: Add a couple more tests.
89 lines
2.3 KiB
Python
89 lines
2.3 KiB
Python
# -*- mode: python; coding: utf-8 -*-
|
|
# Copyright (C) 2018 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/>.
|
|
|
|
|
|
# Test some function that must return exceptions on error. Doing
|
|
# so is mostly a way to improve the coverage report.
|
|
|
|
|
|
import spot
|
|
|
|
try:
|
|
spot.iar(spot.translate('GFa & GFb & GFc'))
|
|
except RuntimeError as e:
|
|
assert 'iar() expects Rabin-like or Streett-like input' in str(e)
|
|
|
|
alt = spot.dualize(spot.translate('FGa | FGb'))
|
|
|
|
try:
|
|
spot.tgba_determinize(alt)
|
|
except RuntimeError as e:
|
|
assert 'tgba_determinize() does not support alternation' in str(e)
|
|
|
|
|
|
aut = spot.translate('a U b U c')
|
|
aps = aut.ap()
|
|
rem = spot.remove_ap()
|
|
rem.add_ap('"a"=0,b')
|
|
aut = rem.strip(aut)
|
|
assert aut.ap() == aps[2:]
|
|
try:
|
|
rem.add_ap('"a=0,b')
|
|
except ValueError as e:
|
|
assert """missing closing '"'""" in str(e)
|
|
|
|
try:
|
|
rem.add_ap('a=0=b')
|
|
except ValueError as e:
|
|
assert """unexpected '=' at position 3""" in str(e)
|
|
|
|
|
|
si = spot.scc_info(alt)
|
|
try:
|
|
si.determine_unknown_acceptance()
|
|
except RuntimeError as e:
|
|
assert "scc_info::determine_unknown_acceptance() does not supp" in str(e)
|
|
|
|
r = spot.twa_run(aut)
|
|
try:
|
|
a = r.as_twa()
|
|
except RuntimeError as e:
|
|
assert "empty cycle" in str(e)
|
|
|
|
try:
|
|
a = r.replay(spot.get_cout())
|
|
except RuntimeError as e:
|
|
assert "empty cycle" in str(e)
|
|
|
|
try:
|
|
a = r.reduce()
|
|
except RuntimeError as e:
|
|
assert "empty cycle" in str(e)
|
|
|
|
f = spot.formula('GF(a | Gb)')
|
|
try:
|
|
spot.gf_guarantee_to_ba(f, spot._bdd_dict)
|
|
except RuntimeError as e:
|
|
assert "guarantee" in str(e)
|
|
|
|
f = spot.formula('FG(a | Fb)')
|
|
try:
|
|
spot.fg_safety_to_dca(f, spot._bdd_dict)
|
|
except RuntimeError as e:
|
|
assert "safety" in str(e)
|