From 21c98c0a01761626184673eac548a6064bc9725b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 14 Apr 2008 11:35:57 +0200 Subject: [PATCH] Kill some FIXMEs. * src/ltlenv/environment.hh, src/ltlvisit/basicreduce.cc: Remove useless FIXMEs. * src/ltlvisit/reduce.cc (reduce_visitor::visit(binop)): Compute syntactic implications only when needed. * src/tgbaalgos/reductgba_sim_del.cc (build_recurse_successor_spoiler): Remplace the FIXME by an assert. * src/tgba/tgbareduc.cc: Reword some comments, discard old commented code. --- ChangeLog | 13 +++ src/ltlenv/environment.hh | 9 +- src/ltlvisit/basicreduce.cc | 5 +- src/ltlvisit/reduce.cc | 19 ++-- src/tgba/tgbareduc.cc | 151 ++++------------------------- src/tgbaalgos/reductgba_sim_del.cc | 6 +- 6 files changed, 47 insertions(+), 156 deletions(-) diff --git a/ChangeLog b/ChangeLog index 13a16b17d..12a5dbd30 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2008-04-14 Alexandre Duret-Lutz + + Kill some FIXMEs. + + * src/ltlenv/environment.hh, src/ltlvisit/basicreduce.cc: Remove + useless FIXMEs. + * src/ltlvisit/reduce.cc (reduce_visitor::visit(binop)): Compute + syntactic implications only when needed. + * src/tgbaalgos/reductgba_sim_del.cc + (build_recurse_successor_spoiler): Remplace the FIXME by an assert. + * src/tgba/tgbareduc.cc: Reword some comments, discard old + commented code. + 2008-03-28 Alexandre Duret-Lutz * src/evtgbaparse/Makefile.am (AM_CXXFLAGS): Remove -Werror diff --git a/src/ltlenv/environment.hh b/src/ltlenv/environment.hh index ba19cde51..6dd6d8f32 100644 --- a/src/ltlenv/environment.hh +++ b/src/ltlenv/environment.hh @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2008 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. // @@ -60,9 +60,6 @@ namespace spot ~environment() { } - - // FIXME: More functions will be needed later, but - // it's enough for now. }; } diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index b5ed9bfc2..9140ce506 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2007, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -309,7 +309,8 @@ namespace spot for (multop::vec::iterator i = res->begin(); i != res->end(); i++) { - // FIXME: why would *i be 0 ? + // An iteration of the loop may zero some later elements + // of the vector to mark them as redundant. Skip them. if (!*i) continue; unop* uo = dynamic_cast(*i); diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index abb439c75..a34161043 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris 6 -// (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Copyright (C) 2004, 2006, 2007, 2008 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. @@ -121,12 +121,6 @@ namespace spot if (opt_ & Reduce_Syntactic_Implications) { - // FIXME: These should be done only when needed. - bool inf = syntactic_implication(f1, f2); - bool infinv = syntactic_implication(f2, f1); - bool infnegleft = syntactic_implication_neg(f2, f1, false); - bool infnegright = syntactic_implication_neg(f2, f1, true); - switch (bo->op()) { case binop::Xor: @@ -136,14 +130,14 @@ namespace spot case binop::U: /* a < b => a U b = b */ - if (inf) + if (syntactic_implication(f1, f2)) { result_ = f2; destroy(f1); return; } /* !b < a => a U b = Fb */ - if (infnegleft) + if (syntactic_implication_neg(f2, f1, false)) { result_ = unop::instance(unop::F, f2); destroy(f1); @@ -164,14 +158,14 @@ namespace spot case binop::R: /* b < a => a R b = b */ - if (infinv) + if (syntactic_implication(f2, f1)) { result_ = f2; destroy(f1); return; } /* b < !a => a R b = Gb */ - if (infnegright) + if (syntactic_implication_neg(f2, f1, true)) { result_ = unop::instance(unop::G, f2); destroy(f1); @@ -247,7 +241,6 @@ namespace spot } } - // FIXME /* f1 < !f2 => f1 & f2 = false !f1 < f2 => f1 | f2 = true */ for (f1 = res->begin(); f1 != res->end(); f1++) diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc index b8d82d91c..89571697a 100644 --- a/src/tgba/tgbareduc.cc +++ b/src/tgba/tgbareduc.cc @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2004, 2005, 2008 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. // @@ -318,10 +318,9 @@ namespace spot void tgba_reduc::remove_state(const spot::state* s) { - // We suppose than the state is not reachable when call by - // merge_state => NO PREDECESSOR !! - // But it can be have some predecessor in state_predecessor_map_ !! - // So, we remove from it. + // 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_. ns_map::iterator k = name_state_map_.find(tgba_explicit::format_state(s)); @@ -341,7 +340,7 @@ namespace spot if (i == state_predecessor_map_.end()) // 0 predecessor return; - // for all predecessor of s. Zero if call by merge_state. + // for all predecessor of s (none when called by merge_state) for (std::list::iterator p = (i->second)->begin(); p != (i->second)->end(); ++p) { @@ -362,7 +361,7 @@ namespace spot } // DESTROY THE STATE !? USELESS - // it will be destroy when the automaton will be delete + // 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)]; } @@ -391,14 +390,14 @@ namespace spot sp_map::iterator i = state_predecessor_map_.find(s1); if (i == state_predecessor_map_.end()) // 0 predecessor { - // We can remove s1 safely, without change the language + // 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 transition whose lead to s1 to s2. + // we redirect to s2 the transitions that lead to s1. for (std::list::iterator p = (i->second)->begin(); p != (i->second)->end(); ++p) { @@ -406,24 +405,24 @@ namespace spot for (tgba_explicit::state::iterator j = (*p)->begin(); j != (*p)->end(); ++j) { - // if the successor if s1. + // if the successor was s1... if ((*j)->dest == s1) { - // We can redirect transition to s2. + // ... make it s2. (*j)->dest = const_cast(s2); } } } - // FIXME: - // Be careful, we have to stock on s2 the acceptance condition on the arc - // leaving s1 (possible when the simulation is delayed). Since s2 simulate - // s1, s2 has some label whose implies these of s1, so we can put the - // acceptance conditions on this arcs. + // 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 (tgba_explicit::state::const_iterator j = s1->begin(); j != s1->end(); ++j) { - // FIXME transition* t = new transition(); t->dest = (*j)->dest; t->condition = (*j)->condition; @@ -434,11 +433,9 @@ namespace spot // We remove all the predecessor of s1. (i->second)->clear(); - // then we can remove s1 safely, without change the language + // then we can remove s1 safely, without changing the language // of the automaton. - // useless because the state is not reachable. this->remove_state(sim1); - } void @@ -621,25 +618,6 @@ namespace spot i != s1->end(); ++i) (*i)->acceptance_conditions = bddfalse; } - /* - else - { - // FIXME - tgba_succ_iterator* si = this->succ_iter(sm->first); - spot::state* s2 = si->current_state(); - seen_map::iterator sm2 = si_.find(s2); - if (sm2->second == n) - { - s1 = name_state_map_[tgba_explicit::format_state(sm2->first)]; - for (state::iterator i = s1->begin(); - i != s1->end(); ++i) - (*i)->acceptance_conditions = bddfalse; - } - delete s2; - delete si; - } - */ - } } @@ -825,7 +803,7 @@ namespace spot void tgba_reduc::remove_scc(spot::state* s) { - // To remove a scc, we remove all his state. + // To remove a scc, we remove all its states. seen_map::iterator sm = si_.find(s); sm = si_.find(s); @@ -842,95 +820,6 @@ namespace spot } - /* - void - tgba_reduc::remove_scc_depth_first(spot::state* s, int n) - { - if (n == -1) - { - assert(seen_ == 0); - seen_ = new seen_map(); - } - - seen_map::const_iterator sm = seen_->find(s); - if (sm == seen_->end()) - seen_->insert(std::pair(s, 1)); - else - return; - - tgba_succ_iterator* j = this->succ_iter(s); - for (j->first(); !j->done(); j->next()) - { - this->remove_scc_depth_first(j->current_state(), 1); - } - this->remove_state(s); - - if (n == -1) - { - delete seen_; - seen_ = 0; - } - } - */ - - /* - bool - tgba_reduc::is_alpha_ball(const spot::state* s, bdd label, int n) - { - /// FIXME - // a SCC is alpha ball if she's terminal but with some acceptance - // condition, and all transition have the same label. - // So we replace this SCC by a single state. - - bool b = false; - - seen_map::const_iterator i; - if ((n == -1) && - (label == bddfalse)) - { - acc_ == bddfalse; - b = true; - assert(seen_ == 0); - seen_ = new seen_map(); - i = si_.find(s); - assert(i->first != 0); - n = i->second; - } - - seen_map::const_iterator sm = seen_->find(s); - if (sm == seen_->end()) - { - seen_->insert(std::pair(s, 1)); - i = si_.find(s); - assert(i->first != 0); - if (n != i->second) - return false; - } - else - { - return true; - } - - bool ret = true; - tgba_succ_iterator* j = this->succ_iter(s); - for (j->first(); !j->done(); j->next()) - { - acc_ |= j->current_acceptance_conditions(); - ret &= this->is_terminal(j->current_state(), n); - } - - if (b) - { - delete seen_; - seen_ = 0; - if (acc_ == this->all_acceptance_conditions()) - ret = false; - } - - return ret; - } - */ - int tgba_reduc::nb_set_acc_cond() const { diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc index 88e03e489..efbe7ae3d 100644 --- a/src/tgbaalgos/reductgba_sim_del.cc +++ b/src/tgbaalgos/reductgba_sim_del.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -389,9 +389,7 @@ namespace spot build_recurse_successor_spoiler(spoiler_node* sn, std::ostringstream& os) { - // FIXME - if (sn == 0) - return; + assert(sn); tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node());