From d7e49255d379b622b0122d8e3dbfa3e1108eb734 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 26 May 2003 14:20:31 +0000
Subject: [PATCH] * src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files.
 * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.

---
 ChangeLog                 |  5 ++-
 src/tgbaalgos/Makefile.am |  4 ++-
 src/tgbaalgos/dotty.cc    | 68 +++++++++++++++++++++++++++++++++++++++
 src/tgbaalgos/dotty.hh    | 13 ++++++++
 4 files changed, 88 insertions(+), 2 deletions(-)
 create mode 100644 src/tgbaalgos/dotty.cc
 create mode 100644 src/tgbaalgos/dotty.hh

diff --git a/ChangeLog b/ChangeLog
index 7d4b8e556..1b70f0749 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,6 +1,9 @@
 2003-05-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
-	* src/tgba/tgbabddtranslatefactory.cc 
+	* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files.
+	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.
+
+	* src/tgba/tgbabddtranslatefactory.cc
 	(tgba_bdd_translate_factory::compute_pairs): Be quiet.
 
 	* src/Makefile.am (SUBDIRS): Add tgbaalgos.
diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am
index 12aabff32..1ea6cb316 100644
--- a/src/tgbaalgos/Makefile.am
+++ b/src/tgbaalgos/Makefile.am
@@ -2,4 +2,6 @@ AM_CPPFLAGS = -I$(srcdir)/..
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 noinst_LTLIBRARIES = libtgbaalgos.la
-libtgbaalgos_la_SOURCES = 
+libtgbaalgos_la_SOURCES = \
+  dotty.cc \
+  dotty.hh
diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc
new file mode 100644
index 000000000..79f9d42ba
--- /dev/null
+++ b/src/tgbaalgos/dotty.cc
@@ -0,0 +1,68 @@
+#include <map>
+#include "dotty.hh"
+#include "tgba/bddprint.hh"
+
+namespace spot
+{
+  typedef std::map<int, int> seen_map;
+  
+  static bool
+  dotty_state(std::ostream& os,
+	      const tgba& g, state_bdd state, seen_map& m, int& node)
+  {
+    bdd s = state.as_bdd();
+    seen_map::iterator i = m.find(s.id());
+    
+    // Already drawn?
+    if (i != m.end())
+      {
+	node = i->second;
+	return false;
+      }
+    
+    node = m.size() + 1;
+    m[s.id()] = node;
+    
+    std::cout << "  " << node << " [label=\"";
+    bdd_print_set(os, g.get_dict(), s) << "\"]" << std::endl;
+    return true;
+  }
+  
+  static void
+  dotty_rec(std::ostream& os,
+	    const tgba& g, state_bdd state, seen_map& m, int father)
+  {
+    tgba_succ_iterator* si = g.succ_iter(state);
+    for (si->first(); !si->done(); si->next())
+      {
+	int node;
+	state_bdd s = si->current_state();
+	bool recurse = dotty_state(os, g, s, m, node);
+	os << "  " << father << " -> " << node << " [label=\"";
+	bdd_print_set(os, g.get_dict(), si->current_condition()) << "\\n";
+	bdd_print_set(os, g.get_dict(), si->current_promise()) << "\"]" 
+							       << std::endl;
+	if (recurse)
+	  dotty_rec(os, g, s, m, node);
+      }
+    delete si;
+  }
+  
+  std::ostream& 
+  dotty_reachable(std::ostream& os, const tgba& g)
+  {
+    seen_map m;
+    state_bdd state = g.get_init_state();
+    os << "digraph G {" << std::endl;
+    os << "  size=\"7.26,10.69\"" << std::endl;
+    os << "  0 [label=\"\", style=invis]" << std::endl;
+    int init;
+    dotty_state(os, g, state, m, init);
+    os << "  0 -> " << init << std::endl;
+    dotty_rec(os, g, state, m, init);
+    os << "}" << std::endl;
+    return os;
+  }
+
+
+}
diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh
new file mode 100644
index 000000000..5f87bad0b
--- /dev/null
+++ b/src/tgbaalgos/dotty.hh
@@ -0,0 +1,13 @@
+#ifndef SPOT_TGBAALGOS_DOTTY_HH
+# define SPOT_TGBAALGOS_DOTTY_HH
+
+#include "tgba/tgba.hh"
+#include <iostream>
+
+namespace spot
+{
+  /// \brief Print reachable states in dot format.
+  std::ostream& dotty_reachable(std::ostream& os, const tgba& g);
+}
+
+#endif // SPOT_TGBAALGOS_DOTTY_HH