* src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::run)

Reuse s->second to avoid a hash lookup.
* src/tgbaalgos/save.cc (save_bfs::process_state): Delete dest.

ChangeLog

@@ -1,5 +1,9 @@
 2004-01-05  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::run)
+	Reuse s->second to avoid a hash lookup.
+	* src/tgbaalgos/save.cc (save_bfs::process_state): Delete dest.
+
 	* src/ltlparse/Makefile.am ($(FROM_LTLPARSE_YY_MAIN)):
 	Use $(FROM_LTLPARSE_YY_MAIN), not $@, because $@ can contains
 	VPATH and we do not want Bison to see absolute paths.

src/tgbaalgos/Makefile.am

@@ -1,4 +1,4 @@
-## Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+## Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
 ## et Marie Curie.
 ##
@@ -32,6 +32,7 @@ tgbaalgos_HEADERS = \
   ltl2tgba_fm.hh \
   ltl2tgba_lacim.hh \
   magic.hh \
+  powerset.hh \
   reachiter.hh \
   save.hh
 
@@ -44,5 +45,6 @@ libtgbaalgos_la_SOURCES = \
   ltl2tgba_fm.cc \
   ltl2tgba_lacim.cc \
   magic.cc \
+  powerset.cc \
   reachiter.cc \
   save.cc

src/tgbaalgos/powerset.cc

@@ -0,0 +1,136 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// 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 <set>
+#include <map>
+#include <deque>
+#include <sstream>
+#include "misc/hash.hh"
+#include "tgbaalgos/powerset.hh"
+#include "bdd.h"
+
+namespace spot
+{
+  tgba_explicit*
+  tgba_powerset(const tgba* aut)
+  {
+    typedef Sgi::hash_set<const state*, state_ptr_hash,
+                          state_ptr_equal> state_set;
+    typedef std::set<const state*, state_ptr_less_than> power_state;
+    typedef std::map<power_state, std::string> power_set;
+    typedef std::deque<power_state> todo_list;
+
+    power_set seen;
+    todo_list todo;
+    tgba_explicit* res = new tgba_explicit(aut->get_dict());
+
+    state_set states;
+
+    {
+      power_state ps;
+      state* s = aut->get_init_state();
+      states.insert(s);
+      ps.insert(s);
+      todo.push_back(ps);
+      seen[ps] = "1";
+    }
+
+    unsigned state_num = 1;
+
+    while (! todo.empty())
+      {
+	power_state src = todo.front();
+	todo.pop_front();
+	// Compute all variables occurring on outgoing arcs.
+	bdd all_vars = bddtrue;
+	power_state::const_iterator i;
+
+	for (i = src.begin(); i != src.end(); ++i)
+	  all_vars &= aut->support_variables(*i);
+
+	// Compute all possible combinations of these variables.
+	bdd all_conds = bddtrue;
+	while (all_conds != bddfalse)
+	  {
+	    bdd cond = bdd_satoneset(all_conds, all_vars, bddtrue);
+	    all_conds -= cond;
+
+	    // Construct the set of all states reachable via COND.
+	    power_state dest;
+	    for (i = src.begin(); i != src.end(); ++i)
+	      {
+		tgba_succ_iterator *si = aut->succ_iter(*i);
+		for (si->first(); ! si->done(); si->next())
+		  if ((cond >> si->current_condition()) == bddtrue)
+		    {
+		      const state* s = si->current_state();
+		      state_set::const_iterator i = states.find(s);
+		      if (i != states.end())
+			{
+			  delete s;
+			  s = *i;
+			}
+		      else
+			{
+			  states.insert(s);
+			}
+		      dest.insert(s);
+		    }
+		delete si;
+	      }
+	    if (dest.empty())
+	      continue;
+
+	    // Add that transition.
+	    power_set::const_iterator i = seen.find(dest);
+	    std::string dest_name;
+	    if (i != seen.end())
+	      {
+		dest_name = i->second;
+	      }
+	    else
+	      {
+		std::ostringstream str;
+		str << ++state_num;
+		dest_name = str.str();
+		seen[dest] = dest_name;
+		todo.push_back(dest);
+	      }
+	    tgba_explicit::transition* t =
+	      res->create_transition(seen[src], dest_name);
+	    res->add_conditions(t, cond);
+	  }
+      }
+    res->merge_transitions();
+
+    // Release all states.
+    state_set::const_iterator i = states.begin();
+    while (i != states.end())
+      {
+	// Advance the iterator before deleting the key.
+	const state* s = *i;
+	++i;
+	delete s;
+      }
+
+    return res;
+  }
+}

src/tgbaalgos/powerset.hh

@@ -0,0 +1,37 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// 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_POWERSET_HH
+# define SPOT_TGBAALGOS_POWERSET_HH
+
+# include "tgba/tgbaexplicit.hh"
+
+namespace spot
+{
+  /// \brief Build a deterministic automaton, ignoring acceptance conditions.
+  ///
+  /// This create a deterministic automaton that recognize the
+  /// same language as \a aut would if its acceptance conditions
+  /// were ignored.  This is the classical powerset algorithm.
+  tgba_explicit* tgba_powerset(const tgba* aut);
+}
+
+#endif // SPOT_TGBAALGOS_POWERSET_HH

src/tgbatest/Makefile.am

@@ -1,4 +1,4 @@
-## Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+## Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
 ## et Marie Curie.
 ##
@@ -28,10 +28,12 @@ check_SCRIPTS = defs
 check_PROGRAMS = \
   bddprod \
   explicit \
+  expldot \
   explprod \
   ltl2tgba \
   ltlprod \
   mixprod \
+  powerset \
   readsave \
   tgbaread \
   tripprod
@@ -40,10 +42,13 @@ check_PROGRAMS = \
 bddprod_SOURCES  = ltlprod.cc
 bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT
 explicit_SOURCES = explicit.cc
+expldot_SOURCES  = powerset.cc
+expldot_CXXFLAGS = -DDOTTY
 explprod_SOURCES = explprod.cc
 ltl2tgba_SOURCES = ltl2tgba.cc
 ltlprod_SOURCES  = ltlprod.cc
 mixprod_SOURCES  = mixprod.cc
+powerset_SOURCES = powerset.cc
 readsave_SOURCES = readsave.cc
 tgbaread_SOURCES = tgbaread.cc
 tripprod_SOURCES = tripprod.cc

src/tgbatest/powerset.cc

@@ -0,0 +1,50 @@
+#include <iostream>
+#include <cassert>
+#include "tgba/tgbaexplicit.hh"
+#include "tgbaalgos/powerset.hh"
+#include "tgbaparse/public.hh"
+#include "tgbaalgos/save.hh"
+#include "ltlast/allnodes.hh"
+#include "tgbaalgos/dotty.hh"
+
+void
+syntax(char* prog)
+{
+  std::cerr << prog << " file" << std::endl;
+  exit(2);
+}
+
+int
+main(int argc, char** argv)
+{
+  int exit_code = 0;
+
+  if (argc != 2)
+    syntax(argv[0]);
+
+  spot::bdd_dict* dict = new spot::bdd_dict();
+
+  spot::ltl::environment& env(spot::ltl::default_environment::instance());
+  spot::tgba_parse_error_list pel;
+  spot::tgba_explicit* a = spot::tgba_parse(argv[1], pel, dict, env);
+  if (spot::format_tgba_parse_errors(std::cerr, pel))
+    return 2;
+
+
+#ifndef DOTTY
+  spot::tgba_explicit* e = spot::tgba_powerset(a);
+  spot::tgba_save_reachable(std::cout, e);
+  delete e;
+#else
+  spot::dotty_reachable(std::cout, a);
+#endif
+
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
+  assert(spot::ltl::atomic_prop::instance_count() != 0);
+  delete a;
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  delete dict;
+  return exit_code;
+}