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

@@ -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):

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<type>(name)) \
+      set_named_prop(name, new type(*prop));
+    COPY_PROP(std::string, "accepted-word");
+    COPY_PROP(std::string, "automaton-name");
+    COPY_PROP(std::vector<unsigned>, "degen-levels");
+    typedef std::map<unsigned, unsigned> hlmap;
+    COPY_PROP(hlmap, "highlight-edges");
+    COPY_PROP(hlmap, "highlight-states");
+    COPY_PROP(std::set<unsigned>, "incomplete-states");
+    COPY_PROP(std::vector<unsigned>, "original-clauses");
+    COPY_PROP(std::vector<unsigned>, "original-states");
+    COPY_PROP(spot::product_states, "product-states");
+    COPY_PROP(std::string, "rejected-word");
+    COPY_PROP(std::vector<unsigned>, "simulated-states");
+    COPY_PROP(std::vector<std::string>, "state-names");
+    COPY_PROP(std::vector<bool>, "state-player");
+    COPY_PROP(std::vector<bool>, "state-winner");
+    COPY_PROP(std::vector<unsigned>, "strategy");
+    COPY_PROP(bdd, "synthesis-outputs");
+  }
 
 }

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

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

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)

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