diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 696378ae0..79016813a 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -32,6 +32,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ bfssteps.hh \ cutscc.hh \ + degen.hh \ dotty.hh \ dottydec.hh \ dupexp.hh \ @@ -69,6 +70,7 @@ noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ bfssteps.cc \ cutscc.cc \ + degen.cc \ dotty.cc \ dottydec.cc \ dupexp.cc \ diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc new file mode 100644 index 000000000..f3a9010a8 --- /dev/null +++ b/src/tgbaalgos/degen.cc @@ -0,0 +1,355 @@ +// Copyright (C) 2012 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 "degen.hh" +#include "tgba/tgbaexplicit.hh" +#include "misc/hash.hh" +#include "misc/hashfunc.hh" +#include "ltlast/constant.hh" +#include +#include + +namespace spot +{ + namespace + { + // A state in the degenalized automaton corresponds to a state in + // the TGBA associated to a level. The level is just an index in + // the list of acceptance sets. + typedef std::pair degen_state; + + struct degen_state_hash + { + size_t + operator()(const degen_state& s) const + { + return s.first->hash() & wang32_hash(s.second); + } + }; + + struct degen_state_equal + { + bool + operator()(const degen_state& left, + const degen_state& right) const + { + if (left.second != right.second) + return false; + return left.first->compare(right.first) == 0; + } + }; + + // Associate the degeneralized state to its number. + typedef Sgi::hash_map ds2num_map; + + // Queue of state to be processed. + typedef std::deque queue_t; + + // Memory management for the input states. + class unicity_table + { + typedef Sgi::hash_set uniq_set; + uniq_set m; + public: + const state* operator()(const state* s) + { + uniq_set::const_iterator i = m.find(s); + if (i == m.end()) + { + m.insert(s); + return s; + } + else + { + s->destroy(); + return *i; + } + } + + ~unicity_table() + { + for (uniq_set::iterator i = m.begin(); i != m.end(); ++i) + (*i)->destroy(); + } + }; + + // Acceptance set common to all outgoing transitions of some state. + class outgoing_acc + { + const tgba* a_; + typedef Sgi::hash_map accmap_t; + mutable accmap_t accmap_; + mutable accmap_t accmapu_; + + public: + outgoing_acc(const tgba* a): a_(a) + { + } + + bdd common_acc(const state* s) + { + // Lookup cache + accmap_t::const_iterator i = accmap_.find(s); + if (i != accmap_.end()) + return i->second; + + bdd common = a_->all_acceptance_conditions(); + tgba_succ_iterator* it = a_->succ_iter(s); + for (it->first(); !it->done() && common != bddfalse; it->next()) + common &= it->current_acceptance_conditions(); + delete it; + + // Populate cache + accmap_[s->clone()] = common; + return common; + } + + bdd union_acc(const state* s) + { + // Lookup cache + accmap_t::const_iterator i = accmapu_.find(s); + if (i != accmapu_.end()) + return i->second; + + bdd common = bddfalse; + tgba_succ_iterator* it = a_->succ_iter(s); + for (it->first(); !it->done(); it->next()) + common |= it->current_acceptance_conditions(); + delete it; + + // Populate cache + accmapu_[s->clone()] = common; + return common; + } + }; + } + + sba* + degeneralize(const tgba* a) + { + bdd_dict* dict = a->get_dict(); + + // The result (degeneralized) automaton uses numbered state. + sba_explicit_number* res = new sba_explicit_number(dict); + dict->register_all_variables_of(a, res); + // FIXME: unregister acceptance conditions. + + // Invent a new acceptance set for the degeneralized automaton. + int accvar = + dict->register_acceptance_variable(ltl::constant::true_instance(), res); + bdd degen_acc = bdd_ithvar(accvar); + res->set_acceptance_conditions(degen_acc); + + // Create an order of acceptance conditions. Each entry in this + // vector correspond to an acceptance set. Each index can + // be used as a level in degen_state to indicate the next expected + // acceptance set. Level order.size() is a special level used to + // denote accepting states. + std::vector order; + { + // The order is arbitrary, but it turns out that using push_back + // instead of push_front often gives better results because + // acceptance sets at the beginning if the cycle are more often + // used in the automaton. (This surprising fact is probably + // related to the order in which we declare the BDD variables + // during the translation.) + bdd all = a->all_acceptance_conditions(); + while (all != bddfalse) + { + bdd next = bdd_satone(all); + all -= next; + order.push_back(next); + } + } + + outgoing_acc outgoing(a); + + // Make sure we always use the same pointer for identical states + // from the input automaton. + unicity_table uniq; + + // These maps make it possible to convert degen_state to number + // and vice-versa. + ds2num_map ds2num; + + queue_t todo; + + const state* s0 = uniq(a->get_init_state()); + degen_state s(s0, 0); + + // As an heuristic, if the initial state has accepting self-loops, + // start the degeneralization on the accepting level. + { + bdd all = a->all_acceptance_conditions(); + tgba_succ_iterator* it = a->succ_iter(s0); + for (it->first(); !it->done(); it->next()) + { + // Look only for transitions that are accepting. + if (all != it->current_acceptance_conditions()) + continue; + // Look only for self-loops. + const state* dest = uniq(it->current_state()); + if (dest == s0) + { + // The initial state has an accepting self-loop. + s.second = order.size(); + break; + } + } + delete it; + } + + ds2num[s] = 0; + todo.push_back(s); + + while (!todo.empty()) + { + s = todo.front(); + todo.pop_front(); + int src = ds2num[s]; + unsigned slevel = s.second; + + // If we have a state on the last level, it should be accepting. + bool is_acc = slevel == order.size(); + // On the accepting level, start again from level 0. + if (is_acc) + slevel = 0; + + tgba_succ_iterator* i = a->succ_iter(s.first); + for (i->first(); !i->done(); i->next()) + { + degen_state d(uniq(i->current_state()), 0); + + // The old level is slevel. What should be the new one? + bdd acc = i->current_acceptance_conditions(); + bdd otheracc = outgoing.common_acc(d.first); + + if (is_acc) + { + // Ignore the last expected acceptance set (the value of + // *prev below) if it is common to all other outgoing + // transitions (of the current state) AND if it is not + // used by any outgoing transition of the destination + // state. + // + // 1) It's correct to do that, because this acceptance + // set is common to other outgoing transitions. + // Therefore if we make a cycle to this state we + // will eventually see that acceptance set thanks + // to the "pulling" of the common acceptance sets + // of the destination state (d.first). + // + // 2) It's also desirable because it makes the + // degeneralization idempotent (up to a renaming of + // states). Consider the following automaton where + // 1 is initial and => marks accepting transitions: + // 1=>1, 1=>2, 2->2, 2->1 This is already an SBA, + // with 1 as accepting state. However if you try + // degeralize it without ignoring *prev, you'll get + // two copies of states 2, depending on whether we + // reach it using 1=>2 or from 2->2. If this + // example was not clear, uncomment this following + // "if" block, and play with the "degenid.test" + // test case. + // + // 3) Ignoring all common acceptance sets would also + // be correct, but it would make the + // degeneralization produce larger automata in some + // cases. The current condition to ignore only one + // acceptance set if is this not used by the next + // state is a heuristic that is compatible with + // point 2) above while not causing more states to + // be generated in our benchmark of 188 formulae + // from the literature. + if (!order.empty()) + { + unsigned prev = order.size() - 1; + bdd common = outgoing.common_acc(s.first); + if ((common & order[prev]) == order[prev]) + { + bdd u = outgoing.union_acc(d.first); + if ((u & order[prev]) != order[prev]) + acc -= order[prev]; + } + } + } + // A transition in the SLEVEL acceptance set should + // be directed to the next acceptance set. If the + // current transition is also in the next acceptance + // set, then go to the one after, etc. + // + // See Denis Oddoux's PhD thesis for a nice + // explanation (in French). + // @PhDThesis{ oddoux.03.phd, + // author = {Denis Oddoux}, + // title = {Utilisation des automates alternants pour un + // model-checking efficace des logiques + // temporelles lin{\'e}aires.}, + // school = {Universit{\'e}e Paris 7}, + // year = {2003}, + // address= {Paris, France}, + // month = {December} + // } + unsigned next = slevel; + // Consider both the current acceptance sets, and the + // acceptance sets common to the outgoing transitions of + // the destination state. + acc |= otheracc; + while (next < order.size() + && (acc & order[next]) == order[next]) + ++next; + + d.second = next; + + // Have we already seen this destination? + int dest; + ds2num_map::const_iterator di = ds2num.find(d); + if (di != ds2num.end()) + { + dest = di->second; + } + else + { + dest = ds2num.size(); + ds2num[d] = dest; + todo.push_back(d); + } + + // Actually create the transition. + state_explicit_number::transition* t + = res->create_transition(src, dest); + t->condition = i->current_condition(); + // If the source state is accepting, we have to put + // degen_acc on all outgoing transitions. (We are still + // building a TGBA; we only assure that it can be used as + // an SBA.) + t->acceptance_conditions = is_acc ? degen_acc : bddfalse; + } + delete i; + } + + res->merge_transitions(); + return res; + } +} diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh new file mode 100644 index 000000000..034dcc63e --- /dev/null +++ b/src/tgbaalgos/degen.hh @@ -0,0 +1,44 @@ +// Copyright (C) 2012 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_TGBAALGOS_DEGEN_HH +# define SPOT_TGBAALGOS_DEGEN_HH + +namespace spot +{ + class sba; + class tgba; + + /// \brief Degeneralize a spot::tgba into an equivalent sba with + /// only one acceptance condition. + /// + /// This algorithms will build a new explicit automaton that has + /// at most (N+1) times the number of states of the original automaton. + /// + /// If you want to build a degeneralized automaton on-the-fly, see + /// spot::tgba_sba_proxy or spot::tgba_tba_proxy. + /// + /// \see tgba_sba_proxy, tgba_tba_proxy + /// \ingroup tgba_misc + sba* degeneralize(const tgba* a); +} + + +#endif diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index c7c74fa36..45aefc5c5 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -41,6 +41,7 @@ #include "tgbaalgos/lbtt.hh" #include "tgba/tgbatba.hh" #include "tgba/tgbasgba.hh" +#include "tgbaalgos/degen.hh" #include "tgba/tgbaproduct.hh" #include "tgba/futurecondcol.hh" #include "tgbaalgos/reducerun.hh" @@ -1012,7 +1013,7 @@ main(int argc, char** argv) } else if (degeneralize_opt == DegenSBA) { - degeneralized = a = new spot::tgba_sba_proxy(a); + degeneralized = a = spot::degeneralize(a); assume_sba = true; } else if (labeling_opt == StateLabeled) @@ -1066,7 +1067,7 @@ main(int argc, char** argv) else if (degeneralize_opt == DegenSBA) { product = product_degeneralized = a = - new spot::tgba_sba_proxy(product); + spot::degeneralize(product); assume_sba = true; } } @@ -1148,7 +1149,7 @@ main(int argc, char** argv) // It is possible that we have applied other // operations to the automaton since its initial // degeneralization. Let's degeneralize again! - spot::tgba_sba_proxy* s = new spot::tgba_sba_proxy(a); + spot::tgba* s = spot::degeneralize(a); spot::never_claim_reachable(std::cout, s, f, spin_comments); delete s; }