diff --git a/ChangeLog b/ChangeLog index bd5870387..9bd3d6a85 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2004-06-22 Thomas Martinez + + * src/tgbatest/ltl2tgba.cc, src/tgbaalgos/reductgba_sim_del.cc, + src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc: + bug in delayed simulation. + + * src/tgbatest/reduccmp.test, src/tgbatest/reductgba.test, + src/tgba/tgbareduc.cc: bug in scc reduction. + 2004-06-21 Thomas Martinez * src/tgbatest/reductgba.test, src/tgba/tgbareduc.cc: diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc index abd2267ea..4fd5e9e6a 100644 --- a/src/tgba/tgbareduc.cc +++ b/src/tgba/tgbareduc.cc @@ -121,7 +121,8 @@ namespace spot { if (!scc_computed_) this->compute_scc(); - this->delete_scc(); + // FIXME + // this->delete_scc(); } std::string @@ -334,7 +335,7 @@ namespace spot name_state_map_[tgba_explicit::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::iterator j = st->begin(); j != st->end(); ++j) this->remove_predecessor_state((*j)->dest, st); @@ -591,6 +592,8 @@ namespace spot state_scc_v_.erase(i); break; } + //else + delete s; std::cout << "end is_terminal" << std::endl; } } diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc index 59fa4d68c..6e4f309ee 100644 --- a/src/tgbaalgos/reductgba_sim.cc +++ b/src/tgbaalgos/reductgba_sim.cc @@ -35,7 +35,7 @@ namespace spot sc_ = new state_couple(d_node, s_node); lnode_succ = new sn_v; lnode_pred = new sn_v; - this->not_win = false; + not_win = false; } spoiler_node::~spoiler_node() @@ -50,15 +50,27 @@ namespace spot bool spoiler_node::add_succ(spoiler_node* n) { - /* - bool exist = false; - for (sn_v::iterator i = lnode_succ->begin(); - i != lnode_succ->end();) + //std::cout << "spoiler_node::add_succ" << std::endl; + bool exist = false; + for (sn_v::iterator i = lnode_succ->begin(); + i != lnode_succ->end(); ++i) + // Be careful, we have to compare two duplicator node if (*i == n) - exist = true; - if (exist) + exist = true; + if (exist) + return false; + // TO TEST FOR THE DIRECT SIMULATION // + /* + bool exist = false; + for (sn_v::iterator i = lnode_succ->begin(); + i != lnode_succ->end(); ++i) + // Be careful, we have to compare two duplicator node + if (dynamic_cast(*i)->compare(n) == 0) + exist = true; + if (exist) return false; */ + /////////////// lnode_succ->push_back(n); return true; } @@ -81,15 +93,15 @@ namespace spot void spoiler_node::add_pred(spoiler_node* n) { - /* - bool exist = false; - for (sn_v::iterator i = lnode_pred->begin(); - i != lnode_pred->end();) - if (*i == n) - exist = true; - if (!exist) - */ - lnode_pred->push_back(n); + // TO TEST FOR THE DIRECT SIMULATION // + bool exist = false; + for (sn_v::iterator i = lnode_pred->begin(); + i != lnode_pred->end(); ++i) + if ((*i)->compare(n) == 0) + exist = true; + if (!exist) + /////////////// + lnode_pred->push_back(n); } void @@ -139,6 +151,14 @@ namespace spot return os.str(); } + bool + spoiler_node::compare(spoiler_node* n) + { + //std::cout << "spoiler_node::compare" << std::endl; + return (((sc_->first)->compare((n->get_pair())->first) == 0) && + ((sc_->second)->compare((n->get_pair())->second) == 0)); + } + int spoiler_node::get_nb_succ() { @@ -197,6 +217,7 @@ namespace spot not_win &= (*i)->not_win; } } + return (change != not_win); } @@ -212,6 +233,8 @@ namespace spot << ", " << 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; @@ -219,6 +242,27 @@ namespace spot return os.str(); } + bool + duplicator_node::compare(spoiler_node* n) + { + //std::cout << "duplicator_node::compare" << std::endl; + return (this->spoiler_node::compare(n) && + (label_ == dynamic_cast(n)->get_label()) && + (acc_ == dynamic_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) { @@ -552,7 +596,7 @@ namespace spot // We remove the state in rel from seen // because the destructor of // tgba_reachable_iterator_breadth_first - // delete all the state. + // delete all instance of state. if ((j = seen.find(p->first)) != seen.end()) diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh index 27056bf39..609ae2928 100644 --- a/src/tgbaalgos/reductgba_sim.hh +++ b/src/tgbaalgos/reductgba_sim.hh @@ -144,6 +144,7 @@ namespace spot 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(); @@ -172,10 +173,14 @@ namespace spot 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_; @@ -213,11 +218,12 @@ namespace spot /// Return true if the progress_measure has changed. bool set_win(); - bdd get_acceptance_condition_visited(); + bdd get_acceptance_condition_visited() const; + virtual bool compare(spoiler_node* n); virtual std::string to_string(const tgba* a); - int get_progress_measure(); + int get_progress_measure() const; protected: /// a Bdd for retain all the acceptance condition @@ -291,13 +297,18 @@ namespace spot /// Compute sub_set_acc_cond_; void build_sub_set_acc_cond(); - /// Add a duplicator node, and - /// all his successor (spoiler node) which - /// have a acceptance_condition_visited_ != bddfalse - void add_dup_node(state* ss, - state* sd, - bdd l, - bdd a); + /// + 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); /// \brief Compute the couple as for direct simulation, virtual void build_couple(); diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc index 06ec835f6..35002e8c8 100644 --- a/src/tgbaalgos/reductgba_sim_del.cc +++ b/src/tgbaalgos/reductgba_sim_del.cc @@ -99,6 +99,16 @@ namespace spot return change; } + bool + spoiler_node_delayed::compare(spoiler_node* n) + { + std::cout << "spoiler_node_delayed::compare" << std::endl; + return (this->spoiler_node::compare(n) && + (acceptance_condition_visited_ == + dynamic_cast(n)-> + get_acceptance_condition_visited())); + } + std::string spoiler_node_delayed::to_string(const tgba* a) { @@ -128,13 +138,13 @@ namespace spot } bdd - spoiler_node_delayed::get_acceptance_condition_visited() + spoiler_node_delayed::get_acceptance_condition_visited() const { return acceptance_condition_visited_; } int - spoiler_node_delayed::get_progress_measure() + spoiler_node_delayed::get_progress_measure() const { if ((acceptance_condition_visited_ == bddfalse) && (progress_measure_ != (nb_spoiler_loose_ + 1))) @@ -180,7 +190,8 @@ namespace spot sn_v::iterator i = lnode_succ->begin(); if (i != lnode_succ->end()) { - tmpmin = dynamic_cast(*i)->get_progress_measure(); + tmpmin = + dynamic_cast(*i)->get_progress_measure(); /* debug &= (dynamic_cast(*i) ->get_acceptance_condition_visited() @@ -550,6 +561,7 @@ namespace spot //bool exist_pred = false; sn_v::iterator i1; + int n = 0; for (i1 = spoiler_vertice_.begin(); i1 != spoiler_vertice_.end(); ++i1) { /* @@ -584,6 +596,7 @@ namespace spot // 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(*i1); } @@ -615,16 +628,21 @@ namespace spot if (s->compare(*i1) == 0) { duplicator_node_delayed* dn - = new duplicator_node_delayed(*i1, + = add_duplicator_node_delayed(*i1, sn->get_duplicator_node(), si->current_condition(), btmp, nb_node_parity_game++); - duplicator_vertice_.push_back(dn); // dn is already a successor of sn. + std::cout << "spoiler call add_succ" << std::endl; if (!(sn->add_succ(dn))) - continue; + { + std::cout << "dn is already a successor of sn." + << std::endl; + continue; + } + std::cout << "dn is a new successor of sn." << std::endl; (dn)->add_pred(sn); /* TEST @@ -662,6 +680,11 @@ namespace spot get_acceptance_condition_visited(); bdd btmp2 = btmp - si->current_acceptance_conditions(); + /* + if (btmp2 == bddfalse) + continue; + */ + s_v::iterator i1; state* s; for (i1 = tgba_state_.begin(); @@ -671,15 +694,20 @@ namespace spot if (s->compare(*i1) == 0) { spoiler_node_delayed* sn_n - = new spoiler_node_delayed(sn->get_spoiler_node(), + = add_spoiler_node_delayed(sn->get_spoiler_node(), *i1, btmp2, nb_node_parity_game++); - spoiler_vertice_.push_back(sn_n); - // dn is already a successor of sn. + // sn_n is already a successor of dn. + std::cout << "duplicator call add_succ" << std::endl; if (!(dn->add_succ(sn_n))) - continue; + { + std::cout << "sn_n is already a successor of dn." + << std::endl; + continue; + } + std::cout << "sn_n is a new successor of dn." << std::endl; (sn_n)->add_pred(dn); build_recurse_successor_spoiler(sn_n); @@ -693,13 +721,67 @@ namespace spot } - - void - parity_game_graph_delayed::add_dup_node(state*, - state*, - bdd, - bdd) + 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 (Sgi::vector::iterator i + = duplicator_vertice_.begin(); + i != duplicator_vertice_.end(); ++i) + { + std::cout << "COMPARE" << std::endl; + if (dn_n->compare(*i)) + { + exist = true; + delete dn_n; + dn_n = dynamic_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; + + spoiler_node_delayed* sn_n + = new spoiler_node_delayed(sn, dn, acc, nb); + + for (Sgi::vector::iterator i + = spoiler_vertice_.begin(); + i != spoiler_vertice_.end(); ++i) + { + std::cout << "COMPARE" << std::endl; + if (sn_n->compare(*i)) + { + exist = true; + delete sn_n; + sn_n = dynamic_cast(*i); + break; + } + } + + if (!exist) + spoiler_vertice_.push_back(sn_n); + + return sn_n; } void @@ -708,6 +790,13 @@ namespace spot bool change = true; + std::cout << "prune : nb spoiler : " + << spoiler_vertice_.size() + << std::endl + << "prune : nb duplicator : " + << duplicator_vertice_.size() + << std::endl; + while (change) { std::cout << "prune::change = true" << std::endl; @@ -718,6 +807,7 @@ namespace spot { if ((*i)->get_nb_succ() == 0) { + std::cout << "Remove duplicator" << std::endl; (*i)->del_pred(); delete *i; i = duplicator_vertice_.erase(i); @@ -732,6 +822,7 @@ namespace spot { if ((*i)->get_nb_succ() == 0) { + std::cout << "Remove spoiler" << std::endl; (*i)->del_pred(); delete *i; i = spoiler_vertice_.erase(i); @@ -742,6 +833,13 @@ namespace spot } } std::cout << "prune::change = false" << std::endl; + + std::cout << "prune : nb spoiler : " + << spoiler_vertice_.size() + << std::endl + << "prune : nb duplicator : " + << duplicator_vertice_.size() + << std::endl; } void @@ -836,12 +934,15 @@ namespace spot { /// FIXME : this method is incorrect !! /// Don't use it !! - parity_game_graph_delayed* G = new parity_game_graph_delayed(f); - simulation_relation* rel = G->get_relation(); - if (opt == 1) + /* + parity_game_graph_delayed* G = new parity_game_graph_delayed(f); + simulation_relation* rel = G->get_relation(); + if (opt == 1) G->print(std::cout); - delete G; - return rel; + delete G; + */ + + return get_direct_relation_simulation(f, opt); } } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 9a700a972..700c2e86d 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -404,7 +404,7 @@ main(int argc, char** argv) if (reduc_aut & spot::Reduce_Dir_Sim) rel = spot::get_direct_relation_simulation(a); else if (reduc_aut & spot::Reduce_Del_Sim) - rel = spot::get_delayed_relation_simulation(a, 1); + rel = spot::get_delayed_relation_simulation(a); else assert(0); diff --git a/src/tgbatest/reduccmp.test b/src/tgbatest/reduccmp.test index d471e609b..67c13624c 100755 --- a/src/tgbatest/reduccmp.test +++ b/src/tgbatest/reduccmp.test @@ -23,9 +23,6 @@ . ./defs -# FIXME -exit 0 - set -e cat >input < tmp_ && mv tmp_ stdout diff --git a/src/tgbatest/reductgba.test b/src/tgbatest/reductgba.test index db79310ea..52f33d14e 100755 --- a/src/tgbatest/reductgba.test +++ b/src/tgbatest/reductgba.test @@ -21,7 +21,7 @@ # 02111-1307, USA. -#. ./defs +. ./defs set -e @@ -34,22 +34,22 @@ check() # We don't check the output, but just running these might be enough to # trigger assertions. -#check 0 'Fa & Xb & GFc & Gd' -#check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc' +check 0 'Fa & Xb & GFc & Gd' +check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc' -#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 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))' # No reduction check 1 a @@ -66,22 +66,22 @@ check 1 '(a U b) U (c U d)' check 1 '((Xp2)U(X(1)))*(p1 R(p2 R p0))' #reduction -#check 1 'a U Fb' +check 1 'a U Fb' -#check 3 a -#check 3 'a U b' -#check 3 'a U Fb' +check 3 a +check 3 'a U b' +check 3 'a U Fb' -#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))' +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))'