diff --git a/ChangeLog b/ChangeLog index 0e1d4336f..c9e21295c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2004-06-22 Thomas Martinez + + * src/ltlvisit/reducform.cc, src/tgba/tgbareduc.cc, + src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh + src/tgbaalgos/reductgba_sim_del.cc, src/tgbatest/reduccmp.test, + src/tgbatest/reductgba.cc: 80 columns and style. + 2004-06-22 Alexandre Duret-Lutz * src/sanity/style.test: Typo. diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc index 47c15cab2..599608271 100644 --- a/src/ltlvisit/reducform.cc +++ b/src/ltlvisit/reducform.cc @@ -202,7 +202,7 @@ namespace spot if (opt_ & Reduce_Syntactic_Implications) { - bool removed = true;; + bool removed = true; multop::vec::iterator f1; multop::vec::iterator f2; @@ -229,7 +229,7 @@ namespace spot } else if ((syntactic_implication(*f2, *f1) && // f2 < f1 (mo->op() == multop::Or)) || - ((syntactic_implication(*f1,* f2)) && // f1 < f2 + ((syntactic_implication(*f1, *f2)) && // f1 < f2 (mo->op() == multop::And))) { // We keep f1 diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc index 4fd5e9e6a..976a1fa50 100644 --- a/src/tgba/tgbareduc.cc +++ b/src/tgba/tgbareduc.cc @@ -40,7 +40,7 @@ namespace spot run(); all_acceptance_conditions_ = a->all_acceptance_conditions(); all_acceptance_conditions_computed_ = true; - seen_ = NULL; + seen_ = 0; scc_computed_ = false; } @@ -355,7 +355,7 @@ namespace spot if ((*j)->dest == st) { // Remove the transition - delete(*j); + delete *j; j = (*p)->erase(j); ++j; } @@ -623,10 +623,10 @@ namespace spot { acc_ = bddfalse; b = true; - assert(seen_ == NULL); + assert(seen_ == 0); seen_ = new seen_map(); i = si_.find(s); - assert(i->first != NULL); + assert(i->first != 0); n = i->second; } /////////////////////////////// @@ -685,8 +685,8 @@ namespace spot seen_->clear(); std::cout << "delete seen_" << std::endl; delete seen_; - std::cout << "seen_ = NULL" << std::endl; - seen_ = NULL; + std::cout << "seen_ = 0" << std::endl; + seen_ = 0; std::cout << "acc_ == this->all_acceptance_conditions()" << std::endl; if (acc_ == this->all_acceptance_conditions()) ret = false; @@ -724,8 +724,8 @@ namespace spot { if (n == -1) { - assert(seen_ == NULL); - seen_ = new seen_map();; + assert(seen_ == 0); + seen_ = new seen_map(); } seen_map::const_iterator sm = seen_->find(s); @@ -744,7 +744,7 @@ namespace spot if (n == -1) { delete seen_; - seen_ = NULL; + seen_ = 0; } } @@ -764,10 +764,10 @@ namespace spot { acc_ == bddfalse; b = true; - assert(seen_ == NULL); + assert(seen_ == 0); seen_ = new seen_map(); i = si_.find(s); - assert(i->first != NULL); + assert(i->first != 0); n = i->second; } @@ -796,7 +796,7 @@ namespace spot if (b) { delete seen_; - seen_ = NULL; + seen_ = 0; if (acc_ == this->all_acceptance_conditions()) ret = false; } diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc index 6e4f309ee..21f52e738 100644 --- a/src/tgbaalgos/reductgba_sim.cc +++ b/src/tgbaalgos/reductgba_sim.cc @@ -54,23 +54,11 @@ namespace spot 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) + if ((*i)->compare(n) == true) 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; } @@ -93,14 +81,12 @@ namespace spot void spoiler_node::add_pred(spoiler_node* 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); } @@ -121,7 +107,7 @@ namespace spot { not_win |= (*i)->not_win; } - return (change != not_win); + return change != not_win; } std::string @@ -218,7 +204,7 @@ namespace spot } } - return (change != not_win); + return change != not_win; } std::string @@ -407,12 +393,12 @@ namespace spot void parity_game_graph_direct::build_couple() { - tgba_succ_iterator* si = NULL; + tgba_succ_iterator* si = 0; typedef Sgi::pair couple_bdd; - couple_bdd *p = NULL; - Sgi::vector* trans = NULL; + couple_bdd *p = 0; + Sgi::vector* trans = 0; bool exist = false; - spot::state* s = NULL; + spot::state* s = 0; for (Sgi::vector::iterator i = tgba_state_.begin(); i != tgba_state_.end(); ++i) @@ -469,11 +455,13 @@ namespace spot s != tgba_state_.end(); ++s) { duplicator_node* n2 - = new duplicator_node(*i, - *s, - si->current_condition(), - si->current_acceptance_conditions(), - nb_node_parity_game++); + = new + duplicator_node(*i, + *s, + si->current_condition(), + si + ->current_acceptance_conditions(), + nb_node_parity_game++); duplicator_vertice_.push_back(n2); } } @@ -498,7 +486,7 @@ namespace spot { int nb_ds = 0; int nb_sd = 0; - spot::state* s = NULL; + spot::state* s = 0; // for each couple of (spoiler, duplicator) for (Sgi::vector::iterator i @@ -509,7 +497,8 @@ namespace spot 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) + if ((*j)->get_spoiler_node() + ->compare((*i)->get_spoiler_node()) == 0) { tgba_succ_iterator* si = automata_->succ_iter((*j)->get_duplicator_node()); @@ -529,7 +518,8 @@ namespace spot } // We add a link between a spoiler and a duplicator. - if ((*j)->get_duplicator_node()->compare((*i)->get_duplicator_node()) == 0) + if ((*j)->get_duplicator_node() + ->compare((*i)->get_duplicator_node()) == 0) { tgba_succ_iterator* si = automata_->succ_iter((*i)->get_spoiler_node()); @@ -579,7 +569,7 @@ namespace spot parity_game_graph_direct::get_relation() { simulation_relation* rel = new simulation_relation(); - state_couple* p = NULL; + state_couple* p = 0; seen_map::iterator j; for (Sgi::vector::iterator i @@ -638,7 +628,7 @@ namespace spot void free_relation_simulation(simulation_relation* rel) { - if (rel == NULL) + if (rel == 0) return; Sgi::hash_mapfirst; ++j; - delete(ptr); + delete ptr; } } diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh index 609ae2928..7f34d0cc5 100644 --- a/src/tgbaalgos/reductgba_sim.hh +++ b/src/tgbaalgos/reductgba_sim.hh @@ -63,7 +63,7 @@ namespace spot /// Compute a delayed simulation relation on state of tgba \a f. /// FIXME : this method is incorrect !! /// Don't use it !! - simulation_relation* get_delayed_relation_simulation(const tgba* a, + simulation_relation* get_delayed_relation_simulation(const tgba* a, int opt = -1); /// To free a simulation relation. diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc index 35002e8c8..b4edc85ed 100644 --- a/src/tgbaalgos/reductgba_sim_del.cc +++ b/src/tgbaalgos/reductgba_sim_del.cc @@ -331,12 +331,12 @@ namespace spot nb_spoiler = 0; nb_duplicator = 0; - tgba_succ_iterator* si = NULL; + tgba_succ_iterator* si = 0; typedef Sgi::pair couple_bdd; - couple_bdd *p = NULL; - Sgi::vector* trans = NULL; + couple_bdd *p = 0; + Sgi::vector* trans = 0; bool exist = false; - spot::state* s = NULL; + spot::state* s = 0; s_v::iterator i; for (i = tgba_state_.begin(); i != tgba_state_.end(); ++i) @@ -448,7 +448,7 @@ namespace spot //std::cout << "build link" << std::endl; int nb_ds = 0; int nb_sd = 0; - spot::state* s = NULL; + spot::state* s = 0; // for each couple of (spoiler, duplicator) sn_v::iterator i; @@ -557,7 +557,7 @@ namespace spot // We create when it's possible a duplicator node // and recursively his successor. - //spot::state* s1 = NULL; + //spot::state* s1 = 0; //bool exist_pred = false; sn_v::iterator i1; @@ -574,7 +574,7 @@ namespace spot { tgba_succ_iterator* si; s_v::iterator i2; - spot::state* s2 = NULL; + spot::state* s2 = 0; for (i2 = tgba_state_.begin(); i2 != tgba_state_.end(); ++i2) { @@ -634,10 +634,10 @@ namespace spot btmp, nb_node_parity_game++); - // dn is already a successor of sn. std::cout << "spoiler call add_succ" << std::endl; if (!(sn->add_succ(dn))) { + // dn is already a successor of sn. std::cout << "dn is already a successor of sn." << std::endl; continue; @@ -645,12 +645,6 @@ namespace spot std::cout << "dn is a new successor of sn." << std::endl; (dn)->add_pred(sn); - /* TEST - bdd btmp2 = - dynamic_cast(sn)-> - get_acceptance_condition_visited(); - */ - build_recurse_successor_duplicator(dn, sn); } delete s; @@ -664,7 +658,7 @@ namespace spot void parity_game_graph_delayed:: build_recurse_successor_duplicator(duplicator_node* dn, - spoiler_node* sn) + spoiler_node*) { std::cout << "build_recurse_successor_duplicator" << std::endl; @@ -675,9 +669,13 @@ namespace spot { std::cout << "transition " << i++ << std::endl; + /* bdd btmp = dynamic_cast(sn)-> get_acceptance_condition_visited(); + */ + + bdd btmp = dn->get_acc(); bdd btmp2 = btmp - si->current_acceptance_conditions(); /* @@ -694,7 +692,7 @@ namespace spot if (s->compare(*i1) == 0) { spoiler_node_delayed* sn_n - = add_spoiler_node_delayed(sn->get_spoiler_node(), + = add_spoiler_node_delayed(dn->get_spoiler_node(), *i1, btmp2, nb_node_parity_game++); @@ -737,7 +735,7 @@ namespace spot = duplicator_vertice_.begin(); i != duplicator_vertice_.end(); ++i) { - std::cout << "COMPARE" << std::endl; + //std::cout << "COMPARE" << std::endl; if (dn_n->compare(*i)) { exist = true; @@ -768,7 +766,7 @@ namespace spot = spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i) { - std::cout << "COMPARE" << std::endl; + //std::cout << "COMPARE" << std::endl; if (sn_n->compare(*i)) { exist = true; @@ -873,7 +871,7 @@ namespace spot parity_game_graph_delayed::get_relation() { simulation_relation* rel = new simulation_relation(); - state_couple* p = NULL; + state_couple* p = 0; seen_map::iterator j; for (Sgi::vector::iterator i @@ -922,7 +920,7 @@ namespace spot this->build_link(); std::cout << "prune" << std::endl; this->prune(); - std::cout << "lift" << std::endl; + std::cout << "lift : " << nb_spoiler_loose_ << std::endl; this->lift(); std::cout << "END" << std::endl; //this->print(std::cout); @@ -934,15 +932,18 @@ 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) || (opt == -1)) G->print(std::cout); - delete G; + delete G; + + return rel; + + /* + return get_direct_relation_simulation(f, opt); */ - return get_direct_relation_simulation(f, opt); } } diff --git a/src/tgbatest/reduccmp.test b/src/tgbatest/reduccmp.test index 67c13624c..f27d52261 100755 --- a/src/tgbatest/reduccmp.test +++ b/src/tgbatest/reduccmp.test @@ -43,6 +43,8 @@ digraph G { } EOF +rm input stdout expected + # FIXME exit 0 @@ -50,5 +52,3 @@ exit 0 # (The order is not guaranteed by SPOT.) sed 's/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout diff stdout expected - -#rm input stdout expected diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc index cb68bd5f4..08815cad4 100644 --- a/src/tgbatest/reductgba.cc +++ b/src/tgbatest/reductgba.cc @@ -85,9 +85,9 @@ main(int argc, char** argv) } int exit_code = 0; - spot::simulation_relation* rel = NULL; - spot::tgba* automata = NULL; - spot::tgba_reduc* automatareduc = NULL; + spot::simulation_relation* rel = 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(); @@ -121,7 +121,7 @@ main(int argc, char** argv) automatareduc->quotient_state(rel); } - if (rel != NULL) + if (rel != 0) { automatareduc->display_rel_sim(rel, std::cout); spot::free_relation_simulation(rel); @@ -133,17 +133,17 @@ main(int argc, char** argv) //automatareduc->display_scc(std::cout); } - if (automatareduc != NULL) + if (automatareduc != 0) { spot::dotty_reachable(std::cout, automatareduc); } - if (automata != NULL) + if (automata != 0) delete automata; - if (automatareduc != NULL) + if (automatareduc != 0) delete automatareduc; #ifndef REDUCCMP - if (f != NULL) + if (f != 0) spot::ltl::destroy(f); #endif @@ -152,7 +152,7 @@ main(int argc, char** argv) assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); - if (dict != NULL) + if (dict != 0) delete dict; return exit_code;