From 7f31d70345ea4d05b24c2a925be10e91d734e643 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 10 Jul 2013 08:34:34 +0200 Subject: [PATCH] * src/tgbaalgos/cutscc.cc: Cosmetics. --- src/tgbaalgos/cutscc.cc | 400 ++++++++++++++++++++-------------------- 1 file changed, 197 insertions(+), 203 deletions(-) diff --git a/src/tgbaalgos/cutscc.cc b/src/tgbaalgos/cutscc.cc index bf1f00231..95cc02df8 100644 --- a/src/tgbaalgos/cutscc.cc +++ b/src/tgbaalgos/cutscc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et +// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -25,214 +25,208 @@ namespace spot { - tgba* cut_scc(const tgba* a, const scc_map& m, - const std::set& s) + namespace { - tgba_explicit_string* sub_a = new tgba_explicit_string(a->get_dict()); - state* cur = a->get_init_state(); - std::queue tovisit; - typedef Sgi::hash_set hash_type; - // Setup - hash_type seen; - unsigned scc_number; - std::string cur_format = a->format_state(cur); - std::set::iterator it; - // Check if we have at least one accepting SCC. - for (it = s.begin(); it != s.end() && !m.accepting(*it); ++it) - continue; - assert(it != s.end()); - tovisit.push(cur); - seen.insert(cur); - sub_a->add_state(cur_format); - sub_a->copy_acceptance_conditions_of(a); - // If the initial is not part of one of the desired SCC, exit - assert(s.find(m.scc_of_state(cur)) != s.end()); - - // Perform BFS to visit each state. - while (!tovisit.empty()) + static tgba* + cut_scc(const tgba* a, const scc_map& m, + const std::set& s) { - cur = tovisit.front(); - tovisit.pop(); - tgba_succ_iterator* sit = a->succ_iter(cur); - for (sit->first(); !sit->done(); sit->next()) - { - cur_format = a->format_state(cur); - state* dst = sit->current_state(); - std::string dst_format = a->format_state(dst); - scc_number= m.scc_of_state(dst); - // Is the successor included in one of the desired SCC ? - if (s.find(scc_number) != s.end()) + tgba_explicit_string* sub_a = new tgba_explicit_string(a->get_dict()); + state* cur = a->get_init_state(); + std::queue tovisit; + typedef Sgi::hash_set hash_type; + // Setup + hash_type seen; + unsigned scc_number; + std::string cur_format = a->format_state(cur); + std::set::iterator it; + // Check if we have at least one accepting SCC. + for (it = s.begin(); it != s.end() && !m.accepting(*it); ++it) + continue; + assert(it != s.end()); + tovisit.push(cur); + seen.insert(cur); + sub_a->add_state(cur_format); + sub_a->copy_acceptance_conditions_of(a); + // If the initial is not part of one of the desired SCC, exit + assert(s.find(m.scc_of_state(cur)) != s.end()); + + // Perform BFS to visit each state. + while (!tovisit.empty()) { - if (seen.find(dst) == seen.end()) - { - tovisit.push(dst); - seen.insert(dst); // has_state? - } + cur = tovisit.front(); + tovisit.pop(); + tgba_succ_iterator* sit = a->succ_iter(cur); + for (sit->first(); !sit->done(); sit->next()) + { + cur_format = a->format_state(cur); + state* dst = sit->current_state(); + std::string dst_format = a->format_state(dst); + scc_number= m.scc_of_state(dst); + // Is the successor included in one of the desired SCC ? + if (s.find(scc_number) != s.end()) + { + if (seen.find(dst) == seen.end()) + { + tovisit.push(dst); + seen.insert(dst); // has_state? + } + else + { + dst->destroy(); + } + state_explicit_string::transition* t = + sub_a->create_transition(cur_format, dst_format); + sub_a->add_conditions(t, sit->current_condition()); + bdd acc = sit->current_acceptance_conditions(); + sub_a->add_acceptance_conditions(t, acc); + } + else + { + dst->destroy(); + } + } + delete sit; + } + + hash_type::iterator it2; + // Free visited states. + for (it2 = seen.begin(); it2 != seen.end(); ++it2) + (*it2)->destroy(); + return sub_a; + } + + static unsigned set_distance(const sccs_set* s1, + const sccs_set* s2, + const std::vector& scc_sizes) + { + // Compute the distance between two sets. + // Formula is : distance = size(s1) + size(s2) - size(s1 inter s2) + std::set::iterator it; + std::set result; + unsigned inter_sum = 0; + std::set_intersection(s1->sccs.begin(), s1->sccs.end(), + s2->sccs.begin(), s2->sccs.end(), + std::inserter(result, result.begin())); + for (it = result.begin(); it != result.end(); ++it) + inter_sum += scc_sizes[*it]; + return s1->size + s2->size - 2*inter_sum; + } + + static sccs_set* set_union(sccs_set* s1, + sccs_set* s2, + const std::vector& scc_sizes) + { + // Perform the union of two sets. + sccs_set* result = new sccs_set; + set_union(s1->sccs.begin(), s1->sccs.end(), + s2->sccs.begin(), s2->sccs.end(), + std::inserter(result->sccs, result->sccs.begin())); + result->size = 0; + std::set::iterator it; + for (it = result->sccs.begin(); it != result->sccs.end(); ++it) + result->size += scc_sizes[*it]; + delete s1; + return result; + } + + struct recurse_data + { + std::set seen; + std::vector >* rec_paths; + }; + + static void find_paths_sub(unsigned init_scc, + const scc_map& m, + recurse_data& d, + const std::vector& scc_sizes) + { + // Find all the paths from the initial states to an accepting SCC + // We need two stacks, one to track the current state, the other to track + // the current iterator of this state. + std::stack it_stack; + std::stack scc_stack; + std::vector scc_succ; + unsigned scc_count = m.scc_count(); + scc_succ.reserve(scc_count); + d.seen.insert(init_scc); + unsigned i; + for (i = 0; i < scc_count; ++i) + scc_succ.push_back(&(m.succ(i))); + // Setup the two stacks with the initial SCC. + scc_stack.push(init_scc); + it_stack.push(scc_succ[init_scc]->begin()); + while (!scc_stack.empty()) + { + unsigned cur_scc = scc_stack.top(); + scc_stack.pop(); + d.seen.insert(cur_scc); + scc_map::succ_type::const_iterator it; + // Find the next unvisited successor. + for (it = it_stack.top(); it != scc_succ[cur_scc]->end() + && d.seen.find(it->first) != d.seen.end(); ++it) + continue; + it_stack.pop(); + // If there are no successors and if the SCC is not accepting, this is + // an useless path. Throw it away. + if (scc_succ[cur_scc]->begin() == scc_succ[cur_scc]->end() + && !m.accepting(cur_scc)) + continue; + std::vector >* rec_paths = d.rec_paths; + // Is there a successor to process ? + if (it != scc_succ[cur_scc]->end()) + { + // Yes, add it to the stack for later processing. + unsigned dst = it->first; + scc_stack.push(cur_scc); + ++it; + it_stack.push(it); + if (d.seen.find(dst) == d.seen.end()) + { + scc_stack.push(dst); + it_stack.push(scc_succ[dst]->begin()); + } + } else - { - dst->destroy(); - } - state_explicit_string::transition* t = - sub_a->create_transition(cur_format, dst_format); - sub_a->add_conditions(t, sit->current_condition()); - sub_a-> - add_acceptance_conditions(t, - sit->current_acceptance_conditions()); + { + // No, all successors have been processed, update the current SCC. + for (it = scc_succ[cur_scc]->begin(); + it != scc_succ[cur_scc]->end(); ++it) + { + unsigned dst = it->first; + std::vector::iterator lit; + // Extend all the reachable paths by adding the current SCC. + for (lit = (*rec_paths)[dst].begin(); + lit != (*rec_paths)[dst].end(); ++lit) + { + sccs_set* path = new sccs_set; + path->sccs = (*lit)->sccs; + path->size = (*lit)->size + scc_sizes[cur_scc]; + path->sccs.insert(path->sccs.begin(), cur_scc); + (*rec_paths)[cur_scc].push_back(path); + } + } + bool has_succ = false; + for (it = scc_succ[cur_scc]->begin(); + it != scc_succ[cur_scc]->end() && !has_succ; ++it) + { + has_succ = !(*rec_paths)[it->first].empty(); + } + // Create a new path iff the SCC is accepting and not included + // in another path. + if (m.accepting(cur_scc) && !has_succ) + { + sccs_set* path = new sccs_set; + path->size = scc_sizes[cur_scc]; + path->sccs.insert(path->sccs.begin(), cur_scc); + (*rec_paths)[cur_scc].push_back(path); + } + } + } - else - { - dst->destroy(); - } - } - delete sit; + return; } - - hash_type::iterator it2; - // Free visited states. - for (it2 = seen.begin(); it2 != seen.end(); ++it2) - (*it2)->destroy(); - return sub_a; - } - - void print_set(const sccs_set* s) - { - std::cout << "set : "; - std::set::iterator vit; - for (vit = s->sccs.begin(); vit != s->sccs.end(); ++vit) - std::cout << *vit << " "; - std::cout << std::endl; - } - - unsigned set_distance(const sccs_set* s1, - const sccs_set* s2, - const std::vector& scc_sizes) - { - // Compute the distance between two sets. - // Formula is : distance = size(s1) + size(s2) - size(s1 inter s2) - std::set::iterator it; - std::set result; - unsigned inter_sum = 0; - std::set_intersection(s1->sccs.begin(), s1->sccs.end(), - s2->sccs.begin(), s2->sccs.end(), - std::inserter(result, result.begin())); - for (it = result.begin(); it != result.end(); ++it) - inter_sum += scc_sizes[*it]; - return s1->size + s2->size - 2*inter_sum; - } - - sccs_set* set_union(sccs_set* s1, - sccs_set* s2, - const std::vector& scc_sizes) - { - // Perform the union of two sets. - sccs_set* result = new sccs_set; - set_union(s1->sccs.begin(), s1->sccs.end(), - s2->sccs.begin(), s2->sccs.end(), - std::inserter(result->sccs, result->sccs.begin())); - result->size = 0; - std::set::iterator it; - for (it = result->sccs.begin(); it != result->sccs.end(); ++it) - result->size += scc_sizes[*it]; - delete s1; - return result; - } - - struct recurse_data - { - std::set seen; - std::vector >* rec_paths; - }; - - void find_paths_sub(unsigned init_scc, - const scc_map& m, - recurse_data& d, - const std::vector& scc_sizes) - { - // Find all the paths from the initial states to an accepting SCC - // We need two stacks, one to track the current state, the other to track - // the current iterator of this state. - std::stack it_stack; - std::stack scc_stack; - std::vector scc_succ; - unsigned scc_count = m.scc_count(); - scc_succ.reserve(scc_count); - d.seen.insert(init_scc); - unsigned i; - for (i = 0; i < scc_count; ++i) - scc_succ.push_back(&(m.succ(i))); - // Setup the two stacks with the initial SCC. - scc_stack.push(init_scc); - it_stack.push(scc_succ[init_scc]->begin()); - while (!scc_stack.empty()) - { - unsigned cur_scc = scc_stack.top(); - scc_stack.pop(); - d.seen.insert(cur_scc); - scc_map::succ_type::const_iterator it; - // Find the next unvisited successor. - for (it = it_stack.top(); it != scc_succ[cur_scc]->end() - && d.seen.find(it->first) != d.seen.end(); ++it) - continue; - it_stack.pop(); - // If there are no successors and if the SCC is not accepting, this is - // an useless path. Throw it away. - if (scc_succ[cur_scc]->begin() == scc_succ[cur_scc]->end() - && !m.accepting(cur_scc)) - continue; - std::vector >* rec_paths = d.rec_paths; - // Is there a successor to process ? - if (it != scc_succ[cur_scc]->end()) - { - // Yes, add it to the stack for later processing. - unsigned dst = it->first; - scc_stack.push(cur_scc); - ++it; - it_stack.push(it); - if (d.seen.find(dst) == d.seen.end()) - { - scc_stack.push(dst); - it_stack.push(scc_succ[dst]->begin()); - } - } - else - { - // No, all successors have been processed, update the current SCC. - for (it = scc_succ[cur_scc]->begin(); - it != scc_succ[cur_scc]->end(); ++it) - { - unsigned dst = it->first; - std::vector::iterator lit; - // Extend all the reachable paths by adding the current SCC. - for (lit = (*rec_paths)[dst].begin(); - lit != (*rec_paths)[dst].end(); ++lit) - { - sccs_set* path = new sccs_set; - path->sccs = (*lit)->sccs; - path->size = (*lit)->size + scc_sizes[cur_scc]; - path->sccs.insert(path->sccs.begin(), cur_scc); - (*rec_paths)[cur_scc].push_back(path); - } - } - bool has_succ = false; - for (it = scc_succ[cur_scc]->begin(); - it != scc_succ[cur_scc]->end() && !has_succ; ++it) - { - has_succ = !(*rec_paths)[it->first].empty(); - } - // Create a new path iff the SCC is accepting and not included - // in another path. - if (m.accepting(cur_scc) && !has_succ) - { - sccs_set* path = new sccs_set; - path->size = scc_sizes[cur_scc]; - path->sccs.insert(path->sccs.begin(), cur_scc); - (*rec_paths)[cur_scc].push_back(path); - } - } - - } - return; } std::vector >* find_paths(tgba* a, const scc_map& m)