highlight: improve support for highlighted edges

* spot/twa/twa.cc, spot/twa/twa.hh: Add a way to
remove named properties.
* spot/twa/twagraph.cc: Clear highlight-edges on operations
that reorder the edge vector.
* spot/twaalgos/randomize.cc, spot/twaalgos/randomize.hh:
Preserve highlighted state, but not highlighted edges.
* spot/twaalgos/hoa.cc: Adjust output of highlight-edge
when the edges are not stored in order.
* tests/core/readsave.test, tests/core/tgbagraph.test,
tests/core/twagraph.cc: More test cases.

spot/twa/twa.cc

@@ -69,6 +69,17 @@ namespace spot
     return !couvreur99(a)->check();
   }
 
+  void
+  twa::set_named_prop(std::string s, std::nullptr_t)
+  {
+    auto p = named_prop_.find(s);
+    if (p == named_prop_.end())
+      return;
+    p->second.second(p->second.first);
+    named_prop_.erase(p);
+    return;
+  }
+
   void
   twa::set_named_prop(std::string s,
                       void* val, std::function<void(void*)> destructor)

spot/twa/twa.hh

@@ -22,6 +22,7 @@
 
 #pragma once
 
+#include <cstddef>
 #include <spot/twa/fwd.hh>
 #include <spot/twa/acc.hh>
 #include <spot/twa/bdddict.hh>
@@ -952,7 +953,7 @@ namespace spot
 #ifndef SWIG
     /// \brief Declare a named property
     ///
-    /// Arbitrary object can be attached to automata.  Those are called
+    /// Arbitrary objects can be attached to automata.  Those are called
     /// named properties.  They are used for instance to name all the
     /// state of an automaton.
     ///
@@ -969,15 +970,16 @@ namespace spot
 
     /// \brief Declare a named property
     ///
-    /// Arbitrary object can be attached to automata.  Those are called
+    /// Arbitrary objects can be attached to automata.  Those are called
     /// named properties.  They are used for instance to name all the
     /// state of an automaton.
     ///
+    ///
     /// This function attaches the object \a val to the current automaton,
     /// under the name \a s.
     ///
-    /// The object will be automatically destroyed when the automaton
+    /// When the automaton is destroyed, the \a destructor function will
-    /// is destroyed.
+    /// be called to destroy the attached object.
     ///
     /// See https://spot.lrde.epita.fr/concepts.html#named-properties
     /// for a list of named properties used by Spot.
@@ -987,6 +989,18 @@ namespace spot
       set_named_prop(s, val, [](void *p) { delete static_cast<T*>(p); });
     }
 
+    /// \brief Erase a named property
+    ///
+    /// Arbitrary objects can be attached to automata.  Those are called
+    /// named properties.  They are used for instance to name all the
+    /// state of an automaton.
+    ///
+    /// This function removes the property \a s if it exists.
+    ///
+    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
+    /// for a list of named properties used by Spot.
+    void set_named_prop(std::string s, std::nullptr_t);
+
     /// \brief Retrieve a named property
     ///
     /// Because named property can be object of any type, retrieving

spot/twa/twagraph.cc

@@ -45,6 +45,7 @@ namespace spot
 
   void twa_graph::merge_edges()
   {
+    set_named_prop("highlight-edges", nullptr);
     g_.remove_dead_edges_();
 
     typedef graph_t::edge_storage_t tr_t;
@@ -272,8 +273,7 @@ namespace spot
   void twa_graph::defrag_states(std::vector<unsigned>&& newst,
                                 unsigned used_states)
   {
-    auto* names = get_named_prop<std::vector<std::string>>("state-names");
+    if (auto* names = get_named_prop<std::vector<std::string>>("state-names"))
-    if (names)
       {
         unsigned size = names->size();
         for (unsigned s = 0; s < size; ++s)
@@ -285,6 +285,18 @@ namespace spot
           }
         names->resize(used_states);
       }
+    if (auto hs = get_named_prop<std::map<unsigned, unsigned>>
+        ("highlight-states"))
+      {
+        std::map<unsigned, unsigned> hs2;
+        for (auto p: *hs)
+          {
+            unsigned dst = newst[p.first];
+            if (dst != -1U)
+              hs2[dst] = p.second;
+          }
+        std::swap(*hs, hs2);
+      }
     g_.defrag_states(std::move(newst), used_states);
   }
 

spot/twaalgos/hoa.cc

@@ -508,9 +508,24 @@ namespace spot
         if (auto hedges = aut->get_named_prop
             <std::map<unsigned, unsigned>>("highlight-edges"))
           {
+            // Numbering edges is a delicate process.  The
+            // "highlight-edges" property uses edges numbers that are
+            // indices in the "edges" vector.  However these edges
+            // need not be sorted.  When edges are output in HOA, they
+            // are output with increasing source state number, and the
+            // edges number expected in the HOA file should use that
+            // order.  So we need to make a first pass on the
+            // automaton to number all edges as they will be output.
+            unsigned maxedge = aut->edge_vector().size();
+            std::vector<unsigned> renum(maxedge);
+            unsigned edge = 0;
+            for (unsigned i = 0; i < num_states; ++i)
+              for (auto& t: aut->out(i))
+                renum[aut->get_graph().index_of_edge(t)] = ++edge;
             os << "spot.highlight.edges:";
             for (auto& p: *hedges)
-              os << ' ' << p.first << ' ' << p.second;
+              if (p.first < maxedge) // highlighted edges could come from user
+                os << ' ' << renum[p.first] << ' ' << p.second;
             os << nl;
           }
       }

spot/twaalgos/randomize.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
+// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -50,6 +50,14 @@ namespace spot
               (*nn)[nums[i]] = (*sn)[i];
             aut->set_named_prop("state-names", nn);
           }
+        if (auto hs = aut->get_named_prop<std::map<unsigned, unsigned>>
+            ("highlight-states"))
+          {
+            std::map<unsigned, unsigned> hs2;
+            for (auto p: *hs)
+              hs2[nums[p.first]] = p.second;
+            std::swap(*hs, hs2);
+          }
       }
     if (randomize_edges)
       {
@@ -57,7 +65,7 @@ namespace spot
         auto& v = g.edge_vector();
         mrandom_shuffle(v.begin() + 1, v.end());
       }
-
+    aut->set_named_prop("highlight-edges", nullptr);
     typedef twa_graph::graph_t::edge_storage_t tr_t;
     g.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
                         { return lhs.src < rhs.src; });

spot/twaalgos/randomize.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -27,6 +27,9 @@ namespace spot
   ///
   /// Make a random permutation of the state, and of the edges
   /// leaving this state.
+  ///
+  /// This function preserves state names, and highlighted states,
+  /// but it does not preserve highlighted edges.
   SPOT_API void
   randomize(twa_graph_ptr& aut,
             bool randomize_states = true,

tests/core/readsave.test

@@ -980,14 +980,14 @@ acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc deterministic
 properties: stutter-invariant terminal
-spot.highlight.edges: 1 0 2 1 3 2 4 3
+spot.highlight.edges: 3 0 1 1 4 3 2 2
 spot.highlight.states: 0 0 2 3
 --BODY--
+State: 1  /* Defined before State 0 on purpose */
+[2] 0     /* because it affects the edge numbering */
+[1&!2] 1  /* used in spot.highlight.edges */
 State: 0 {0}
 [t] 0
-State: 1
-[2] 0
-[1&!2] 1
 State: 2
 [2] 0
 [!0&1&!2] 1

tests/core/tgbagraph.test

@@ -226,17 +226,34 @@ digraph G {
   node [shape="circle"]
   I [label="", style=invis, width=0]
   I -> 2
-  0 [label="s1"]
+  0 [label="s1", style="bold", color="#F15854"]
   1 [label="s2"]
-  2 [label="s3"]
+  2 [label="s3", style="bold", color="#4D4D4D"]
 }
 digraph G {
   rankdir=LR
   node [shape="circle"]
   I [label="", style=invis, width=0]
   I -> 0
-  0 [label="s3"]
+  0 [label="s3", style="bold", color="#4D4D4D"]
 }
+HOA: v1.1
+States: 3
+Start: 2
+AP: 0
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+spot.highlight.edges: 3 1 2 2 1 3
+--BODY--
+State: 0
+[t] 0
+State: 1
+[t] 0
+State: 2
+[t] 1
+--END--
 EOF
 
 diff stdout expected

tests/core/twagraph.cc

@@ -21,6 +21,7 @@
 #include <iostream>
 #include <spot/twa/twagraph.hh>
 #include <spot/twaalgos/dot.hh>
+#include <spot/twaalgos/hoa.hh>
 #include <spot/tl/defaultenv.hh>
 
 static void f1()
@@ -84,7 +85,7 @@ static void f1()
   spot::print_dot(std::cout, tg);
 }
 
-// Test purge with named states.
+// Test purge with named and highlighted states.
 static void f2()
 {
   auto d = spot::make_bdd_dict();
@@ -93,20 +94,44 @@ static void f2()
   auto s1 = tg->new_state();
   auto s2 = tg->new_state();
   auto s3 = tg->new_state();
-  (void) s1;
   (void) s2;
-  std::vector<std::string>* names;
+  tg->set_named_prop("state-names",
-  names = new std::vector<std::string>({"s1", "s2", "s3"});
+                     new std::vector<std::string>({"s1", "s2", "s3"}));
-
+  {
-  tg->set_named_prop<std::vector<std::string>>("state-names", names);
+    auto hs = new std::map<unsigned, unsigned>;
+    hs->emplace(s1, 5);
+    hs->emplace(s3, 7);
+    tg->set_named_prop("highlight-states", hs);
+  }
   tg->set_init_state(s3);
   spot::print_dot(std::cout, tg);
   tg->purge_unreachable_states();
   spot::print_dot(std::cout, tg);
 }
 
+// Make sure the HOA printer adjusts the highlighted edges numbers
+static void f3()
+{
+  auto d = spot::make_bdd_dict();
+  auto tg = make_twa_graph(d);
+
+  auto hs = new std::map<unsigned, unsigned>;
+  tg->set_named_prop("highlight-edges", hs);
+
+  auto s1 = tg->new_state();
+  auto s2 = tg->new_state();
+  auto s3 = tg->new_state();
+  tg->set_init_state(s3);
+  hs->emplace(tg->new_edge(s3, s2, bddtrue), 1);
+  hs->emplace(tg->new_edge(s2, s1, bddtrue), 2);
+  hs->emplace(tg->new_edge(s1, s1, bddtrue), 3);
+
+  spot::print_hoa(std::cout, tg, "1.1") << '\n';
+}
+
 int main()
 {
   f1();
   f2();
+  f3();
 }