From 3fd49da15960c06b97a2b9402fb3265c6a6a0271 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Feb 2013 18:01:32 +0100 Subject: [PATCH] complete: new algorithm for TGBAs * src/tgbaalgos/complete.cc, src/tgbaalgos/complete.hh: New files. * src/tgbaalgos/Makefile.am: Add them. --- src/tgbaalgos/Makefile.am | 10 ++-- src/tgbaalgos/complete.cc | 118 ++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/complete.hh | 32 +++++++++++ 3 files changed, 156 insertions(+), 4 deletions(-) create mode 100644 src/tgbaalgos/complete.cc create mode 100644 src/tgbaalgos/complete.hh diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 42e21446e..7905aa803 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -29,13 +29,14 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ bfssteps.hh \ + complete.hh \ compsusp.hh \ cutscc.hh \ cycles.hh \ dbacomp.hh \ degen.hh \ - dotty.hh \ dottydec.hh \ + dotty.hh \ dupexp.hh \ eltl2tgba_lacim.hh \ emptiness.hh \ @@ -56,12 +57,13 @@ tgbaalgos_HEADERS = \ randomgraph.hh \ reachiter.hh \ reducerun.hh \ + reductgba_sim.hh \ replayrun.hh \ rundotdec.hh \ safety.hh \ save.hh \ - scc.hh \ sccfilter.hh \ + scc.hh \ se05.hh \ simulation.hh \ stats.hh \ @@ -69,12 +71,12 @@ tgbaalgos_HEADERS = \ tau03.hh \ tau03opt.hh \ translate.hh \ - reductgba_sim.hh \ word.hh noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ bfssteps.cc \ + complete.cc \ compsusp.cc \ cutscc.cc \ cycles.cc \ @@ -102,6 +104,7 @@ libtgbaalgos_la_SOURCES = \ randomgraph.cc \ reachiter.cc \ reducerun.cc \ + reductgba_sim.cc \ replayrun.cc \ rundotdec.cc \ safety.cc \ @@ -115,7 +118,6 @@ libtgbaalgos_la_SOURCES = \ tau03.cc \ tau03opt.cc \ translate.cc \ - reductgba_sim.cc \ weight.cc \ weight.hh \ word.cc diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc new file mode 100644 index 000000000..8de040498 --- /dev/null +++ b/src/tgbaalgos/complete.cc @@ -0,0 +1,118 @@ +// -*- 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 "complete.hh" +#include "reachiter.hh" +#include "ltlast/constant.hh" + +namespace spot +{ + + namespace + { + class tgbacomplete_iter: + public tgba_reachable_iterator_depth_first_stack + { + bdd_dict* dict_; + tgba_explicit_number* out_; + bdd addacc_; + + typedef state_explicit_number::transition trans; + public: + tgbacomplete_iter(const tgba* a) + : tgba_reachable_iterator_depth_first_stack(a), + dict_(a->get_dict()), + out_(new tgba_explicit_number(dict_)), + addacc_(bddfalse) + { + dict_->register_all_variables_of(a, out_); + + if (a->number_of_acceptance_conditions() == 0) + { + const ltl::formula* t = ltl::constant::true_instance(); + int accvar = + dict_->register_acceptance_variable(t, out_); + addacc_ = bdd_ithvar(accvar); + out_->set_acceptance_conditions(addacc_); + } + else + { + out_->set_acceptance_conditions(a->all_acceptance_conditions()); + } + } + + 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; + } + } + + 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); + trans* t1 = out_->create_transition(in, out); + + t1->condition = si->current_condition(); + t1->acceptance_conditions = + si->current_acceptance_conditions() | addacc_; + } + + }; + + } // anonymous + + tgba_explicit_number* tgba_complete(const tgba* aut) + { + tgbacomplete_iter ci(aut); + ci.run(); + return ci.result(); + } +} + + diff --git a/src/tgbaalgos/complete.hh b/src/tgbaalgos/complete.hh new file mode 100644 index 000000000..35a173980 --- /dev/null +++ b/src/tgbaalgos/complete.hh @@ -0,0 +1,32 @@ +// -*- 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_COMPLETE_HH +# define SPOT_TGBAALGOS_COMPLETE_HH + +#include "tgba/tgbaexplicit.hh" + +namespace spot +{ + /// Complete a TGBA + SPOT_API tgba_explicit_number* + tgba_complete(const tgba* aut); +} + +#endif // SPOT_TGBAALGOS_COMPLETE_HH