diff --git a/NEWS b/NEWS index 6a4fc8736..5608a76a6 100644 --- a/NEWS +++ b/NEWS @@ -38,6 +38,9 @@ New in spot 2.3.1.dev (not yet released) - spot::twa_graph::set_univ_init_state() could not be called with an initializer list. + - the Python wrappers for spot::twa_graph::state_from_number and + spot::twa_graph::state_acc_sets were broken in 2.3. + Deprecation notices: - Using --format=%a to print the number of atomic propositions in diff --git a/python/spot/impl.i b/python/spot/impl.i index 87a5de307..ec7b2c431 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -488,12 +488,12 @@ def out(self, src: 'unsigned int'): return $action(self, src) %} %feature("shadow") spot::twa_graph::state_from_number %{ -def state_from_number(self, s: 'unsigned int') -> "spot::twa_graph_state const *": +def state_from_number(self, src: 'unsigned int') -> "spot::twa_graph_state const *": self.report_univ_dest(src) return $action(self, src) %} %feature("shadow") spot::twa_graph::state_acc_sets %{ -def state_acc_sets(self, s: 'unsigned int') -> "spot::acc_cond::mark_t": +def state_acc_sets(self, src: 'unsigned int') -> "spot::acc_cond::mark_t": self.report_univ_dest(src) return $action(self, src) %} diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 24d4c8552..0594ab092 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -257,7 +257,7 @@ namespace spot { if (SPOT_UNLIKELY(s >= num_states())) throw std::invalid_argument - ("set_init_state() called with nonexisiting state"); + ("set_init_state() called with nonexisting state"); init_number_ = s; } @@ -273,7 +273,7 @@ namespace spot for (I i = dst_begin; i != dst_end; ++i) if (SPOT_UNLIKELY(*i >= ns)) throw std::invalid_argument - ("set_univ_init_state() called with nonexisiting state"); + ("set_univ_init_state() called with nonexisting state"); init_number_ = g_.new_univ_dests(dst_begin, dst_end); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 1e1336f9a..a2ab932c8 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -349,6 +349,7 @@ TESTS_python = \ python/sccfilter.py \ python/setxor.py \ python/trival.py \ + python/twagraph.py \ $(TESTS_ipython) endif diff --git a/tests/python/twagraph.py b/tests/python/twagraph.py new file mode 100644 index 000000000..b87cfdb45 --- /dev/null +++ b/tests/python/twagraph.py @@ -0,0 +1,90 @@ +# -*- 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 +from buddy import bddtrue + +aut = spot.make_twa_graph(spot.make_bdd_dict()) + +try: + print(aut.to_str()) + exit(2) +except RuntimeError as e: + assert "no state" in str(e) + +try: + aut.set_init_state(2) +except ValueError as e: + assert "nonexisting" in str(e) + +try: + aut.set_univ_init_state([2, 1]) +except ValueError as e: + assert "nonexisting" in str(e) + +aut.new_states(3) +aut.set_init_state(2) +assert aut.get_init_state_number() == 2 +e = aut.set_univ_init_state([2, 1]) +assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number())) + +try: + aut.get_init_state() +except RuntimeError as e: + s = str(e) + assert "abstract interface" in s and "alternating automata" in s + +all = aut.set_buchi() +aut.new_acc_edge(0, 1, bddtrue, True) + +try: + s = aut.state_acc_sets(0) +except RuntimeError as e: + assert "state-based acceptance" in str(e) + +try: + s = aut.state_is_accepting(0) +except RuntimeError as e: + assert "state-based acceptance" in str(e) + +aut.prop_state_acc(True) + +assert aut.state_acc_sets(0) == all +assert aut.state_is_accepting(0) == True + +aut.set_init_state(0) +aut.purge_unreachable_states() +i = aut.get_init_state() +assert aut.state_is_accepting(i) == True + +it = aut.succ_iter(i) +it.first() +assert aut.edge_number(it) == 1 +assert aut.state_number(it.dst()) == 1 +assert aut.edge_storage(it).src == 0 +assert aut.edge_storage(1).src == 0 +assert aut.edge_data(it).cond == bddtrue +assert aut.edge_data(1).cond == bddtrue +aut.release_iter(it) + +aut.purge_dead_states() +assert aut.state_is_accepting(i) == False