Keep track of conditions in SCC, and add a more verbose dump.

* src/tgbaalgos/scc.hh (scc_map::scc_of_state,
scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
New functions.
(scc_map::scc::conds): New attribute.
(dump_scc_dot): Take an optional VERBOSE argument.
* src/tgbaalgos/scc.cc (scc_map::scc_of_state,
scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
Implement these new functions.
(dump_scc_dot): Display number of states, conditions and
acceptance conditions, with VERBOSE is set.
(build_map): Fill the new scc_map::scc::cond field.

ChangeLog

@@ -1,3 +1,19 @@
+2009-05-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Keep track of conditions in SCC, and add a more verbose dump.
+
+	* src/tgbaalgos/scc.hh (scc_map::scc_of_state,
+	scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
+	New functions.
+	(scc_map::scc::conds): New attribute.
+	(dump_scc_dot): Take an optional VERBOSE argument.
+	* src/tgbaalgos/scc.cc (scc_map::scc_of_state,
+	scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
+	Implement these new functions.
+	(dump_scc_dot): Display number of states, conditions and
+	acceptance conditions, with VERBOSE is set.
+	(build_map): Fill the new scc_map::scc::cond field.
+
 2009-05-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* src/tgbaalgos/scc.cc (scc_map::relabel_component): Make sure

src/tgbaalgos/scc.cc

@@ -21,6 +21,7 @@
 #include <queue>
 #include <set>
 #include <iostream>
+#include <sstream>
 #include "scc.hh"
 #include "tgba/bddprint.hh"
 
@@ -160,8 +161,7 @@ namespace spot
 	  }
 
 	// We have a successor to look at.
-	// Fetch the values (destination state, acceptance conditions
+	// Fetch the values we are interested in...
-	// of the arc) we are interested in...
 	const state* dest = succ->current_state();
 	bdd acc = succ->current_acceptance_conditions();
 	bdd cond = succ->current_condition();
@@ -186,7 +186,7 @@ namespace spot
 	    continue;
 	  }
 
-	// Have we reached maximal SCC?
+	// Have we reached a maximal SCC?
 	if (spi->second < 0)
 	  {
 	    int dest = spi->second;
@@ -215,6 +215,8 @@ namespace spot
 	int threshold = spi->second;
 	std::list<const state*> states;
 	succ_type succs;
+	cond_set conds;
+	conds.insert(cond);
 	while (threshold < root_.front().index)
 	  {
 	    assert(!root_.empty());
@@ -225,23 +227,53 @@ namespace spot
 	    states.splice(states.end(), root_.front().states);
 	    succs.insert(root_.front().succ.begin(),
 			 root_.front().succ.end());
+	    conds.insert(arc_cond_.top());
+	    conds.insert(root_.front().conds.begin(),
+			 root_.front().conds.end());
 	    root_.pop_front();
 	    arc_acc_.pop();
 	    arc_cond_.pop();
 	  }
+
 	// Note that we do not always have
 	//  threshold == root_.front().index
 	// after this loop, the SCC whose index is threshold might have
 	// been merged with a lower SCC.
 
-	// Accumulate all acceptance conditions into the merged SCC.
+	// Accumulate all acceptance conditions, states, SCC
+	// successors, and conditions into the merged SCC.
 	root_.front().acc |= acc;
 	root_.front().states.splice(root_.front().states.end(), states);
-	// Likewise with SCC successors.
 	root_.front().succ.insert(succs.begin(), succs.end());
+	root_.front().conds.insert(conds.begin(), conds.end());
       }
   }
 
+  int scc_map::scc_of_state(const state* s) const
+  {
+    hash_type::const_iterator i = h_.find(s);
+    assert(i != h_.end());
+    return i->second;
+  }
+
+  const scc_map::cond_set& scc_map::cond_set_of(int n) const
+  {
+    scc_map_type::const_iterator i = scc_map_.find(n);
+    return i->second.conds;
+  }
+
+  bdd scc_map::acc_set_of(int n) const
+  {
+    scc_map_type::const_iterator i = scc_map_.find(n);
+    return i->second.acc;
+  }
+
+  const std::list<const state*>& scc_map::states_of(int n) const
+  {
+    scc_map_type::const_iterator i = scc_map_.find(n);
+    return i->second.states;
+  }
+
   int scc_map::scc_count() const
   {
     return -scc_num_;
@@ -326,7 +358,7 @@ namespace spot
   }
 
   std::ostream&
-  dump_scc_dot(const scc_map& m, std::ostream& out)
+  dump_scc_dot(const scc_map& m, std::ostream& out, bool verbose)
   {
     out << "digraph G {\n  0 [label=\"\", style=invis, height=0]" << std::endl;
     int start = m.initial();
@@ -343,10 +375,33 @@ namespace spot
 	int state = q.front();
 	q.pop();
 
-	if (m.accepting(state))
+	const scc_map::cond_set& cs = m.cond_set_of(state);
-	  std::cout << "  " << -state << " [shape=doublecircle]" << std::endl;
+
-	else
+	std::ostringstream ostr;
-	  std::cout << "  " << -state << " [shape=circle]" << std::endl;
+	ostr << -state;
+	if (verbose)
+	  {
+	    size_t n = m.states_of(state).size();
+	    ostr << " (" << n << " state";
+	    if (n > 1)
+	      ostr << "s";
+	    ostr << ")\\naccs=";
+	    bdd_print_accset(ostr, m.get_aut()->get_dict(),
+			     m.acc_set_of(state));
+	    ostr << "\\nconds=[";
+	    for (scc_map::cond_set::const_iterator i = cs.begin();
+		 i != cs.end(); ++i)
+	      {
+		if (i != cs.begin())
+		  ostr << ", ";
+		bdd_print_formula(ostr, m.get_aut()->get_dict(), *i);
+	      }
+	    ostr << "]";
+	  }
+
+	std::cout << "  " << -state << " [shape=box,"
+		  << (m.accepting(state) ? "style=bold," : "")
+		  << "label=\"" << ostr.str() << "\"]" << std::endl;
 
 	const scc_map::succ_type& succ = m.succ(state);
 
@@ -357,9 +412,9 @@ namespace spot
 	    bdd label = it->second;
 
 	    out << "  " << -state << " -> " << -dest
-		<< " [label=\""
+		<< " [label=\"";
-		<< bdd_format_formula(m.get_aut()->get_dict(), label)
+	    bdd_print_formula(out, m.get_aut()->get_dict(), label);
-		<< "\"]" << std::endl;
+	    out << "\"]" << std::endl;
 
 	    seen_map::const_iterator it = seen.find(dest);
 	    if (it != seen.end())
@@ -376,11 +431,11 @@ namespace spot
   }
 
   std::ostream&
-  dump_scc_dot(const tgba* a, std::ostream& out)
+  dump_scc_dot(const tgba* a, std::ostream& out, bool verbose)
   {
     scc_map m(a);
     m.build_map();
-    return dump_scc_dot(m, out);
+    return dump_scc_dot(m, out, verbose);
   }
 
 }

src/tgbaalgos/scc.hh

@@ -26,6 +26,7 @@
 #include "tgba/tgba.hh"
 #include <iosfwd>
 #include "misc/hash.hh"
+#include "misc/bddlt.hh"
 
 namespace spot
 {
@@ -59,12 +60,18 @@ namespace spot
   {
   public:
     typedef std::map<int, bdd> succ_type;
+    typedef std::set<bdd, bdd_less_than> cond_set;
 
     scc_map(const tgba* aut);
 
     void build_map();
     void relabel_component(int n);
 
+    int scc_of_state(const state* s) const;
+    const cond_set& cond_set_of(int n) const;
+    bdd acc_set_of(int n) const;
+    const std::list<const state*>& states_of(int n) const;
+
     const tgba* get_aut() const;
 
     int scc_count() const;
@@ -86,6 +93,8 @@ namespace spot
       bdd acc;
       /// States of the component.
       std::list<const state*> states;
+      /// Set of conditions used in the SCC.
+      cond_set conds;
       /// Successor SCC.
       succ_type succ;
     };
@@ -113,14 +122,17 @@ namespace spot
 				       // but STATE should not because
 				       // it is used as a key in H.
 
-    std::map<int, scc> scc_map_; // Map of constructed maximal SCC.
+    typedef std::map<int, scc> scc_map_type;
+    scc_map_type scc_map_; // Map of constructed maximal SCC.
   };
 
   scc_stats build_scc_stats(const tgba* a);
   scc_stats build_scc_stats(const scc_map& m);
 
-  std::ostream& dump_scc_dot(const tgba* a, std::ostream& out);
+  std::ostream& dump_scc_dot(const tgba* a, std::ostream& out,
-  std::ostream& dump_scc_dot(const scc_map& m, std::ostream& out);
+			     bool verbose = false);
+  std::ostream& dump_scc_dot(const scc_map& m, std::ostream& out,
+			     bool verbose = false);
 }
 
 #endif // SPOT_TGBAALGOS_SCC_HH

src/tgbatest/ltl2tgba.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008 Laboratoire
+// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire
 // d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
 // Coopératifs (SRC), Université Pierre et Marie Curie.
 //
@@ -93,7 +93,8 @@ syntax(char* prog)
 	    << " (requires -e)" << std::endl
 	    << "  -k    display statistics on the TGBA instead of dumping it"
 	    << std::endl
-	    << "  -K    dump the graph of SCCs in dot"
+	    << "  -K    dump the graph of SCCs in dot format" << std::endl
+	    << "  -KV   verbosely dump the graph of SCCs in dot format"
 	    << std::endl
             << "  -L    fair-loop approximation (implies -f)" << std::endl
 	    << "  -m    try to reduce accepting runs, in a second pass"
@@ -332,6 +333,10 @@ main(int argc, char** argv)
 	{
 	  output = 10;
 	}
+      else if (!strcmp(argv[formula_index], "-KV"))
+	{
+	  output = 11;
+	}
       else if (!strcmp(argv[formula_index], "-L"))
 	{
 	  fair_loop_approx = true;
@@ -742,7 +747,10 @@ main(int argc, char** argv)
 	  build_scc_stats(a).dump(std::cout);
 	  break;
 	case 10:
-	  dump_scc_dot(a, std::cout);
+	  dump_scc_dot(a, std::cout, false);
+	  break;
+	case 11:
+	  dump_scc_dot(a, std::cout, true);
 	  break;
 	default:
 	  assert(!"unknown output option");