Introduce a class to complement a WDBA on-the-fly.

* src/tgba/wdbacomp.hh, src/tgba/wdbacomp.cc: New file.
* src/tgba/Makefile.am: Add them.
* src/tgbaalgos/minimize.cc (minimize_obligation): Use
wdba_complement().

ChangeLog

@@ -1,3 +1,12 @@
+2011-01-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Introduce a class to complement a WDBA on-the-fly.
+
+	* src/tgba/wdbacomp.hh, src/tgba/wdbacomp.cc: New file.
+	* src/tgba/Makefile.am: Add them.
+	* src/tgbaalgos/minimize.cc (minimize_obligation): Use
+	wdba_complement().
+
 2011-01-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* src/tgbatest/Makefile.am: Remove the unused minimize program.

src/tgba/Makefile.am

@@ -1,4 +1,4 @@
-## Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+## Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
 ## de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -51,7 +51,8 @@ tgba_HEADERS = \
   tgbasgba.hh \
   tgbasafracomplement.hh \
   tgbatba.hh \
-  tgbaunion.hh
+  tgbaunion.hh \
+  wdbacomp.hh
 
 noinst_LTLIBRARIES = libtgba.la
 libtgba_la_SOURCES = \
@@ -75,4 +76,5 @@ libtgba_la_SOURCES = \
   tgbascc.cc \
   tgbasgba.cc \
   tgbatba.cc \
-  tgbaunion.cc
+  tgbaunion.cc \
+  wdbacomp.cc

src/tgba/wdbacomp.cc

@@ -0,0 +1,292 @@
+// Copyright (C) 2011 Laboratoire de Recherche et Développement 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 "wdbacomp.hh"
+#include "ltlast/constant.hh"
+
+namespace spot
+{
+  namespace
+  {
+    class state_wdba_comp_proxy : public state
+    {
+    public:
+      state_wdba_comp_proxy(state* s) : s_(s)
+      {
+      }
+
+      /// Copy constructor
+      state_wdba_comp_proxy(const state_wdba_comp_proxy& o)
+	: state(),
+	  s_(o.real_state())
+      {
+	if (s_)
+	  s_ = s_->clone();
+      }
+
+      virtual
+      ~state_wdba_comp_proxy()
+      {
+	delete s_;
+      }
+
+      state*
+      real_state() const
+      {
+	return s_;
+      }
+
+      virtual int
+      compare(const state* other) const
+      {
+	const state_wdba_comp_proxy* o =
+	  dynamic_cast<const state_wdba_comp_proxy*>(other);
+	assert(o);
+	const state* oo = o->real_state();
+	if (s_ == 0)
+	  return oo ? 1 : 0;
+	if (oo == 0)
+	  return -1;
+
+	return s_->compare(oo);
+      }
+
+      virtual size_t
+      hash() const
+      {
+	if (s_)
+	  return s_->hash();
+	return 0;
+      }
+
+      virtual
+      state_wdba_comp_proxy* clone() const
+      {
+	return new state_wdba_comp_proxy(*this);
+      }
+
+    private:
+      state* s_; // 0 if sink-state.
+    };
+
+    class tgba_wdba_comp_proxy_succ_iterator: public tgba_succ_iterator
+    {
+    public:
+      tgba_wdba_comp_proxy_succ_iterator(tgba_succ_iterator* it,
+					 bdd the_acceptance_cond)
+	: it_(it), the_acceptance_cond_(the_acceptance_cond), left_(bddtrue)
+      {
+      }
+
+      virtual
+      ~tgba_wdba_comp_proxy_succ_iterator()
+      {
+	delete it_;
+      }
+
+      // iteration
+
+      void
+      first()
+      {
+	if (it_)
+	  it_->first();
+	left_ = bddtrue;
+      }
+
+      void
+      next()
+      {
+	left_ -= current_condition();
+	if (it_)
+	  it_->next();
+      }
+
+      bool
+      done() const
+      {
+	return left_ == bddfalse;
+      }
+
+      // inspection
+
+      state_wdba_comp_proxy*
+      current_state() const
+      {
+	if (!it_ || it_->done())
+	  return new state_wdba_comp_proxy(0);
+	return new state_wdba_comp_proxy(it_->current_state());
+      }
+
+      bdd
+      current_condition() const
+      {
+	if (!it_ || it_->done())
+	  return left_;
+	return it_->current_condition();
+      }
+
+      bdd
+      current_acceptance_conditions() const
+      {
+	if (!it_ || it_->done())
+	  // The sink state is accepting in the negated automaton.
+	  return the_acceptance_cond_;
+
+	if (it_->current_acceptance_conditions() == bddfalse)
+	  return the_acceptance_cond_;
+	else
+	  return bddfalse;
+      }
+
+    protected:
+      tgba_succ_iterator* it_;
+      const bdd the_acceptance_cond_;
+      bdd left_;
+    };
+
+    class tgba_wdba_comp_proxy: public tgba
+    {
+    public:
+      tgba_wdba_comp_proxy(const tgba* a)
+	: a_(a)
+      {
+	the_acceptance_cond_ = a->all_acceptance_conditions();
+	if (the_acceptance_cond_ == bddfalse)
+	  {
+	    int v = get_dict()
+	      ->register_acceptance_variable(ltl::constant::true_instance(),
+					     this);
+	    the_acceptance_cond_ = bdd_ithvar(v);
+	  }
+      }
+
+      virtual ~tgba_wdba_comp_proxy()
+      {
+	get_dict()->unregister_all_my_variables(this);
+      }
+
+      virtual state* get_init_state() const
+      {
+	return new state_wdba_comp_proxy(a_->get_init_state());
+      }
+
+      virtual tgba_succ_iterator*
+      succ_iter(const state* local_state,
+		const state* global_state = 0,
+		const tgba* global_automaton = 0) const
+      {
+	const state_wdba_comp_proxy* s =
+	  dynamic_cast<const state_wdba_comp_proxy*>(local_state);
+	assert(s);
+
+	const state* o = s->real_state();
+	tgba_succ_iterator* it = 0;
+	if (o)
+	   it = a_->succ_iter(s->real_state(), global_state, global_automaton);
+	return new tgba_wdba_comp_proxy_succ_iterator(it,
+						      the_acceptance_cond_);
+      }
+
+      virtual bdd_dict*
+      get_dict() const
+      {
+	return a_->get_dict();
+      }
+
+      virtual std::string
+      format_state(const state* ostate) const
+      {
+	const state_wdba_comp_proxy* s =
+	  dynamic_cast<const state_wdba_comp_proxy*>(ostate);
+	assert(s);
+	const state* rs = s->real_state();
+	if (rs)
+	  return a_->format_state(s->real_state());
+	else
+	  return "(*)"; // sink state
+      }
+
+      virtual state*
+      project_state(const state* s, const tgba* t) const
+      {
+	const state_wdba_comp_proxy* s2 =
+	  dynamic_cast<const state_wdba_comp_proxy*>(s);
+	assert(s2);
+	if (t == this)
+	  return s2->clone();
+	return a_->project_state(s2->real_state(), t);
+      }
+
+      virtual bdd
+      all_acceptance_conditions() const
+      {
+	return the_acceptance_cond_;
+      }
+
+      virtual bdd
+      neg_acceptance_conditions() const
+      {
+	return !the_acceptance_cond_;
+      }
+
+  protected:
+    virtual bdd
+    compute_support_conditions(const state* ostate) const
+      {
+	const state_wdba_comp_proxy* s =
+	  dynamic_cast<const state_wdba_comp_proxy*>(ostate);
+	assert(s);
+	const state* rs = s->real_state();
+	if (rs)
+	  return a_->support_conditions(rs);
+	else
+	  return bddtrue;
+      }
+
+      virtual bdd compute_support_variables(const state* ostate) const
+      {
+	const state_wdba_comp_proxy* s =
+	  dynamic_cast<const state_wdba_comp_proxy*>(ostate);
+	assert(s);
+	const state* rs = s->real_state();
+	if (rs)
+	  return a_->support_variables(rs);
+	else
+	  return bddtrue;
+      }
+
+      const tgba* a_;
+    private:
+      bdd the_acceptance_cond_;
+
+      // Disallow copy.
+      tgba_wdba_comp_proxy(const tgba_wdba_comp_proxy&);
+      tgba_wdba_comp_proxy& operator=(const tgba_wdba_comp_proxy&);
+    };
+
+  }
+
+  tgba*
+  wdba_complement(const tgba* aut)
+  {
+    return new tgba_wdba_comp_proxy(aut);
+  }
+}

src/tgba/wdbacomp.hh

@@ -0,0 +1,35 @@
+// Copyright (C) 2011 Laboratoire de Recherche et Développement 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_TGBA_WDBACOMP_HH
+# define SPOT_TGBA_WDBACOMP_HH
+
+#include "tgba.hh"
+
+namespace spot
+{
+  /// \brief Complement a weak deterministic Büchi automaton
+  /// \ingroup tgba_on_the_fly_algorithms
+  /// \param aut a weak deterministic Büchi automaton to complement
+  /// \return a new automaton that recognizes the complement language
+  tgba* wdba_complement(const tgba* aut);
+}
+
+#endif

src/tgbaalgos/minimize.cc

@@ -39,6 +39,7 @@
 #include "misc/bddlt.hh"
 #include "tgba/tgbaproduct.hh"
 #include "tgba/tgbatba.hh"
+#include "tgba/wdbacomp.hh"
 #include "tgbaalgos/powerset.hh"
 #include "tgbaalgos/gtec/gtec.hh"
 #include "tgbaalgos/safety.hh"
@@ -636,9 +637,11 @@ namespace spot
       {
 	delete ec;
 	delete p;
+
 	// Complement the minimized WDBA.
-	min_aut_f->complement_all_acceptance_conditions();
-	tgba* p = new tgba_product(aut_f, min_aut_f);
+	tgba* neg_min_aut_f = wdba_complement(min_aut_f);
+
+	tgba* p = new tgba_product(aut_f, neg_min_aut_f);
 	emptiness_check* ec = couvreur99(p);
 	res = ec->check();
 
@@ -647,13 +650,12 @@ namespace spot
 	    // Finally, we are now sure that it was safe
 	    // to minimize the automaton.
 	    ok = true;
-	    // Get the original automaton back.
-	    min_aut_f->complement_all_acceptance_conditions();
 	  }
 
 	delete res;
 	delete ec;
 	delete p;
+	delete neg_min_aut_f;
       }
     else
       {