diff --git a/ChangeLog b/ChangeLog index f7b2c0d3c..9188ddca4 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2004-07-02 Thomas Martinez + + * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh, + src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh, + src/tgbaalgos/reductgba_sim_del.cc: Remove some comments. + + * src/tgbatest/ltl2tgba.cc, src/tgbatest/reductgba.cc: Adjust ... + * src/tgbatest/spotlbtt.test: More test (delayed simulation) + 2004-06-29 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.0w. diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc index b6cfd889b..b10b41e2e 100644 --- a/src/tgba/tgbareduc.cc +++ b/src/tgba/tgbareduc.cc @@ -122,7 +122,6 @@ namespace spot if (!scc_computed_) this->compute_scc(); this->prune_acc(); - // FIXME this->delete_scc(); } @@ -144,26 +143,6 @@ namespace spot return i->second; } - int - tgba_reduc::get_nb_state() - { - return state_name_map_.size(); - } - - int - tgba_reduc::get_nb_transition() - { - int nb_transition = 0; - sn_map::iterator i; - for (i = state_name_map_.begin(); - i != state_name_map_.end(); ++i) - { - nb_transition += (i->first)->size(); - } - - return nb_transition; - } - //////////////////////////////////////////// void diff --git a/src/tgba/tgbareduc.hh b/src/tgba/tgbareduc.hh index d83208c6a..98cd97216 100644 --- a/src/tgba/tgbareduc.hh +++ b/src/tgba/tgbareduc.hh @@ -64,11 +64,7 @@ namespace spot /// Add the SCC index to the display of the state \a state. virtual std::string format_state(const spot::state* state) const; - /// Obsolete. - int get_nb_state(); - int get_nb_transition(); - - // Just for Debug !! + // For Debug void display_rel_sim(simulation_relation* rel, std::ostream& os); void display_scc(std::ostream& os); diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc index 04c918045..f9539382e 100644 --- a/src/tgbaalgos/reductgba_sim.cc +++ b/src/tgbaalgos/reductgba_sim.cc @@ -50,7 +50,6 @@ namespace spot bool spoiler_node::add_succ(spoiler_node* n) { - //std::cout << "spoiler_node::add_succ" << std::endl; bool exist = false; for (sn_v::iterator i = lnode_succ->begin(); i != lnode_succ->end(); ++i) @@ -84,15 +83,6 @@ namespace spot spoiler_node::add_pred(spoiler_node* n) { lnode_pred->push_back(n); - /* - 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 @@ -120,25 +110,10 @@ namespace spot return change != not_win; } - /* - bool - spoiler_node::set_win() - { - bool change = not_win; - for (Sgi::vector::iterator i = lnode_succ->begin(); - i != lnode_succ->end(); ++i) - { - not_win |= (*i)->not_win; - } - return change != not_win; - } - */ - std::string spoiler_node::to_string(const tgba* a) { std::ostringstream os; - // print the node. os << num_ << " [shape=box, label=\"(" << a->format_state(sc_->first) @@ -164,7 +139,6 @@ namespace spot 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)); } @@ -235,34 +209,10 @@ namespace spot return change != not_win; } - /* - bool - duplicator_node::set_win() - { - bool change = not_win; - - if (!this->get_nb_succ()) - not_win = true; - else - { - not_win = true; - for (Sgi::vector::iterator i = lnode_succ->begin(); - i != lnode_succ->end(); ++i) - { - not_win &= (*i)->not_win; - } - } - - return change != not_win; - } - */ - std::string duplicator_node::to_string(const tgba* a) { std::ostringstream os; - - // print the node. os << num_ << " [shape=box, label=\"(" << a->format_state(sc_->first) @@ -274,14 +224,12 @@ namespace spot bdd_print_acc(os, a->get_dict(), acc_); os << ")\"]" << std::endl; - 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())); @@ -591,216 +539,6 @@ namespace spot } } - /* - void - parity_game_graph_direct::build_couple() - { - // 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; - 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) - build_recurse_successor_spoiler(*j, os); - - } - - void - parity_game_graph_direct:: - build_recurse_successor_spoiler(spoiler_node* sn, - std::ostringstream& os) - { - //std::cout << os.str() << "build_recurse_successor_spoiler : begin" - //<< std::endl; - - tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node()); - - for (si->first(); !si->done(); si->next()) - { - - bdd btmp = 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) - { - delete s; - duplicator_node* dn - = add_duplicator_node(*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 - delete s; - } - } - - delete si; - - //std::cout << os.str() << "build_recurse_successor_spoiler : end" << - //std::endl; - } - - void - parity_game_graph_direct:: - build_recurse_successor_duplicator(duplicator_node* dn, - spoiler_node* , - std::ostringstream& os) - { - //std::cout << "build_recurse_successor_duplicator : begin" << std::endl; - - tgba_succ_iterator* si = automata_->succ_iter(dn->get_duplicator_node()); - - for (si->first(); !si->done(); si->next()) - { - - // if si->current_condition() doesn't implies sn->get_label() - // then duplicator can't play. - if ((!dn->get_label() | si->current_condition()) != 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) - { - delete s; - spoiler_node* sn_n - = add_spoiler_node(dn->get_spoiler_node(), - *i1, - 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 - delete s; - } - } - - delete si; - - //std::cout << os.str() << "build_recurse_successor_duplicator : end" - //<< std::endl; - } - - duplicator_node* - parity_game_graph_direct::add_duplicator_node(const spot::state* sn, - const spot::state* dn, - bdd acc, - bdd label, - int nb) - { - bool exist = false; - - duplicator_node* dn_n - = new duplicator_node(sn, dn, acc, label, nb); - - for (Sgi::vector::iterator i - = duplicator_vertice_.begin(); - i != duplicator_vertice_.end(); ++i) - { - if (dn_n->compare(*i)) - { - exist = true; - delete dn_n; - dn_n = *i; - break; - } - } - - if (!exist) - duplicator_vertice_.push_back(dn_n); - - return dn_n; - } - - spoiler_node* - parity_game_graph_direct::add_spoiler_node(const spot::state* sn, - const spot::state* dn, - int nb) - { - bool exist = false; - - spoiler_node* sn_n - = new spoiler_node(sn, dn, nb); - - for (Sgi::vector::iterator i - = spoiler_vertice_.begin(); - i != spoiler_vertice_.end(); ++i) - { - if (sn_n->compare(*i)) - { - exist = true; - delete sn_n; - sn_n = *i; - break; - } - } - - if (!exist) - spoiler_vertice_.push_back(sn_n); - - return sn_n; - } - */ - - /* - void - parity_game_graph_direct::lift() - { - for (Sgi::vector::iterator i - = spoiler_vertice_.begin(); - i != spoiler_vertice_.end(); ++i) - { - (*i)->set_win(); - } - } - */ - void parity_game_graph_direct::lift() { @@ -874,12 +612,14 @@ namespace spot /////////////////////////////////////////////////////////////////////// simulation_relation* - get_direct_relation_simulation(const tgba* f, int opt) + get_direct_relation_simulation(const tgba* f, + std::ostream& os, + int opt) { parity_game_graph_direct* G = new parity_game_graph_direct(f); simulation_relation* rel = G->get_relation(); if (opt == 1) - G->print(std::cout); + G->print(os); delete G; return rel; } @@ -931,7 +671,7 @@ namespace spot if (opt & Reduce_Dir_Sim) { simulation_relation* rel - = get_direct_relation_simulation(automatareduc); + = get_direct_relation_simulation(automatareduc, std::cout); automatareduc->display_rel_sim(rel, std::cout); automatareduc->prune_automata(rel); @@ -942,7 +682,7 @@ namespace spot if (opt & Reduce_Del_Sim) { simulation_relation* rel - = get_delayed_relation_simulation(automatareduc); + = get_delayed_relation_simulation(automatareduc, std::cout); automatareduc->display_rel_sim(rel, std::cout); automatareduc->prune_automata(rel); @@ -952,7 +692,6 @@ namespace spot if (opt & Reduce_Scc) { - automatareduc->compute_scc(); automatareduc->prune_scc(); } diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh index 5fab6ddbc..225e43265 100644 --- a/src/tgbaalgos/reductgba_sim.hh +++ b/src/tgbaalgos/reductgba_sim.hh @@ -58,21 +58,19 @@ namespace spot /// \brief Compute a direct simulation relation on state of tgba \a f. 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. - /// FIXME : this method is incorrect !! - /// Don't use it !! + // FIXME: This method is correct but she build sometime (when there are more + // than one acceptance condition) only a part of the simulation relation. simulation_relation* get_delayed_relation_simulation(const tgba* a, + std::ostream& os, int opt = -1); /// To free a simulation relation. void free_relation_simulation(simulation_relation* rel); - /// Test if the initial state of a2 fair simulate this of a1. - /// Not implemented. - bool is_include(const tgba* a1, const tgba* a2); - /////////////////////////////////////////////////////////////////////// // simulation. @@ -108,11 +106,6 @@ namespace spot /// \brief Compute each node of the graph. virtual void build_graph() = 0; - /// \brief Compute the link of the graph. - /// Successor of spoiler node (resp. duplicator node) - /// are duplicator node (resp. spoiler node). - //virtual void build_link() = 0; - /// \brief Remove edge from spoiler to duplicator that make /// duplicator loose. /// Spoiler node whose still have some link, reveal @@ -156,7 +149,6 @@ namespace spot protected: sn_v* lnode_succ; sn_v* lnode_pred; - //Sgi::vector* lnode_succ; state_couple* sc_; }; @@ -200,23 +192,6 @@ namespace spot virtual void lift(); void build_link(); - /* - private: - 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); - duplicator_node* add_duplicator_node(const spot::state* sn, - const spot::state* dn, - bdd acc, - bdd label, - int nb); - spoiler_node* add_spoiler_node(const spot::state* sn, - const spot::state* dn, - int nb); - */ - }; @@ -230,8 +205,7 @@ namespace spot spoiler_node_delayed(const state* d_node, const state* s_node, bdd a, - int num, - bool l2a = true); + int num); ~spoiler_node_delayed(); /// Return true if the progress_measure has changed. @@ -242,16 +216,16 @@ namespace spot int get_progress_measure() const; bool get_lead_2_acc_all(); - /* - void set_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. @@ -271,9 +245,12 @@ namespace spot bool implies_label(bdd l); bool implies_acc(bdd a); int get_progress_measure(); - bool get_lead_2_acc_all(); - void set_lead_2_acc_all(); + 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_; @@ -316,9 +293,6 @@ namespace spot /// Return the number of acceptance condition. int nb_set_acc_cond(); - /// Compute sub_set_acc_cond_; - void build_sub_set_acc_cond(); - /// duplicator_node_delayed* add_duplicator_node_delayed(const spot::state* sn, const spot::state* dn, @@ -332,21 +306,18 @@ namespace spot bdd acc, int nb); - /// \brief Compute the couple as for direct simulation, - virtual void build_graph(); - //virtual void build_link(); - 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(); - /// \brief Remove all node so as to there is no dead ends (terminal node). - //virtual void prune(); }; } diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc index 1816f227a..bc39a29c6 100644 --- a/src/tgbaalgos/reductgba_sim_del.cc +++ b/src/tgbaalgos/reductgba_sim_del.cc @@ -33,7 +33,13 @@ namespace spot static int nb_spoiler; static int nb_duplicator; - //static int nb_node; + static bdd all_acc_cond = bddfalse; + + static Sgi::vector bool_v; + + //static int nb_node = 0; + + //seen_map_node seen_node_; /////////////////////////////////////////////////////////////////////// // spoiler_node_delayed @@ -41,8 +47,7 @@ namespace spot spoiler_node_delayed::spoiler_node_delayed(const state* d_node, const state* s_node, bdd a, - int num, - bool l2a) + int num) : spoiler_node(d_node, s_node, num), acceptance_condition_visited_(a) { @@ -50,12 +55,16 @@ namespace spot progress_measure_ = 0; if (acceptance_condition_visited_ != bddfalse) nb_spoiler_loose_++; - lead_2_acc_all_ = l2a; + lead_2_acc_all_ = false; + + seen_ = false; + //seen_ = new bool(false); + //bool_v[nb_node++] = seen_; } spoiler_node_delayed::~spoiler_node_delayed() { - if (acceptance_condition_visited_ != bddfalse) + if (acceptance_condition_visited_ != bddfalse) nb_spoiler_loose_--; } @@ -76,11 +85,14 @@ namespace spot bool change; int tmpmax = 0; int tmp = 0; + int tmpmaxwin = -1; sn_v::iterator i = lnode_succ->begin(); if (i != lnode_succ->end()) { tmpmax = dynamic_cast(*i)->get_progress_measure(); + if (dynamic_cast(*i)->get_lead_2_acc_all()) + tmpmaxwin = tmpmax; ++i; } for (; i != lnode_succ->end(); ++i) @@ -89,8 +101,14 @@ namespace spot dynamic_cast(*i)->get_progress_measure(); if (tmp > tmpmax) tmpmax = tmp; + if (dynamic_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. @@ -136,8 +154,12 @@ namespace spot os << "ACC"; } os << ")" - << " pm = " << progress_measure_ << "\"]" - << std::endl; + << " pm = " << progress_measure_; + if (lead_2_acc_all_) + os << ", 1\"]"; + else + os << ", 0\"]"; + os << std::endl; return os.str(); } @@ -161,15 +183,31 @@ namespace spot bool spoiler_node_delayed::get_lead_2_acc_all() { + //std::cout << "spoiler_node_delayed::get_lead_2_acc_all" << std::endl; return lead_2_acc_all_; } - /* - void - spoiler_node_delayed::set_lead_2_acc_all() + + bool + spoiler_node_delayed::set_lead_2_acc_all(bdd acc) { + //std::cout << "spoiler_node_delayed::set_lead_2_acc_all" << std::endl; + if (!seen_) + { + seen_ = true; + for (sn_v::iterator i = lnode_succ->begin(); + i != lnode_succ->end(); ++i) + dynamic_cast(*i)->set_lead_2_acc_all(acc); + } + else + { + //seen_ = true; + if (acc == all_acc_cond) + lead_2_acc_all_ = true; + } + return lead_2_acc_all_; } - */ + /////////////////////////////////////////////////////////////////////// // duplicator_node_delayed @@ -183,6 +221,13 @@ namespace spot { nb_duplicator++; progress_measure_ = 0; + all_acc_cond |= a; + lead_2_acc_all_ = false; + + seen_ = false; + //seen_ = new bool(false); + //bool_v[nb_node++] = seen_; + } duplicator_node_delayed::~duplicator_node_delayed() @@ -239,8 +284,12 @@ namespace spot //<< ", "; //bdd_print_acc(os, a->get_dict(), acc_); os << ")" - << " pm = " << progress_measure_ << "\"]" - << std::endl; + << " pm = " << progress_measure_; + if (lead_2_acc_all_) + os << ", 1\"]"; + else + os << ", 0\"]"; + os << std::endl; return os.str(); } @@ -266,17 +315,24 @@ namespace spot bool duplicator_node_delayed::get_lead_2_acc_all() { + //std::cout << "duplicator_node_delayed::get_lead_2_acc_all" << std::endl; return lead_2_acc_all_; } - void - duplicator_node_delayed::set_lead_2_acc_all() + bool + duplicator_node_delayed::set_lead_2_acc_all(bdd acc) { - if (!lead_2_acc_all_) - for (sn_v::iterator i = lnode_succ->begin(); - i != lnode_succ->end(); ++i) - lead_2_acc_all_ - |= dynamic_cast(*i)->get_lead_2_acc_all(); + //std::cout << "duplicator_node_delayed::set_lead_2_acc_all" << std::endl; + acc |= acc_; + if (!seen_) + { + seen_ = true; + for (sn_v::iterator i = lnode_succ->begin(); + i != lnode_succ->end(); ++i) + lead_2_acc_all_ + |= dynamic_cast(*i)->set_lead_2_acc_all(acc); + } + return lead_2_acc_all_; } /////////////////////////////////////////////////////////////////////// @@ -297,252 +353,6 @@ namespace spot return count; } - void - parity_game_graph_delayed::build_sub_set_acc_cond() - { - // compute the number of acceptance conditions - bdd acc, all; - acc = all = automata_->all_acceptance_conditions(); - int count = 0; - while (all != bddfalse) - { - //std::cout << "add acc" << std::endl; - sub_set_acc_cond_.push_back(bdd_satone(all)); - all -= bdd_satone(all); - count++; - } - // sub_set_acc_cond_ contains all the acceptance condition. - // but we must have all the sub-set of acceptance condition. - // In fact we must have 2^count sub-set. - - if (count == 2) - { - sub_set_acc_cond_.push_back(acc); - sub_set_acc_cond_.push_back(bddfalse); - } - - /* - bdd_v::iterator i; - - bdd_v::iterator j; - for (i = sub_set_acc_cond_.begin(); i != sub_set_acc_cond_.end(); ++i) - for (j = sub_set_acc_cond_.begin(); j != sub_set_acc_cond_.end(); ++j) - sub_set_acc_cond_.push_back(*i | *j); - - std::cout << std::endl; - for (i = sub_set_acc_cond_.begin(); i != sub_set_acc_cond_.end();) - { - bdd_print_acc(std::cout, automata_->get_dict(), *i); - std::cout << " // " << std::endl; - ++i; - } - std::cout << std::endl; - */ - } - - /* - void - parity_game_graph_delayed::build_couple() - { - //std::cout << "build couple" << std::endl; - - nb_spoiler = 0; - nb_duplicator = 0; - - tgba_succ_iterator* si = 0; - typedef Sgi::pair couple_bdd; - couple_bdd *p = 0; - Sgi::vector* trans = 0; - bool exist = false; - spot::state* s = 0; - - s_v::iterator i; - for (i = tgba_state_.begin(); i != tgba_state_.end(); ++i) - { - - // for each sub-set of the set of acceptance condition. - bdd_v::iterator i2; - for (i2 = sub_set_acc_cond_.begin(); - i2 != sub_set_acc_cond_.end(); ++i2) - { - - // spoiler node are all state couple (i,j) - // multiply by 2^(|F|) - s_v::iterator i3; - for (i3 = tgba_state_.begin(); - i3 != tgba_state_.end(); ++i3) - { - //nb_spoiler++; - spoiler_node_delayed* n1 - = new spoiler_node_delayed(*i, - *i3, - *i2, - nb_node_parity_game++); - spoiler_vertice_.push_back(n1); - } - - // duplicator node are all state couple where - // the first state i are reachable. - trans = new Sgi::vector; - for (i3 = tgba_state_.begin(); - i3 != tgba_state_.end(); ++i3) - { - si = automata_->succ_iter(*i3); - 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; - Sgi::vector::iterator i4; - for (i4 = trans->begin(); - i4 != trans->end(); ++i4) - { - if ((si->current_condition() == (*i4)->first)) - // We don't need the acceptance condition - //&& - //(si->current_acceptance_conditions() - //== (*i4)->second)) - exist = true; - } - - if (!exist) - { - // We build all the state couple with the label p. - // multiply by 2^(|F|) - trans->push_back(p); - Sgi::vector::iterator i5; - for (i5 = tgba_state_.begin(); - i5 != tgba_state_.end(); ++i5) - { - //nb_duplicator++; - int nb = nb_node_parity_game++; - duplicator_node_delayed* n2 - = new - duplicator_node_delayed(*i, - *i5, - si-> - current_condition(), - *i2, - nb); - duplicator_vertice_.push_back(n2); - } - } - else - delete p; - } - delete s; - } - delete si; - } - Sgi::vector::iterator i6; - for (i6 = trans->begin(); i6 != trans->end(); ++i6) - { - delete *i6; - } - delete trans; - } - } - nb_spoiler_loose_++; - - //std::cout << "spoiler node : " << nb_spoiler << std::endl; - //std::cout << "duplicator node : " << nb_duplicator << std::endl; - //std::cout << "nb_spoiler_loose_ : " << nb_spoiler_loose_ << std::endl; - } - - void - parity_game_graph_delayed::build_link() - { - //std::cout << "build link" << std::endl; - int nb_ds = 0; - int nb_sd = 0; - spot::state* s = 0; - - // for each couple of (spoiler, duplicator) - sn_v::iterator i; - for (i = spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i) - { - dn_v::iterator i2; - for (i2 = duplicator_vertice_.begin(); - i2 != duplicator_vertice_.end(); ++i2) - { - - // We add a link between a duplicator and a spoiler. - if ((*i2)->get_spoiler_node()->compare((*i) - ->get_spoiler_node()) == 0) - { - tgba_succ_iterator* si - = automata_->succ_iter((*i2)->get_duplicator_node()); - for (si->first(); !si->done(); si->next()) - { - s = si->current_state(); - - bdd btmp2 = dynamic_cast(*i)-> - get_acceptance_condition_visited(); - bdd btmp = btmp2 - si->current_acceptance_conditions(); - - //if ((s->compare((*i)->get_duplicator_node()) == 0) && - //dynamic_cast(*i2)-> - // implies_label(si->current_condition()) && - //(btmp == btmp2)) - - if ((s->compare((*i)->get_duplicator_node()) == 0) && - dynamic_cast(*i2)-> - implies_label(si->current_condition()) && - (dynamic_cast(*i)-> - get_acceptance_condition_visited() != bddfalse)) - { - //std::cout << "add duplicator -> spoiler" << std::endl; - (*i2)->add_succ(*i); - (*i)->add_pred(*i2); - nb_ds++; - } - delete s; - } - delete si; - } - - // We add a link between a spoiler and a duplicator. - if ((*i2)->get_duplicator_node() - ->compare((*i)->get_duplicator_node()) == 0) - { - tgba_succ_iterator* si - = automata_->succ_iter((*i)->get_spoiler_node()); - for (si->first(); !si->done(); si->next()) - { - s = si->current_state(); - - bdd btmp = si->current_acceptance_conditions() | - dynamic_cast(*i)-> - get_acceptance_condition_visited(); - if ((s->compare((*i2)->get_spoiler_node()) == 0) && - (*i2)->match(si->current_condition(), btmp)) - { - //std::cout << "add spoiler -> duplicator" << std::endl; - (*i)->add_succ(*i2); - (*i2)->add_pred(*i); - nb_sd++; - } - delete s; - } - delete si; - } - - } - } - } - */ - // We build only node which are reachable void parity_game_graph_delayed::build_graph() @@ -577,16 +387,6 @@ namespace spot // The acc of the duplicator must contains the // acceptance_condition_visited_ of the spoiler. //std::cout << "build_link : iter " << ++n << std::endl; - - /* - std::cout << "[" - << automata_->format_state((*j)->get_spoiler_node()) - << "] // [" - << automata_->format_state((*j)->get_duplicator_node()) - << "]" - << std::endl; - */ - build_recurse_successor_spoiler(*j, os); } @@ -615,25 +415,6 @@ namespace spot dynamic_cast(sn)-> get_acceptance_condition_visited(); - - // If the spoiler node has witnessed an accepting condition, - // so we force to play on an arc which have a different accepting - // condition. => FALSE !!!!!! - /* - if ((dynamic_cast(sn)-> - get_acceptance_condition_visited() == - si->current_acceptance_conditions()) && - (si->current_acceptance_conditions() != bddfalse)) - continue; - */ - - /* - if (btmp == bddfalse) - std::cout << "btmp == bddfasle" << std::endl; - else - std::cout << "btmp != bddfasle" << std::endl; - */ - s_v::iterator i1; state* s; for (i1 = tgba_state_.begin(); @@ -675,23 +456,46 @@ namespace spot spoiler_node* , std::ostringstream& os) { - //std::cout << "build_recurse_successor_duplicator : begin" << std::endl; + /* + std::cout << os.str() << "build_recurse_successor_duplicator : begin" + << std::endl; + */ tgba_succ_iterator* si = automata_->succ_iter(dn->get_duplicator_node()); for (si->first(); !si->done(); si->next()) { - // if si->current_condition() doesn't implies sn->get_label() - // then duplicator can't play. - if ((!dn->get_label() | si->current_condition()) != bddtrue) - continue; - - // FIXME /* - bdd btmp = dn->get_acc(); - bdd btmp2 = btmp - (btmp & si->current_acceptance_conditions()); + std::cout << automata_->format_state(dn->get_spoiler_node()) + << std::endl; + std::cout << automata_->format_state(dn->get_duplicator_node()) + << std::endl; */ + + /* + bdd_print_acc(std::cout, + automata_->get_dict(), + si->current_condition()); + std::cout << " // "; + bdd_print_acc(std::cout, + automata_->get_dict(), + dn->get_label()); + std::cout << " // "; + bdd_print_acc(std::cout, + automata_->get_dict(), + si->current_condition() | !dn->get_label()); + std::cout << std::endl; + */ + + // if si->current_condition() doesn't implies dn->get_label() + // then duplicator can't play. + if ((si->current_condition() | !dn->get_label()) != bddtrue) + { + //std::cout << "doesn't implies" << std::endl; + continue; + } + bdd btmp = dn->get_acc() - (dn->get_acc() & si->current_acceptance_conditions()); @@ -725,8 +529,10 @@ namespace spot delete si; - //std::cout << os.str() << "build_recurse_successor_duplicator : end" - //<< std::endl; + /* + std::cout << os.str() << "build_recurse_successor_duplicator : end" + << std::endl; + */ } duplicator_node_delayed* @@ -770,7 +576,7 @@ namespace spot //bool l2a = (acc != automata_->all_acceptance_conditions()); spoiler_node_delayed* sn_n - = new spoiler_node_delayed(sn, dn, acc, nb, false); + = new spoiler_node_delayed(sn, dn, acc, nb); for (Sgi::vector::iterator i = spoiler_vertice_.begin(); @@ -791,79 +597,44 @@ namespace spot return sn_n; } - /* - void - parity_game_graph_delayed::prune() - { - - 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; - change = false; - for (Sgi::vector::iterator i - = duplicator_vertice_.begin(); - i != duplicator_vertice_.end();) - { - if ((*i)->get_nb_succ() == 0) - { - std::cout << "Remove duplicator" << std::endl; - (*i)->del_pred(); - delete *i; - i = duplicator_vertice_.erase(i); - change = true; - } - else - ++i; - } - for (Sgi::vector::iterator i - = spoiler_vertice_.begin(); - i != spoiler_vertice_.end();) - { - if ((*i)->get_nb_succ() == 0) - { - std::cout << "Remove spoiler" << std::endl; - (*i)->del_pred(); - delete *i; - i = spoiler_vertice_.erase(i); - change = true; - } - else - ++i; - } - } - 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 parity_game_graph_delayed::lift() { - // Before the lift we compute each vertices - // to know if he belong to a all accepting cycle - // of the graph. + // TEST of the hash_map of node + /* for (Sgi::vector::iterator i = duplicator_vertice_.begin(); i != duplicator_vertice_.end(); ++i) - { - if (dynamic_cast(*i)->get_lead_2_acc_all()) + seen_node_[*i] = 1; + + for (Sgi::vector::iterator i + = spoiler_vertice_.begin(); + i != spoiler_vertice_.end(); ++i) + seen_node_[*i] = 1; + */ + // + + + // Before the lift we compute each vertices + // to know if he belong to a all accepting cycle + // of the graph. + /* FIXME + if (this->nb_set_acc_cond() > 1) + for (Sgi::vector::iterator i + = duplicator_vertice_.begin(); + i != duplicator_vertice_.end(); ++i) + { + for (Sgi::vector::iterator i2 + = duplicator_vertice_.begin(); + i2 != duplicator_vertice_.end(); ++i2) + dynamic_cast(*i2)->seen_ = false; + for (Sgi::vector::iterator i3 + = spoiler_vertice_.begin(); + i3 != spoiler_vertice_.end(); ++i3) + dynamic_cast(*i3)->seen_ = false; dynamic_cast(*i)->set_lead_2_acc_all(); - } + } + */ // Jurdzinski's algorithm //int iter = 0; @@ -937,38 +708,24 @@ namespace spot return; */ - //this->build_sub_set_acc_cond(); //std::cout << "build couple" << std::endl; this->build_graph(); - //std::cout << "build link" << std::endl; - //this->build_link(); - //std::cout << "prune" << std::endl; - //this->prune(); - std::cout << "lift begin : " << nb_spoiler_loose_ << std::endl; + //std::cout << "lift begin : " << nb_spoiler_loose_ << std::endl; this->lift(); - std::cout << "lift end : " << nb_spoiler_loose_ << std::endl; + //std::cout << "lift end : " << nb_spoiler_loose_ << std::endl; //std::cout << "END" << std::endl; - //this->print(std::cout); } /////////////////////////////////////////// simulation_relation* - get_delayed_relation_simulation(const tgba* f, int opt) + get_delayed_relation_simulation(const tgba* f, std::ostream& os, int opt) { - /// 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) - G->print(std::cout); + G->print(os); delete G; - return rel; - - /* - return get_direct_relation_simulation(f, opt); - */ - } } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index d846678c7..37677c31f 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -98,6 +98,8 @@ syntax(char* prog) << std::endl << " -Rd to display simulation relation" << std::endl + << " -RD to display parity game (dot format)" + << std::endl << " -s convert to explicit automata, and number states " << "in DFS order" << std::endl << " -S convert to explicit automata, and number states " @@ -138,6 +140,7 @@ main(int argc, char** argv) int redopt = spot::ltl::Reduce_None; bool display_reduce_form = false; bool display_rel_sim = false; + bool display_parity_game = false; bool post_branching = false; bool fair_loop_approx = false; @@ -257,6 +260,30 @@ main(int argc, char** argv) { output = 3; } + else if (!strcmp(argv[formula_index], "-R1")) + { + reduc_aut |= spot::Reduce_Dir_Sim; + } + else if (!strcmp(argv[formula_index], "-R2")) + { + reduc_aut |= spot::Reduce_Del_Sim; + } + else if (!strcmp(argv[formula_index], "-R3")) + { + reduc_aut |= spot::Reduce_Scc; + } + else if (!strcmp(argv[formula_index], "-rd")) + { + 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], "-s")) { dupexp = DFS; @@ -291,26 +318,6 @@ main(int argc, char** argv) fm_opt = true; fm_symb_merge_opt = false; } - else if (!strcmp(argv[formula_index], "-R1")) - { - reduc_aut |= spot::Reduce_Dir_Sim; - } - else if (!strcmp(argv[formula_index], "-R2")) - { - reduc_aut |= spot::Reduce_Del_Sim; - } - else if (!strcmp(argv[formula_index], "-R3")) - { - reduc_aut |= spot::Reduce_Scc; - } - else if (!strcmp(argv[formula_index], "-rd")) - { - display_reduce_form = true; - } - else if (!strcmp(argv[formula_index], "-Rd")) - { - display_rel_sim = true; - } else { break; @@ -399,14 +406,22 @@ main(int argc, char** argv) if (reduc_aut != spot::Reduce_None) { a = aut_red = new spot::tgba_reduc(a); + + if (reduc_aut & spot::Reduce_Scc) + aut_red->prune_scc(); + if ((reduc_aut & spot::Reduce_Dir_Sim) || (reduc_aut & spot::Reduce_Del_Sim)) { spot::simulation_relation* rel; if (reduc_aut & spot::Reduce_Dir_Sim) - rel = spot::get_direct_relation_simulation(a); + rel = spot::get_direct_relation_simulation(a, + std::cout, + display_parity_game); else if (reduc_aut & spot::Reduce_Del_Sim) - rel = spot::get_delayed_relation_simulation(a); + rel = spot::get_delayed_relation_simulation(a, + std::cout, + display_parity_game); else assert(0); @@ -422,9 +437,6 @@ main(int argc, char** argv) spot::free_relation_simulation(rel); } - - if (reduc_aut & spot::Reduce_Scc) - aut_red->prune_scc(); } spot::tgba_explicit* expl = 0; diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc index 8bcf7a312..c6a61b4b5 100644 --- a/src/tgbatest/reductgba.cc +++ b/src/tgbatest/reductgba.cc @@ -112,12 +112,12 @@ main(int argc, char** argv) if (o & spot::Reduce_Dir_Sim) { - rel = spot::get_direct_relation_simulation(automatareduc); + rel = spot::get_direct_relation_simulation(automatareduc, std::cout); automatareduc->prune_automata(rel); } else if (o & spot::Reduce_Del_Sim) { - rel = spot::get_delayed_relation_simulation(automatareduc); + rel = spot::get_delayed_relation_simulation(automatareduc, std::cout); automatareduc->quotient_state(rel); } diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 660ff163b..79c327319 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -98,6 +98,13 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM), post reduction with delayed simulation" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -R2 -F -f -t'" + Enabled = yes +} + Algorithm { Name = "Spot (Couvreur -- FM), post reduction with scc"