From 0cf2d285b6d5ffeea486661926e1342902285d9b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 8 Jul 2021 09:33:57 +0200 Subject: [PATCH] python: implement twa_graph.__copy__ Fixes #470, suggested by Cambridge Yang. * python/spot/__init__.py (twa_graph.__copy__): Call make_twa_graph. * tests/python/twagraph.py: Test it. * NEWS: Mention it. --- NEWS | 5 ++++- python/spot/__init__.py | 5 ++++- tests/python/twagraph.py | 9 ++++++++- 3 files changed, 16 insertions(+), 3 deletions(-) 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: