Introduce scc.cc to compute SCC stats and map.

ChangeLog

@@ -1,3 +1,10 @@
+2008-12-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	* src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc: New files.
+	* src/tgbaalgos/Makefile.am: Add them.
+	* src/tgbatest/ltl2tgba.cc (-k): Also call build_scc_stats().
+	(-K): New option that dumps the SCCs for dot.
+
 2008-12-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* src/tgbatest/ltl2tgba.cc (-k): New option that calls

src/tgbaalgos/Makefile.am

@@ -1,4 +1,4 @@
-## Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+## Copyright (C) 2003, 2004, 2005, 2008  Laboratoire d'Informatique de Paris 6 (LIP6),
 ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
 ## et Marie Curie.
 ##
@@ -48,6 +48,7 @@ tgbaalgos_HEADERS = \
   replayrun.hh \
   rundotdec.hh \
   save.hh \
+  scc.hh \
   se05.hh \
   stats.hh \
   tau03.hh \
@@ -78,6 +79,7 @@ libtgbaalgos_la_SOURCES = \
   replayrun.cc \
   rundotdec.cc \
   save.cc \
+  scc.cc \
   se05.cc \
   stats.cc \
   tau03.cc \

src/tgbaalgos/scc.cc

@@ -0,0 +1,306 @@
+// Copyright (C) 2008  Laboratoire de Recherche et Developpement de
+// l'Epita.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <queue>
+#include <set>
+#include <iostream>
+#include "scc.hh"
+#include "tgba/bddprint.hh"
+
+namespace spot
+{
+  std::ostream&
+  scc_stats::dump(std::ostream& out) const
+  {
+    out << "total SCCs: " << scc_total << std::endl;
+    return out;
+  }
+
+
+  scc_map::scc_map(const tgba* aut)
+    : aut_(aut)
+  {
+  }
+
+  int
+  scc_map::initial() const
+  {
+    state* in = aut_->get_init_state();
+    hash_type::const_iterator i = h_.find(in);
+    assert(i != h_.end());
+    int val = i->second;
+    delete in;
+    return val;
+  }
+
+  const scc_map::succ_type&
+  scc_map::succ(int i) const
+  {
+    std::map<int, scc>::const_iterator j = scc_map_.find(i);
+    assert (j != scc_map_.end());
+    return j->second.succ;
+  }
+
+  bool
+  scc_map::accepting(int i) const
+  {
+    std::map<int, scc>::const_iterator j = scc_map_.find(i);
+    assert (j != scc_map_.end());
+    return j->second.acc == aut_->all_acceptance_conditions();
+  }
+
+  const tgba*
+  scc_map::get_aut() const
+  {
+    return aut_;
+  }
+
+
+  void
+  scc_map::relabel_component(int n)
+  {
+    assert(!root_.front().states.empty());
+    std::list<const state*>::iterator i;
+    for (i = root_.front().states.begin(); i != root_.front().states.end(); ++i)
+      {
+	hash_type::iterator spi = h_.find(*i);
+	assert(spi != h_.end());
+	assert(spi->first == *i);
+	assert(spi->second != -1);
+	spi->second = n;
+      }
+    scc_map_.insert(std::make_pair(n, root_.front()));
+  }
+
+  void
+  scc_map::build_map()
+  {
+    // Setup depth-first search from the initial state.
+    {
+      state* init = aut_->get_init_state();
+      num_ = 1;
+      scc_num_ = 0;
+      h_.insert(std::make_pair(init, 1));
+      root_.push_front(scc(1));
+      arc_.push(bddfalse);
+      tgba_succ_iterator* iter = aut_->succ_iter(init);
+      iter->first();
+      todo_.push(pair_state_iter(init, iter));
+    }
+
+    while (!todo_.empty())
+      {
+	assert(root_.size() == arc_.size());
+
+	// We are looking at the next successor in SUCC.
+	tgba_succ_iterator* succ = todo_.top().second;
+
+	// If there is no more successor, backtrack.
+	if (succ->done())
+	  {
+	    // We have explored all successors of state CURR.
+	    const state* curr = todo_.top().first;
+
+	    // Backtrack TODO_.
+	    todo_.pop();
+
+	    // Fill rem with any component removed, so that
+	    // remove_component() does not have to traverse the SCC
+	    // again.
+	    hash_type::const_iterator spi = h_.find(curr);
+	    assert(spi != h_.end());
+	    root_.front().states.push_front(spi->first);
+
+	    // When backtracking the root of an SCC, we must also
+	    // remove that SCC from the ARC/ROOT stacks.  We must
+	    // discard from H all reachable states from this SCC.
+	    assert(!root_.empty());
+	    if (root_.front().index == spi->second)
+	      {
+		assert(!arc_.empty());
+		arc_.pop();
+		relabel_component(--scc_num_);
+		root_.pop_front();
+	      }
+
+	    delete succ;
+	    // Do not delete CURR: it is a key in H.
+	    continue;
+	  }
+
+	// We have a successor to look at.
+	// Fetch the values (destination state, acceptance conditions
+	// of the arc) we are interested in...
+	const state* dest = succ->current_state();
+	bdd acc = succ->current_acceptance_conditions();
+	bdd cond = succ->current_condition();
+	// ... and point the iterator to the next successor, for
+	// the next iteration.
+	succ->next();
+	// We do not need SUCC from now on.
+
+	// Are we going to a new state?
+	hash_type::const_iterator spi = h_.find(dest);
+	if (spi == h_.end())
+	  {
+	    // Yes.  Number it, stack it, and register its successors
+	    // for later processing.
+	    h_.insert(std::make_pair(dest, ++num_));
+	    root_.push_front(scc(num_));
+	    arc_.push(acc);
+	    tgba_succ_iterator* iter = aut_->succ_iter(dest);
+	    iter->first();
+	    todo_.push(pair_state_iter(dest, iter));
+	    continue;
+	  }
+
+	// Have we reached maximal SCC?
+	if (spi->second < 0)
+	  {
+	    int dest = spi->second;
+	    // Record that there is a transition from this SCC to the
+	    // dest SCC labelled with cond.
+	    succ_type::iterator i = root_.front().succ.find(dest);
+	    if (i == root_.front().succ.end())
+	      root_.front().succ.insert(std::make_pair(dest, cond));
+	    else
+	      i->second |= cond;
+
+	    continue;
+	  }
+
+	// Now this is the most interesting case.  We have reached a
+	// state S1 which is already part of a non-dead SCC.  Any such
+	// non-dead SCC has necessarily been crossed by our path to
+	// this state: there is a state S2 in our path which belongs
+	// to this SCC too.  We are going to merge all states between
+	// this S1 and S2 into this SCC.
+	//
+	// This merge is easy to do because the order of the SCC in
+	// ROOT is ascending: we just have to merge all SCCs from the
+	// top of ROOT that have an index greater to the one of
+	// the SCC of S2 (called the "threshold").
+	int threshold = spi->second;
+	std::list<const state*> states;
+	succ_type succs;
+	while (threshold < root_.front().index)
+	  {
+	    assert(!root_.empty());
+	    assert(!arc_.empty());
+	    acc |= root_.front().acc;
+	    acc |= arc_.top();
+	    states.splice(states.end(), root_.front().states);
+	    succs.insert(root_.front().succ.begin(),
+			 root_.front().succ.end());
+	    root_.pop_front();
+	    arc_.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.
+	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());
+      }
+  }
+
+  int scc_map::scc_count() const
+  {
+    return -scc_num_;
+  }
+
+  scc_stats build_scc_stats(const scc_map& m)
+  {
+    scc_stats res;
+    res.scc_total = m.scc_count();
+    return res;
+  }
+
+  scc_stats
+  build_scc_stats(const tgba* a)
+  {
+    scc_map m(a);
+    m.build_map();
+    return build_scc_stats(m);
+  }
+
+  std::ostream&
+  dump_scc_dot(const scc_map& m, std::ostream& out)
+  {
+    out << "digraph G {\n  0 [label=\"\", style=invis, height=0]" << std::endl;
+    int start = m.initial();
+    out << "  0 -> " << -start << std::endl;
+
+    typedef std::set<int> seen_map;
+    seen_map seen;
+    seen.insert(start);
+
+    std::queue<int> q;
+    q.push(start);
+    while (!q.empty())
+      {
+	int state = q.front();
+	q.pop();
+
+	if (m.accepting(state))
+	  std::cout << "  " << -state << " [shape=doublecircle]" << std::endl;
+	else
+	  std::cout << "  " << -state << " [shape=circle]" << std::endl;
+
+	const scc_map::succ_type& succ = m.succ(state);
+
+	scc_map::succ_type::const_iterator it;
+	for (it = succ.begin(); it != succ.end(); ++it)
+	  {
+	    int dest = it->first;
+	    bdd label = it->second;
+
+	    out << "  " << -state << " -> " << -dest
+		<< " [label=\""
+		<< bdd_format_formula(m.get_aut()->get_dict(), label)
+		<< "\"]" << std::endl;
+
+	    seen_map::const_iterator it = seen.find(dest);
+	    if (it != seen.end())
+	      continue;
+
+	    seen.insert(dest);
+	    q.push(dest);
+	  }
+      }
+
+    out << "}" << std::endl;
+
+    return out;
+  }
+
+  std::ostream&
+  dump_scc_dot(const tgba* a, std::ostream& out)
+  {
+    scc_map m(a);
+    m.build_map();
+    return dump_scc_dot(m, out);
+  }
+
+}

src/tgbaalgos/scc.hh

@@ -0,0 +1,105 @@
+// Copyright (C) 2008  Laboratoire de Recherche et Developpement de
+// l'Epita.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TGBAALGOS_SCC_HH
+# define SPOT_TGBAALGOS_SCC_HH
+
+#include <map>
+#include <stack>
+#include "tgba/tgba.hh"
+#include <iosfwd>
+
+namespace spot
+{
+
+  struct scc_stats
+  {
+    unsigned scc_total;
+
+    std::ostream& dump(std::ostream& out) const;
+  };
+
+  class scc_map
+  {
+  public:
+    typedef std::map<int, bdd> succ_type;
+
+    scc_map(const tgba* aut);
+
+    void build_map();
+    void relabel_component(int n);
+
+    const tgba* get_aut() const;
+
+    int scc_count() const;
+
+    int initial() const;
+
+    const succ_type& succ(int i) const;
+    bool accepting(int i) const;
+
+  protected:
+    struct scc
+    {
+    public:
+      scc(int index) : index(index), acc(bddfalse) {};
+      /// Index of the SCC.
+      int index;
+      /// The union of all acceptance conditions of transitions which
+      /// connect the states of the connected component.
+      bdd acc;
+      /// States of the component.
+      std::list<const state*> states;
+      /// Successor SCC.
+      succ_type succ;
+    };
+
+    const tgba* aut_;		// Automata to decompose.
+    typedef std::list<scc> stack_type;
+    stack_type root_;		// Stack of SCC roots.
+    std::stack<bdd> arc_;	// A stack of acceptance conditions
+				// between each of these SCC.
+    typedef Sgi::hash_map<const state*, int,
+			  state_ptr_hash, state_ptr_equal> hash_type;
+    hash_type h_;		// Map of visited states.
+    int num_;			// Number of visited nodes.
+    int scc_num_;		// Opposite of the number of
+				// maximal SCC constructed.
+    typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
+    std::stack<pair_state_iter> todo_; // DFS stack.  Holds (STATE,
+				       // ITERATOR) pairs where
+				       // ITERATOR is an iterator over
+				       // the successors of STATE.
+				       // ITERATOR should always be
+				       // freed when TODO is popped,
+				       // but STATE should not because
+				       // it is used as a key in H.
+
+    std::map<int, scc> 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 scc_map& m, std::ostream& out);
+}
+
+#endif // SPOT_TGBAALGOS_SCC_HH

src/tgbatest/ltl2tgba.cc

@@ -47,6 +47,7 @@
 #include "tgbaalgos/rundotdec.hh"
 
 #include "tgbaalgos/stats.hh"
+#include "tgbaalgos/scc.hh"
 #include "tgbaalgos/emptiness_stats.hh"
 
 void
@@ -91,6 +92,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"
+	    << std::endl
             << "  -L    fair-loop approximation (implies -f)" << std::endl
 	    << "  -m    try to reduce accepting runs, in a second pass"
 	    << std::endl
@@ -324,6 +327,10 @@ main(int argc, char** argv)
 	{
 	  output = 9;
 	}
+      else if (!strcmp(argv[formula_index], "-K"))
+	{
+	  output = 10;
+	}
       else if (!strcmp(argv[formula_index], "-L"))
 	{
 	  fair_loop_approx = true;
@@ -731,6 +738,10 @@ main(int argc, char** argv)
 	  }
 	case 9:
 	  stats_reachable(a).dump(std::cout);
+	  build_scc_stats(a).dump(std::cout);
+	  break;
+	case 10:
+	  dump_scc_dot(a, std::cout);
 	  break;
 	default:
 	  assert(!"unknown output option");