From 31a681c2850b9e743be65a4cf99599224232c254 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 8 Jul 2021 10:30:19 +0200 Subject: [PATCH] twa: implement a copy_named_properties_of() method It was noted in #470 that make_twa_graph did not copy named properties. Let's fix that. * spot/twa/twa.hh, spot/twa/twa.cc (copy_named_properties_of): New method. * spot/twa/twagraph.hh (make_twa_graph): Add an extra argument to call copy_named_properties_of() optionally. * python/spot/__init__.py (twa_graph.__copy__): Use it. * tests/python/twagraph.py: Test that. * tests/sanity/namedprop.test: Ensure copy_named_properties_of copies all known named properties. --- python/spot/__init__.py | 2 +- spot/twa/twa.cc | 25 ++++++++++++++++++++++++- spot/twa/twa.hh | 5 ++++- spot/twa/twagraph.hh | 14 +++++++++++--- tests/python/twagraph.py | 6 ++++++ tests/sanity/namedprop.test | 28 ++++++++++++++++++++++++---- 6 files changed, 70 insertions(+), 10 deletions(-) diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 46f649449..b49538fbe 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -222,7 +222,7 @@ class twa_graph: return SVG(_ostream_to_svg(ostr)) def __copy__(self): - return make_twa_graph(self, twa_prop_set.all()) + return make_twa_graph(self, twa_prop_set.all(), True) def make_twa_graph(*args): diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index 986aeb397..d3ba85fd6 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -290,6 +290,29 @@ namespace spot bddaps_ = bdd_exist(bddaps_, bdd_ithvar(b)); } - + void + twa::copy_named_properties_of(const const_twa_ptr& a) + { +#define COPY_PROP(type, name) \ + if (auto* prop = a->get_named_prop(name)) \ + set_named_prop(name, new type(*prop)); + COPY_PROP(std::string, "accepted-word"); + COPY_PROP(std::string, "automaton-name"); + COPY_PROP(std::vector, "degen-levels"); + typedef std::map hlmap; + COPY_PROP(hlmap, "highlight-edges"); + COPY_PROP(hlmap, "highlight-states"); + COPY_PROP(std::set, "incomplete-states"); + COPY_PROP(std::vector, "original-clauses"); + COPY_PROP(std::vector, "original-states"); + COPY_PROP(spot::product_states, "product-states"); + COPY_PROP(std::string, "rejected-word"); + COPY_PROP(std::vector, "simulated-states"); + COPY_PROP(std::vector, "state-names"); + COPY_PROP(std::vector, "state-player"); + COPY_PROP(std::vector, "state-winner"); + COPY_PROP(std::vector, "strategy"); + COPY_PROP(bdd, "synthesis-outputs"); + } } diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 426d44b31..cb1e208ec 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2013-2020 Laboratoire de Recherche et +// Copyright (C) 2009, 2011, 2013-2021 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é @@ -972,6 +972,9 @@ namespace spot this->register_ap(f); } + /// Copy all the named properties of \a a into this automaton. + void copy_named_properties_of(const const_twa_ptr& a); + /// \brief Set generalized Büchi acceptance /// /// \param num the number of acceptance sets to use diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index c5bd22d4e..cd0bbe592 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -773,11 +773,19 @@ namespace spot } /// \ingroup twa_representation - /// \brief Build an explicit automaton from all states of \a aut, + /// \brief Clone a twa_graph + /// + /// The \a p and \a preserve_name_properties argument are used to + /// select what automata properties should be preserved by the copy. + /// inline twa_graph_ptr make_twa_graph(const const_twa_graph_ptr& aut, - twa::prop_set p) + twa::prop_set p, + bool preserve_name_properties = false) { - return SPOT_make_shared_enabled__(twa_graph, aut, p); + twa_graph_ptr res = SPOT_make_shared_enabled__(twa_graph, aut, p); + if (preserve_name_properties) + res->copy_named_properties_of(aut); + return res; } /// \ingroup twa_representation diff --git a/tests/python/twagraph.py b/tests/python/twagraph.py index 743059717..6e2593f4a 100644 --- a/tests/python/twagraph.py +++ b/tests/python/twagraph.py @@ -62,10 +62,15 @@ aut.new_acc_edge(0, 1, bddtrue, True) assert aut.num_edges() == 1 + cpy.num_edges() aut.prop_universal(True) +aut.set_name("some name") cpy = spot.make_twa_graph(aut, spot.twa_prop_set(False, False, False, False, False, False)) assert cpy.prop_universal() != aut.prop_universal() assert cpy.prop_universal() == spot.trival.maybe() +assert cpy.get_name() == None +cpy = spot.make_twa_graph(aut, spot.twa_prop_set(False, False, False, + False, False, False), True) +assert cpy.get_name() == "some name" from copy import copy cpy = copy(aut) @@ -73,6 +78,7 @@ 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 +assert cpy.get_name() == "some name" try: s = aut.state_acc_sets(0) diff --git a/tests/sanity/namedprop.test b/tests/sanity/namedprop.test index 864d603d3..46bbc9fd1 100755 --- a/tests/sanity/namedprop.test +++ b/tests/sanity/namedprop.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2017, 2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -26,6 +26,8 @@ set +x DOC=doc/org/concepts.org +CPY=spot/twa/twa.cc +err=0 rm -f namedprop.log @@ -40,14 +42,32 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do done | xargs sed -n 's/.*get_named_prop<.*>("\([^"]*\)").*/\1/p s/.*set_named_prop("\([^"]*\)",.*/\1/p' | -sort | uniq | +sort | uniq > proplist.lst + while read prop; do if ! grep -q "$prop" "$TOP/$DOC"; then echo "* $prop" >>namedprop.log fi -done +done < proplist.lst if test -f namedprop.log; then echo "The following named properties are not documented in $DOC:" cat namedprop.log - exit 1 + err=1 fi + +rm -f namedprop.log + +while read prop; do + if ! grep -q "COPY_PROP.*$prop" "$TOP/$CPY"; then + echo "* $prop" >>namedprop.log + fi +done < proplist.lst +if test -f namedprop.log; then + echo "These properties are not copied by copy_named_properties_of() ($CPY):" + cat namedprop.log + err=1 +fi + +rm -f namedprop.log proplist.lst + +exit $err