more documentation for twa_graph internals

* spot/graph/graph.hh, spot/twa/twagraph.hh, spot/twa/twagraph.cc:
Implement a dump_storage_as_dot() method.
* python/spot/__init__.py (twa_graph.show_storage): New method, above
dump_storage_as_dot().
* tests/python/twagraph-internals.ipynb: New file, with documentation
about the twa_graph internals, using show_storage() to illustrate
everything.
* tests/Makefile.am, doc/org/tut.org: Add it.
* python/spot/impl.i: Add bindings for out_iterasor, demonstrated in
the Python notebook.
* spot/twa/twa.hh: Add prop_reset().  Used in the notebook.
* NEWS: Mention the new notebook and function.
* doc/org/tut50.org: Link to the notebook.
* tests/python/ipnbdoctest.py: Adjust for twa_graph_ptr being
redefined in the spot namespace.

NEWS

@@ -14,6 +14,11 @@ New in spot 2.6.0.dev  (not yet released)
       formula::F(unsigned, unsigned, formula)
       formula::G(unsigned, unsigned, formula)
 
+  - The twa_graph class has a new dump_storage_as_dot() method
+    to show its data structure.  This is more conveniently used
+    as aut.show_storage() in a Jupyter notebook.  See
+    https://spot.lrde.epita.fr/ipynb/twagraph-internals.html
+
 New in spot 2.6  (2018-07-04)
 
   Command-line tools:

doc/org/tut.org

@@ -85,3 +85,4 @@ real notebooks instead.
 - [[https://spot.lrde.epita.fr/ipynb/alternation.html][=alternation.ipynb=]] examples of alternating automata.
 - [[https://spot.lrde.epita.fr/ipynb/stutter-inv.html][=stutter-inv.ipynb=]] working with stutter-invariant formulas properties.
 - [[https://spot.lrde.epita.fr/ipynb/satmin.html][=satmin.ipynb=]] Python interface for [[file:satmin.org][SAT-based minimization of deterministic ω-automata]].
+- [[https://spot.lrde.epita.fr/ipynb/twagraph-internals.html][=twagraph-internals.ipynb=]] Inner workings of the =twa_graph= class.

doc/org/tut50.org

@@ -21,9 +21,10 @@ from the initial state of an automaton.
 
 The explicit interface can only be used on =twa_graph= objects.  In
 this interface, states and edges are referred to by numbers that are
-indices into state and edge vectors.  This interface is lightweight,
-and is the preferred interface for writing most automata algorithms in
-Spot.
+indices into state and edge vectors (the [[https://spot.lrde.epita.fr/ipynb/satmin.html][=twagraph-internals.ipynb=]]
+notebook shows these vectors graphically).  This interface is
+lightweight, and is the preferred interface for writing most automata
+algorithms in Spot.
 
 ** How this interface works
 

python/spot/__init__.py

@@ -175,6 +175,13 @@ class twa:
                 f.write('\n')
         return a
 
+@_extend(twa_graph)
+class twa_graph:
+    def show_storage(self, opt=None):
+        ostr = ostringstream()
+        self.dump_storage_as_dot(ostr, opt)
+        from IPython.display import SVG
+        return SVG(_ostream_to_svg(ostr))
 
 @_extend(formula)
 class formula:
@@ -761,6 +768,7 @@ def postprocess(automaton, *args, formula=None):
 
 twa.postprocess = postprocess
 
+
 # Wrap C++-functions into lambdas so that they get converted into
 # instance methods (i.e., self passed as first argument
 # automatically), because only user-defined functions are converted as

python/spot/impl.i

@@ -509,6 +509,7 @@ namespace std {
 %include <spot/graph/graph.hh>
 %nodefaultctor spot::digraph;
 %nodefaultctor spot::internal::state_out;
+%nodefaultctor spot::internal::killer_edge_iterator;
 %nodefaultctor spot::internal::all_trans;
 %nodefaultctor spot::internal::universal_dests;
 %traits_swigtype(spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >);
@@ -556,6 +557,7 @@ def state_is_accepting(self, src) -> "bool":
 
 %include <spot/twa/twagraph.hh>
 %template(twa_graph_state_out) spot::internal::state_out<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>>;
+%template(twa_graph_killer_edge_iterator) spot::internal::killer_edge_iterator<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>>;
 %template(twa_graph_all_trans) spot::internal::all_trans<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>>;
 %template(twa_graph_edge_boxed_data) spot::internal::boxed_label<spot::twa_graph_edge_data, false>;
 %template(twa_graph_edge_storage) spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >;
@@ -799,6 +801,23 @@ def state_is_accepting(self, src) -> "bool":
    }
 }
 
+%extend spot::internal::killer_edge_iterator<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>> {
+
+  spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >& current()
+  {
+    return **self;
+  }
+
+  void advance()
+  {
+    ++*self;
+  }
+  bool __bool__()
+  {
+    return *self;
+  }
+}
+
 %extend spot::internal::all_trans<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>> {
   swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
    {

spot/graph/graph.hh

@@ -1059,6 +1059,156 @@ namespace spot
         }
     }
 
+    enum dump_storage_items {
+      DSI_GraphHeader = 1,
+      DSI_GraphFooter = 2,
+      DSI_StatesHeader = 4,
+      DSI_StatesBody = 8,
+      DSI_StatesFooter = 16,
+      DSI_States = DSI_StatesHeader | DSI_StatesBody | DSI_StatesFooter,
+      DSI_EdgesHeader = 32,
+      DSI_EdgesBody = 64,
+      DSI_EdgesFooter = 128,
+      DSI_Edges = DSI_EdgesHeader | DSI_EdgesBody | DSI_EdgesFooter,
+      DSI_DestsHeader = 256,
+      DSI_DestsBody = 512,
+      DSI_DestsFooter = 1024,
+      DSI_Dests = DSI_DestsHeader | DSI_DestsBody | DSI_DestsFooter,
+      DSI_All =
+      DSI_GraphHeader | DSI_States | DSI_Edges | DSI_Dests | DSI_GraphFooter,
+    };
+
+    /// Dump the state and edge storage for debugging
+    void dump_storage_as_dot(std::ostream& o, int dsi = DSI_All) const
+    {
+      if (dsi & DSI_GraphHeader)
+        o << "digraph g { \nnode [shape=plaintext]\n";
+      unsigned send = states_.size();
+      if (dsi & DSI_StatesHeader)
+        {
+          o << ("states [label=<\n"
+                "<table border='0' cellborder='1' cellspacing='0'>\n"
+                "<tr><td sides='b' bgcolor='yellow' port='s'>states</td>\n");
+          for (unsigned s = 0; s < send; ++s)
+            o << "<td sides='b' bgcolor='yellow' port='s" << s << "'>"
+              << s << "</td>\n";
+          o << "</tr>\n";
+        }
+      if (dsi & DSI_StatesBody)
+        {
+          o << "<tr><td port='ss'>succ</td>\n";
+          for (unsigned s = 0; s < send; ++s)
+            {
+              o << "<td port='ss" << s;
+              if (states_[s].succ)
+                o << "' bgcolor='cyan";
+              o << "'>" << states_[s].succ << "</td>\n";
+            }
+          o << "</tr><tr><td port='st'>succ_tail</td>\n";
+          for (unsigned s = 0; s < send; ++s)
+            {
+              o << "<td port='st" << s;
+              if (states_[s].succ_tail)
+                o << "' bgcolor='cyan";
+              o << "'>" << states_[s].succ_tail << "</td>\n";
+            }
+          o << "</tr>\n";
+        }
+      if (dsi & DSI_StatesFooter)
+        o << "</table>>]\n";
+      unsigned eend = edges_.size();
+      if (dsi & DSI_EdgesHeader)
+        {
+          o << ("edges [label=<\n"
+                "<table border='0' cellborder='1' cellspacing='0'>\n"
+                "<tr><td sides='b' bgcolor='cyan' port='e'>edges</td>\n");
+          for (unsigned e = 1; e < eend; ++e)
+            {
+              o << "<td sides='b' bgcolor='"
+                << (e != edges_[e].next_succ ? "cyan" : "gray")
+                << "' port='e" << e << "'>" << e << "</td>\n";
+            }
+          o << "</tr>";
+        }
+      if (dsi & DSI_EdgesBody)
+        {
+          o << "<tr><td port='ed'>dst</td>\n";
+          for (unsigned e = 1; e < eend; ++e)
+            {
+              o << "<td port='ed" << e;
+              int d = edges_[e].dst;
+              if (d < 0)
+                o << "' bgcolor='pink'>~" << ~d;
+              else
+                o << "' bgcolor='yellow'>" << d;
+              o << "</td>\n";
+            }
+          o << "</tr><tr><td port='en'>next_succ</td>\n";
+          for (unsigned e = 1; e < eend; ++e)
+            {
+              o << "<td port='en" << e;
+              if (edges_[e].next_succ)
+                {
+                  if (edges_[e].next_succ != e)
+                    o << "' bgcolor='cyan";
+                  else
+                    o << "' bgcolor='gray";
+                }
+              o << "'>" << edges_[e].next_succ << "</td>\n";
+            }
+          o << "</tr><tr><td port='es'>src</td>\n";
+          for (unsigned e = 1; e < eend; ++e)
+            o << "<td port='es" << e << "' bgcolor='yellow'>"
+              << edges_[e].src << "</td>\n";
+          o << "</tr>\n";
+        }
+      if (dsi & DSI_EdgesFooter)
+        o << "</table>>]\n";
+      if (!dests_.empty())
+        {
+          unsigned dend = dests_.size();
+          if (dsi & DSI_DestsHeader)
+            {
+              o << ("dests [label=<\n"
+                    "<table border='0' cellborder='1' cellspacing='0'>\n"
+                    "<tr><td sides='b' bgcolor='pink' port='d'>dests</td>\n");
+              unsigned d = 0;
+              while (d < dend)
+                {
+                  o << "<td sides='b' bgcolor='pink' port='d"
+                    << d << "'>~" << d << "</td>\n";
+                  unsigned cnt = dests_[d];
+                  d += cnt + 1;
+                  while (cnt--)
+                    o << "<td sides='b'></td>\n";
+                }
+              o << "</tr>\n";
+            }
+          if (dsi & DSI_DestsBody)
+            {
+              o << "<tr><td port='dd'>#cnt/dst</td>\n";
+              unsigned d = 0;
+              while (d < dend)
+                {
+                  unsigned cnt = dests_[d];
+                  o << "<td port='d'>#" << cnt << "</td>\n";
+                  ++d;
+                  while (cnt--)
+                    {
+                      o << "<td bgcolor='yellow' port='dd"
+                        << d << "'>" << dests_[d] << "</td>\n";
+                      ++d;
+                    }
+                }
+              o << "</tr>\n";
+            }
+          if (dsi & DSI_DestsFooter)
+            o << "</table>>]\n";
+        }
+      if (dsi & DSI_GraphFooter)
+        o << "}\n";
+    }
+
     /// \brief Remove all dead edges.
     ///
     /// The edges_ vector is left in a state that is incorrect and

spot/twa/twa.hh

@@ -1071,6 +1071,7 @@ namespace spot
       bprop is;
     };
 
+  protected:
 #ifndef SWIG
     // Dynamic properties, are given with a name and a destructor function.
     std::unordered_map<std::string,
@@ -1686,6 +1687,10 @@ namespace spot
         prop_stutter_invariant(trival::maybe());
     }
 
+    void prop_reset()
+    {
+      prop_keep({});
+    }
   };
 
 #ifndef SWIG

spot/twa/twagraph.cc

@@ -21,6 +21,8 @@
 #include <spot/twa/twagraph.hh>
 #include <spot/tl/print.hh>
 #include <spot/misc/bddlt.hh>
+#include <spot/twa/bddprint.hh>
+#include <spot/misc/escape.hh>
 #include <vector>
 #include <deque>
 
@@ -764,6 +766,141 @@ namespace spot
     set_named_prop("state-names", names.release());
   }
 
+  void twa_graph::dump_storage_as_dot(std::ostream& out,
+                                      const char* opt) const
+  {
+    bool want_vectors = false;
+    bool want_data = false;
+    bool want_properties = false;
+    if (!opt || !*opt)
+      {
+        want_vectors = want_data = want_properties = true;
+      }
+    else
+      {
+        while (*opt)
+          switch (*opt++)
+            {
+            case 'v':
+              want_vectors = true;
+              break;
+            case 'd':
+              want_data = true;
+              break;
+            case 'p':
+              want_properties = true;
+              break;
+            default:
+              throw std::runtime_error(std::string("dump_storage_as_dow(): "
+                                                   "unsupported option '")
+                                       + opt[-1] +"'");
+            }
+      }
+
+    const graph_t& g = get_graph();
+
+    g.dump_storage_as_dot(out, graph_t::DSI_GraphHeader);
+    out << "rankdir=BT\n";
+
+    if (want_vectors)
+      {
+        out << "{rank=same;\n";
+
+        g.dump_storage_as_dot(out, graph_t::DSI_States |
+                              graph_t::DSI_EdgesHeader);
+
+        auto edges = g.edge_vector();
+        unsigned eend = edges.size();
+        out << "<tr><td>cond</td>\n";
+        for (unsigned e = 1; e < eend; ++e)
+          {
+            out << "<td>";
+            std::string f = bdd_format_formula(get_dict(), edges[e].cond);
+            escape_html(out, f);
+            out << "</td>\n";
+          }
+        out << "</tr>\n<tr><td>acc</td>\n";
+        for (unsigned e = 1; e < eend; ++e)
+          out << "<td>" << edges[e].acc << "</td>\n";
+        out << "</tr>\n";
+
+        g.dump_storage_as_dot(out, graph_t::DSI_EdgesBody
+                              | graph_t::DSI_EdgesFooter
+                              | graph_t::DSI_Dests);
+        out << "}\n";
+      }
+    if (want_data || want_properties)
+      {
+        out << "{rank=same;\n";
+
+        if (want_data)
+          {
+            out << ("meta [label=<\n"
+                    "<table border='0' cellborder='0' cellspacing='0'>\n");
+            unsigned d = get_init_state_number();
+            out << ("<tr><td align='left'>init_state:</td>"
+                    "<td align='left' bgcolor='");
+            if ((int)d < 0)
+              out << "pink'>~" << ~d;
+            else
+              out << "yellow'>" << d;
+            out << ("</td></tr><tr><td align='left'>num_sets:</td>"
+                    "<td align='left' >")
+                << num_sets()
+                << ("</td></tr><tr><td align='left'>acceptance:</td>"
+                    "<td align='left' >");
+            get_acceptance().to_html(out);
+            out << ("</td></tr><tr><td align='left'>ap_vars:</td>"
+                    "<td align='left'>");
+            escape_html(out, bdd_format_sat(get_dict(), ap_vars()));
+            out << "</td></tr></table>>]\n";
+          }
+        if (want_properties)
+          {
+            out << ("props [label=<\n"
+                    "<table border='0' cellborder='0' cellspacing='0'>\n");
+#define print_prop(name)                                                \
+            out << ("<tr><td align='left'>" #name ":</td>"              \
+                    "<td align='left' >") << name() << "</td></tr>\n";
+            print_prop(prop_state_acc);
+            print_prop(prop_inherently_weak);
+            print_prop(prop_terminal);
+            print_prop(prop_weak);
+            print_prop(prop_very_weak);
+            print_prop(prop_complete);
+            print_prop(prop_universal);
+            print_prop(prop_unambiguous);
+            print_prop(prop_semi_deterministic);
+            print_prop(prop_stutter_invariant);
+#undef print_prop
+            out << "</table>>]\n";
+
+            if (!named_prop_.empty())
+              {
+                out << "namedprops [label=\"named properties:\n";
+                for (auto p: named_prop_)
+                  escape_html(out, p.first) << '\n';
+                out << "\"]\n";
+              }
+          }
+        out << "}\n";
+      }
+
+    if (want_data && want_vectors)
+      out << "meta -> states [style=invis]\n";
+    if (want_properties && want_vectors)
+      {
+        out << "props -> edges [style=invis]\n";
+        if (!named_prop_.empty())
+          {
+            out << "namedprops -> edges [style=invis]\n";
+            if (!is_existential())
+              out << "namedprops -> dests [style=invis]\n";
+          }
+      }
+    g.dump_storage_as_dot(out, graph_t::DSI_GraphFooter);
+  }
+
   namespace
   {
     twa_graph_ptr

spot/twa/twagraph.hh

@@ -471,6 +471,12 @@ namespace spot
       return g_.out(src);
     }
 
+    internal::killer_edge_iterator<graph_t>
+    out_iteraser(unsigned src)
+    {
+      return g_.out_iteraser(src);
+    }
+
     internal::const_universal_dests
     univ_dests(unsigned d) const noexcept
     {
@@ -525,11 +531,18 @@ namespace spot
       SPOT_RETURN(g_.edge_vector());
     auto edge_vector()
       SPOT_RETURN(g_.edge_vector());
-
-    auto is_dead_edge(const graph_t::edge_storage_t& t) const
-      SPOT_RETURN(g_.is_dead_edge(t));
 #endif
 
+    bool is_dead_edge(unsigned t) const
+    {
+      return g_.is_dead_edge(t);
+    }
+
+    bool is_dead_edge(const graph_t::edge_storage_t& t) const
+    {
+      return g_.is_dead_edge(t);
+    }
+
     /// \brief Merge edges that can be merged.
     ///
     /// This makes two passes over the automaton to reduce the number
@@ -682,6 +695,14 @@ namespace spot
     /// Use -1U to erase a state.
     /// \param used_states the number of states used (after renumbering)
     void defrag_states(std::vector<unsigned>&& newst, unsigned used_states);
+
+    /// \brief Print the data structures used to represent the
+    /// automaton in dot's format.
+    ///
+    /// \a opt should be a substring of "vdp" if you want to print
+    /// only the vectors, data, or properties.
+    void dump_storage_as_dot(std::ostream& out,
+                             const char* opt = nullptr) const;
   };
 
   /// \ingroup twa_representation

tests/Makefile.am

@@ -351,6 +351,7 @@ TESTS_ipython = \
   python/satmin.ipynb \
   python/stutter-inv.ipynb \
   python/testingaut.ipynb \
+  python/twagraph-internals.ipynb \
   python/word.ipynb
 
 # TESTS_python contains all tests.  It may includes notebooks we

tests/python/ipnbdoctest.py

@@ -81,6 +81,9 @@ def canonicalize(s, type, ignores):
     # normalize UUIDs:
     s = re.sub(r'[a-f0-9]{8}(\-[a-f0-9]{4}){3}\-[a-f0-9]{12}', 'U-U-I-D', s)
 
+    # class from spot.impl. may be redefined in spot. without notice.
+    s = re.sub(r'<spot.impl.', '<spot.', s)
+
     # normalize graphviz version
     s = re.sub(r'Generated by graphviz version.*', 'VERSION', s)
 
@@ -108,10 +111,14 @@ def canonicalize(s, type, ignores):
     # be in 2.38.
     s = re.sub(r'"#000000"', '"black"', s)
     s = re.sub(r'"#ffffff"', '"white"', s)
+    s = re.sub(r'"#ffff00"', '"yellow"', s)
+    s = re.sub(r'"#00ffff"', '"cyan"', s)
+    s = re.sub(r'"#ffc0cb"', '"pink"', s)
     s = re.sub(r'"#00ff00"', '"green"', s)
     s = re.sub(r'"#ff0000"', '"red"', s)
     s = re.sub(r'"#c0c0c0"', '"grey"', s)
     s = re.sub(r'"#ffa500"', '"orange"', s)
+    s = re.sub(r'"gray"', '"grey"', s)
     s = re.sub(r' fill="black"', '', s)
     s = re.sub(r' stroke="transparent"', ' stroke="none"', s)
     s = re.sub(r'><title>', '>\n<title>', s)