fix typos and make formula_from_bdd more usable in Python
* python/spot/impl.i (formula_from_bdd): Instantiate for twa_graph. * spot/twa/twa.hh (register_aps_from_dict): Typo in exception. * tests/python/except.py: More tests for the above. * tests/python/bdddict.py: Typo in comment.
This commit is contained in:
parent
187bacc254
commit
0745e735bb
4 changed files with 42 additions and 4 deletions
|
|
@ -533,6 +533,8 @@ namespace std {
|
|||
%include <spot/twa/bdddict.hh>
|
||||
%include <spot/twa/bddprint.hh>
|
||||
%include <spot/twa/formula2bdd.hh>
|
||||
%template(formula_to_bdd) spot::formula_to_bdd<spot::twa_graph>;
|
||||
|
||||
%include <spot/twa/fwd.hh>
|
||||
/* These operators may raise exceptions, and we do not
|
||||
want Swig4 to convert those exceptions to NotImplemented. */
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2011, 2013-2021 Laboratoire de Recherche et
|
||||
// Copyright (C) 2009, 2011, 2013-2022 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
|
||||
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
|
||||
|
|
@ -761,7 +761,7 @@ namespace spot
|
|||
void register_aps_from_dict()
|
||||
{
|
||||
if (!aps_.empty())
|
||||
throw std::runtime_error("register_ap_from_dict() may not be"
|
||||
throw std::runtime_error("register_aps_from_dict() may not be"
|
||||
" called on an automaton that has already"
|
||||
" registered some AP");
|
||||
auto& m = get_dict()->bdd_map;
|
||||
|
|
|
|||
|
|
@ -17,8 +17,8 @@
|
|||
# You should have received a copy of the GNU General Public License
|
||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
# Make sure we can leep track of BDD association in Python using bdd_dict, as
|
||||
# discussed in issue #372.
|
||||
# Make sure we can keep track of BDD association in Python using bdd_dict, as
|
||||
# discussed in (deleted???) issue #372.
|
||||
|
||||
# CPython use reference counting, so that automata are destructed
|
||||
# when we expect them to be. However other implementations like
|
||||
|
|
|
|||
|
|
@ -295,3 +295,39 @@ except RuntimeError as e:
|
|||
se = str(e)
|
||||
tc.assertIn("synthesis-outputs", se)
|
||||
tc.assertIn("unregistered proposition", se)
|
||||
else:
|
||||
report_missing_exception()
|
||||
|
||||
|
||||
a = spot.make_twa_graph()
|
||||
s = a.new_state()
|
||||
b = spot.formula_to_bdd("a & b", a.get_dict(), a)
|
||||
a.new_edge(s, s, b, [])
|
||||
try:
|
||||
print(a.to_str('hoa'))
|
||||
except RuntimeError as e:
|
||||
tc.assertIn("unregistered atomic propositions", str(e))
|
||||
else:
|
||||
report_missing_exception()
|
||||
|
||||
a.register_aps_from_dict()
|
||||
tc.assertEqual(a.to_str('hoa'), """HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: all
|
||||
Acceptance: 0 t
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[0&1] 0
|
||||
--END--""")
|
||||
|
||||
try:
|
||||
a.register_aps_from_dict()
|
||||
except RuntimeError as e:
|
||||
se = str(e)
|
||||
tc.assertIn("register_aps_from_dict", se)
|
||||
tc.assertIn("already registered", se)
|
||||
else:
|
||||
report_missing_exception()
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue