Introduce a dba_complement() function.

Loosely based on "Complementing Deterministic Büchi Automata in
Polynomial Time", R. P. Kurshan, 1987, J. Comp. Syst. Sci. 35.

* src/tgbaalgos/dbacomp.cc, src/tgbaalgos/dbacomp.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltl2tgba.cc (-DC): New option to test it.

src/tgbaalgos/Makefile.am

@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
-## et Développement de l'Epita (LRDE).
+## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de
+## Recherche et Développement de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004, 2005 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 = \
   compsusp.hh \
   cutscc.hh \
   cycles.hh \
+  dbacomp.hh \
   degen.hh \
   dotty.hh \
   dottydec.hh \
@@ -77,6 +78,7 @@ libtgbaalgos_la_SOURCES = \
   compsusp.cc \
   cutscc.cc \
   cycles.cc \
+  dbacomp.cc \
   degen.cc \
   dotty.cc \
   dottydec.cc \

src/tgbaalgos/dbacomp.cc

@@ -0,0 +1,134 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "dbacomp.hh"
+#include "ltlast/constant.hh"
+#include "reachiter.hh"
+
+namespace spot
+{
+
+  namespace
+  {
+    class dbacomp_iter: public tgba_reachable_iterator_depth_first
+    {
+      bdd orig_acc_;
+      bdd acc_;
+      bdd_dict* dict_;
+      tgba_explicit_number* out_;
+      typedef state_explicit_number::transition trans;
+    public:
+      dbacomp_iter(const tgba* a)
+	: tgba_reachable_iterator_depth_first(a),
+	  dict_(a->get_dict()),
+	  out_(new tgba_explicit_number(dict_))
+      {
+	dict_->register_all_variables_of(a, out_);
+	unsigned c = a->number_of_acceptance_conditions();
+	orig_acc_ = a->all_acceptance_conditions();
+	if (c == 1)
+	  {
+	    out_->copy_acceptance_conditions_of(a);
+	    acc_ = orig_acc_;
+	  }
+	else
+	  {
+	    // If there is no acceptance conditions in the original
+	    // automaton, add one.
+	    assert(c == 0);
+	    int accvar = dict_->register_acceptance_variable
+	      (ltl::constant::true_instance(), out_);
+	    acc_ = bdd_ithvar(accvar);
+	    out_->set_acceptance_conditions(acc_);
+	  }
+      }
+
+      tgba_explicit_number*
+      result()
+      {
+	return out_;
+      }
+
+      void
+      end()
+      {
+	out_->merge_transitions();
+	// create a sink state if needed.
+	if (out_->has_state(0))
+	  {
+	    trans* t = out_->create_transition(0, 0);
+	    t->condition = bddtrue;
+	    t->acceptance_conditions = acc_;
+	  }
+      }
+
+      void process_state(const state*, int n,
+			 tgba_succ_iterator* i)
+      {
+	// add a transition to a sink state if the state is not complete.
+	bdd all = bddtrue;
+	for (i->first(); !i->done(); i->next())
+	  all -= i->current_condition();
+	if (all != bddfalse)
+	  {
+	    trans* t = out_->create_transition(n, 0);
+	    t->condition = all;
+	  }
+      }
+
+      void
+      process_link(const state*, int in,
+		   const state*, int out,
+		   const tgba_succ_iterator* si)
+      {
+	assert(in > 0);
+	assert(out > 0);
+	bdd a = si->current_acceptance_conditions();
+
+	// Positive states represent a non-accepting copy of the
+	// original automaton.
+	trans* t1 = out_->create_transition(in, out);
+	t1->condition = si->current_condition();
+
+	// Negative states encode a copy of the automaton in which all
+	// accepting transitions have been removed, and all the
+	// remaining transitions are now accepting.
+	if (a != orig_acc_)
+	  {
+	    trans* t2 = out_->create_transition(-in, -out);
+	    t2->condition = si->current_condition();
+	    t2->acceptance_conditions = acc_;
+	  }
+
+	// A non-deterministic transition between the two copies.
+	trans* t3 = out_->create_transition(in, -out);
+	t3->condition = si->current_condition();
+      }
+
+    };
+
+  } // anonymous
+
+  tgba_explicit_number* dba_complement(const tgba* aut)
+  {
+    dbacomp_iter dci(aut);
+    dci.run();
+    return dci.result();
+  }
+}

src/tgbaalgos/dbacomp.hh

@@ -0,0 +1,39 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#ifndef SPOT_TGBAALGOS_DBACOMP_HH
+# define SPOT_TGBAALGOS_DBACOMP_HH
+
+#include "tgba/tgbaexplicit.hh"
+
+namespace spot
+{
+
+
+  /// Complement a deterministic Büchi automaton
+  ///
+  /// The automaton \a aut should be deterministic and should have at
+  /// most a single acceptance condition.  It can be transition-based,
+  /// or state-based.  The resulting automaton is very unlikely to be
+  /// deterministic.
+  SPOT_API tgba_explicit_number*
+  dba_complement(const tgba* aut);
+}
+
+#endif // SPOT_TGBAALGOS_DBACOMP_HH

src/tgbatest/ltl2tgba.cc

@@ -70,6 +70,7 @@
 #include "tgbaalgos/simulation.hh"
 #include "tgbaalgos/compsusp.hh"
 #include "tgbaalgos/powerset.hh"
+#include "tgbaalgos/dbacomp.hh"
 
 #include "taalgos/tgba2ta.hh"
 #include "taalgos/dotty.hh"
@@ -388,6 +389,7 @@ main(int argc, char** argv)
   bool opt_reduce = false;
   bool opt_minimize = false;
   bool opt_determinize = false;
+  bool opt_dbacomp = false;
   bool reject_bigger = false;
   bool opt_bisim_ta = false;
   bool opt_monitor = false;
@@ -473,6 +475,10 @@ main(int argc, char** argv)
 	{
 	  degeneralize_opt = DegenTBA;
 	}
+      else if (!strcmp(argv[formula_index], "-DC"))
+	{
+	  opt_dbacomp = true;
+	}
       else if (!strncmp(argv[formula_index], "-DS", 3))
 	{
 	  degeneralize_opt = DegenSBA;
@@ -1441,6 +1447,14 @@ main(int argc, char** argv)
 	  tm.stop("determinization");
 	}
 
+      spot::tgba* complemented = 0;
+      if (opt_dbacomp)
+	{
+	  tm.start("DBA complement");
+	  a = complemented = dba_complement(a);
+	  tm.stop("DBA complement");
+	}
+
       const spot::tgba* expl = 0;
       switch (dupexp)
 	{
@@ -1894,8 +1908,9 @@ main(int argc, char** argv)
       delete expl;
       delete monitor;
       delete minimized;
-      delete determinized;
       delete degeneralized;
+      delete determinized;
+      delete complemented;
       delete aut_scc;
       delete to_free;
       delete echeck_inst;