diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 1d762a429..f9eca4358 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -48,7 +48,6 @@ tgba_HEADERS = \ tgbakvcomplement.hh \ tgbascc.hh \ tgbaproduct.hh \ - tgbareduc.hh \ tgbasgba.hh \ tgbasafracomplement.hh \ tgbatba.hh \ @@ -72,7 +71,6 @@ libtgba_la_SOURCES = \ tgbaexplicit.cc \ tgbakvcomplement.cc \ tgbaproduct.cc \ - tgbareduc.cc \ tgbasafracomplement.cc \ tgbascc.cc \ tgbasgba.cc \ diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc deleted file mode 100644 index 4ef9b6894..000000000 --- a/src/tgba/tgbareduc.cc +++ /dev/null @@ -1,443 +0,0 @@ -// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE). -// Copyright (C) 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 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 "tgbareduc.hh" -#include - -namespace spot -{ - namespace - { - typedef std::pair pair_state_iter; - } - - tgba_reduc::tgba_reduc(const tgba* a) - : tgba_explicit_string(a->get_dict()), - tgba_reachable_iterator_breadth_first(a) - { - dict_->register_all_variables_of(a, this); - - run(); - all_acceptance_conditions_ = a->all_acceptance_conditions(); - all_acceptance_conditions_computed_ = true; - } - - tgba_reduc::~tgba_reduc() - { - sp_map::iterator i; - for (i = state_predecessor_map_.begin(); - i!= state_predecessor_map_.end(); ++i) - { - delete i->second; - } - } - - void - tgba_reduc::quotient_state(direct_simulation_relation* rel) - { - // Remember that for each state couple - // (*i)->second simulate (*i)->first. - - for (direct_simulation_relation::iterator i = rel->begin(); - i != rel->end(); ++i) - { - - // All state simulate himself. - if (((*i)->first)->compare((*i)->second) == 0) - continue; - - // We check if the two state are co-simulate. - bool recip = false; - for (direct_simulation_relation::iterator j = i; - j != rel->end(); ++j) - if ((((*i)->first)->compare((*j)->second) == 0) && - (((*j)->first)->compare((*i)->second) == 0)) - recip = true; - - if (recip) - //this->redirect_transition((*i)->first, (*i)->second); - this->merge_state((*i)->first, (*i)->second); - } - - this->merge_transitions(); - } - - void - tgba_reduc::quotient_state(delayed_simulation_relation* rel) - { - if (nb_set_acc_cond() > 1) - return; - - //this->quotient_state(rel); - - for (delayed_simulation_relation::iterator i = rel->begin(); - i != rel->end(); ++i) - { - - // All state simulate himself. - if (((*i)->first)->compare((*i)->second) == 0) - continue; - - // We check if the two state are co-simulate. - bool recip = false; - for (delayed_simulation_relation::iterator j = i; - j != rel->end(); ++j) - if ((((*i)->first)->compare((*j)->second) == 0) && - (((*j)->first)->compare((*i)->second) == 0)) - recip = true; - - if (recip) - this->merge_state((*i)->first, (*i)->second); - } - - this->merge_transitions(); - } - - void - tgba_reduc::delete_transitions(simulation_relation* rel) - { - for (simulation_relation::iterator i = rel->begin(); - i != rel->end(); ++i) - { - if (((*i)->first)->compare((*i)->second) == 0) - continue; - this->redirect_transition((*i)->first, (*i)->second); - } - this->merge_transitions(); - } - - //////////////////////////////////////////// - // for build tgba_reduc - - void - tgba_reduc::process_state(const spot::state* s, int, tgba_succ_iterator* si) - { - spot::state* init = aut_->get_init_state(); - if (init->compare(s) == 0) - this->set_init_state(aut_->format_state(s)); - init->destroy(); - - transition* t; - for (si->first(); !si->done(); si->next()) - { - init = si->current_state(); - t = this->create_transition(s, init); - this->add_conditions(t, si->current_condition()); - this->add_acceptance_conditions(t, si->current_acceptance_conditions()); - init->destroy(); - } - } - - tgba_explicit_string::transition* - tgba_reduc::create_transition(const spot::state* source, - const spot::state* dest) - { - const std::string ss = aut_->format_state(source); - const std::string sd = aut_->format_state(dest); - - state_explicit_string* s = tgba_explicit_string::add_state(ss); - state_explicit_string* d = tgba_explicit_string::add_state(sd); - - transition t; - t.dest = d; - - sp_map::iterator i = state_predecessor_map_.find(d); - if (i == state_predecessor_map_.end()) - { - std::list* pred = new std::list; - pred->push_back(s); - state_predecessor_map_[d] = pred; - } - else - { - (i->second)->push_back(s); - } - - t.condition = bddtrue; - t.acceptance_conditions = bddfalse; - state_explicit_string::transitions_t::iterator is - = s->successors.insert(s->successors.end(), t); - return &*is; - } - - /////////////////////////////////////////////////// - - void - tgba_reduc::redirect_transition(const spot::state* s, - const spot::state* simul) - { - bool belong = false; - bdd cond_simul; - bdd acc_simul; - std::list ltmp; - const state_explicit_string* s1 = - &(ls_[tgba_explicit_string::format_state(s)]); - const state_explicit_string* s2 = - &(ls_[tgba_explicit_string::format_state(simul)]); - - sp_map::iterator i = state_predecessor_map_.find(s1); - if (i == state_predecessor_map_.end()) // 0 predecessor - return; - - // for all predecessor of s. - for (std::list::iterator p = (i->second)->begin(); - p != (i->second)->end(); ++p) - { - // We check if simul belong to the successor of p, - // as s belong too. - for (state_explicit_string::transitions_t::iterator - j = (*p)->successors.begin(); - j != (*p)->successors.end(); ++j) - if (j->dest == s2) // simul belong to the successor of p. - { - belong = true; - cond_simul = j->condition; - acc_simul = j->acceptance_conditions; - break; - } - - // If not, we check for another predecessor of s. - if (!belong) - continue; - - // for all successor of p, a predecessor of s and simul. - for (state_explicit_string::transitions_t::iterator - j = (*p)->successors.begin(); - j != (*p)->successors.end(); ++j) - { - // if the transition lead to s. - if ((j->dest == s1) && - // if the label of the transition whose lead to s implies - // this leading to simul. - (((!j->condition | cond_simul) == bddtrue) && - ((!j->acceptance_conditions) | acc_simul) == bddtrue)) - { - // We can redirect transition leading to s on simul. - j->dest = const_cast(s2); - - // We memorize that we have to remove p - // of the predecessor of s. - ltmp.push_back(*p); - } - } - belong = false; - } - - // We remove all the predecessor of s than we have memorized. - std::list::iterator k; - for (k = ltmp.begin(); - k != ltmp.end(); ++k) - this->remove_predecessor_state(i->first, *k); - } - - void - tgba_reduc::remove_predecessor_state(const state* s, const state* p) - { - sp_map::iterator i = state_predecessor_map_.find(s); - if (i == state_predecessor_map_.end()) // 0 predecessor - return; - - // for all predecessor of s we remove p. - for (std::list::iterator j = (i->second)->begin(); - j != (i->second)->end();) - if (p == *j) - j = (i->second)->erase(j); - else - ++j; - } - - void - tgba_reduc::remove_state(const spot::state* s) - { - // We suppose that the state is not reachable when called by - // merge_state => NO PREDECESSOR. But it can be have some - // predecessor in state_predecessor_map_. - - ls_map::iterator k = - ls_.find(tgba_explicit_string::format_state(s)); - if (k == ls_.end()) // 0 predecessor - return; - - state_explicit_string* st = - &(ls_[tgba_explicit_string::format_state(s)]); - - // for all successor q of s, we remove s of the predecessor of q. - // Note that the initial node can't be removed. - for (state_explicit_string::transitions_t::iterator j = - st->successors.begin(); j != st->successors.end(); ++j) - this->remove_predecessor_state(down_cast - (j->dest), st); - - - sp_map::iterator i = state_predecessor_map_.find(st); - if (i == state_predecessor_map_.end()) // 0 predecessor - return; - - // for all predecessor of s (none when called by merge_state) - for (std::list::iterator p = (i->second)->begin(); - p != (i->second)->end(); ++p) - { - // for all transition of p, a predecessor of s. - for (state_explicit_string::transitions_t::iterator - j = (*p)->successors.begin(); - j != (*p)->successors.end();) - { - if (j->dest == st) - { - // Remove the transition - j = (*p)->successors.erase(j); - ++j; - } - else - ++j; - } - } - - // DESTROY THE STATE !? USELESS - // it will be destroyed when the automaton is deleted - // name_state_map_::iterator = name_state_map_[st]; - // const tgba_explicit::state* st = name_state_map_[this->format_state(s)]; - } - - void - tgba_reduc::merge_state(const spot::state* sim1, const spot::state* sim2) - { - const state_explicit_string* s1 = - &(ls_[tgba_explicit_string::format_state(sim1)]); - const state_explicit_string* s2 = - &(ls_[tgba_explicit_string::format_state(sim2)]); - const state_explicit_string* stmp = s1; - const spot::state* simtmp = sim1; - - // if sim1 is the init state, we remove sim2. - spot::state* init = this->get_init_state(); - if (sim1->compare(init) == 0) - { - s1 = s2; - s2 = stmp; - sim1 = sim2; - sim2 = simtmp; - } - init->destroy(); - - sp_map::iterator i = state_predecessor_map_.find(s1); - if (i == state_predecessor_map_.end()) // 0 predecessor - { - // We can remove s1 safely, without changing the language - // of the automaton. - this->remove_state(sim1); - return; - } - - // for all predecessor of s1, not the initial state, - // we redirect to s2 the transitions that lead to s1. - for (std::list::iterator p = (i->second)->begin(); - p != (i->second)->end(); ++p) - { - // for all successor of p, a predecessor of s1. - for (state_explicit_string::transitions_t::iterator - j = (*p)->successors.begin(); - j != (*p)->successors.end(); ++j) - { - // if the successor was s1... - if (j->dest == s1) - { - // ... make it s2. - j->dest = const_cast(s2); - } - } - } - - // FIXME: The following justification sounds really dubious. - // - // We have to stock on s2 the acceptance condition of the arc - // leaving s1 (possible when the simulation is delayed). Since s2 - // simulates s1, s2 has some labels that imply these of s1, so we - // can put the acceptance conditions on its arcs. - for (state_explicit_string::transitions_t::const_iterator - j = s1->successors.begin(); - j != s1->successors.end(); ++j) - { - transition t; - t.dest = j->dest; - t.condition = j->condition; - t.acceptance_conditions = j->acceptance_conditions; - const_cast(s2)->successors.push_back(t); - } - - // We remove all the predecessor of s1. - (i->second)->clear(); - - // then we can remove s1 safely, without changing the language - // of the automaton. - this->remove_state(sim1); - } - - void - tgba_reduc::merge_state_delayed(const spot::state*, - const spot::state*) - { - // TO DO - } - - int - tgba_reduc::nb_set_acc_cond() const - { - bdd acc, all; - acc = all = this->all_acceptance_conditions(); - int count = 0; - while (all != bddfalse) - { - all -= bdd_satone(all); - ++count; - } - return count; - } - - //////// JUST FOR DEBUG ////////// - - void - tgba_reduc::display_rel_sim(simulation_relation* rel, - std::ostream& os) - { - int n = 0; - simulation_relation::iterator i; - for (i = rel->begin(); i != rel->end(); ++i) - { - if (((*i)->first)->compare((*i)->second) == 0) - continue; - - ++n; - os << "couple " << n - << std::endl - << " " << " [label=\"" - << this->format_state((*i)->first) << "\"]" - << std::endl - << " " << " [label=\"" - << this->format_state((*i)->second) << "\"]" - << std::endl - << std::endl; - } - } - -} diff --git a/src/tgba/tgbareduc.hh b/src/tgba/tgbareduc.hh deleted file mode 100644 index dd53be3ec..000000000 --- a/src/tgba/tgbareduc.hh +++ /dev/null @@ -1,167 +0,0 @@ -// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2004, 2005, 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 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_TGBA_TGBAREDUC_HH -# define SPOT_TGBA_TGBAREDUC_HH - -#include "tgbaexplicit.hh" -#include "tgbaalgos/reachiter.hh" - -#include -#include - -namespace spot -{ - typedef std::pair state_couple; - typedef std::vector simulation_relation; - - /* - typedef std::vector direct_simulation_relation; - typedef std::vector delayed_simulation_relation; - */ - - class direct_simulation_relation: public simulation_relation - { - }; - class delayed_simulation_relation: public simulation_relation - { - }; - - - /// Explicit automata used in reductions. - /// \ingroup tgba_representation - class tgba_reduc: - public tgba_explicit_string, public tgba_reachable_iterator_breadth_first - { - public: - tgba_reduc(const tgba* a); - - ~tgba_reduc(); - - /// Reduce the automata using a relation simulation - /// Do not call this method with a delayed simulation relation. - void quotient_state(direct_simulation_relation* rel); - - /// Build the quotient automata. Call this method - /// when use to a delayed simulation relation. - void quotient_state(delayed_simulation_relation* rel); - - /// \brief Delete some transitions with help of a simulation - /// relation. - void delete_transitions(simulation_relation* rel); - - // For Debug - void display_rel_sim(simulation_relation* rel, std::ostream& os); - void display_scc(std::ostream& os); - - protected: - typedef Sgi::hash_map*, - ptr_hash > sp_map; - sp_map state_predecessor_map_; - - // Interface of tgba_reachable_iterator_breadth_first - void process_state(const spot::state* s, int n, tgba_succ_iterator* si); - - /// Create a transition using two state of a TGBA. - transition* create_transition(const spot::state* source, - const spot::state* dest); - - - /// Remove all the transition from the state q, predecessor - /// of both \a s and \a simul, which can be removed. - void redirect_transition(const spot::state* s, - const spot::state* simul); - - /// Remove p of the predecessor of s. - void remove_predecessor_state(const state* s, const state* p); - - /// Remove all the transition leading to s. - /// s is then unreachable and can be consider as remove. - void remove_state(const spot::state* s); - - /// Redirect all transition leading to s1 to s2. - /// Note that we can do the reverse because - /// s1 and s2 belong to a co-simulate relation. - void merge_state(const spot::state* s1, - const spot::state* s2); - - /// Redirect all transition leading to s1 to s2. - /// Note that we can do the reverse because - /// s1 and s2 belong to a co-simulate relation. - void merge_state_delayed(const spot::state* s1, - const spot::state* s2); - - /// Remove all the scc which are terminal and doesn't - /// contains all the acceptance conditions. - void delete_scc(); - - /// Return true if the scc which contains \a s - /// is an fixed-formula alpha-ball. - /// this is explain in - /// \verbatim - /// @InProceedings{ etessami.00.concur, - /// author = {Kousha Etessami and Gerard J. Holzmann}, - /// title = {Optimizing {B\"u}chi Automata}, - /// booktitle = {Proceedings of the 11th International Conference on - /// Concurrency Theory (Concur'2000)}, - /// pages = {153--167}, - /// year = {2000}, - /// editor = {C. Palamidessi}, - /// volume = {1877}, - /// series = {Lecture Notes in Computer Science}, - /// publisher = {Springer-Verlag} - /// } - /// \endverbatim - // bool is_alpha_ball(const spot::state* s, - // bdd label = bddfalse, - // int n = -1); - - // Return true if we can't reach a state with - // an other value of scc. - bool is_terminal(const spot::state* s, - int n = -1); - - // Return false if the scc contains all the acceptance conditions. - bool is_not_accepting(const spot::state* s, - int n = -1); - - /// If a scc maximal do not contains all the acceptance conditions - /// we can remove all the acceptance conditions in this scc. - void remove_acc(const spot::state* s); - - /// Remove all the state which belong to the same scc that s. - void remove_scc(spot::state* s); - - /// Same as remove_scc but more efficient. - // void remove_scc_depth_first(spot::state* s, int n = -1); - - /// For compute_scc. - void remove_component(const spot::state* from); - - int nb_set_acc_cond() const; - - }; -} - -#endif // SPOT_TGBA_TGBAREDUC_HH diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index d35a24191..696378ae0 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -1,8 +1,9 @@ -## Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## -*- coding: utf-8 -*- +## Copyright (C) 2008, 2009, 2010, 2011, 2012 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. +## 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. ## @@ -99,7 +100,6 @@ libtgbaalgos_la_SOURCES = \ tau03.cc \ tau03opt.cc \ reductgba_sim.cc \ - reductgba_sim_del.cc \ weight.cc libtgbaalgos_la_LIBADD = gtec/libgtec.la diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc index 03f499a58..f99e0993e 100644 --- a/src/tgbaalgos/reductgba_sim.cc +++ b/src/tgbaalgos/reductgba_sim.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -22,633 +22,12 @@ // 02111-1307, USA. #include "reductgba_sim.hh" -#include "tgba/bddprint.hh" #include "sccfilter.hh" +#include "simulation.hh" +#include "dupexp.hh" namespace spot { - /////////////////////////////////////////////////////////////////////// - // spoiler_node - - spoiler_node::spoiler_node(const state* d_node, - const state* s_node, - int num) - { - num_ = num; - sc_ = new state_couple(d_node, s_node); - lnode_succ = new sn_v; - lnode_pred = new sn_v; - not_win = false; - } - - spoiler_node::~spoiler_node() - { - lnode_succ->clear(); - lnode_pred->clear(); - delete lnode_succ; - delete lnode_pred; - delete sc_; - } - - bool - spoiler_node::add_succ(spoiler_node* n) - { - bool exist = false; - for (sn_v::iterator i = lnode_succ->begin(); - i != lnode_succ->end(); ++i) - if ((*i == n) || - ((*i)->compare(n) == true)) - exist = true; - if (exist) - return false; - - lnode_succ->push_back(n); - n->add_pred(this); - return true; - } - - void - spoiler_node::del_succ(spoiler_node* n) - { - for (sn_v::iterator i = lnode_succ->begin(); - i != lnode_succ->end();) - { - if (*i == n) - { - i = lnode_succ->erase(i); - } - else - ++i; - } - } - - void - spoiler_node::add_pred(spoiler_node* n) - { - lnode_pred->push_back(n); - } - - void - spoiler_node::del_pred() - { - for (sn_v::iterator i = lnode_pred->begin(); - i != lnode_pred->end(); ++i) - (*i)->del_succ(this); - } - - bool - spoiler_node::set_win() - { - bool change = not_win; - for (std::vector::iterator i = lnode_succ->begin(); - i != lnode_succ->end(); ++i) - { - not_win |= (*i)->not_win; - } - if (change != not_win) - for (std::vector::iterator i = lnode_pred->begin(); - i != lnode_pred->end(); ++i) - (*i)->set_win(); - - return change != not_win; - } - - std::string - spoiler_node::to_string(const tgba* a) - { - std::ostringstream os; - os << num_ - << " [shape=box, label=\"(" - << a->format_state(sc_->first) - << ", " - << a->format_state(sc_->second) - << ")\"]" - << std::endl; - return os.str(); - } - - std::string - spoiler_node::succ_to_string() - { - std::ostringstream os; - sn_v::iterator i; - for (i = lnode_succ->begin(); i != lnode_succ->end(); ++i) - { - os << num_ << " -> " << (*i)->num_ << std::endl; - } - return os.str(); - } - - bool - spoiler_node::compare(spoiler_node* n) - { - return (((sc_->first)->compare((n->get_pair())->first) == 0) && - ((sc_->second)->compare((n->get_pair())->second) == 0)); - } - - int - spoiler_node::get_nb_succ() - { - return lnode_succ->size(); - } - - const state* - spoiler_node::get_spoiler_node() - { - return sc_->first; - } - - const state* - spoiler_node::get_duplicator_node() - { - return sc_->second; - } - - state_couple* - spoiler_node::get_pair() - { - return sc_; - } - - /////////////////////////////////////////////////////////////////////// - // duplicator_node - - duplicator_node::duplicator_node(const state* d_node, - const state* s_node, - bdd l, - bdd a, - int num) - : spoiler_node(d_node, s_node, num), - label_(l), - acc_(a) - { - } - - duplicator_node::~duplicator_node() - { - } - - bool - duplicator_node::set_win() - { - bool change = not_win; - - if (!this->get_nb_succ()) - not_win = true; - else - { - not_win = true; - for (std::vector::iterator i = lnode_succ->begin(); - i != lnode_succ->end(); ++i) - { - not_win &= (*i)->not_win; - } - } - if (change != not_win) - for (std::vector::iterator i = lnode_pred->begin(); - i != lnode_pred->end(); ++i) - (*i)->set_win(); - - return change != not_win; - } - - std::string - duplicator_node::to_string(const tgba* a) - { - std::ostringstream os; - os << num_ - << " [shape=box, label=\"(" - << a->format_state(sc_->first) - << ", " - << a->format_state(sc_->second) - << ", "; - bdd_print_acc(os, a->get_dict(), label_); - os << ", "; - bdd_print_acc(os, a->get_dict(), acc_); - os << ")\"]" - << std::endl; - return os.str(); - } - - bool - duplicator_node::compare(spoiler_node* n) - { - return (this->spoiler_node::compare(n) && - (label_ == static_cast(n)->get_label()) && - (acc_ == static_cast(n)->get_acc())); - } - - bdd - duplicator_node::get_label() const - { - return label_; - } - - bdd - duplicator_node::get_acc() const - { - return acc_; - } - - bool - duplicator_node::match(bdd l, bdd a) - { - return ((l == label_) && (a == acc_)); - } - - bool - duplicator_node::implies(bdd l, bdd a) - { - // if (a | !b) == true then (a => b). - return (((l | !label_) == bddtrue) && - ((a | !acc_) == bddtrue)); - } - - /////////////////////////////////////////////////////////////////////// - // parity_game_graph - - void - parity_game_graph::process_state(const state* s, - int, - tgba_succ_iterator*) - { - tgba_state_.push_back(s); - } - - void - parity_game_graph::print(std::ostream& os) - { - std::vector::iterator i1; - std::vector::iterator i2; - - int n = 0; - - os << "digraph G {" << std::endl; - - os << "{" << std::endl - << "rank = same;" << std::endl - << "node [color=red];" << std::endl; - for (i1 = spoiler_vertice_.begin(); - i1 != spoiler_vertice_.end(); ++i1) - { - os << (*i1)->to_string(aut_); - ++n; - if (n > 20) - { - n = 0; - os << "}" << std::endl << std::endl - << "{" << std::endl - << "rank = same" << std::endl - << "node [color=red];" << std::endl; - } - } - os << "}" << std::endl; - - n = 0; - os << "{" << std::endl - << "rank = same;" << std::endl - << "node [color=green];" << std::endl; - for (i2 = duplicator_vertice_.begin(); - i2 != duplicator_vertice_.end(); ++i2) - { - os << (*i2)->to_string(aut_); - ++n; - if (n > 20) - { - n = 0; - os << "}" << std::endl << std::endl - << "{" << std::endl - << "rank = same" << std::endl - << "node [color=green];" << std::endl; - } - } - os << "}" << std::endl << std::endl; - - os << "edge [color=red];" << std::endl; - for (i1 = spoiler_vertice_.begin(); - i1 != spoiler_vertice_.end(); ++i1) - { - os << (*i1)->succ_to_string(); - } - - os << std::endl - << "edge [color=green];" << std::endl; - for (i2 = duplicator_vertice_.begin(); - i2 != duplicator_vertice_.end(); ++i2) - { - os << (*i2)->succ_to_string(); - } - - os << "}" << std::endl; - - } - - parity_game_graph::~parity_game_graph() - { - std::vector::iterator i1; - std::vector::iterator i2; - - for (i1 = spoiler_vertice_.begin(); - i1 != spoiler_vertice_.end(); ++i1) - { - delete *i1; - } - - for (i2 = duplicator_vertice_.begin(); - i2 != duplicator_vertice_.end(); ++i2) - { - delete *i2; - } - - spoiler_vertice_.clear(); - duplicator_vertice_.clear(); - } - - parity_game_graph::parity_game_graph(const tgba* a) - : tgba_reachable_iterator_breadth_first(a) - { - this->run(); - nb_node_parity_game = 0; - } - - /////////////////////////////////////////////////////////////////////// - // parity_game_graph_direct - - void - parity_game_graph_direct::build_graph() - { - tgba_succ_iterator* si = 0; - typedef std::pair couple_bdd; - couple_bdd *p = 0; - std::vector* trans = 0; - bool exist = false; - spot::state* s = 0; - - for (std::vector::iterator i = tgba_state_.begin(); - i != tgba_state_.end(); ++i) - { - - // spoiler node are all state couple (i,j) - for (std::vector::iterator j = tgba_state_.begin(); - j != tgba_state_.end(); ++j) - { - spoiler_node* n1 = new spoiler_node(*i, - *j, - nb_node_parity_game++); - spoiler_vertice_.push_back(n1); - } - - // duplicator node are all state couple where - // the first state i are reachable. - trans = new std::vector; - for (std::vector::iterator j = tgba_state_.begin(); - j != tgba_state_.end(); ++j) - { - si = aut_->succ_iter(*j); - for (si->first(); !si->done(); si->next()) - { - - // if there exist a predecessor of i named j - s = si->current_state(); - if (s->compare(*i) == 0) - { - - // p is the label of the transition j->i - p = new couple_bdd(si->current_condition(), - si->current_acceptance_conditions()); - - // If an other predecessor of i has the same label p - // to reach i, then we don't compute the duplicator node. - exist = false; - for (std::vector::iterator v - = trans->begin(); - v != trans->end(); ++v) - { - if ((si->current_condition() == (*v)->first) && - (si->current_acceptance_conditions() - == (*v)->second)) - exist = true; - } - - if (!exist) - { - // We build all the state couple with the label p. - trans->push_back(p); - for (std::vector::iterator s - = tgba_state_.begin(); - s != tgba_state_.end(); ++s) - { - duplicator_node* n2 - = new - duplicator_node(*i, - *s, - si->current_condition(), - si - ->current_acceptance_conditions(), - nb_node_parity_game++); - duplicator_vertice_.push_back(n2); - } - } - else - delete p; - } - s->destroy(); - } - delete si; - } - std::vector::iterator i2; - for (i2 = trans->begin(); i2 != trans->end(); ++i2) - { - delete *i2; - } - delete trans; - } - } - - void - parity_game_graph_direct::build_link() - { - int nb_ds = 0; - int nb_sd = 0; - spot::state* s = 0; - - // for each couple of (spoiler, duplicator) - for (std::vector::iterator i - = spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i) - { - for (std::vector::iterator j - = duplicator_vertice_.begin(); - j != duplicator_vertice_.end(); ++j) - { - // We add a link between a duplicator and a spoiler. - if ((*j)->get_spoiler_node() - ->compare((*i)->get_spoiler_node()) == 0) - { - tgba_succ_iterator* si - = aut_->succ_iter((*j)->get_duplicator_node()); - for (si->first(); !si->done(); si->next()) - { - s = si->current_state(); - if ((s->compare((*i)->get_duplicator_node()) == 0) && - (*j)->implies(si->current_condition(), - si->current_acceptance_conditions())) - { - (*j)->add_succ(*i); - ++nb_ds; - } - s->destroy(); - } - delete si; - } - - // We add a link between a spoiler and a duplicator. - if ((*j)->get_duplicator_node() - ->compare((*i)->get_duplicator_node()) == 0) - { - tgba_succ_iterator* si - = aut_->succ_iter((*i)->get_spoiler_node()); - for (si->first(); !si->done(); si->next()) - { - s = si->current_state(); - if ((s->compare((*j)->get_spoiler_node()) == 0) && - (*j)->match(si->current_condition(), - si->current_acceptance_conditions())) - { - (*i)->add_succ(*j); - ++nb_sd; - } - s->destroy(); - } - delete si; - } - } - } - } - - void - parity_game_graph_direct::lift() - { - bool change = true; - - while (change) - { - change = false; - for (std::vector::iterator i - = duplicator_vertice_.begin(); - i != duplicator_vertice_.end(); ++i) - { - change |= (*i)->set_win(); - } - for (std::vector::iterator i - = spoiler_vertice_.begin(); - i != spoiler_vertice_.end(); ++i) - { - change |= (*i)->set_win(); - } - } - } - - direct_simulation_relation* - parity_game_graph_direct::get_relation() - { - direct_simulation_relation* rel = new direct_simulation_relation; - state_couple* p = 0; - seen_map::iterator j; - - for (std::vector::iterator i - = spoiler_vertice_.begin(); - i != spoiler_vertice_.end(); ++i) - { - if (!(*i)->not_win) - { - p = new state_couple((*i)->get_spoiler_node(), - (*i)->get_duplicator_node()); - rel->push_back(p); - - - // We remove the state in rel from seen - // because the destructor of - // tgba_reachable_iterator_breadth_first - // delete all instance of state. - - - if ((j = seen.find(p->first)) != seen.end()) - seen.erase(j); - if ((j = seen.find(p->second)) != seen.end()) - seen.erase(j); - - } - } - - return rel; - } - - parity_game_graph_direct::~parity_game_graph_direct() - { - } - - parity_game_graph_direct::parity_game_graph_direct(const tgba* a) - : parity_game_graph(a) - { - this->build_graph(); - this->build_link(); - this->lift(); - } - - /////////////////////////////////////////////////////////////////////// - - direct_simulation_relation* - get_direct_relation_simulation(const tgba* f, - std::ostream& os, - int opt) - { - parity_game_graph_direct* G = new parity_game_graph_direct(f); - direct_simulation_relation* rel = G->get_relation(); - if (opt == 1) - G->print(os); - delete G; - return rel; - } - - void - free_relation_simulation(direct_simulation_relation* rel) - { - if (rel == 0) - return; - - Sgi::hash_map seen; - Sgi::hash_map::iterator j; - - simulation_relation::iterator i; - for (i = rel->begin(); i != rel->end(); ++i) - { - if ((j = seen.find((*i)->first)) == seen.end()) - seen[(*i)->first] = 0; - - if ((j = seen.find((*i)->second)) == seen.end()) - seen[(*i)->second] = 0; - - delete *i; - } - delete rel; - rel = 0; - - for (j = seen.begin(); j != seen.end();) - { - const state* ptr = j->first; - ++j; - ptr->destroy(); - } - } - - bool - is_include(const tgba*, const tgba*) - { - return false; - } - const tgba* reduc_tgba_sim(const tgba* f, int opt) { @@ -661,41 +40,18 @@ namespace spot return f; } - spot::tgba_reduc* automatareduc = new spot::tgba_reduc(f); - - // Destroy the automaton created by scc_filter. - if (opt & Reduce_Scc) - delete f; - - if (opt & (Reduce_quotient_Dir_Sim | Reduce_transition_Dir_Sim)) + if (opt & (Reduce_quotient_Dir_Sim | Reduce_transition_Dir_Sim + | Reduce_quotient_Del_Sim | Reduce_transition_Del_Sim)) { - direct_simulation_relation* rel - = get_direct_relation_simulation(automatareduc, std::cout); + tgba* res = simulation(f); - assert(rel); + if (opt & Reduce_Scc) + delete f; - automatareduc->display_rel_sim(rel, std::cout); - automatareduc->quotient_state(rel); - automatareduc->delete_transitions(rel); - - free_relation_simulation(rel); + return res; } - else - if (opt & (Reduce_quotient_Del_Sim | Reduce_transition_Del_Sim)) - { - delayed_simulation_relation* rel - = get_delayed_relation_simulation(automatareduc, std::cout); - assert(rel); - - automatareduc->display_rel_sim(rel, std::cout); - automatareduc->quotient_state(rel); - automatareduc->delete_transitions(rel); - - free_relation_simulation(rel); - } - - return automatareduc; + return tgba_dupexp_dfs(f); } } diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh index 917e51846..8d9c3bc45 100644 --- a/src/tgbaalgos/reductgba_sim.hh +++ b/src/tgbaalgos/reductgba_sim.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -25,14 +25,9 @@ #ifndef SPOT_TGBAALGOS_REDUCTGBA_SIM_HH #define SPOT_TGBAALGOS_REDUCTGBA_SIM_HH -#include "tgba/tgbareduc.hh" -#include "tgbaalgos/reachiter.hh" -#include -#include -#include - namespace spot { + class tgba; /// \addtogroup tgba_reduction /// @{ @@ -62,280 +57,34 @@ namespace spot #endif }; - /// \brief Remove some node of the automata using a simulation - /// relation. +#if __GNUC__ + /// \brief Simplify the automaton using a simulation relation. /// - /// \param a the automata to reduce. + /// Do not use this obsolete function. + /// + /// \param a the automata to reduce /// \param opt a conjonction of spot::reduce_tgba_options specifying - /// which optimizations to apply. - /// \return the reduced automata. + /// which optimizations to apply. Actually any + /// simulation-related flag will cause direct simulation + /// to be applied. + /// \return the reduced automaton + /// \deprecated Use scc_filter(), minimize_wdba(), or simulation(). + const tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All) + __attribute__ ((deprecated)); +#else + /// \brief Simplify the automaton using a simulation relation. + /// + /// Do not use this obsolete function. + /// + /// \param a the automata to reduce + /// \param opt a conjonction of spot::reduce_tgba_options specifying + /// which optimizations to apply. Actually any + /// simulation-related flag will cause direct simulation + /// to be applied. + /// \return the reduced automaton + /// \deprecated Use scc_filter(), minimize_wdba(), or simulation(). const tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All); - -#ifndef SWIG - - /// \brief Compute a direct simulation relation on state of tgba \a f. - direct_simulation_relation* get_direct_relation_simulation(const tgba* a, - std::ostream& os, - int opt = -1); - - /// Compute a delayed simulation relation on state of tgba \a f. - /// \bug Does not work for generalized automata. - delayed_simulation_relation* get_delayed_relation_simulation(const tgba* a, - std::ostream& os, - int opt = -1); - - /// To free a simulation relation. - void free_relation_simulation(direct_simulation_relation* rel); - /// To free a simulation relation. - void free_relation_simulation(delayed_simulation_relation* rel); - - /////////////////////////////////////////////////////////////////////// - // simulation. - - class spoiler_node; - class duplicator_node; - - typedef std::vector sn_v; - typedef std::vector dn_v; - typedef std::vector s_v; - - /// \brief Parity game graph which compute a simulation relation. - class parity_game_graph : public tgba_reachable_iterator_breadth_first - { - public: - parity_game_graph(const tgba* a); - virtual ~parity_game_graph(); - - virtual simulation_relation* get_relation() = 0; - - void print(std::ostream& os); - - protected: - sn_v spoiler_vertice_; - dn_v duplicator_vertice_; - s_v tgba_state_; - int nb_node_parity_game; - - void process_state(const state* s, int n, tgba_succ_iterator* si); - - /// \brief Compute each node of the graph. - virtual void build_graph() = 0; - - /// \brief Remove edge from spoiler to duplicator that make - /// duplicator loose. - /// Spoiler node whose still have some link, reveal - /// a direct simulation relation. - virtual void lift() = 0; - }; - - /////////////////////////////////////////////////////////////////////// - // Direct simulation. - - /// Spoiler node of parity game graph. - class spoiler_node - { - public: - spoiler_node(const state* d_node, - const state* s_node, - int num); - virtual ~spoiler_node(); - - /// \brief Add a successor. - /// Return true if \a n wasn't yet in the list of successor, - /// false eitherwise. - bool add_succ(spoiler_node* n); - void del_succ(spoiler_node* n); - virtual void add_pred(spoiler_node* n); - virtual void del_pred(); - int get_nb_succ(); - bool prune(); - virtual bool set_win(); - virtual std::string to_string(const tgba* a); - virtual std::string succ_to_string(); - virtual bool compare(spoiler_node* n); - - const state* get_spoiler_node(); - const state* get_duplicator_node(); - state_couple* get_pair(); - - bool not_win; - int num_; // for the dot display. - - protected: - sn_v* lnode_succ; - sn_v* lnode_pred; - state_couple* sc_; - }; - - /// Duplicator node of parity game graph. - class duplicator_node : public spoiler_node - { - public: - duplicator_node(const state* d_node, - const state* s_node, - bdd l, - bdd a, - int num); - virtual ~duplicator_node(); - - virtual bool set_win(); - virtual std::string to_string(const tgba* a); - virtual bool compare(spoiler_node* n); - - bool match(bdd l, bdd a); - bool implies(bdd l, bdd a); - - bdd get_label() const; - bdd get_acc() const; - - protected: - bdd label_; - bdd acc_; - }; - - /// Parity game graph which compute the direct simulation relation. - class parity_game_graph_direct : public parity_game_graph - { - public: - parity_game_graph_direct(const tgba* a); - ~parity_game_graph_direct(); - - virtual direct_simulation_relation* get_relation(); - - protected: - virtual void build_graph(); - virtual void lift(); - void build_link(); - - }; - - - /////////////////////////////////////////////////////////////////////// - // Delayed simulation. - - /// Spoiler node of parity game graph for delayed simulation. - class spoiler_node_delayed : public spoiler_node - { - public: - spoiler_node_delayed(const state* d_node, - const state* s_node, - bdd a, - int num); - ~spoiler_node_delayed(); - - /// Return true if the progress_measure has changed. - bool set_win(); - bdd get_acceptance_condition_visited() const; - virtual bool compare(spoiler_node* n); - virtual std::string to_string(const tgba* a); - int get_progress_measure() const; - - bool get_lead_2_acc_all(); - bool set_lead_2_acc_all(bdd acc = bddfalse); - - // - bool seen_; - protected: - /// a Bdd for retain all the acceptance condition - /// that a node has visited. - bdd acceptance_condition_visited_; - int progress_measure_; - bool lead_2_acc_all_; - }; - - /// Duplicator node of parity game graph for delayed simulation. - class duplicator_node_delayed : public duplicator_node - { - public: - duplicator_node_delayed(const state* d_node, - const state* s_node, - bdd l, - bdd a, - int num); - ~duplicator_node_delayed(); - - /// Return true if the progress_measure has changed. - bool set_win(); - virtual std::string to_string(const tgba* a); - bool implies_label(bdd l); - bool implies_acc(bdd a); - int get_progress_measure(); - - bool get_lead_2_acc_all(); - bool set_lead_2_acc_all(bdd acc = bddfalse); - - // - bool seen_; - protected: - int progress_measure_; - bool lead_2_acc_all_; - }; - - - /// Parity game graph which computes the delayed simulation relation - /// as explained in - /// \verbatim - /// @InProceedings{etessami.01.alp, - /// author = {Kousha Etessami and Thomas Wilke and Rebecca A. Schuller}, - /// title = {Fair Simulation Relations, Parity Games, and State Space - /// Reduction for Buchi Automata}, - /// booktitle = {Proceedings of the 28th international colloquium on - /// Automata, Languages and Programming}, - /// pages = {694--707}, - /// year = {2001}, - /// editor = {Fernando Orejas and Paul G. Spirakis and Jan van Leeuwen}, - /// volume = {2076}, - /// series = {Lecture Notes in Computer Science}, - /// address = {Crete, Greece}, - /// month = {July}, - /// publisher = {Springer-Verlag} - /// } - /// \endverbatim - class parity_game_graph_delayed: public parity_game_graph - { - public: - parity_game_graph_delayed(const tgba* a); - ~parity_game_graph_delayed(); - - virtual delayed_simulation_relation* get_relation(); - - private: - - /// Vector which contain all the sub-set of the set - /// of acceptance condition. - typedef std::vector bdd_v; - bdd_v sub_set_acc_cond_; - - /// Return the number of acceptance condition. - int nb_set_acc_cond(); - - /// - duplicator_node_delayed* add_duplicator_node_delayed(const spot::state* sn, - const spot::state* dn, - bdd acc, - bdd label, - int nb); - - /// - spoiler_node_delayed* add_spoiler_node_delayed(const spot::state* sn, - const spot::state* dn, - bdd acc, - int nb); - - void build_recurse_successor_spoiler(spoiler_node* sn, - std::ostringstream& os); - void build_recurse_successor_duplicator(duplicator_node* dn, - spoiler_node* sn, - std::ostringstream& os); - - /// \brief Compute the couple as for direct simulation, - virtual void build_graph(); - - /// \brief The Jurdzinski's lifting algorithm. - virtual void lift(); - }; - -#endif // SWIG +#endif /// @} } diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc deleted file mode 100644 index d2df0a0f4..000000000 --- a/src/tgbaalgos/reductgba_sim_del.cc +++ /dev/null @@ -1,675 +0,0 @@ -// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 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 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 "reductgba_sim.hh" -#include "tgba/bddprint.hh" - -namespace spot -{ - /// Number of spoiler node with a one priority (see icalp2001). - /// The one priority is represent by a \a acceptance_condition_visited_ - /// which differ of bddfalse. - /// This spoiler node are looser for the duplicator. - /// FIXME: get rid of these ugly globals - static int nb_spoiler_loose_; - - static int nb_spoiler; - static int nb_duplicator; - - static bdd all_acc_cond = bddfalse; - - static std::vector bool_v; - - //static int nb_node = 0; - - //seen_map_node seen_node_; - - /////////////////////////////////////////////////////////////////////// - // spoiler_node_delayed - - spoiler_node_delayed::spoiler_node_delayed(const state* d_node, - const state* s_node, - bdd a, - int num) - : spoiler_node(d_node, s_node, num), - acceptance_condition_visited_(a) - { - ++nb_spoiler; - progress_measure_ = 0; - if (acceptance_condition_visited_ != bddfalse) - ++nb_spoiler_loose_; - lead_2_acc_all_ = false; - - seen_ = false; - } - - spoiler_node_delayed::~spoiler_node_delayed() - { - if (acceptance_condition_visited_ != bddfalse) - --nb_spoiler_loose_; - } - - bool - spoiler_node_delayed::set_win() - { - // We take the max of the progress measure of the successor node - // because we are on a spoiler. - - if (lnode_succ->empty()) - progress_measure_ = nb_spoiler_loose_ + 1; - - if (progress_measure_ >= nb_spoiler_loose_ + 1) - return false; - - bool change; - int tmpmax = 0; - int tmp = 0; - int tmpmaxwin = -1; - sn_v::iterator i = lnode_succ->begin(); - if (i != lnode_succ->end()) - { - tmpmax = - static_cast(*i)->get_progress_measure(); - if (static_cast(*i)->get_lead_2_acc_all()) - tmpmaxwin = tmpmax; - ++i; - } - for (; i != lnode_succ->end(); ++i) - { - tmp = - static_cast(*i)->get_progress_measure(); - if (tmp > tmpmax) - tmpmax = tmp; - if (static_cast(*i)->get_lead_2_acc_all() && - (tmp > tmpmaxwin)) - tmpmaxwin = tmp; - } - - if (tmpmaxwin != -1) - tmpmax = tmpmaxwin; - - // If the priority of the node is 1 - // acceptance_condition_visited_ != bddfalse - // then we increment the progress measure of 1. - if ((acceptance_condition_visited_ != bddfalse) && - (tmpmax < (nb_spoiler_loose_ + 1))) - ++tmpmax; - - change = (progress_measure_ < tmpmax); - - progress_measure_ = tmpmax; - return change; - } - - bool - spoiler_node_delayed::compare(spoiler_node* n) - { - return (this->spoiler_node::compare(n) && - (acceptance_condition_visited_ == - static_cast(n)-> - get_acceptance_condition_visited())); - } - - std::string - spoiler_node_delayed::to_string(const tgba* a) - { - std::ostringstream os; - - // print the node. - os << num_ - << " [shape=box, label=\"(" - << a->format_state(sc_->first) - << ", " - << a->format_state(sc_->second) - << ", "; - //bdd_print_acc(os, a->get_dict(), acceptance_condition_visited_); - if (acceptance_condition_visited_ == bddfalse) - { - os << "false"; - } - else - { - os << "ACC"; - } - os << ")" - << " pm = " << progress_measure_; - if (lead_2_acc_all_) - os << ", 1\"]"; - else - os << ", 0\"]"; - os << std::endl; - - return os.str(); - } - - bdd - spoiler_node_delayed::get_acceptance_condition_visited() const - { - return acceptance_condition_visited_; - } - - int - spoiler_node_delayed::get_progress_measure() const - { - if ((acceptance_condition_visited_ == bddfalse) && - (progress_measure_ != (nb_spoiler_loose_ + 1))) - return 0; - else - return progress_measure_; - } - - bool - spoiler_node_delayed::get_lead_2_acc_all() - { - return lead_2_acc_all_; - } - - - bool - spoiler_node_delayed::set_lead_2_acc_all(bdd acc) - { - if (!seen_) - { - seen_ = true; - for (sn_v::iterator i = lnode_succ->begin(); - i != lnode_succ->end(); ++i) - static_cast(*i)->set_lead_2_acc_all(acc); - } - else - { - if (acc == all_acc_cond) - lead_2_acc_all_ = true; - } - return lead_2_acc_all_; - } - - - /////////////////////////////////////////////////////////////////////// - // duplicator_node_delayed - - duplicator_node_delayed::duplicator_node_delayed(const state* d_node, - const state* s_node, - bdd l, - bdd a, - int num) - : duplicator_node(d_node, s_node, l, a, num) - { - ++nb_duplicator; - progress_measure_ = 0; - all_acc_cond |= a; - lead_2_acc_all_ = false; - - seen_ = false; - } - - duplicator_node_delayed::~duplicator_node_delayed() - { - } - - bool - duplicator_node_delayed::set_win() - { - // We take the min of the progress measure of the successor node - // because we are on a duplicator. - - if (lnode_succ->empty()) - progress_measure_ = nb_spoiler_loose_ + 1; - - if (progress_measure_ >= nb_spoiler_loose_ + 1) - return false; - - bool change; - int tmpmin = 0; - int tmp = 0; - int tmpminwin = -1; - sn_v::iterator i = lnode_succ->begin(); - if (i != lnode_succ->end()) - { - tmpmin = - static_cast(*i)->get_progress_measure(); - if (static_cast(*i)->get_lead_2_acc_all()) - tmpminwin = tmpmin; - ++i; - } - for (; i != lnode_succ->end(); ++i) - { - tmp = static_cast(*i)->get_progress_measure(); - if (tmp < tmpmin) - tmpmin = tmp; - if (static_cast(*i)->get_lead_2_acc_all() && - (tmp > tmpminwin)) - tmpminwin = tmp; - } - if (tmpminwin != -1) - tmpmin = tmpminwin; - - change = (progress_measure_ < tmpmin); - progress_measure_ = tmpmin; - return change; - } - - std::string - duplicator_node_delayed::to_string(const tgba* a) - { - std::ostringstream os; - - // print the node. - os << num_ - << " [shape=box, label=\"(" - << a->format_state(sc_->first) - << ", " - << a->format_state(sc_->second) - << ", "; - if (label_ == bddfalse) - os << "0"; - else if (label_ == bddtrue) - os << "1"; - else - bdd_print_acc(os, a->get_dict(), label_); - //<< ", "; - //bdd_print_acc(os, a->get_dict(), acc_); - os << ")" - << " pm = " << progress_measure_; - if (lead_2_acc_all_) - os << ", 1\"]"; - else - os << ", 0\"]"; - os << std::endl; - - return os.str(); - } - - bool - duplicator_node_delayed::implies_label(bdd l) - { - return ((l | !label_) == bddtrue); - } - - bool - duplicator_node_delayed::implies_acc(bdd a) - { - return ((a | !acc_) == bddtrue); - } - - int - duplicator_node_delayed::get_progress_measure() - { - return progress_measure_; - } - - bool - duplicator_node_delayed::get_lead_2_acc_all() - { - return lead_2_acc_all_; - } - - bool - duplicator_node_delayed::set_lead_2_acc_all(bdd acc) - { - acc |= acc_; - if (!seen_) - { - seen_ = true; - for (sn_v::iterator i = lnode_succ->begin(); - i != lnode_succ->end(); ++i) - lead_2_acc_all_ - |= static_cast(*i)->set_lead_2_acc_all(acc); - } - return lead_2_acc_all_; - } - - /////////////////////////////////////////////////////////////////////// - // parity_game_graph_delayed - - int - parity_game_graph_delayed::nb_set_acc_cond() - { - return aut_->number_of_acceptance_conditions(); - } - - // We build only node which are reachable - void - parity_game_graph_delayed::build_graph() - { - // We build only some "basic" spoiler node. - sn_v tab_temp; - s_v::iterator i1; - for (i1 = tgba_state_.begin(); i1 != tgba_state_.end(); ++i1) - { - - // spoiler node are all state couple (i,j) - s_v::iterator i2; - for (i2 = tgba_state_.begin(); - i2 != tgba_state_.end(); ++i2) - { - //std::cout << "add spoiler node" << std::endl; - ++nb_spoiler; - spoiler_node_delayed* n1 - = new spoiler_node_delayed(*i1, *i2, - bddfalse, - nb_node_parity_game++); - spoiler_vertice_.push_back(n1); - tab_temp.push_back(n1); - } - } - - sn_v::iterator j; - std::ostringstream os; - for (j = tab_temp.begin(); j != tab_temp.end(); ++j) - { - // We add a link between a spoiler and a (new) duplicator. - // The acc of the duplicator must contains the - // acceptance_condition_visited_ of the spoiler. - //std::cout << "build_link : iter " << ++n << std::endl; - build_recurse_successor_spoiler(*j, os); - - } - } - - void - parity_game_graph_delayed:: - build_recurse_successor_spoiler(spoiler_node* sn, - std::ostringstream& os) - { - assert(sn); - - tgba_succ_iterator* si = aut_->succ_iter(sn->get_spoiler_node()); - - for (si->first(); !si->done(); si->next()) - { - bdd btmp = si->current_acceptance_conditions() | - static_cast(sn)-> - get_acceptance_condition_visited(); - - s_v::iterator i1; - state* s; - for (i1 = tgba_state_.begin(); - i1 != tgba_state_.end(); ++i1) - { - - s = si->current_state(); - if (s->compare(*i1) == 0) - { - s->destroy(); - duplicator_node_delayed* dn - = add_duplicator_node_delayed(*i1, - sn->get_duplicator_node(), - si->current_condition(), - btmp, - nb_node_parity_game++); - - if (!(sn->add_succ(dn))) - continue; - - std::ostringstream os2; - os2 << os.str() << " "; - build_recurse_successor_duplicator(dn, sn, os2); - } - else - s->destroy(); - } - } - - delete si; - } - - void - parity_game_graph_delayed:: - build_recurse_successor_duplicator(duplicator_node* dn, - spoiler_node* , - std::ostringstream& os) - { - tgba_succ_iterator* si = aut_->succ_iter(dn->get_duplicator_node()); - - for (si->first(); !si->done(); si->next()) - { - - // if si->current_condition() doesn't implies dn->get_label() - // then duplicator can't play. - if ((si->current_condition() | !dn->get_label()) != bddtrue) - { - continue; - } - - bdd btmp = dn->get_acc() - - (dn->get_acc() & si->current_acceptance_conditions()); - - s_v::iterator i1; - state* s; - for (i1 = tgba_state_.begin(); - i1 != tgba_state_.end(); ++i1) - { - s = si->current_state(); - - if (s->compare(*i1) == 0) - { - s->destroy(); - spoiler_node_delayed* sn_n - = add_spoiler_node_delayed(dn->get_spoiler_node(), - *i1, - btmp, - nb_node_parity_game++); - - if (!(dn->add_succ(sn_n))) - continue; - - std::ostringstream os2; - os2 << os.str() << " "; - build_recurse_successor_spoiler(sn_n, os2); - } - else - s->destroy(); - } - } - - delete si; - } - - duplicator_node_delayed* - parity_game_graph_delayed::add_duplicator_node_delayed(const spot::state* sn, - const spot::state* dn, - bdd acc, - bdd label, - int nb) - { - bool exist = false; - - duplicator_node_delayed* dn_n - = new duplicator_node_delayed(sn, dn, acc, label, nb); - - for (std::vector::iterator i - = duplicator_vertice_.begin(); - i != duplicator_vertice_.end(); ++i) - { - if (dn_n->compare(*i)) - { - exist = true; - delete dn_n; - dn_n = static_cast(*i); - break; - } - } - - if (!exist) - duplicator_vertice_.push_back(dn_n); - - return dn_n; - } - - spoiler_node_delayed* - parity_game_graph_delayed::add_spoiler_node_delayed(const spot::state* sn, - const spot::state* dn, - bdd acc, - int nb) - { - bool exist = false; - - //bool l2a = (acc != aut_->all_acceptance_conditions()); - spoiler_node_delayed* sn_n - = new spoiler_node_delayed(sn, dn, acc, nb); - - for (std::vector::iterator i - = spoiler_vertice_.begin(); - i != spoiler_vertice_.end(); ++i) - { - if (sn_n->compare(*i)) - { - exist = true; - delete sn_n; - sn_n = static_cast(*i); - break; - } - } - - if (!exist) - spoiler_vertice_.push_back(sn_n); - - return sn_n; - } - - void - parity_game_graph_delayed::lift() - { - // Jurdzinski's algorithm - bool change = true; - - while (change) - { - //std::cout << "lift::change = true" << std::endl; - change = false; - for (std::vector::iterator i - = duplicator_vertice_.begin(); - i != duplicator_vertice_.end(); ++i) - { - change |= (*i)->set_win(); - } - for (std::vector::iterator i - = spoiler_vertice_.begin(); - i != spoiler_vertice_.end(); ++i) - { - change |= (*i)->set_win(); - } - } - //std::cout << "lift::change = false" << std::endl; - } - - delayed_simulation_relation* - parity_game_graph_delayed::get_relation() - { - delayed_simulation_relation* rel = new delayed_simulation_relation; - state_couple* p = 0; - seen_map::iterator j; - - // This does not work for generalized automata. A tarjan-like - // algorithm is required to tell whether a state can lead to an - // acceptance cycle. - if (this->nb_set_acc_cond() > 1) - return rel; - - for (std::vector::iterator i - = spoiler_vertice_.begin(); - i != spoiler_vertice_.end(); ++i) - { - if ((static_cast(*i)->get_progress_measure() - < nb_spoiler_loose_ + 1) && - (static_cast(*i) - ->get_acceptance_condition_visited() == bddfalse)) - { - p = new state_couple((*i)->get_spoiler_node(), - (*i)->get_duplicator_node()); - rel->push_back(p); - - // We remove the state in rel from seen - // because the destructor of - // tgba_reachable_iterator_breadth_first - // delete all the state. - - if ((j = seen.find(p->first)) != seen.end()) - seen.erase(j); - if ((j = seen.find(p->second)) != seen.end()) - seen.erase(j); - } - - } - - return rel; - } - - parity_game_graph_delayed::~parity_game_graph_delayed() - { - } - - parity_game_graph_delayed::parity_game_graph_delayed(const tgba* a) - : parity_game_graph(a) - { - nb_spoiler_loose_ = 0; - this->build_graph(); - this->lift(); - } - - /////////////////////////////////////////// - delayed_simulation_relation* - get_delayed_relation_simulation(const tgba* f, std::ostream& os, int opt) - { - parity_game_graph_delayed* G = new parity_game_graph_delayed(f); - delayed_simulation_relation* rel = G->get_relation(); - if (opt == 1) - G->print(os); - delete G; - return rel; - } - - void - free_relation_simulation(delayed_simulation_relation* rel) - { - if (rel == 0) - return; - - Sgi::hash_map seen; - Sgi::hash_map::iterator j; - - delayed_simulation_relation::iterator i; - for (i = rel->begin(); i != rel->end(); ++i) - { - if ((j = seen.find((*i)->first)) == seen.end()) - seen[(*i)->first] = 0; - - if ((j = seen.find((*i)->second)) == seen.end()) - seen[(*i)->second] = 0; - - delete *i; - } - delete rel; - rel = 0; - - for (j = seen.begin(); j != seen.end();) - { - const state* ptr = j->first; - ++j; - ptr->destroy(); - } - } - -} diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 0a2983479..865368015 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -43,8 +43,6 @@ check_PROGRAMS = \ ltlprod \ mixprod \ powerset \ - reductgba \ - reduccmp \ taatgba \ tgbaread \ tripprod @@ -65,9 +63,6 @@ ltlprod_SOURCES = ltlprod.cc mixprod_SOURCES = mixprod.cc powerset_SOURCES = powerset.cc randtgba_SOURCES = randtgba.cc -reductgba_SOURCES = reductgba.cc -reduccmp_SOURCES = reductgba.cc -reduccmp_CXXFLAGS = -DREDUCCMP taatgba_SOURCES = taatgba.cc tgbaread_SOURCES = tgbaread.cc tripprod_SOURCES = tripprod.cc @@ -97,8 +92,6 @@ TESTS = \ degendet.test \ degenid.test \ kv.test \ - reduccmp.test \ - reductgba.test \ scc.test \ sccsimpl.test \ obligation.test \ diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 1a2e5d15c..2e4b3e7c9 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2007, 2008, 2009, 2010, 2011 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012 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. +// 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. // @@ -49,7 +50,6 @@ #include "tgbaalgos/dupexp.hh" #include "tgbaalgos/minimize.hh" #include "tgbaalgos/neverclaim.hh" -#include "tgbaalgos/reductgba_sim.hh" #include "tgbaalgos/replayrun.hh" #include "tgbaalgos/rundotdec.hh" #include "tgbaalgos/sccfilter.hh" @@ -196,22 +196,11 @@ syntax(char* prog) << "Automaton simplifications (after translation):" << std::endl - << " -R1q merge states using direct simulation " - << "(use -L for more reduction)" - << std::endl - << " -R1t remove transitions using direct simulation " - << "(use -L for more reduction)" - << std::endl - << " -R2q merge states using delayed simulation" << std::endl - << " -R2t remove transitions using delayed simulation" - << std::endl << " -R3 use SCC to reduce the automata" << std::endl << " -R3f clean more acceptance conditions than -R3" << std::endl << " " << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)" << std::endl - << " -Rd display the simulation relation" << std::endl - << " -RD display the parity game (dot format)" << std::endl << " -Rm attempt to minimize the automata" << std::endl << std::endl @@ -314,13 +303,11 @@ main(int argc, char** argv) bool accepting_run_replay = false; bool from_file = false; bool read_neverclaim = false; - int reduc_aut = spot::Reduce_None; int redopt = spot::ltl::Reduce_None; + bool scc_filter = false; bool scc_filter_all = false; bool symbolic_scc_pruning = false; bool display_reduce_form = false; - bool display_rel_sim = false; - bool display_parity_game = false; bool post_branching = false; bool fair_loop_approx = false; bool graph_run_opt = false; @@ -621,33 +608,22 @@ main(int argc, char** argv) { output = 3; } - else if (!strcmp(argv[formula_index], "-R1q")) + else if (!strcmp(argv[formula_index], "-R1q") + || !strcmp(argv[formula_index], "-R1t") + || !strcmp(argv[formula_index], "-R2q") + || !strcmp(argv[formula_index], "-R2t")) { - reduc_aut |= spot::Reduce_quotient_Dir_Sim; - } - else if (!strcmp(argv[formula_index], "-RSD")) - { - reduction_dir_sim = true; - } - else if (!strcmp(argv[formula_index], "-R1t")) - { - reduc_aut |= spot::Reduce_transition_Dir_Sim; - } - else if (!strcmp(argv[formula_index], "-R2q")) - { - reduc_aut |= spot::Reduce_quotient_Del_Sim; - } - else if (!strcmp(argv[formula_index], "-R2t")) - { - reduc_aut |= spot::Reduce_transition_Del_Sim; + // For backward compatibility, make all these options + // equal to -RSD. + reduction_dir_sim = true; } else if (!strcmp(argv[formula_index], "-R3")) { - reduc_aut |= spot::Reduce_Scc; + scc_filter = true; } else if (!strcmp(argv[formula_index], "-R3f")) { - reduc_aut |= spot::Reduce_Scc; + scc_filter = true; scc_filter_all = true; } else if (!strcmp(argv[formula_index], "-R3b")) @@ -658,18 +634,14 @@ main(int argc, char** argv) { display_reduce_form = true; } - else if (!strcmp(argv[formula_index], "-Rd")) - { - display_rel_sim = true; - } - else if (!strcmp(argv[formula_index], "-RD")) - { - display_parity_game = true; - } else if (!strcmp(argv[formula_index], "-Rm")) { opt_minimize = true; } + else if (!strcmp(argv[formula_index], "-RSD")) + { + reduction_dir_sim = true; + } else if (!strcmp(argv[formula_index], "-M")) { opt_monitor = true; @@ -898,12 +870,12 @@ main(int argc, char** argv) to_free = a; } - if (opt_monitor && ((reduc_aut & spot::Reduce_Scc) == 0)) + if (opt_monitor && !scc_filter) { if (dynamic_cast(a)) symbolic_scc_pruning = true; else - reduc_aut |= spot::Reduce_Scc; + scc_filter = true; } if (symbolic_scc_pruning) @@ -932,7 +904,7 @@ main(int argc, char** argv) // Remove dead SCCs and useless acceptance conditions before // degeneralization. const spot::tgba* aut_scc = 0; - if (reduc_aut & spot::Reduce_Scc) + if (scc_filter) { tm.start("reducing A_f w/ SCC"); a = aut_scc = spot::scc_filter(a, scc_filter_all); @@ -1019,67 +991,6 @@ main(int argc, char** argv) // pointless. } - - - spot::tgba_reduc* aut_red = 0; - if (reduc_aut != spot::Reduce_None) - { - if (reduc_aut & ~spot::Reduce_Scc) - { - tm.start("reducing A_f w/ sim."); - a = aut_red = new spot::tgba_reduc(a); - - if (reduc_aut & (spot::Reduce_quotient_Dir_Sim | - spot::Reduce_transition_Dir_Sim | - spot::Reduce_quotient_Del_Sim | - spot::Reduce_transition_Del_Sim)) - { - spot::direct_simulation_relation* rel_dir = 0; - spot::delayed_simulation_relation* rel_del = 0; - - if (reduc_aut & (spot::Reduce_quotient_Dir_Sim | - spot::Reduce_transition_Dir_Sim)) - { - rel_dir = - spot::get_direct_relation_simulation - (a, std::cout, display_parity_game); - assert(rel_dir); - } - if (reduc_aut & (spot::Reduce_quotient_Del_Sim | - spot::Reduce_transition_Del_Sim)) - { - rel_del = - spot::get_delayed_relation_simulation - (a, std::cout, display_parity_game); - assert(rel_del); - } - - if (display_rel_sim) - { - if (rel_dir) - aut_red->display_rel_sim(rel_dir, std::cout); - if (rel_del) - aut_red->display_rel_sim(rel_del, std::cout); - } - - if (reduc_aut & spot::Reduce_quotient_Dir_Sim) - aut_red->quotient_state(rel_dir); - if (reduc_aut & spot::Reduce_transition_Dir_Sim) - aut_red->delete_transitions(rel_dir); - if (reduc_aut & spot::Reduce_quotient_Del_Sim) - aut_red->quotient_state(rel_del); - if (reduc_aut & spot::Reduce_transition_Del_Sim) - aut_red->delete_transitions(rel_del); - - if (rel_dir) - spot::free_relation_simulation(rel_dir); - if (rel_del) - spot::free_relation_simulation(rel_del); - } - tm.stop("reducing A_f w/ sim."); - } - } - const spot::tgba_explicit_string* expl = 0; switch (dupexp) { @@ -1394,7 +1305,6 @@ main(int argc, char** argv) delete product_to_free; delete system; delete expl; - delete aut_red; delete minimized; delete degeneralized; delete aut_scc; diff --git a/src/tgbatest/reduccmp.test b/src/tgbatest/reduccmp.test deleted file mode 100755 index f6fafc9b6..000000000 --- a/src/tgbatest/reduccmp.test +++ /dev/null @@ -1,59 +0,0 @@ -#!/bin/sh -# Copyright (C) 2009 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# Copyright (C) 2003, 2004 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 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. - - -. ./defs - -set -e - -# FIXME -exit 0 - -cat >input < stdout - -cat >expected < 1 - 1 [label="s1, SCC -1"] -} -EOF - -rm input stdout expected - -# Sort out some possible inversions in the output. -# (The order is not guaranteed by SPOT.) -sed 's/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout -diff stdout expected - -# FIXME -exit 0 diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc deleted file mode 100644 index 608754bd5..000000000 --- a/src/tgbatest/reductgba.cc +++ /dev/null @@ -1,180 +0,0 @@ -// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// 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 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 - -#include "tgbaalgos/ltl2tgba_fm.hh" -#include "tgbaalgos/reductgba_sim.hh" -#include "tgba/tgbareduc.hh" - -#include "ltlvisit/reduce.hh" -#include "ltlast/allnodes.hh" -#include "ltlparse/public.hh" -#include "tgbaalgos/ltl2tgba_lacim.hh" -#include "tgbaalgos/ltl2tgba_fm.hh" -#include "tgba/bddprint.hh" -#include "tgbaalgos/dotty.hh" -#include "tgbaalgos/lbtt.hh" -#include "tgba/tgbatba.hh" -#include "tgbaalgos/magic.hh" -#include "tgbaalgos/gtec/gtec.hh" -#include "tgbaalgos/gtec/ce.hh" -#include "tgbaparse/public.hh" -#include "tgbaalgos/dupexp.hh" -#include "tgbaalgos/neverclaim.hh" -#include "tgbaalgos/sccfilter.hh" - -#include "misc/escape.hh" - -void -syntax(char* prog) -{ -#ifdef REDUCCMP - std::cerr << prog << " option file" << std::endl; -#else - std::cerr << prog << " option formula" << std::endl; -#endif - exit(2); -} - -int -main(int argc, char** argv) -{ - if (argc < 3) - syntax(argv[0]); - - int o = spot::ltl::Reduce_None; - switch (atoi(argv[1])) - { - case 0: - o = spot::Reduce_Scc; - break; - case 1: - o = spot::Reduce_quotient_Dir_Sim; - break; - case 2: - o = spot::Reduce_transition_Dir_Sim; - break; - case 3: - o = spot::Reduce_quotient_Del_Sim; - break; - case 4: - o = spot::Reduce_transition_Del_Sim; - break; - case 5: - o = spot::Reduce_quotient_Dir_Sim | - spot::Reduce_transition_Dir_Sim | - spot::Reduce_Scc; - break; - case 6: - o = spot::Reduce_quotient_Del_Sim | - spot::Reduce_transition_Del_Sim | - spot::Reduce_Scc; - break; - case 7: - // No Reduction - break; - default: - return 2; - } - - int exit_code = 0; - spot::direct_simulation_relation* rel_dir = 0; - spot::delayed_simulation_relation* rel_del = 0; - spot::tgba* automata = 0; - spot::tgba_reduc* automatareduc = 0; - - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::bdd_dict* dict = new spot::bdd_dict(); - -#ifdef REDUCCMP - spot::tgba_parse_error_list pel; - automata = spot::tgba_parse(argv[2], pel, dict, env, env, false); - if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel)) - return 2; -#else - spot::ltl::parse_error_list p1; - spot::ltl::formula* f = spot::ltl::parse(argv[2], p1, env); - if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1)) - return 2; - automata = spot::ltl_to_tgba_fm(f, dict, - false, true, - false, true); -#endif - - spot::dotty_reachable(std::cout, automata); - automatareduc = new spot::tgba_reduc(automata); - - if (o & spot::Reduce_quotient_Dir_Sim) - { - rel_dir = spot::get_direct_relation_simulation(automatareduc, std::cout); - automatareduc->quotient_state(rel_dir); - } - else if (o & spot::Reduce_quotient_Del_Sim) - { - std::cout << "get delayed" << std::endl; - rel_del = spot::get_delayed_relation_simulation(automatareduc, std::cout); - std::cout << "quotient state" << std::endl; - automatareduc->quotient_state(rel_del); - std::cout << "end" << std::endl; - } - - if (rel_dir != 0) - { - automatareduc->display_rel_sim(rel_dir, std::cout); - spot::free_relation_simulation(rel_dir); - } - - if (rel_del != 0) - { - automatareduc->display_rel_sim(rel_del, std::cout); - spot::free_relation_simulation(rel_del); - } - - spot::tgba* res = automatareduc; - - if (o & spot::Reduce_Scc) - { - res = spot::scc_filter(automatareduc); - delete automatareduc; - } - - spot::dotty_reachable(std::cout, res); - - delete res; - delete automata; -#ifndef REDUCCMP - if (f != 0) - f->destroy(); -#endif - - assert(spot::ltl::atomic_prop::instance_count() == 0); - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); - - if (dict != 0) - delete dict; - - return exit_code; -} diff --git a/src/tgbatest/reductgba.test b/src/tgbatest/reductgba.test deleted file mode 100755 index ecde3d817..000000000 --- a/src/tgbatest/reductgba.test +++ /dev/null @@ -1,92 +0,0 @@ -#!/bin/sh -# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# Copyright (C) 2003, 2004 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 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. - - -. ./defs - -set -e - -check() -{ - #run 0 ../reductgba "$1" "$2" - ../reductgba "$1" "$2" -} - -# We don't check the output, but just running these might be enough to -# trigger assertions. - -check 0 a -check 0 'a U b' -check 0 'a U Fb' -check 0 'X a' -check 0 'a & b & c' -check 0 'a | b | (c U (d & (g U (h ^ i))))' -check 0 'Xa & (b U !a) & (b U !a)' -check 0 'Fa & Xb & GFc & Gd' -check 0 'Fa & Xa & GFc & Gc' -check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc' -check 0 'a R (b R c)' -check 0 '(a U b) U (c U d)' -check 0 '((Xp2)U(X(1)))&(p1 R(p2 R p0))' -check 0 '((p3 | Xp3 | Xp2) & (X!p3 | (!p3 & X!p2))) R F(0)' - -check 1 a -check 1 'a U b' -check 1 'X a' -check 1 'a & b & c' -check 1 'a | b | (c U (d & (g U (h ^ i))))' -check 1 'Xa & (b U !a) & (b U !a)' -check 1 'Fa & Xb & GFc & Gd' -check 1 'Fa & Xa & GFc & Gc' -check 1 'Fc & X(a | Xb) & GF(a | Xb) & Gc' -check 1 'a R (b R c)' -check 1 '(a U b) U (c U d)' -check 1 '((Xp2)U(X(1)))&(p1 R(p2 R p0))' - -check 2 a -check 2 'a U b' -check 2 'X a' -check 2 'a & b & c' -check 2 'a | b | (c U (d & (g U (h ^ i))))' -check 2 'Xa & (b U !a) & (b U !a)' -check 2 'Fa & Xb & GFc & Gd' -check 2 'Fa & Xa & GFc & Gc' -check 2 'Fc & X(a | Xb) & GF(a | Xb) & Gc' -check 2 'a R (b R c)' -check 2 '(a U b) U (c U d)' -check 2 '((Xp2)U(X(1)))&(p1 R(p2 R p0))' - -check 3 a -check 3 'a U b' -check 3 'a U Fb' -check 3 'X a' -check 3 'a & b & c' -check 3 'a | b | (c U (d & (g U (h ^ i))))' -check 3 'Xa & (b U !a) & (b U !a)' -check 3 'Fa & Xb & GFc & Gd' -check 3 'Fa & Xa & GFc & Gc' -check 3 'Fc & X(a | Xb) & GF(a | Xb) & Gc' -check 3 'a R (b R c)' -check 3 '(a U b) U (c U d)' -check 3 '((Xp2)U(X(1)))&(p1 R(p2 R p0))' diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index c909fc21f..7157e87ec 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.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, 2012 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. +# 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. # @@ -150,22 +151,6 @@ Algorithm Enabled = no } -Algorithm -{ - Name = "Spot (Couvreur -- FM), post reduction with direct simulation" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -R1q -R1t -R3 -r4 -F -f -t'" - Enabled = yes -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM), post reduction with delayed simulation" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -R2q -R2t -F -f -t'" - Enabled = yes -} - Algorithm { Name = "Spot (Couvreur -- FM), post reduction with scc" @@ -174,14 +159,6 @@ Algorithm Enabled = yes } -Algorithm -{ - Name = "Spot (Couvreur -- FM), pre + post reduction" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r4 -R1q -R1t -R3 -F -f -t'" - Enabled = yes -} - Algorithm { Name = "Spot (Couvreur -- FM), +pre +WDBA" @@ -198,14 +175,6 @@ Algorithm Enabled = yes } -Algorithm -{ - Name = "Spot (Couvreur -- FM), pre + allpost reduction" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r4 -R1q -R1t -R2q -R2t -R3 -F -f -t'" - Enabled = no -} - Algorithm { Name = "Spot (Couvreur -- FM), without symb_merge" diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 64b0ad59f..6f24c98a4 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -96,7 +96,6 @@ #include "tgbaalgos/magic.hh" #include "tgbaalgos/minimize.hh" #include "tgbaalgos/neverclaim.hh" -#include "tgbaalgos/reductgba_sim.hh" #include "tgbaalgos/rundotdec.hh" #include "tgbaalgos/save.hh" #include "tgbaalgos/sccfilter.hh" @@ -180,7 +179,6 @@ using namespace spot; %feature("new") spot::ltl_to_tgba_lacim; %feature("new") spot::minimize_wdba; %feature("new") spot::minimize_monitor; -%feature("new") spot::reduc_tgba_sim; %feature("new") spot::scc_filter; %feature("new") spot::tgba_dupexp_bfs; %feature("new") spot::tgba_dupexp_dfs; @@ -226,7 +224,6 @@ using namespace spot; %include "tgbaalgos/magic.hh" %include "tgbaalgos/minimize.hh" %include "tgbaalgos/neverclaim.hh" -%include "tgbaalgos/reductgba_sim.hh" %include "tgbaalgos/rundotdec.hh" %include "tgbaalgos/save.hh" %include "tgbaalgos/sccfilter.hh"