From 7e81306d45d6a452f4a35eeb5d4c6897723c5aee Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 26 Nov 2003 17:34:09 +0000
Subject: [PATCH] * src/tgba/bddprint.cc (print_accset_handler,
 bdd_print_accset): New functions. * src/tgba/bddprint.cc (bdd_print_accset):
 Declare it. * src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use it. *
 src/tgbatest/tgbaread.test, src/tgbatest/explicit.test: Adjust expected
 output.

---
 ChangeLog                  |  9 +++++++++
 src/tgba/bddprint.cc       | 40 +++++++++++++++++++++++++++++---------
 src/tgba/bddprint.hh       | 10 ++++++++++
 src/tgbaalgos/dotty.cc     |  5 +++--
 src/tgbatest/explicit.test |  6 +++---
 src/tgbatest/tgbaread.test |  6 +++---
 6 files changed, 59 insertions(+), 17 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index e2f15e84c..bd1f0fa38 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,12 @@
+2003-11-26  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/tgba/bddprint.cc (print_accset_handler, bdd_print_accset): New
+	functions.
+	* src/tgba/bddprint.cc (bdd_print_accset): Declare it.
+	* src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use it.
+	* src/tgbatest/tgbaread.test, src/tgbatest/explicit.test: Adjust
+	expected output.
+
 2003-11-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/tgbaparse/tgbaparse.yy: Remove a random character.
diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc
index 5de4acd76..37a9c22da 100644
--- a/src/tgba/bddprint.cc
+++ b/src/tgba/bddprint.cc
@@ -117,15 +117,11 @@ namespace spot
   print_acc_handler(char* varset, int size)
   {
     for (int v = 0; v < size; ++v)
-      {
-	if (varset[v] < 0)
-	  continue;
-	if (varset[v] > 0)
-	  {
-	    *where << " ";
-	    print_handler(*where, v);
-	  }
-      }
+      if (varset[v] > 0)
+	{
+	  *where << " ";
+	  print_handler(*where, v);
+	}
   }
 
   std::ostream&
@@ -138,6 +134,32 @@ namespace spot
     return os;
   }
 
+  static bool first_done = false;
+  static void
+  print_accset_handler(char* varset, int size)
+  {
+    for (int v = 0; v < size; ++v)
+      if (varset[v] > 0)
+	{
+	  *where << (first_done ? ", " : "{");
+	  print_handler(*where, v);
+	  first_done = true;
+	}
+  }
+
+  std::ostream&
+  bdd_print_accset(std::ostream& os, const bdd_dict* d, bdd b)
+  {
+    dict = d;
+    where = &os;
+    want_acc = true;
+    first_done = false;
+    bdd_allsat(b, print_accset_handler);
+    if (first_done)
+      *where << "}";
+    return os;
+  }
+
   std::string
   bdd_format_sat(const bdd_dict* d, bdd b)
   {
diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh
index a2dcf26a6..9756abff2 100644
--- a/src/tgba/bddprint.hh
+++ b/src/tgba/bddprint.hh
@@ -57,6 +57,16 @@ namespace spot
   std::ostream& bdd_print_acc(std::ostream& os,
 			      const bdd_dict* dict, bdd b);
 
+  /// \brief Print a BDD as a set of accepting conditions.
+  ///
+  /// This is used when saving a TGBA.
+  /// \param os The output stream.
+  /// \param dict The dictionary to use, to lookup variables.
+  /// \param b The BDD to print.
+  /// \return The BDD formated as a string.
+  std::ostream& bdd_print_accset(std::ostream& os,
+				 const bdd_dict* dict, bdd b);
+
   /// \brief Print a BDD as a set.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc
index d2b4c065c..a007417dc 100644
--- a/src/tgbaalgos/dotty.cc
+++ b/src/tgbaalgos/dotty.cc
@@ -62,8 +62,9 @@ namespace spot
       os_ << "  " << in << " -> " << out << " [label=\"";
       bdd_print_formula(os_, automata_->get_dict(),
 			si->current_condition()) << "\\n";
-      bdd_print_set(os_, automata_->get_dict(),
-		    si->current_accepting_conditions()) << "\"]" << std::endl;
+      bdd_print_accset(os_, automata_->get_dict(),
+		       si->current_accepting_conditions()) << "\"]"
+							   << std::endl;
     }
 
   private:
diff --git a/src/tgbatest/explicit.test b/src/tgbatest/explicit.test
index 6feaaf419..e6144f216 100755
--- a/src/tgbatest/explicit.test
+++ b/src/tgbatest/explicit.test
@@ -32,11 +32,11 @@ digraph G {
   0 [label="", style=invis, height=0]
   0 -> 1
   1 [label="state 0"]
-  1 -> 2 [label="1\n<Acc[p]:0, Acc[q]:1, Acc[r]:0><Acc[p]:1, Acc[q]:0, Acc[r]:0>"]
+  1 -> 2 [label="1\n{Acc[q], Acc[p]}"]
   2 [label="state 1"]
-  2 -> 3 [label="a\n<Acc[p]:0, Acc[q]:0, Acc[r]:1>"]
+  2 -> 3 [label="a\n{Acc[r]}"]
   3 [label="state 2"]
-  3 -> 1 [label="(b & c)\nF"]
+  3 -> 1 [label="(b & c)\n"]
 }
 EOF
 
diff --git a/src/tgbatest/tgbaread.test b/src/tgbatest/tgbaread.test
index 14ec7eb85..ee955c1eb 100755
--- a/src/tgbatest/tgbaread.test
+++ b/src/tgbatest/tgbaread.test
@@ -39,11 +39,11 @@ digraph G {
   0 [label="", style=invis, height=0]
   0 -> 1
   1 [label="s1"]
-  1 -> 2 [label="(a & !b)\n<Acc[c]:0, Acc[d]:1><Acc[c]:1, Acc[d]:0>"]
+  1 -> 2 [label="(a & !b)\n{Acc[d], Acc[c]}"]
   2 [label="s2"]
-  2 -> 3 [label="a\n<Acc[c]:1, Acc[d]:0>"]
+  2 -> 3 [label="a\n{Acc[c]}"]
   3 [label="state 3"]
-  3 -> 1 [label="1\nF"]
+  3 -> 1 [label="1\n"]
 }
 EOF