diff --git a/ChangeLog b/ChangeLog index e0c420e7f..8d9c170b2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,18 @@ +2008-01-08 Alexandre Duret-Lutz + + This is something Soheib and I worked on back in July, but a + intricate memory corruption bug prevented me to check the patch + in. It took me two days to realize why find_state() must do a + double loop over the candidates to check for equality before + checking for inclusion(s). + + * iface/gspn/ltlgspn.cc: New options, -e45 and -n. + * iface/gspn/ssp.cc, iface/gspn/ssp.hh: Handle these. + * src/tgbaalgos/gtec/gtec.cc (TRACE): Add some debugging traces. + (couvreur99_check_shy::dump_queue): New function. + * src/tgbaalgos/gtec/gtec.hh (couvreur99_check_shy::dump_queue): + New function. + 2007-11-29 Alexandre Duret-Lutz Keep libtool's files under CVS so that we don't use the broken diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index fbcb0350e..646bfcf62 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2006, 2007 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, 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. // @@ -73,6 +73,7 @@ syntax(char* prog) << " -e4 use semi-d. incl. Couvreur's emptiness-check's " << "shy variant" << std::endl + << " -e45 mix of -e4 and -e5 " << std::endl << " -e5 use d. incl. Couvreur's emptiness-check's shy variant" << std::endl << " -e6 like -e5, but without inclusion checks in the " @@ -80,6 +81,9 @@ syntax(char* prog) #endif << " -m degeneralize and perform a magic-search" << std::endl << std::endl +#ifdef SSP + << " -n do not perform any decomposition" << std::endl +#endif << " -l use Couvreur's LaCIM algorithm for translation (default)" << std::endl << " -f use Couvreur's FM algorithm for translation" << std::endl @@ -111,6 +115,8 @@ main(int argc, char **argv) bool doublehash = true; bool stack_inclusion = true; bool pushfront = false; + bool double_inclusion = false; + bool no_decomp = false; #endif std::string dead = "true"; @@ -161,6 +167,11 @@ main(int argc, char **argv) { check = Couvreur4; } + else if (!strcmp(argv[formula_index], "-e45")) + { + check = Couvreur5; + double_inclusion = true; + } else if (!strcmp(argv[formula_index], "-e5")) { check = Couvreur5; @@ -175,6 +186,12 @@ main(int argc, char **argv) { check = Magic; } +#ifdef SSP + else if (!strcmp(argv[formula_index], "-n")) + { + no_decomp = true; + } +#endif else if (!strcmp(argv[formula_index], "-l")) { trans = Lacim; @@ -276,7 +293,9 @@ main(int argc, char **argv) ec = spot::couvreur99_check_ssp_shy_semi(prod); break; case Couvreur5: - ec = spot::couvreur99_check_ssp_shy(prod, stack_inclusion); + ec = spot::couvreur99_check_ssp_shy(prod, stack_inclusion, + double_inclusion, + no_decomp); break; #endif default: @@ -389,6 +408,7 @@ main(int argc, char **argv) #else delete model; delete control; + delete ca; #endif delete a_f; delete dict; diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index 6d720229b..850c9b941 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2005, 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. // @@ -240,10 +240,11 @@ namespace spot virtual state* current_state() const { - return + state_gspn_ssp* s = new state_gspn_ssp(successors_[current_succ_].succ_, (state_array_[successors_[current_succ_] .arc->curr_state])->clone()); + return s; } virtual bdd @@ -992,13 +993,16 @@ namespace spot class couvreur99_check_shy_ssp : public couvreur99_check_shy { public: - couvreur99_check_shy_ssp(const tgba* a, bool stack_inclusion) + couvreur99_check_shy_ssp(const tgba* a, bool stack_inclusion, + bool double_inclusion, bool no_decomp) : couvreur99_check_shy(a, option_map(), numbered_state_heap_ssp_factory_semi::instance()), inclusion_count_heap(0), inclusion_count_stack(0), - stack_inclusion(stack_inclusion) + stack_inclusion(stack_inclusion), + double_inclusion(double_inclusion), + no_decomp(no_decomp) { onepass_ = true; @@ -1017,6 +1021,8 @@ namespace spot unsigned inclusion_count_heap; unsigned inclusion_count_stack; bool stack_inclusion; + bool double_inclusion; + bool no_decomp; protected: unsigned @@ -1063,6 +1069,7 @@ namespace spot const state_list& l = k->second; state_list::const_iterator j; + // Make a first pass looking for identical states. for (j = l.begin(); j != l.end(); ++j) { const state_gspn_ssp* old_state = @@ -1073,7 +1080,18 @@ namespace spot assert(new_state); if (old_state->left() == new_state->left()) - break; + goto found_match; + } + + // Now, check for inclusions. + for (j = l.begin(); j != l.end(); ++j) + { + const state_gspn_ssp* old_state = + dynamic_cast(*j); + const state_gspn_ssp* new_state = + dynamic_cast(s); + assert(old_state); + assert(new_state); if (old_state->left() && new_state->left()) { @@ -1090,42 +1108,83 @@ namespace spot } else { + if (stack_inclusion + && double_inclusion + && spot_inclusion(new_state->left(), + old_state->left())) + break; if (stack_inclusion && spot_inclusion(old_state->left(), new_state->left())) { ++inclusion_count_stack; - State* succ_tgba_ = 0; - size_t size_tgba_ = 0; succ_queue& queue = todo.back().q; - - Diff_succ(old_state->left(), new_state->left(), - &succ_tgba_, &size_tgba_); - succ_queue::iterator old; if (pos == queue.end()) old = queue.begin(); else - old = pos; - - for (size_t i = 0; i < size_tgba_; i++) { - state_gspn_ssp* s = - new state_gspn_ssp - (succ_tgba_[i], - old_state->right()->clone()); - queue.push_back(successor(old->acc, - s)); - inc_depth(); + old = pos; + // Should not happen, because onepass_ == 1 + assert(0); } - if (size_tgba_ != 0) - diff_succ_free(succ_tgba_); + + if (no_decomp) + { + queue.push_back // why not push_front? + (successor(old->acc, + old_state->clone())); + + assert(pos == queue.end()); + + inc_depth(); + + // If we had not done the first loop + // over the container to check for + // equal states, we would have to do + // one here to make sure that state + // s is not equal to another known + // state. (We risk some intricate + // memory corruption if we don't + // delete "clone states" at this + // point.) + + // Since we have that first loop and + // we therefore know that state s is + // genuinely new, position j so that + // we won't delete it. + j = l.end(); + } + else + { + State* succ_tgba_ = 0; + size_t size_tgba_ = 0; + + Diff_succ(old_state->left(), + new_state->left(), + &succ_tgba_, &size_tgba_); + + for (size_t i = 0; i < size_tgba_; i++) + { + state_gspn_ssp* s = + new state_gspn_ssp + (succ_tgba_[i], + old_state->right()->clone()); + // why not push_front? + queue.push_back(successor(old->acc, s)); + inc_depth(); + } + if (size_tgba_ != 0) + diff_succ_free(succ_tgba_); + } + break; } } } } + found_match: if (j != l.end()) { if (s != *j) @@ -1166,6 +1225,7 @@ namespace spot res.first = k->first; res.second = &k->second; } + return res; } }; @@ -1235,10 +1295,12 @@ namespace spot } couvreur99_check* - couvreur99_check_ssp_shy(const tgba* ssp_automata, bool stack_inclusion) + couvreur99_check_ssp_shy(const tgba* ssp_automata, bool stack_inclusion, + bool double_inclusion, bool no_decomp) { assert(dynamic_cast(ssp_automata)); - return new couvreur99_check_shy_ssp(ssp_automata, stack_inclusion); + return new couvreur99_check_shy_ssp(ssp_automata, stack_inclusion, + double_inclusion, no_decomp); } #if 0 diff --git a/iface/gspn/ssp.hh b/iface/gspn/ssp.hh index dbb7df02f..cbc06ede4 100644 --- a/iface/gspn/ssp.hh +++ b/iface/gspn/ssp.hh @@ -56,7 +56,9 @@ namespace spot couvreur99_check* couvreur99_check_ssp_semi(const tgba* ssp_automata); couvreur99_check* couvreur99_check_ssp_shy_semi(const tgba* ssp_automata); couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata, - bool stack_inclusion = true); + bool stack_inclusion = true, + bool double_inclusion = false, + bool no_decomp = false); /// @} diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index c71fbb0ae..a643e900b 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +// Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -19,6 +19,15 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +// #define TRACE + +#include +#ifdef TRACE +#define trace std::cerr +#else +#define trace while (0) std::cerr +#endif + #include "gtec.hh" #include "ce.hh" #include "misc/memusage.hh" @@ -374,6 +383,27 @@ namespace spot assert(depth() == 0); } + void + couvreur99_check_shy::dump_queue(std::ostream& os) + { + os << "--- TODO ---" << std::endl; + unsigned pos = 0; + for (todo_list::const_iterator ti = todo.begin(); ti != todo.end(); ++ti) + { + ++pos; + os << "#" << pos << " s:" << ti->s << " n:" << ti->n + << " q:{"; + for (succ_queue::const_iterator qi = ti->q.begin(); qi != ti->q.end();) + { + os << qi->s; + ++qi; + if (qi != ti->q.end()) + os << ", "; + } + os << "}" << std::endl;; + } + } + emptiness_check_result* couvreur99_check_shy::check() { @@ -382,6 +412,10 @@ namespace spot for (;;) { +#ifdef TRACE + dump_queue(); +#endif + assert(ecs_->root.size() == 1 + arc.size()); // Get the successors of the current state. @@ -390,6 +424,7 @@ namespace spot // If there is no more successor, backtrack. if (queue.empty()) { + trace << "backtrack" << std::endl; // We have explored all successors of state CURR. const state* curr = todo.back().s; @@ -451,18 +486,23 @@ namespace spot old = pos; successor succ = *old; // Beware: the implementation of find_state in ifage/gspn/ssp.cc - // uses POS and modify QUEUE. + // uses POS and modifies QUEUE. numbered_state_heap::state_index_p sip = find_state(succ.s); if (pos != queue.end()) ++pos; int* i = sip.second; + trace << "picked state " << succ.s << std::endl; + if (!i) { // It's a new state. // If we are seeking known states, just skip it. if (pos != queue.end()) continue; + + trace << "new state" << std::endl; + // Otherwise, number it and stack it so we recurse. queue.erase(old); dec_depth(); @@ -480,7 +520,12 @@ namespace spot // Skip dead states. if (*i == -1) - continue; + { + trace << "dead state" << std::endl; + continue; + } + + trace << "merging..." << std::endl; // Now this is the most interesting case. We have // reached a state S1 which is already part of a @@ -542,7 +587,7 @@ namespace spot todo_list::reverse_iterator last = prev++; // If group2 is used we insert the last->q in front // of prev->q so that the states in prev->q are checked - // for existence again after we have done with the states + // for existence again after we have processed the states // of last->q. Otherwise we just append to the end. prev->q.splice(group2_ ? prev->q.begin() : prev->q.end(), last->q); diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index de1918081..c37a496da 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +// Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -238,6 +238,9 @@ namespace spot void clear_todo(); + /// Dump the queue for debugging. + void dump_queue(std::ostream& os = std::cerr); + /// Whether successors should be grouped for states in the same SCC. bool group_; // If the "group2" option is set (it implies "group"), we