From 16c6219988e180f332c8ed1046ffca640876cc97 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 26 May 2003 13:37:14 +0000
Subject: [PATCH] * src/tgba/bddprint.hh, src/tgba/bddprint.cc: New files. *
 src/tgba/Makefile.am (libtgba_la_SOURCES): Add them. * src/tgba/public.hh:
 Include bddprint.hh.

---
 ChangeLog            |  6 +++-
 src/tgba/Makefile.am |  2 ++
 src/tgba/bddprint.cc | 77 ++++++++++++++++++++++++++++++++++++++++++++
 src/tgba/bddprint.hh | 22 +++++++++++++
 src/tgba/public.hh   |  1 +
 5 files changed, 107 insertions(+), 1 deletion(-)
 create mode 100644 src/tgba/bddprint.cc
 create mode 100644 src/tgba/bddprint.hh

diff --git a/ChangeLog b/ChangeLog
index c20c1869c..92cca9619 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,12 +1,16 @@
 2003-05-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/tgba/bddprint.hh, src/tgba/bddprint.cc: New files.
+	* src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.
+	* src/tgba/public.hh: Include bddprint.hh.
+
 	* src/tgba/tgba.hh: Rename as ...
 	* src/tgba/public.hh: .. this.
 	* src/tgba/tgba.hh: New file.
 	* src/tgba/Makefile.am (libtgba_la_SOURCES): Add public.hh.
 	* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Inherit from tgba.
 	(tgba_bdd_concrete::init_iter): Delete.
-	(tgba_bdd_concrete::succ_iter): Take a state_bdd as argument, 
+	(tgba_bdd_concrete::succ_iter): Take a state_bdd as argument,
 	not a bdd.
 	* src/tgba/tgbabddconcrete.cc: Likewise.
 
diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am
index 39605da82..b7d44e091 100644
--- a/src/tgba/Makefile.am
+++ b/src/tgba/Makefile.am
@@ -5,6 +5,8 @@ noinst_LTLIBRARIES = libtgba.la
 libtgba_la_SOURCES = \
   bddfactory.cc \
   bddfactory.hh \
+  bddprint.cc \
+  bddprint.hh \
   dictunion.cc \
   dictunion.hh \
   ltl2tgba.cc \
diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc
new file mode 100644
index 000000000..e02a2ebae
--- /dev/null
+++ b/src/tgba/bddprint.cc
@@ -0,0 +1,77 @@
+#include "bddprint.hh"
+#include "ltlvisit/tostring.hh"
+
+namespace spot
+{
+
+  const tgba_bdd_dict* dict;
+
+  static void
+  print_handler(std::ostream& o, int var)
+  {
+    tgba_bdd_dict::vf_map::const_iterator isi = 
+      dict->var_formula_map.find(var);
+    if (isi != dict->var_formula_map.end())
+      to_string(isi->second, o);
+    else
+      {
+	isi = dict->prom_formula_map.find(var);
+	if (isi != dict->prom_formula_map.end())
+	  {
+	    o << "Prom["; to_string(isi->second, o) << "]";
+	  }
+	else
+	  {
+	    isi = dict->now_formula_map.find(var);
+	    if (isi != dict->now_formula_map.end())
+	      {
+		o << "Now["; to_string(isi->second, o) << "]";
+	      }
+	    else
+	      {
+		isi = dict->now_formula_map.find(var - 1);
+		if (isi != dict->now_formula_map.end())
+		  {
+		    o << "Next["; to_string(isi->second, o) << "]";
+		  }
+		else
+		  {
+		    o << "?" << var;
+		  }
+	      }
+	  }
+      }
+  }
+  
+
+  std::ostream& 
+  bdd_print_set(std::ostream& os, const tgba_bdd_dict& d, bdd b)
+  {
+    dict = &d;
+    bdd_strm_hook(print_handler);
+    os << bddset << b;
+    bdd_strm_hook(0);
+    return os;
+  }
+
+  std::ostream& 
+  bdd_print_dot(std::ostream& os, const tgba_bdd_dict& d, bdd b)
+  {
+    dict = &d;
+    bdd_strm_hook(print_handler);
+    os << bdddot << b;
+    bdd_strm_hook(0);
+    return os;
+  }
+  
+  std::ostream& 
+  bdd_print_table(std::ostream& os, const tgba_bdd_dict& d, bdd b)
+  {
+    dict = &d;
+    bdd_strm_hook(print_handler);
+    os << bddtable << b;
+    bdd_strm_hook(0);
+    return os;
+  }
+
+}
diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh
new file mode 100644
index 000000000..42cfef456
--- /dev/null
+++ b/src/tgba/bddprint.hh
@@ -0,0 +1,22 @@
+#ifndef SPOT_TGBA_BDDPRINT_HH
+# define SPOT_TGBA_BDDPRINT_HH
+
+#include <iostream>
+#include "tgbabdddict.hh"
+#include <bdd.h>
+
+namespace spot
+{
+  
+  std::ostream& bdd_print_set(std::ostream& os, 
+			      const tgba_bdd_dict& dict, bdd b);
+
+  std::ostream& bdd_print_dot(std::ostream& os, 
+			      const tgba_bdd_dict& dict, bdd b);
+
+  std::ostream& bdd_print_table(std::ostream& os, 
+				const tgba_bdd_dict& dict, bdd b);
+
+}
+
+#endif // SPOT_TGBA_BDDPRINT_HH
diff --git a/src/tgba/public.hh b/src/tgba/public.hh
index 011420f60..c86039d78 100644
--- a/src/tgba/public.hh
+++ b/src/tgba/public.hh
@@ -5,5 +5,6 @@
 # include "tgbabddconcrete.hh"
 # include "tgbabddconcreteproduct.hh"
 # include "ltl2tgba.hh"
+# include "bddprint.hh"
 
 #endif // SPOT_TGBA_PUBLIC_HH