diff --git a/NEWS b/NEWS index 271d6cacb..5f513f974 100644 --- a/NEWS +++ b/NEWS @@ -235,7 +235,10 @@ New in spot 2.9.7.dev (not yet released) See https://spot.lrde.epita.fr/ipynb/games.html for examples. - spot::twa::prop_set was previously abstent from the Python - binding. It is now available as spot.twa_prop_set (issue #453). + bindings, making it impossible to call make_twa_graph() for copying + a twa. It is now available as spot.twa_prop_set (issue #453). + Also for convenience, the twa_graph.__copy__() method, called by + copy.copy(), will duplicate a twa_graph (issue #470). Bugs fixed: diff --git a/python/spot/__init__.py b/python/spot/__init__.py index dee08467a..46f649449 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2014-2020 Laboratoire de +# Copyright (C) 2014-2021 Laboratoire de # Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -221,6 +221,9 @@ class twa_graph: from spot.jupyter import SVG return SVG(_ostream_to_svg(ostr)) + def __copy__(self): + return make_twa_graph(self, twa_prop_set.all()) + def make_twa_graph(*args): from spot.impl import make_twa_graph as mtg diff --git a/tests/python/twagraph.py b/tests/python/twagraph.py index 69afa735d..743059717 100644 --- a/tests/python/twagraph.py +++ b/tests/python/twagraph.py @@ -44,7 +44,7 @@ except ValueError as 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]) +aut.set_univ_init_state([2, 1]) assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number())) try: @@ -67,6 +67,13 @@ cpy = spot.make_twa_graph(aut, spot.twa_prop_set(False, False, False, assert cpy.prop_universal() != aut.prop_universal() assert cpy.prop_universal() == spot.trival.maybe() +from copy import copy +cpy = copy(aut) +assert aut.to_str() == cpy.to_str() +cpy.set_init_state(1) +assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number())) +assert cpy.get_init_state_number() == 1 + try: s = aut.state_acc_sets(0) except RuntimeError as e: