From bd2e78c1edf206e39831b2d408125bedd6af2606 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 21 Jan 2013 14:45:44 +0100 Subject: [PATCH] Introduce a dba_complement() function. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 6 +- src/tgbaalgos/dbacomp.cc | 134 ++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/dbacomp.hh | 39 +++++++++++ src/tgbatest/ltl2tgba.cc | 17 ++++- 4 files changed, 193 insertions(+), 3 deletions(-) create mode 100644 src/tgbaalgos/dbacomp.cc create mode 100644 src/tgbaalgos/dbacomp.hh 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;