diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am
index e24f4dfb6..42e21446e 100644
--- a/src/tgbaalgos/Makefile.am
+++ b/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 \
diff --git a/src/tgbaalgos/dbacomp.cc b/src/tgbaalgos/dbacomp.cc
new file mode 100644
index 000000000..8632c0358
--- /dev/null
+++ b/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 .
+
+#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();
+ }
+}
diff --git a/src/tgbaalgos/dbacomp.hh b/src/tgbaalgos/dbacomp.hh
new file mode 100644
index 000000000..62f45a14b
--- /dev/null
+++ b/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 .
+
+#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
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 46f903811..6b2283410 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/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;