diff --git a/src/saba/sabacomplementtgba.cc b/src/saba/sabacomplementtgba.cc index 1ded578de..b375475c5 100644 --- a/src/saba/sabacomplementtgba.cc +++ b/src/saba/sabacomplementtgba.cc @@ -24,6 +24,7 @@ #include #include #include "misc/hash.hh" +#include "misc/bddlt.hh" #include "tgbaalgos/degen.hh" #include "tgbaalgos/bfssteps.hh" #include "misc/hashfunc.hh" diff --git a/src/saba/sabacomplementtgba.hh b/src/saba/sabacomplementtgba.hh index 7b25404ab..fbd5343cd 100644 --- a/src/saba/sabacomplementtgba.hh +++ b/src/saba/sabacomplementtgba.hh @@ -20,11 +20,12 @@ #define SPOT_SABA_SABACOMPLEMENTTGBA_HH #include -#include #include "saba.hh" namespace spot { + class tgba_digraph; + /// \ingroup saba /// \brief Complement a TGBA and produce a SABA. /// diff --git a/src/sabatest/sabacomplementtgba.cc b/src/sabatest/sabacomplementtgba.cc index 29a46c201..326253f87 100644 --- a/src/sabatest/sabacomplementtgba.cc +++ b/src/sabatest/sabacomplementtgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2012, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -24,7 +24,6 @@ #include #include #include -#include #include #include #include diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index e60c205a0..a2c2d4843 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -42,7 +42,6 @@ tgba_HEADERS = \ tgbaproduct.hh \ tgbasgba.hh \ tgbasafracomplement.hh \ - tgbatba.hh \ tgbaunion.hh \ wdbacomp.hh @@ -61,6 +60,5 @@ libtgba_la_SOURCES = \ tgbasafracomplement.cc \ tgbascc.cc \ tgbasgba.cc \ - tgbatba.cc \ tgbaunion.cc \ wdbacomp.cc diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc deleted file mode 100644 index f814096ac..000000000 --- a/src/tgba/tgbatba.cc +++ /dev/null @@ -1,542 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche -// et Développement de l'Epita. -// 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. -// -// 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 -#include "tgbatba.hh" -#include "bddprint.hh" -#include "ltlast/constant.hh" -#include "misc/hashfunc.hh" - -namespace spot -{ - namespace - { - /// \brief A state for spot::tgba_tba_proxy. - /// - /// This state is in fact a pair of states: the state from the tgba - /// automaton, and a state of the "counter" (we use a pointer - /// to the position in the cycle_acc_ list). - class state_tba_proxy: public state - { - typedef tgba_tba_proxy::cycle_list::const_iterator iterator; - public: - state_tba_proxy(state* s, iterator acc) - : s_(s), acc_(acc) - { - } - - // Note: There is a default copy constructor, needed by - // std::unordered_set. It does not clone the state "s", because the - // destructor will not destroy it either. Actually, the states - // are all destroyed in the tgba_tba_proxy destructor. - - virtual - ~state_tba_proxy() - { - } - - void - destroy() const - { - } - - state* - real_state() const - { - return s_; - } - - bdd - acceptance_cond() const - { - return *acc_; - } - - iterator - acceptance_iterator() const - { - return acc_; - } - - virtual int - compare(const state* other) const - { - const state_tba_proxy* o = down_cast(other); - assert(o); - // Do not simply return "o - this", it might not fit in an int. - if (o < this) - return -1; - if (o > this) - return 1; - return 0; - } - - virtual size_t - hash() const - { - return wang32_hash(s_->hash()) ^ wang32_hash(acc_->id()); - } - - virtual - state_tba_proxy* clone() const - { - return const_cast(this); - } - - private: - state* s_; - iterator acc_; - }; - - struct state_tba_proxy_hash - { - size_t - operator()(const state_tba_proxy& s) const - { - return s.state_tba_proxy::hash(); - } - }; - - struct state_tba_proxy_equal - { - bool - operator()(const state_tba_proxy& left, - const state_tba_proxy& right) const - { - if (left.acceptance_iterator() != right.acceptance_iterator()) - return false; - return left.real_state()->compare(right.real_state()) == 0; - } - }; - - typedef std::unordered_set uniq_map_t; - - typedef std::pair state_ptr_bool_t; - - struct state_ptr_bool_hash: - public std::unary_function - { - size_t - operator()(const state_ptr_bool_t& s) const - { - if (s.second) - return s.first->hash() ^ 12421; - else - return s.first->hash(); - } - }; - - struct state_ptr_bool_equal: - public std::binary_function - { - bool - operator()(const state_ptr_bool_t& left, - const state_ptr_bool_t& right) const - { - if (left.second != right.second) - return false; - return left.first->compare(right.first) == 0; - } - }; - - /// \brief Iterate over the successors of tgba_tba_proxy computed - /// on the fly. - class tgba_tba_proxy_succ_iterator: public tgba_succ_iterator - { - typedef tgba_tba_proxy::cycle_list list; - typedef tgba_tba_proxy::cycle_list::const_iterator iterator; - public: - tgba_tba_proxy_succ_iterator(tgba::succ_iterable&& iterable, - iterator expected, - const list& cycle, - bdd the_acceptance_cond, - const tgba_tba_proxy* aut) - : the_acceptance_cond_(the_acceptance_cond) - { - recycle(std::move(iterable), expected, cycle, aut); - } - - void recycle(tgba::succ_iterable&& iterable, - iterator expected, - const list& cycle, - const tgba_tba_proxy* aut) - { - if (!transmap_.empty()) - { - translist_.clear(); - transmap_.clear(); - } - - for (auto it: iterable) - { - bool accepting; - bdd acc = it->current_acceptance_conditions(); - // As an extra optimization step, gather the acceptance - // conditions common to all outgoing transitions of the - // destination state. We will later add these to "acc" to - // pretend they are already present on this transition. - state* odest = it->current_state(); - bdd otheracc = - aut->common_acceptance_conditions_of_original_state(odest); - - // A transition in the *EXPECTED 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} - // } - iterator next = expected; - // Consider both the current acceptance sets, and the - // acceptance sets common to the outgoing transition of - // the destination state. - acc |= otheracc; - while (next != cycle.end() && bdd_implies(*next, acc)) - ++next; - if (next != cycle.end()) - { - accepting = false; - } - else - { - // The transition is accepting. - accepting = true; - // Skip as much acceptance conditions as we can on our cycle. - next = cycle.begin(); - while (next != expected && bdd_implies(*next, acc)) - ++next; - } - state_tba_proxy* dest = - down_cast(aut->create_state(odest, next)); - // Is DEST already reachable with the same value of ACCEPTING? - state_ptr_bool_t key(dest, accepting); - transmap_t::iterator id = transmap_.find(key); - if (id == transmap_.end()) // No - { - mapit_t pos = - transmap_.emplace(key, it->current_condition()).first; - // Keep the order of the transitions in the - // degeneralized automaton related to the order of the - // transitions in the input automaton: in the past we - // used to simply iterate over transmap_ in whatever - // order the transitions were stored, but the output - // would change between different runs depending on - // the memory address of the states. Now we keep the - // order using translist_. We only arrange it - // slightly so that accepting transitions come first: - // this way they are processed early during - // emptiness-check. - if (accepting) - translist_.push_front(pos); - else - translist_.push_back(pos); - } - else // Yes, combine labels. - { - id->second |= it->current_condition(); - dest->destroy(); - } - } - } - - virtual - ~tgba_tba_proxy_succ_iterator() - { - } - - // iteration - - bool - first() - { - it_ = translist_.begin(); - return it_ != translist_.end(); - } - - bool - next() - { - ++it_; - return it_ != translist_.end(); - } - - bool - done() const - { - return it_ == translist_.end(); - } - - // inspection - - state_tba_proxy* - current_state() const - { - return (*it_)->first.first->clone(); - } - - bdd - current_condition() const - { - return (*it_)->second; - } - - bdd - current_acceptance_conditions() const - { - return (*it_)->first.second ? the_acceptance_cond_ : bddfalse; - } - - protected: - const bdd the_acceptance_cond_; - - typedef std::unordered_map transmap_t; - transmap_t transmap_; - typedef transmap_t::const_iterator mapit_t; - typedef std::list translist_t; - translist_t translist_; - translist_t::const_iterator it_; - }; - - } // anonymous - - tgba_tba_proxy::tgba_tba_proxy(const tgba* a) - : a_(a), uniq_map_(new uniq_map_t) - { - // We will use one acceptance condition for this automata. - // Let's call it Acc[True]. - bdd_dict* d = get_dict(); - d->register_all_variables_of(a, this); - d->unregister_all_typed_variables(bdd_dict::acc, this); - - int v = d - ->register_acceptance_variable(ltl::constant::true_instance(), this); - the_acceptance_cond_ = bdd_ithvar(v); - - if (a->number_of_acceptance_conditions() == 0) - { - acc_cycle_.push_front(bddtrue); - } - else - { - // Build a cycle of expected acceptance conditions. - // - // The order is arbitrary, but it turns out that using - // push_back instead of push_front often gives better results - // because acceptance conditions 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; - acc_cycle_.push_back(next); - } - } - } - - tgba_tba_proxy::~tgba_tba_proxy() - { - get_dict()->unregister_all_my_variables(this); - - accmap_t::const_iterator i = accmap_.begin(); - while (i != accmap_.end()) - { - // Advance the iterator before deleting the key. - const state* s = i->first; - ++i; - s->destroy(); - } - i = accmapu_.begin(); - while (i != accmapu_.end()) - { - // Advance the iterator before deleting the key. - const state* s = i->first; - ++i; - s->destroy(); - } - - uniq_map_t* m = static_cast(uniq_map_); - uniq_map_t::const_iterator j = m->begin(); - while (j != m->end()) - { - const state* s = j->real_state(); - ++j; - s->destroy(); - } - delete m; - - // This has already been destroyed. - // Prevent destroying by tgba::~tgba. - this->last_support_conditions_input_ = 0; - } - - state* - tgba_tba_proxy::create_state(state* s, cycle_list::const_iterator acc) const - { - uniq_map_t* m = static_cast(uniq_map_); - state_tba_proxy st(s, acc); - - std::pair res = m->insert(st); - if (!res.second) - s->destroy(); - - return const_cast(&(*res.first)); - } - - - - state* - tgba_tba_proxy::get_init_state() const - { - return create_state(a_->get_init_state(), acc_cycle_.begin()); - } - - tgba_succ_iterator* - tgba_tba_proxy::succ_iter(const state* st) const - { - const state_tba_proxy* s = down_cast(st); - assert(s); - const state* rs = s->real_state(); - - if (iter_cache_) - { - tgba_tba_proxy_succ_iterator* res = - down_cast(iter_cache_); - res->recycle(a_->succ(rs), - s->acceptance_iterator(), acc_cycle_, this); - iter_cache_ = nullptr; - return res; - } - return new tgba_tba_proxy_succ_iterator(a_->succ(rs), - s->acceptance_iterator(), - acc_cycle_, the_acceptance_cond_, - this); - } - - bdd - tgba_tba_proxy::common_acceptance_conditions_of_original_state(const state* s) - const - { - // Lookup cache - accmap_t::const_iterator i = accmap_.find(s); - if (i != accmap_.end()) - return i->second; - - bdd common = a_->all_acceptance_conditions(); - for (auto it: a_->succ(s)) - { - common &= it->current_acceptance_conditions(); - if (common == bddfalse) - break; - } - - // Populate cache - accmap_[s->clone()] = common; - return common; - } - - bdd - tgba_tba_proxy::union_acceptance_conditions_of_original_state(const state* s) - const - { - // Lookup cache - accmap_t::const_iterator i = accmapu_.find(s); - if (i != accmapu_.end()) - return i->second; - - bdd common = bddfalse; - for (auto it: a_->succ(s)) - common |= it->current_acceptance_conditions(); - - // Populate cache - accmapu_[s->clone()] = common; - return common; - } - - bdd_dict* - tgba_tba_proxy::get_dict() const - { - return a_->get_dict(); - } - - std::string - tgba_tba_proxy::format_state(const state* state) const - { - const state_tba_proxy* s = down_cast(state); - assert(s); - std::string a = bdd_format_accset(get_dict(), s->acceptance_cond()); - if (a != "") - a = " " + a; - return a_->format_state(s->real_state()) + a; - } - - state* - tgba_tba_proxy::project_state(const state* s, const tgba* t) const - { - const state_tba_proxy* s2 = down_cast(s); - assert(s2); - if (t == this) - return s2->clone(); - return a_->project_state(s2->real_state(), t); - } - - - bdd - tgba_tba_proxy::all_acceptance_conditions() const - { - return the_acceptance_cond_; - } - - bdd - tgba_tba_proxy::neg_acceptance_conditions() const - { - return !the_acceptance_cond_; - } - - bdd - tgba_tba_proxy::compute_support_conditions(const state* state) const - { - const state_tba_proxy* s = - down_cast(state); - assert(s); - return a_->support_conditions(s->real_state()); - } - -} diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh deleted file mode 100644 index 075f742b2..000000000 --- a/src/tgba/tgbatba.hh +++ /dev/null @@ -1,122 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche -// et Développement de l'Epita. -// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. -// -// 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_TGBA_TGBATBA_HH -# define SPOT_TGBA_TGBATBA_HH - -#include -#include "tgba.hh" -#include "misc/bddlt.hh" -#include "misc/hash.hh" - -namespace spot -{ - - /// \ingroup tgba_on_the_fly_algorithms - /// \brief Degeneralize a spot::tgba on the fly, producing a TBA. - /// - /// This class acts as a proxy in front of a spot::tgba, that should - /// be degeneralized on the fly. The result is still a spot::tgba, - /// but it will always have exactly one acceptance condition so - /// it could be called TBA (without the G). - /// - /// The degeneralization is done by synchronizing the input - /// automaton with a "counter" automaton such as the one shown in - /// "On-the-fly Verification of Linear Temporal Logic" (Jean-Michel - /// Couveur, FME99). - /// - /// If the input automaton uses N acceptance conditions, the output - /// automaton can have at most max(N,1) times more states and - /// transitions. - class SPOT_API tgba_tba_proxy : public tgba - { - public: - tgba_tba_proxy(const tgba* a); - - virtual ~tgba_tba_proxy(); - - virtual state* get_init_state() const; - - virtual tgba_succ_iterator* succ_iter(const state* state) const; - - virtual bdd_dict* get_dict() const; - - virtual std::string format_state(const state* state) const; - - virtual state* project_state(const state* s, const tgba* t) const; - - virtual bdd all_acceptance_conditions() const; - virtual bdd neg_acceptance_conditions() const; - - typedef std::list cycle_list; - - - /// \brief Return the acceptance conditions common to all outgoing - /// transitions of state \a ostate in the original automaton. - /// - /// This internal function is only meant to be used to implement - /// the iterator returned by succ_iter. - /// - /// The result of this function is computed the first time, and - /// then cached. - bdd common_acceptance_conditions_of_original_state(const state* - ostate) const; - - /// \brief Return the union of acceptance conditions of all outgoing - /// transitions of state \a ostate in the original automaton. - /// - /// This internal function is only meant to be used to implement - /// the iterator returned by succ_iter. - /// - /// The result of this function is computed the first time, and - /// then cached. - bdd union_acceptance_conditions_of_original_state(const state* s) const; - - /// \brief Create a degeneralized state using the unicity table. - /// - /// This is an internal function. \a s should be a fresh state - /// from the source automaton. - state* create_state(state* s, cycle_list::const_iterator acc) const; - - protected: - virtual bdd compute_support_conditions(const state* state) const; - - cycle_list acc_cycle_; - const tgba* a_; - - private: - bdd the_acceptance_cond_; - typedef std::unordered_map accmap_t; - mutable accmap_t accmap_; - mutable accmap_t accmapu_; - - /// Unicity table for degeneralized states. See create_state() - mutable void* uniq_map_; - - // Disallow copy. - tgba_tba_proxy(const tgba_tba_proxy&) SPOT_DELETED; - tgba_tba_proxy& operator=(const tgba_tba_proxy&) SPOT_DELETED; - }; - -} -#endif // SPOT_TGBA_TGBATBA_HH diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index 2ea97a431..e3100176b 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -249,363 +249,408 @@ namespace spot i->second.print(i->first, dict); } }; + + template + tgba_digraph* + degeneralize_aux(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders, + int use_lvl_cache, bool skip_levels) + { + bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl; + + bdd_dict* dict = a->get_dict(); + + // The result automaton is an SBA. + auto res = new tgba_digraph(dict); + if (want_sba) + res->set_bprop(tgba_digraph::StateBasedAcc); + + // We use the same BDD variables as the input, except for the + // acceptance. + dict->register_all_variables_of(a, res); + dict->unregister_all_typed_variables(bdd_dict::acc, res); + + // 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); + } + } + + // Initialize scc_orders + bdd allacc = a->all_acceptance_conditions(); + scc_orders orders(a->all_acceptance_conditions(), skip_levels); + + // Make sure we always use the same pointer for identical states + // from the input automaton. + state_unicity_table uniq; + + // Accepting loop checker, for some heuristics. + has_acc_loop acc_loop(a, uniq); + + // These maps make it possible to convert degen_state to number + // and vice-versa. + ds2num_map ds2num; + + // This map is used to find transitions that go to the same + // destination with the same acceptance. The integer key is + // (dest*2+acc) where dest is the destination state number, and + // acc is 1 iff the transition is accepting. The source + // is always that of the current iteration. + typedef std::map tr_cache_t; + tr_cache_t tr_cache; + + // State level cache + typedef std::map lvl_cache_t; + lvl_cache_t lvl_cache; + + // Compute SCCs in order to use any optimization. + scc_map m(a); + if (use_scc) + m.build_map(); + + // Cache for common outgoing acceptances. + outgoing_acc outgoing(a, use_scc ? &m : 0); + + queue_t todo; + + const state* s0 = uniq(a->get_init_state()); + degen_state s(s0, 0); + + // As a heuristic for building SBA, if the initial state has at + // least one accepting self-loop, start the degeneralization on + // the accepting level. + if (want_sba && acc_loop.check(s0)) + s.second = order.size(); + // Otherwise, check for acceptance conditions common to all + // outgoing transitions, and assume we have already seen these and + // start on the associated level. + if (s.second == 0) + { + bdd acc = outgoing.common_acc(s.first); + if (use_cust_acc_orders) + s.second = orders.next_level(m.initial(), s.second, acc); + else + while (s.second < order.size() && bdd_implies(order[s.second], acc)) + { + ++s.second; + if (!skip_levels) + break; + } + // There is not accepting level for TBA, let reuse level 0. + if (!want_sba && s.second == order.size()) + s.second = 0; + } + + ds2num[s] = res->new_state(); + todo.push_back(s); + + // If use_lvl_cache is on insert initial state to level cache + // Level cache stores first encountered level for each state. + // When entering an SCC first the lvl_cache is checked. + // If such state exists level from chache is used. + // If not, a new level (starting with 0) is computed. + if (use_lvl_cache) + lvl_cache[s.first] = s.second; + + 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 (want_sba && is_acc) + slevel = 0; + + // Check SCC for state s + int s_scc = -1; + if (use_scc) + s_scc = m.scc_of_state(s.first); + + for (auto i: a->succ(s.first)) + { + degen_state d(uniq(i->current_state()), 0); + + // Check whether the target SCC is accepting + bool is_scc_acc; + int scc; + if (use_scc) + { + scc = m.scc_of_state(d.first); + is_scc_acc = m.accepting(scc); + } + else + { + // If we have no SCC information, treat all SCCs as + // accepting. + scc = -1; + is_scc_acc = true; + } + + // 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 (want_sba && 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 state + // 2, depending on whether we reach it using 1=>2 + // or from 2->2. If this example was not clear, + // 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 (bdd_implies(order[prev], common)) + { + bdd u = outgoing.union_acc(d.first); + if (!bdd_implies(order[prev], u)) + 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} + // } + if (is_scc_acc) + { + // If lvl_cache is used and switching SCCs, use level + // from cache + if (use_lvl_cache && s_scc != scc + && lvl_cache.find(d.first) != lvl_cache.end()) + { + d.second = lvl_cache[d.first]; + } + else + { + // Complete (or replace) the acceptance sets of + // this link with the acceptance sets common to + // all transitions leaving the destination state. + if (s_scc == scc) + acc |= otheracc; + else + acc = otheracc; + + // If use_z_lvl is on, start with level zero 0 when + // swhitching SCCs + unsigned next = (!use_z_lvl || s_scc == scc) ? slevel : 0; + + // If using custom acc orders, get next level + // for this scc + if (use_cust_acc_orders) + { + d.second = orders.next_level(scc, next, acc); + } + // Else compute level according the global acc order + else + { + // As a heuristic, if we enter the SCC on a + // state that has at least one accepting + // self-loop, start the degeneralization on + // the accepting level. + if (s_scc != scc && acc_loop.check(d.first)) + { + d.second = order.size(); + } + else + { + // Consider both the current acceptance + // sets, and the acceptance sets common to + // the outgoing transitions of the + // destination state. But don't do + // that if the state is accepting and we + // are not skipping levels. + if (skip_levels || !is_acc) + while (next < order.size() + && bdd_implies(order[next], acc)) + { + ++next; + if (!skip_levels) + break; + } + d.second = next; + } + } + } + } + + // In case we are building a TBA is_acc has to be + // set differently for each transition, and + // we do not need to stay use final level. + if (!want_sba) + { + is_acc = d.second == order.size(); + if (is_acc) // The transition is accepting + { + d.second = 0; // Make it go to the first level. + // Skip levels as much as possible. + if (acc != allacc && !skip_levels) + { + if (use_cust_acc_orders) + { + d.second = orders.next_level(scc, d.second, acc); + } + else + { + while (d.second < order.size() && + bdd_implies(order[d.second], acc)) + ++d.second; + } + } + } + } + + // 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 = res->new_state(); + ds2num[d] = dest; + todo.push_back(d); + // Insert new state to cache + + if (use_lvl_cache) + { + auto res = lvl_cache.emplace(d.first, d.second); + + if (!res.second) + { + if (use_lvl_cache == 3) + res.first->second = + std::max(res.first->second, d.second); + else if (use_lvl_cache == 2) + res.first->second = + std::min(res.first->second, d.second); + } + } + } + + unsigned& t = tr_cache[dest * 2 + is_acc]; + + if (t == 0) + { + // Actually create the transition. 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.) + bdd acc = bddfalse; + if (is_acc) + acc = degen_acc; + t = res->new_transition(src, dest, + i->current_condition(), acc); + } + else + { + res->trans_data(t).cond |= i->current_condition(); + } + } + tr_cache.clear(); + } + +#ifdef DEGEN_DEBUG + std::vector::iterator i; + std::cout << "Orig. order: \t"; + for (i = order.begin(); i != order.end(); i++) + { + bdd_print_acc(std::cout, dict, *i); + std::cout << ", "; + } + std::cout << std::endl; + orders.print(dict); +#endif + + res->merge_transitions(); + return res; + } } tgba_digraph* degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders, int use_lvl_cache, bool skip_levels) { - bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl; + return degeneralize_aux(a, use_z_lvl, use_cust_acc_orders, + use_lvl_cache, skip_levels); + } - bdd_dict* dict = a->get_dict(); - - // The result automaton is an SBA. - auto res = new tgba_digraph(dict); - res->set_bprop(tgba_digraph::SBA); - - // We use the same BDD variables as the input, except for the - // acceptance. - dict->register_all_variables_of(a, res); - dict->unregister_all_typed_variables(bdd_dict::acc, res); - - // 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); - } - } - - // Initialize scc_orders - scc_orders orders(a->all_acceptance_conditions(), skip_levels); - - // Make sure we always use the same pointer for identical states - // from the input automaton. - state_unicity_table uniq; - - // Accepting loop checker, for some heuristics. - has_acc_loop acc_loop(a, uniq); - - // These maps make it possible to convert degen_state to number - // and vice-versa. - ds2num_map ds2num; - - // This map is used to find transitions that go to the same - // destination with the same acceptance. The integer key is - // (dest*2+acc) where dest is the destination state number, and - // acc is 1 iff the transition is accepting. The source - // is always that of the current iteration. - typedef std::map tr_cache_t; - tr_cache_t tr_cache; - - // State level cache - typedef std::map lvl_cache_t; - lvl_cache_t lvl_cache; - - // Compute SCCs in order to use any optimization. - scc_map m(a); - if (use_scc) - m.build_map(); - - // Cache for common outgoing acceptances. - outgoing_acc outgoing(a, use_scc ? &m : 0); - - queue_t todo; - - const state* s0 = uniq(a->get_init_state()); - degen_state s(s0, 0); - - // As an heuristic, if the initial state at least one accepting - // self-loop, start the degeneralization on the accepting level. - if (acc_loop.check(s0)) - s.second = order.size(); - // Otherwise, check for acceptance conditions common to all - // outgoing transitions, and assume we have already seen these and - // start on the associated level. - if (s.second == 0) - { - bdd acc = outgoing.common_acc(s.first); - if (use_cust_acc_orders) - s.second = orders.next_level(m.initial(), s.second, acc); - else - while (s.second < order.size() && bdd_implies(order[s.second], acc)) - { - ++s.second; - if (!skip_levels) - break; - } - } - - ds2num[s] = res->new_state(); - todo.push_back(s); - - // If use_lvl_cache is on insert initial state to level cache - // Level cache stores first encountered level for each state. - // When entering an SCC first the lvl_cache is checked. - // If such state exists level from chache is used. - // If not, a new level (starting with 0) is computed. - if (use_lvl_cache) - lvl_cache[s.first] = s.second; - - 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; - - // Check SCC for state s - int s_scc = -1; - if (use_scc) - s_scc = m.scc_of_state(s.first); - - for (auto i: a->succ(s.first)) - { - degen_state d(uniq(i->current_state()), 0); - -#ifdef DEGEN_DEBUG - if (names.find(d.first) == names.end()) - names[d.first] = uniq.size(); -#endif - // Check whether the target SCC is accepting - bool is_scc_acc; - int scc; - if (use_scc) - { - scc = m.scc_of_state(d.first); - is_scc_acc = m.accepting(scc); - } - else - { - // If we have no SCC information, treat all SCCs as - // accepting. - scc = -1; - is_scc_acc = true; - } - - // 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 state 2, depending on whether we - // reach it using 1=>2 or from 2->2. If this - // example was not clear, uncomment the 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 (bdd_implies(order[prev], common)) - { - bdd u = outgoing.union_acc(d.first); - if (!bdd_implies(order[prev], u)) - 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} - // } - if (is_scc_acc) - { - // If lvl_cache is used and switching SCCs, use level - // from cache - if (use_lvl_cache && s_scc != scc - && lvl_cache.find(d.first) != lvl_cache.end()) - { - d.second = lvl_cache[d.first]; - } - else - { - // Complete (or replace) the acceptance sets of - // this link with the acceptance sets common to - // all transitions leaving the destination state. - if (s_scc == scc) - acc |= otheracc; - else - acc = otheracc; - - // If use_z_lvl is on, start with level zero 0 when - // swhitching SCCs - unsigned next = (!use_z_lvl || s_scc == scc) ? slevel : 0; - - // If using custom acc orders, get next level for this scc - if (use_cust_acc_orders) - { - d.second = orders.next_level(scc, next, acc); - } - // Else compute level according the global acc order - else - { - // As a heuristic, if we enter the SCC on a - // state that has at least one accepting - // self-loop, start the degeneralization on - // the accepting level. - if (s_scc != scc && acc_loop.check(d.first)) - { - d.second = order.size(); - } - else - { - // Consider both the current acceptance - // sets, and the acceptance sets common to - // the outgoing transitions of the - // destination state. But don't do - // that if the state is accepting and we - // are not skipping levels. - if (skip_levels || !is_acc) - while (next < order.size() - && bdd_implies(order[next], acc)) - { - ++next; - if (!skip_levels) - break; - } - 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 = res->new_state(); - ds2num[d] = dest; - todo.push_back(d); - // Insert new state to cache - - if (use_lvl_cache) - { - auto res = lvl_cache.emplace(d.first, d.second); - - if (!res.second) - { - if (use_lvl_cache == 3) - res.first->second = - std::max(res.first->second, d.second); - else if (use_lvl_cache == 2) - res.first->second = - std::min(res.first->second, d.second); - } - } - } - - unsigned& t = tr_cache[dest * 2 + is_acc]; - - if (t == 0) - { - // Actually create the transition. 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.) - bdd acc = bddfalse; - if (is_acc) - acc = degen_acc; - t = res->new_transition(src, dest, - i->current_condition(), acc); - } - else - { - res->trans_data(t).cond |= i->current_condition(); - } - } - tr_cache.clear(); - } - -#ifdef DEGEN_DEBUG - std::vector::iterator i; - std::cout << "Orig. order: \t"; - for (i = order.begin(); i != order.end(); i++) - { - bdd_print_acc(std::cout, dict, *i); - std::cout << ", "; - } - std::cout << std::endl; - orders.print(dict); -#endif - - res->merge_transitions(); - return res; + tgba_digraph* + degeneralize_tba(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders, + int use_lvl_cache, bool skip_levels) + { + return degeneralize_aux(a, use_z_lvl, use_cust_acc_orders, + use_lvl_cache, skip_levels); } } diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh index 2255c4112..4774330fc 100644 --- a/src/tgbaalgos/degen.hh +++ b/src/tgbaalgos/degen.hh @@ -45,12 +45,21 @@ namespace spot /// Any of these three options will cause the SCCs of the automaton /// \a a to be computed prior to its actual degeneralization. /// - /// \see tgba_tba_proxy + /// The degeneralize_tba() variant produce a degeneralized automaton + /// with transition-based acceptance. + /// \@{ SPOT_API tgba_digraph* degeneralize(const tgba* a, bool use_z_lvl = true, bool use_cust_acc_orders = false, int use_lvl_cache = 1, bool skip_levels = true); + + SPOT_API tgba_digraph* + degeneralize_tba(const tgba* a, bool use_z_lvl = true, + bool use_cust_acc_orders = false, + int use_lvl_cache = 1, + bool skip_levels = true); + /// \@} } diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 99b3f9c83..80ab3e066 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -37,7 +37,6 @@ #include "misc/hash.hh" #include "misc/bddlt.hh" #include "tgba/tgbaproduct.hh" -#include "tgba/tgbatba.hh" #include "tgba/wdbacomp.hh" #include "tgbaalgos/powerset.hh" #include "tgbaalgos/gtec/gtec.hh" diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 3a81338f7..6b320c4a4 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -23,9 +23,9 @@ #include #include #include "bdd.h" -#include "tgba/tgbagraph.hh" #include "neverclaim.hh" #include "tgba/bddprint.hh" +#include "tgba/tgbagraph.hh" #include "reachiter.hh" #include "ltlvisit/tostring.hh" #include "tgba/formula2bdd.hh" diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh index 4c3d1ab57..b31b78c55 100644 --- a/src/tgbaalgos/neverclaim.hh +++ b/src/tgbaalgos/neverclaim.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -25,10 +25,11 @@ #include #include "ltlast/formula.hh" -#include "tgba/tgbatba.hh" namespace spot { + class tgba; + /// \ingroup tgba_io /// \brief Print reachable states in Spin never claim format. /// diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index d8fe0a842..1ae46dd2f 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -28,7 +28,6 @@ #include "priv/countstates.hh" #include "powerset.hh" #include "isdet.hh" -#include "tgba/tgbatba.hh" #include "dtbasat.hh" #include "dtgbasat.hh" #include "complete.hh" @@ -273,14 +272,14 @@ namespace spot // If we don't have a DBA, attempt tba-determinization if requested. if (tba_determinisation_ && !dba) { - const tgba* tmpd = 0; + const tgba_digraph* tmpd = 0; if (PREF_ == Deterministic && f && f->is_syntactic_recurrence() && sim->number_of_acceptance_conditions() > 1) - tmpd = new tgba_tba_proxy(sim); + tmpd = degeneralize_tba(sim); - const tgba* in = tmpd ? tmpd : sim; + auto in = tmpd ? tmpd : sim; // These thresholds are arbitrary. // @@ -293,7 +292,7 @@ namespace spot // are 8 times bigger, with no more that 2^15 cycle per SCC. // The cycle threshold is the most important limit here. You // may up it if you want to try producing larger automata. - const tgba* tmp = + auto tmp = tba_determinize_check(in, (PREF_ == Small) ? 2 : 8, 1 << ((PREF_ == Small) ? 13 : 15), @@ -341,8 +340,8 @@ namespace spot // sure it is at least 1. target_acc = original_acc > 0 ? original_acc : 1; - const tgba* in = 0; - const tgba* to_free = 0; + const tgba_digraph* in = 0; + const tgba_digraph* to_free = 0; if (target_acc == 1) { // If we are seeking a minimal DBA with unknown number of @@ -351,7 +350,7 @@ namespace spot if (state_based_) to_free = in = degeneralize(dba); else if (dba->number_of_acceptance_conditions() != 1) - to_free = in = new tgba_tba_proxy(dba); + to_free = in = degeneralize_tba(dba); else in = dba; } diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 61a6042bf..44f8c4677 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -32,7 +32,6 @@ #include "tgbaalgos/stats.hh" #include "tgbaalgos/emptiness_stats.hh" #include "tgbaalgos/degen.hh" -#include "tgba/tgbatba.hh" #include "tgba/tgbasafracomplement.hh" #include "tgba/tgbakvcomplement.hh" diff --git a/src/tgbatest/degenid.test b/src/tgbatest/degenid.test index b1fb3c00c..8f549ac4c 100755 --- a/src/tgbatest/degenid.test +++ b/src/tgbatest/degenid.test @@ -1,6 +1,7 @@ #!/bin/sh -# Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# -*- coding: utf-8 -*- +# Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -24,7 +25,7 @@ set -e # Make sure degeneralization is idempotent for f in 'FGa|GFb' 'GFa & GFb & GFc' 'GF(a->FGb)&GF(c->FGd)'; do - for opt in -DS -D; do + for opt in -DS -DT; do ../ltl2tgba $opt -b "$f" > autX.spot ../ltl2tgba -X -kt autX.spot > base.size cat base.size diff --git a/src/tgbatest/det.test b/src/tgbatest/det.test index 3c6e92634..2da949802 100755 --- a/src/tgbatest/det.test +++ b/src/tgbatest/det.test @@ -24,9 +24,9 @@ set -e ltl2tgba=../../bin/ltl2tgba cat >formulas <<'EOF' -1,14,X((a M F((!b & !c) | (b & c))) W (G!c U b)) +1,13,X((a M F((!b & !c) | (b & c))) W (G!c U b)) 1,5,X(((a & b) R (!a U !c)) R b) -1,10,XXG(Fa U Xb) +1,9,XXG(Fa U Xb) 1,5,(!a M !b) W F!c 1,3,(b & Fa & GFc) R a 1,2,(a R (b W a)) W G(!a M (b | c)) diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index c7105f853..7cbbc443e 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -1,9 +1,10 @@ #!/bin/sh +# -*- coding: utf-8 -*- # Copyright (C) 2008, 2009, 2010, 2014 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# 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. +# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +# Université Pierre et Marie Curie. # # This file is part of Spot, a model checking library. # @@ -34,13 +35,13 @@ expect_ce_do() expect_ce() { expect_ce_do -CR -e -taa "$1" - expect_ce_do -CR -e -taa -D "$1" + expect_ce_do -CR -e -taa -DT "$1" expect_ce_do -CR -e -f "$1" - expect_ce_do -CR -e -f -D "$1" + expect_ce_do -CR -e -f -DT "$1" expect_ce_do -CR -e'Cou99(shy)' -taa "$1" - expect_ce_do -CR -e'Cou99(shy)' -taa -D "$1" + expect_ce_do -CR -e'Cou99(shy)' -taa -DT "$1" expect_ce_do -CR -e'Cou99(shy)' -f "$1" - expect_ce_do -CR -e'Cou99(shy)' -f -D "$1" + expect_ce_do -CR -e'Cou99(shy)' -f -DT "$1" expect_ce_do -CR -eCVWY90 -taa "$1" expect_ce_do -CR -eCVWY90 -f "$1" run 0 ../ltl2tgba -CR -e'CVWY90(bsh=10M)' -taa "$1" @@ -61,13 +62,13 @@ expect_ce() expect_no() { run 0 ../ltl2tgba -CR -E -taa "$1" - run 0 ../ltl2tgba -CR -E -taa -D "$1" + run 0 ../ltl2tgba -CR -E -taa -DT "$1" run 0 ../ltl2tgba -CR -E -f "$1" - run 0 ../ltl2tgba -CR -E -f -D "$1" + run 0 ../ltl2tgba -CR -E -f -DT "$1" run 0 ../ltl2tgba -CR -E'Cou99(shy)' -taa "$1" - run 0 ../ltl2tgba -CR -E'Cou99(shy)' -taa -D "$1" + run 0 ../ltl2tgba -CR -E'Cou99(shy)' -taa -DT "$1" run 0 ../ltl2tgba -CR -E'Cou99(shy)' -f "$1" - run 0 ../ltl2tgba -CR -E'Cou99(shy)' -f -D "$1" + run 0 ../ltl2tgba -CR -E'Cou99(shy)' -f -DT "$1" run 0 ../ltl2tgba -CR -ECVWY90 -taa "$1" run 0 ../ltl2tgba -CR -ECVWY90 -f "$1" run 0 ../ltl2tgba -CR -E'CVWY90(bsh=10M)' -taa "$1" @@ -88,11 +89,11 @@ expect_ce 'a' 1 expect_ce 'a U b' 1 expect_ce 'X a' 1 expect_ce 'a & b & c' 1 -expect_ce 'a | b | (c U (d & (g U (h ^ i))))' 2 +expect_ce 'a | b | (c U (d & (g U (h ^ i))))' 1 expect_ce 'Xa & (b U !a) & (b U !a)' 1 expect_ce 'Fa & Xb & GFc & Gd' 1 expect_ce 'Fa & Xa & GFc & Gc' 2 expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' 1 -expect_ce '!((FF a) <=> (F x))' 3 +expect_ce '!((FF a) <=> (F x))' 2 expect_no 'Xa && (!a U b) && !b && X!b' 2 expect_no '(a U !b) && Gb' 2 diff --git a/src/tgbatest/emptchke.test b/src/tgbatest/emptchke.test index 700028562..277afe7e9 100755 --- a/src/tgbatest/emptchke.test +++ b/src/tgbatest/emptchke.test @@ -1,9 +1,10 @@ #!/bin/sh -# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# -*- coding: utf-8 -*- +# Copyright (C) 2009, 2010, 2014 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. +# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +# Université Pierre et Marie Curie. # # This file is part of Spot, a model checking library. # @@ -28,9 +29,9 @@ set -e expect_ce() { run 0 ../ltl2tgba -CR -e -X "$1" - run 0 ../ltl2tgba -CR -e -D -X "$1" + run 0 ../ltl2tgba -CR -e -DT -X "$1" run 0 ../ltl2tgba -CR -e'Cou99(shy)' -X "$1" - run 0 ../ltl2tgba -CR -e'Cou99(shy)' -D -X "$1" + run 0 ../ltl2tgba -CR -e'Cou99(shy)' -DT -X "$1" run 0 ../ltl2tgba -CR -eCVWY90 -X "$1" run 0 ../ltl2tgba -CR -eGV04 -X "$1" run 0 ../ltl2tgba -CR -eSE05 -X "$1" diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 8ee42b88f..c1c88ebe8 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -36,7 +36,6 @@ #include "tgbaalgos/save.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" -#include "tgba/tgbatba.hh" #include "tgba/tgbasgba.hh" #include "tgbaalgos/degen.hh" #include "tgba/tgbaproduct.hh" @@ -190,7 +189,7 @@ syntax(char* prog) << std::endl << " -lS move generalized acceptance conditions to states " << "(SGBA)" << std::endl - << " -D degeneralize the automaton as a TBA" << std::endl + << " -DT degeneralize the automaton as a TBA" << std::endl << " -DS degeneralize the automaton as an SBA" << std::endl << " (append z/Z, o/O, l/L: to turn on/off options " << "(default: zol)\n " @@ -451,15 +450,18 @@ main(int argc, char** argv) } else if (!strcmp(argv[formula_index], "-D")) { - degeneralize_opt = DegenTBA; + std::cerr << "-D was renamed to -DT\n"; + abort(); } else if (!strcmp(argv[formula_index], "-DC")) { opt_dtgbacomp = true; } - else if (!strncmp(argv[formula_index], "-DS", 3)) + else if (!strncmp(argv[formula_index], "-DS", 3) + || !strncmp(argv[formula_index], "-DT", 3)) { - degeneralize_opt = DegenSBA; + degeneralize_opt = + argv[formula_index][2] == 'S' ? DegenSBA : DegenTBA; const char* p = argv[formula_index] + 3; while (*p) { @@ -1354,7 +1356,10 @@ main(int argc, char** argv) { if (degeneralize_opt == DegenTBA) { - degeneralized = a = new spot::tgba_tba_proxy(a); + degeneralized = a = spot::degeneralize_tba(a, + degen_reset, + degen_order, + degen_cache); } else if (degeneralize_opt == DegenSBA) { @@ -1604,7 +1609,13 @@ main(int argc, char** argv) degeneralize_opt = DegenTBA; if (degeneralize_opt == DegenTBA) { - product_degeneralized = a = new spot::tgba_tba_proxy(a); + tm.start("degeneralize product"); + product_degeneralized = a = + spot::degeneralize_tba(a, + degen_reset, + degen_order, + degen_cache); + tm.stop("degeneralize product"); } else if (degeneralize_opt == DegenSBA) { diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 880bf6f13..ce0e62159 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -119,7 +119,7 @@ run 0 ../ltl2tgba -e -R3 '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))' # Make sure 'a U (b U c)' has 3 states and 6 transitions, # before and after degeneralization. -for opt in '' -D -DS; do +for opt in '' -DT -DS; do ../ltl2tgba -ks -f -R3 $opt 'a U (b U c)' > stdout grep 'transitions: 6$' stdout grep 'states: 3$' stdout @@ -127,7 +127,7 @@ done # Make sure '!(Ga U b)' has 3 states and 6 transitions, # before and after degeneralization. -for opt in '' -D -DS; do +for opt in '' -DT -DS; do ../ltl2tgba -kt -f -R3 $opt '!(Ga U b)' > stdout grep 'sub trans.: 11$' stdout grep 'transitions: 6$' stdout @@ -136,7 +136,7 @@ done # Make sure 'Ga U b' has 4 states and 6 transitions, # before and after degeneralization. -for opt in '' -D -DS; do +for opt in '' -DT -DS; do ../ltl2tgba -kt -f -R3 $opt 'Ga U b' > stdout grep 'sub trans.: 12$' stdout grep 'transitions: 6$' stdout @@ -146,7 +146,7 @@ done # Make sure '(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))' # has 6 states and 15 transitions, before and after degeneralization. f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))' -for opt in '' -D -DS; do +for opt in '' -DT -DS; do ../ltl2tgba -ks -f -R3 $opt "$f" > stdout grep 'transitions: 15$' stdout grep 'states: 6$' stdout diff --git a/src/tgbatest/ltlcounter.test b/src/tgbatest/ltlcounter.test index 9082aeae9..eea3d8318 100755 --- a/src/tgbatest/ltlcounter.test +++ b/src/tgbatest/ltlcounter.test @@ -1,7 +1,7 @@ #!/bin/sh - -# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -# Développement de l'EPITA (LRDE) +# -*- coding: utf-8 -*- +# Copyright (C) 2009, 2010, 2011, 2012, 2014 Laboratoire de Recherche +# et Développement de l'EPITA (LRDE) # # This file is part of Spot, a model checking library. # @@ -33,7 +33,7 @@ check_formula() # First, check the satisfiability of the formula with Spot $run ../ltl2tgba -CR -e -x -f "$1" >/dev/null # Also check the satisfiability of the degeneralized formula - $run ../ltl2tgba -CR -e -D -x -f "$1" >/dev/null + $run ../ltl2tgba -CR -e -DT -x -f "$1" >/dev/null $run ../ltl2tgba -CR -e -DS -x -f "$1" >/dev/null } diff --git a/src/tgbatest/ltlcross.test b/src/tgbatest/ltlcross.test index 7af064457..ce801ac5a 100755 --- a/src/tgbatest/ltlcross.test +++ b/src/tgbatest/ltlcross.test @@ -31,16 +31,16 @@ ltl2tgba=../ltl2tgba "$ltl2tgba -t -f -R3 %f > %T" \ "$ltl2tgba -t -f -R3 -Rm %f > %T" \ "$ltl2tgba -t -f -R3 -RM %f > %T" \ - "$ltl2tgba -t -f -D %f > %T" \ - "$ltl2tgba -t -f -D %f > %T" \ + "$ltl2tgba -t -f -DT %f > %T" \ + "$ltl2tgba -t -f -DS %f > %T" \ "$ltl2tgba -t -f -r4 -R3 -RDS %f > %T" \ "$ltl2tgba -t -f -r4 -R3 -RRS %f > %T" \ "$ltl2tgba -t -f -r4 -R3 -RIS %f > %T" \ "$ltl2tgba -t -f -r4 -R3 -RDS -DS %f > %T" \ "$ltl2tgba -t -f -x -p %f > %T" \ "$ltl2tgba -t -f -x -p -L %f > %T" \ - "$ltl2tgba -t -f -x -p -D %f > %T" \ - "$ltl2tgba -t -f -x -p -L -D %f > %T" \ + "$ltl2tgba -t -f -x -p -DT %f > %T" \ + "$ltl2tgba -t -f -x -p -L -DT %f > %T" \ "$ltl2tgba -t -taa -r4 %f > %T" \ "$ltl2tgba -t -taa -r4 -c %f > %T" \ "$ltl2tgba -t -taa -r4 -R3 -RDS %f > %T" diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 79909e100..7f8de3055 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -45,7 +45,7 @@ #include "tgbaparse/public.hh" #include "misc/random.hh" #include "misc/optionmap.hh" -#include "tgba/tgbatba.hh" +#include "tgbaalgos/degen.hh" #include "tgba/tgbaproduct.hh" #include "misc/timer.hh" @@ -928,7 +928,7 @@ main(int argc, char** argv) { spot::tgba* degen = 0; if (opt_degen && real_n_acc > 1) - degen = new spot::tgba_tba_proxy(a); + degen = degeneralize_tba(a); int n_alg = ec_algos.size(); int n_ec = 0; diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 27b80da4e..8e75c582a 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -1,9 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- - # Copyright (C) 2009, 2010, 2011, 2012, 2014 Laboratoire de Recherche # et Développement de l'Epita (LRDE). - # Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire # d'Informatique de Paris 6 (LIP6), département Systèmes Répartis # Coopératifs (SRC), Université Pierre et Marie Curie. @@ -124,7 +122,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), degeneralized" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -t -D'" + Parameters = "--spot '../ltl2tgba -F -f -t -DT'" Enabled = yes } @@ -237,7 +235,7 @@ Algorithm { Name = "Spot (Couvreur -- FM post_branch + exprop), degeneralized" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -p -x -t -D'" + Parameters = "--spot '../ltl2tgba -F -f -p -x -t -DT'" Enabled = yes } @@ -245,8 +243,8 @@ Algorithm { Name = "Spot (Couvreur -- FM post_branch + exprop + flapprox), degeneralized" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -p -x -t -L -D'" - Enabled = yes + Parameters = "--spot '../ltl2tgba -F -f -p -x -t -L -DT'" + ENABLED = yes } Algorithm diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 69d38cc31..b203fac1d 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -79,7 +79,6 @@ namespace std { #include "tgba/tgba.hh" #include "tgba/taatgba.hh" #include "tgba/tgbaproduct.hh" -#include "tgba/tgbatba.hh" #include "tgbaalgos/dottydec.hh" #include "tgbaalgos/dotty.hh" @@ -201,6 +200,7 @@ using namespace spot; %feature("new") spot::cosimulation; %feature("new") spot::iterated_simulations; %feature("new") spot::degeneralize; +%feature("new") spot::degeneralize_tba; %feature("new") spot::tgba_parse; %feature("new") spot::tgba_to_ta; %feature("new") spot::tgba_to_tgta; @@ -219,7 +219,6 @@ using namespace spot; %include "tgba/tgba.hh" %include "tgba/taatgba.hh" %include "tgba/tgbaproduct.hh" -%include "tgba/tgbatba.hh" // We won't parse tgba_digraph, so just pretend it is a subclass of tgba. %nodefaultctor spot::tgba_digraph; diff --git a/wrap/python/tests/ltl2tgba.py b/wrap/python/tests/ltl2tgba.py index 8bc9e4248..c7bf1d9dd 100755 --- a/wrap/python/tests/ltl2tgba.py +++ b/wrap/python/tests/ltl2tgba.py @@ -99,7 +99,7 @@ if f: degeneralized = None if degeneralize_opt: - a = degeneralized = spot.tgba_tba_proxy(a) + a = degeneralized = spot.degeneralize(a) if output == 0: spot.dotty_reachable(cout, a)