diff --git a/ChangeLog b/ChangeLog index 7c470245f..bad990033 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2006-04-05 Alexandre Duret-Lutz + + * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh: + (couvreur99_check_shy_ssp): Add a onepass_ attribute to + disable the "shyness", and do not increment pos before calling + find_state since gspn's implementation uses it. + * iface/gspn/ssp.cc: Enable "onepass_" for all "shy" variants, + and also fix find_state for the case where onepass_ is + disabled (but I do not yet know why the latter fix isn't enough). + 2006-02-15 Alexandre Duret-Lutz * src/tgbaalgos/gtec/gtec.cc: Add a third level hash, to split diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index 213635c9d..5c3d2d288 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -994,6 +994,8 @@ namespace spot inclusion_count_stack(0), stack_inclusion(stack_inclusion) { + onepass_ = true; + stats["inclusion count heap"] = static_cast (&couvreur99_check_shy_ssp::get_inclusion_count_heap); @@ -1046,6 +1048,7 @@ namespace spot const state_gspn_ssp* s_ = dynamic_cast(s); const void* cont = container_(s_->left()); contained_map::const_iterator i = contained.find(cont); + if (i != contained.end()) { f_map::const_iterator k = i->second.find(s_->right()); @@ -1094,13 +1097,19 @@ namespace spot 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(queue.begin()->acc, + queue.push_back(successor(old->acc, s)); inc_depth(); } @@ -1166,6 +1175,8 @@ namespace spot numbered_state_heap_ssp_factory_semi::instance()), inclusion_count(0) { + onepass_ = true; + stats["find_state count"] = static_cast (&couvreur99_check_shy_semi_ssp::get_inclusion_count); diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index d4897c4a4..adb1cb030 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -322,6 +322,7 @@ namespace spot group_ = o.get("group", 1); group2_ = o.get("group2", 0); group_ |= group2_; + onepass_ = o.get("onepass", 0); // Setup depth-first search from the initial state. const state* i = ecs_->aut->get_init_state(); @@ -364,7 +365,7 @@ namespace spot couvreur99_check_shy::check() { // Position in the loop seeking known successors. - succ_queue::iterator pos = todo.back().q.begin(); + pos = todo.back().q.begin(); for (;;) { @@ -429,13 +430,18 @@ namespace spot // which state we are considering. Otherwise just pick the // first one. succ_queue::iterator old; + if (onepass_) + pos = queue.end(); if (pos == queue.end()) old = queue.begin(); else - old = pos++; + old = pos; successor succ = *old; - + // Beware: the implementation of find_state in ifage/gspn/ssp.cc + // uses POS and modify QUEUE. numbered_state_heap::state_index_p sip = find_state(succ.s); + if (pos != queue.end()) + ++pos; int* i = sip.second; if (!i) diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 7c31e4fb5..85110aff5 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -221,6 +221,9 @@ namespace spot // (ACCEPTANCE_CONDITIONS, STATE) pairs. typedef std::list succ_queue; + // Position in the loop seeking known successors. + succ_queue::iterator pos; + struct todo_item { const state* s; @@ -239,6 +242,10 @@ namespace spot // If the "group2" option is set (it implies "group"), we // reprocess the successor states of SCC that have been merged. bool group2_; + // If the onepass option is true, do only one pass. This cancels + // all the "shyness" of the algorithm, but we need the framework + // of the implementation when working with GreatSPN. + bool onepass_; /// \brief find the SCC number of a unprocessed state. ///