alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

python: implement twa_graph.__copy__

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2021-07-08 09:33:57 +02:00
parent 0509263f82
commit 0cf2d285b6
3 changed files with 16 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -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. See https://spot.lrde.epita.fr/ipynb/games.html for examples.
- spot::twa::prop_set was previously abstent from the Python - 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: Bugs fixed:

5
python/spot/__init__.py
View file

@ -1,5 +1,5 @@
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2014-2020 Laboratoire de # Copyright (C) 2014-2021 Laboratoire de
# Recherche et Développement de l'Epita (LRDE). # Recherche et Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -221,6 +221,9 @@ class twa_graph:
from spot.jupyter import SVG from spot.jupyter import SVG
return SVG(_ostream_to_svg(ostr)) return SVG(_ostream_to_svg(ostr))
def __copy__(self):
return make_twa_graph(self, twa_prop_set.all())
def make_twa_graph(*args): def make_twa_graph(*args):
from spot.impl import make_twa_graph as mtg from spot.impl import make_twa_graph as mtg

9
tests/python/twagraph.py
View file

@ -44,7 +44,7 @@ except ValueError as e:
aut.new_states(3) aut.new_states(3)
aut.set_init_state(2) aut.set_init_state(2)
assert aut.get_init_state_number() == 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())) assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number()))
try: 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() != aut.prop_universal()
assert cpy.prop_universal() == spot.trival.maybe() 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: try:
s = aut.state_acc_sets(0) s = aut.state_acc_sets(0)
except RuntimeError as e: except RuntimeError as e: