From 9782b822f0a6fa4e9d4cad14366e82f95c5d7ac6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 10 Dec 2004 16:16:38 +0000 Subject: [PATCH] * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::couvreur99_check_shy): Add the group option, and redefine todo as a list so it can be iterated over. * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Introduce couvreur99_shy- (for group=false) in addition to couvreur99_shy (for group=true). * iface/gspn/ssp.cc (couvreur99_check_ssp_shy_semi, couvreur99_check_ssp_shy): Use group=true; --- ChangeLog | 9 +++++++++ iface/gspn/ssp.cc | 6 ++++-- src/tgbaalgos/gtec/gtec.cc | 41 ++++++++++++++++++++++++++++---------- src/tgbaalgos/gtec/gtec.hh | 13 +++++++++++- src/tgbatest/ltl2tgba.cc | 10 +++++++++- src/tgbatest/randtgba.cc | 7 +++++++ 6 files changed, 72 insertions(+), 14 deletions(-) diff --git a/ChangeLog b/ChangeLog index 4e86ae5d5..c406469b2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,14 @@ 2004-12-10 Alexandre Duret-Lutz + * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc + (couvreur99_check_shy::couvreur99_check_shy): Add the group option, + and redefine todo as a list so it can be iterated over. + * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Introduce + couvreur99_shy- (for group=false) in addition to couvreur99_shy + (for group=true). + * iface/gspn/ssp.cc (couvreur99_check_ssp_shy_semi, + couvreur99_check_ssp_shy): Use group=true; + * src/tgbaalgos/randomgraph.cc (random_graph): Do not use the pointer of the state created as keys in sets; otherwise the graph created depends on the memory layout. diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index 1dad0144d..a65b85b04 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -900,6 +900,7 @@ namespace spot public: couvreur99_check_shy_ssp(const tgba* a) : couvreur99_check_shy(a, + true, numbered_state_heap_ssp_factory_semi::instance()) { } @@ -944,7 +945,7 @@ namespace spot { State* succ_tgba_ = 0; size_t size_tgba_ = 0; - succ_queue& queue = todo.top().second; + succ_queue& queue = todo.back().second; Diff_succ(old_state->left(), new_state->left(), &succ_tgba_, &size_tgba_); @@ -991,7 +992,8 @@ namespace spot return new couvreur99_check_shy (ssp_automata, - numbered_state_heap_ssp_factory_semi::instance()); + true, + numbered_state_heap_ssp_factory_semi::instance()); } couvreur99_check* diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 2cacb7b91..d99db8d15 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -256,14 +256,15 @@ namespace spot ////////////////////////////////////////////////////////////////////// couvreur99_check_shy::couvreur99_check_shy(const tgba* a, + bool group, const numbered_state_heap_factory* nshf) - : couvreur99_check(a, nshf), num(1) + : couvreur99_check(a, nshf), num(1), group_(group) { // Setup depth-first search from the initial state. - todo.push(pair_state_successors(0, succ_queue())); + todo.push_back(pair_state_successors(0, succ_queue())); inc_depth(); - todo.top().second.push_front(successor(bddtrue, + todo.back().second.push_front(successor(bddtrue, ecs_->aut->get_init_state())); } @@ -279,7 +280,7 @@ namespace spot assert(ecs_->root.size() == arc.size()); // Get the successors of the current state. - succ_queue& queue = todo.top().second; + succ_queue& queue = todo.back().second; // First, we process all successors that we have already seen. // This is an idea from Soheib Baarir. It helps to merge SCCs @@ -342,7 +343,7 @@ namespace spot // unless they are used as keys in H. while (!todo.empty()) { - succ_queue& queue = todo.top().second; + succ_queue& queue = todo.back().second; for (succ_queue::iterator q = queue.begin(); q != queue.end(); ++q) { @@ -354,7 +355,7 @@ namespace spot if (spi.first == 0) delete q->s; } - todo.pop(); + todo.pop_back(); dec_depth(); } set_states(ecs_->states()); @@ -367,13 +368,33 @@ namespace spot queue.erase(old); } + // Group the pending successors of formed SCC of requested. + if (group_ && todo.back().first != 0) + { + int top_index = *ecs_->h->index(todo.back().first).second; + if (ecs_->root.top().index < top_index) + { + do + { + todo_list::reverse_iterator prev = todo.rbegin(); + todo_list::reverse_iterator last = prev++; + prev->second.splice(prev->second.end(), last->second); + todo.pop_back(); + dec_depth(); + top_index = *ecs_->h->index(todo.back().first).second; + } + while (ecs_->root.top().index < top_index); + continue; + } + } + // If there is no more successor, backtrack. if (queue.empty()) { // We have explored all successors of state CURR. - const state* curr = todo.top().first; + const state* curr = todo.back().first; // Backtrack TODO. - todo.pop(); + todo.pop_back(); dec_depth(); if (todo.empty()) { @@ -408,9 +429,9 @@ namespace spot ecs_->h->insert(succ.s, ++num); ecs_->root.push(num); arc.push(succ.acc); - todo.push(pair_state_successors(succ.s, succ_queue())); + todo.push_back(pair_state_successors(succ.s, succ_queue())); inc_depth(); - succ_queue& new_queue = todo.top().second; + succ_queue& new_queue = todo.back().second; tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s); for (iter->first(); !iter->done(); iter->next(), inc_transitions()) new_queue.push_back(successor(iter->current_acceptance_conditions(), diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 660c9f833..5912c7981 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -108,11 +108,17 @@ namespace spot /// \brief A version of spot::couvreur99_check that tries to visit /// known states first. /// + /// If \a group is true (the default), the successors of all the + /// states that belong to the same SCC will be considered when + /// choosing a successor. Otherwise, only the successor of the + /// topmost state on the DFS stack are considered. + /// /// See the documentation for spot::couvreur99_check class couvreur99_check_shy : public couvreur99_check { public: couvreur99_check_shy(const tgba* a, + bool group = true, const numbered_state_heap_factory* nshf = numbered_state_heap_hash_map_factory::instance()); virtual ~couvreur99_check_shy(); @@ -140,7 +146,12 @@ namespace spot // (ACCEPTANCE_CONDITIONS, STATE) pairs. typedef std::list succ_queue; typedef std::pair pair_state_successors; - std::stack todo; + typedef std::list todo_list; + todo_list todo; + + // Whether successors should be grouped for states in the same + // SCC. + bool group_; /// \brief find the SCC number of a unprocessed state. /// diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index c007ba91a..62fd82268 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -122,6 +122,7 @@ syntax(char* prog) << std::endl << "Where ALGO should be one of:" << std::endl << " couvreur99 (the default)" << std::endl + << " couvreur99_shy-" << std::endl << " couvreur99_shy" << std::endl << " magic_search" << std::endl << " magic_search_repeated" << std::endl @@ -159,6 +160,7 @@ main(int argc, char** argv) enum { None, Couvreur, Couvreur2, MagicSearch, Se05Search, Tau03Search, Tau03OptSearch, Gv04 } echeck = None; enum { NoneDup, BFS, DFS } dupexp = NoneDup; + bool couv_group = true; bool search_many = false; bool bit_state_hashing = false; int heap_size = 10*1024*1024; @@ -381,6 +383,12 @@ main(int argc, char** argv) else if (echeck_algo == "couvreur99_shy") { echeck = Couvreur2; + couv_group = true; + } + else if (echeck_algo == "couvreur99_shy-") + { + echeck = Couvreur2; + couv_group = false; } else if (echeck_algo == "magic_search") { @@ -670,7 +678,7 @@ main(int argc, char** argv) break; case Couvreur2: - ec = new spot::couvreur99_check_shy(a); + ec = new spot::couvreur99_check_shy(a, couv_group); break; case MagicSearch: diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 37fab16c5..ca63e2542 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -59,6 +59,12 @@ couvreur99_shy_cons(const spot::tgba* a) return new spot::couvreur99_check_shy(a); } +spot::emptiness_check* +couvreur99_shy_minus_cons(const spot::tgba* a) +{ + return new spot::couvreur99_check_shy(a, false); +} + spot::emptiness_check* bsh_ms_cons(const spot::tgba* a) { @@ -82,6 +88,7 @@ struct ec_algo ec_algo ec_algos[] = { { "couvreur99", couvreur99_cons, 0, -1U, true }, + { "couvreur99_shy-", couvreur99_shy_minus_cons, 0, -1U, true }, { "couvreur99_shy", couvreur99_shy_cons, 0, -1U, true }, { "explicit_magic_search", spot::explicit_magic_search, 0, 1, true }, { "bit_state_hashing_magic_search",