Vaucanson 1.4
|
00001 // minimization_hopcroft.hxx: this file is part of the Vaucanson project. 00002 // 00003 // Vaucanson, a generic library for finite state machines. 00004 // 00005 // Copyright (C) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008 The Vaucanson Group. 00006 // 00007 // This program is free software; you can redistribute it and/or 00008 // modify it under the terms of the GNU General Public License 00009 // as published by the Free Software Foundation; either version 2 00010 // of the License, or (at your option) any later version. 00011 // 00012 // The complete GNU General Public Licence Notice can be found as the 00013 // `COPYING' file in the root directory. 00014 // 00015 // The Vaucanson Group consists of people listed in the `AUTHORS' file. 00016 // 00017 #ifndef VCSN_ALGORITHMS_MINIMIZATION_HOPCROFT_HXX 00018 # define VCSN_ALGORITHMS_MINIMIZATION_HOPCROFT_HXX 00019 00020 # include <algorithm> 00021 # include <list> 00022 # include <queue> 00023 # include <set> 00024 # include <vector> 00025 00026 # include <vaucanson/algebra/implementation/semiring/numerical_semiring.hh> 00027 # include <vaucanson/algorithms/minimization_hopcroft.hh> 00028 # include <vaucanson/algorithms/is_deterministic.hh> 00029 # include <vaucanson/algorithms/complete.hh> 00030 # include <vaucanson/automata/concept/automata_base.hh> 00031 # include <vaucanson/misc/usual_macros.hh> 00032 00033 # ifndef VCSN_NDEBUG 00034 # include <vaucanson/algorithms/is_deterministic.hh> 00035 # endif // ! VCSN_NDEBUG 00036 00037 namespace vcsn 00038 { 00039 00040 namespace internal 00041 { 00042 namespace hopcroft_minimization_det 00043 { 00044 00045 # define HOPCROFT_TYPES() \ 00046 typedef std::set<hstate_t> hstates_t; \ 00047 typedef std::vector<hstates_t> partition_t; \ 00048 typedef std::vector<unsigned> class_of_t; \ 00049 typedef std::queue<std::pair<hstates_t*, unsigned> > to_treat_t; 00050 00054 template <typename input_t> 00055 struct splitter_functor 00056 { 00057 AUTOMATON_TYPES (input_t); 00058 AUTOMATON_FREEMONOID_TYPES (input_t); 00059 HOPCROFT_TYPES (); 00060 00061 const input_t& input_; 00062 hstates_t going_in_; 00063 class_of_t& class_of_; 00064 std::list<unsigned> maybe_splittable_; 00065 std::vector<unsigned> count_for_; 00066 00067 splitter_functor (const input_t& input, unsigned int max_state, 00068 class_of_t& class_of) 00069 : input_ (input), going_in_ (), class_of_(class_of), 00070 count_for_ (max_state) 00071 {} 00072 00074 bool compute_states_going_in (const hstates_t& ss, letter_t l) 00075 { 00076 going_in_.clear (); 00077 maybe_splittable_.clear (); 00078 for_all_const_ (hstates_t, i, ss) 00079 { 00080 for (rdelta_iterator t(input_.value(), *i); ! t.done(); t.next()) 00081 { 00082 monoid_elt_t w(input_.series_of(*t).structure().monoid(), l); 00083 if (input_.series_of(*t).get(w) != input_.series().semiring().wzero_) 00084 { 00085 hstate_t s = input_.src_of(*t); 00086 unsigned class_of_state = class_of_[s]; 00087 00088 if (count_for_[class_of_state] == 0) 00089 maybe_splittable_.push_back (class_of_state); 00090 count_for_[class_of_state]++; 00091 going_in_.insert (s); 00092 } 00093 } 00094 } 00095 return not going_in_.empty (); 00096 } 00097 00099 void execute (partition_t& partition, to_treat_t& to_treat, 00100 unsigned& n_partition) 00101 { 00102 for_all (std::list<unsigned>, inpartition, maybe_splittable_) 00103 { 00104 hstates_t& states = partition[*inpartition]; 00105 if (states.size () == count_for_[*inpartition]) 00106 { // All elements in states are predecessors, no split. 00107 count_for_[*inpartition] = 0; 00108 continue; 00109 } 00110 count_for_[*inpartition] = 0; 00111 hstates_t states_inter_going_in; 00112 hstates_t& states_minus_going_in = partition[n_partition]; 00113 // Compute @a states \ @a going_in_. 00114 set_difference 00115 (states.begin (), states.end (), 00116 going_in_.begin (), going_in_.end (), 00117 std::insert_iterator<hstates_t> (states_minus_going_in, 00118 states_minus_going_in.begin ())); 00119 // Compute @a states Inter @a going_in_. 00120 set_intersection 00121 (states.begin(), states.end (), 00122 going_in_.begin (), going_in_.end (), 00123 std::insert_iterator<hstates_t> (states_inter_going_in, 00124 states_inter_going_in.begin ())); 00125 // A split MUST occur. 00126 assertion (not (states_inter_going_in.empty () 00127 or states_minus_going_in.empty ())); 00128 // @a states must be the bigger one. 00129 if (states_minus_going_in.size () > states_inter_going_in.size ()) 00130 { 00131 states.swap (states_minus_going_in); 00132 states_minus_going_in.swap (states_inter_going_in); 00133 } 00134 else 00135 states.swap (states_inter_going_in); 00136 for_all_const_ (hstates_t, istate, states_minus_going_in) 00137 class_of_[*istate] = n_partition; 00138 to_treat.push (std::make_pair (&states_minus_going_in, 00139 n_partition++)); 00140 } 00141 } 00142 }; 00143 00145 template <typename input_t, typename output_t> 00146 struct transition_adder_functor 00147 { 00148 AUTOMATON_TYPES (input_t); 00149 HOPCROFT_TYPES (); 00150 00151 const input_t& input_; 00152 output_t& output_; 00153 const class_of_t& class_of_; 00154 00155 unsigned src_; 00156 00157 transition_adder_functor (const input_t& input, output_t& output, 00158 const class_of_t& class_of) 00159 : input_ (input), output_ (output), class_of_ (class_of) 00160 {} 00161 00163 void execute (hstate_t representative) 00164 { 00165 src_ = class_of_[representative]; 00166 for (delta_iterator t(input_.value(), representative); ! t.done(); t.next()) 00167 { 00168 output_.add_series_transition (src_, class_of_[input_.dst_of (*t)], 00169 input_.series_of (*t)); 00170 } 00171 } 00172 }; 00173 } 00174 } 00175 00176 00177 template <typename A, typename AI1, typename AI2> 00178 void 00179 do_hopcroft_minimization_det(const AutomataBase<A>&, 00180 Element<A, AI2>& output, 00181 const Element<A, AI1>& input) 00182 { 00183 typedef Element<A, AI1> input_t; 00184 typedef Element<A, AI2> output_t; 00185 AUTOMATON_TYPES (input_t); 00186 AUTOMATON_FREEMONOID_TYPES (input_t); 00187 HOPCROFT_TYPES (); 00188 00189 using namespace internal::hopcroft_minimization_det; 00190 00191 precondition(is_deterministic(input)); 00192 00193 unsigned max_state = input.states ().back () + 1; 00194 partition_t partition (max_state); 00195 class_of_t class_of (max_state); 00196 to_treat_t to_treat; 00197 unsigned n_partition = 0; 00198 const alphabet_t& alphabet = 00199 input.structure ().series ().monoid ().alphabet (); 00200 00201 { 00202 // Initialize Partition = {Q \ F , F } 00203 hstates_t* finals = 0, * others = 0; 00204 int n_finals = -1, n_others = -1, 00205 count_finals = 0, count_others = 0; 00206 00207 # define add_to_class(Name) \ 00208 do { \ 00209 if (not Name) \ 00210 { \ 00211 Name = &(partition[n_partition]); \ 00212 n_ ## Name = n_partition++; \ 00213 } \ 00214 count_ ## Name ++; \ 00215 (*Name).insert (*state); \ 00216 class_of[*state] = n_ ## Name; \ 00217 } while (0) 00218 00219 for_all_const_states (state, input) 00220 if (input.is_final (*state)) 00221 add_to_class (finals); 00222 else 00223 add_to_class (others); 00224 # undef add_to_class 00225 00226 if (n_partition == 0) 00227 return; 00228 if (n_partition == 1) 00229 { 00230 output = input; 00231 return; 00232 } 00233 // Put F or Q \ F in the "To treat" list T. 00234 if (count_finals > count_others) 00235 to_treat.push (std::make_pair (others, n_others)); 00236 else 00237 to_treat.push (std::make_pair (finals, n_finals)); 00238 } 00239 00240 { 00241 splitter_functor<input_t> splitter (input, max_state, class_of); 00242 00243 // While T is not empty, 00244 while (not to_treat.empty () && n_partition < max_state) 00245 { 00246 // Remove a set S of T , 00247 hstates_t& states = *(to_treat.front ().first); 00248 to_treat.pop (); 00249 00250 // For each letter l in Alphabet, 00251 for_all_const_letters (letter, alphabet) 00252 { 00253 if (not splitter.compute_states_going_in (states, *letter)) 00254 continue; 00255 splitter.execute (partition, to_treat, n_partition); 00256 if (n_partition == max_state) 00257 break; 00258 } 00259 } 00260 } 00261 00262 // Build the automaton. 00263 // Assume that states are numbers starting from 0. 00264 for (unsigned i = 0; i < n_partition; ++i) 00265 output.add_state (); 00266 00267 transition_adder_functor<input_t, output_t> 00268 transition_adder (input, output, class_of); 00269 00270 typename partition_t::iterator istates = partition.begin (); 00271 for (unsigned i = 0; i < n_partition; ++i, ++istates) 00272 { 00273 hstate_t representative = *(*istates).begin(); 00274 00275 if (input.is_final (representative)) 00276 output.set_final (class_of[representative]); 00277 transition_adder.execute (representative); 00278 } 00279 00280 for_all_const_initial_states (state, input) 00281 output.set_initial (class_of[*state]); 00282 } 00283 00284 # undef HOPCROFT_TYPES 00285 00295 template<typename A, typename AI> 00296 Element<A, AI> 00297 minimization_hopcroft(const Element<A, AI>& a) 00298 { 00299 BENCH_TASK_SCOPED("minimization_hopcroft"); 00300 precondition(is_deterministic(a)); 00301 precondition(is_complete(a)); 00302 Element<A, AI> output(a.structure()); 00303 do_hopcroft_minimization_det(a.structure(), output, a); 00304 return output; 00305 } 00306 00307 00308 /*-------------------------------------. 00309 | Quotient with Boolean multiplicities | 00310 `-------------------------------------*/ 00311 namespace internal 00312 { 00313 namespace hopcroft_minimization_undet 00314 { 00315 00316 # define QUOTIENT_TYPES() \ 00317 typedef std::list<hstate_t> partition_t; \ 00318 typedef std::vector<partition_t> partition_set_t; \ 00319 typedef typename partition_t::iterator partition_iterator; \ 00320 typedef std::vector<unsigned> class_of_t; \ 00321 typedef std::pair<unsigned, letter_t> pair_t; \ 00322 typedef std::list<pair_t> to_treat_t; 00323 00324 template <typename input_t> 00325 class quotient_splitter 00326 { 00327 public: 00328 AUTOMATON_TYPES(input_t); 00329 AUTOMATON_FREEMONOID_TYPES(input_t); 00330 QUOTIENT_TYPES(); 00331 00332 typedef std::vector<bool> going_in_t; 00333 00334 quotient_splitter (const automaton_t& input, class_of_t& class_of, 00335 unsigned max_states) 00336 : input_(input), 00337 alphabet_(input.series().monoid().alphabet()), 00338 class_(class_of), 00339 count_for_(max_states, 0), 00340 twin_(max_states, 0), 00341 going_in_(max_states, false) 00342 { } 00343 00345 bool compute_going_in_states (partition_t& p, letter_t a) 00346 { 00347 for_all_(going_in_t, s, going_in_) 00348 *s = false; 00349 00350 00351 semiring_elt_t weight_zero = input_.series().semiring().wzero_; 00352 monoid_elt_t w(input_.series().monoid(), a); 00353 00354 for_all_(partition_t, s, p) 00355 { 00356 for (rdelta_iterator t(input_.value(), *s); ! t.done(); t.next()) 00357 { 00358 series_set_elt_t st = input_.series_of(*t); 00359 if (st.get(w) != weight_zero) 00360 { 00361 hstate_t s = input_.src_of(*t); 00362 if (!going_in_[s]) 00363 { 00365 going_in_[s] = true; 00366 const unsigned i = class_[s]; 00367 if (count_for_[i] == 0) 00368 met_class_.push_back(i); 00369 count_for_[i]++; 00370 } 00371 } 00372 } 00373 } 00374 return !met_class_.empty(); 00375 } 00376 00378 void split (partition_set_t& parts, unsigned& max_partitions) 00379 { 00380 for_all_(std::list<unsigned>, klass, met_class_) 00381 { 00382 // if all states are predecessors there is no needed split 00383 if (count_for_[*klass] == parts[*klass].size()) 00384 continue; 00385 00386 if (twin_[*klass] == 0) 00387 twin_[*klass] = max_partitions++; 00388 unsigned new_klass = twin_[*klass]; 00389 00390 typename partition_t::iterator q; 00391 for (typename partition_t::iterator next = parts[*klass].begin(); 00392 next != parts[*klass].end();) 00393 { 00394 q = next; 00395 ++next; 00396 if (going_in_[*q]) 00397 { 00398 parts[new_klass].insert(parts[new_klass].end(), *q); 00399 class_[*q] = new_klass; 00400 parts[*klass].erase(q); 00401 } 00402 } 00403 } 00404 } 00405 00406 void add_new_partitions(to_treat_t& to_treat, 00407 const partition_set_t& part) 00408 { 00409 for_all_(std::list<unsigned>, klass, met_class_) 00410 { 00411 if (twin_[*klass] != 0) 00412 { 00413 for_all_const_letters(e, alphabet_) 00414 { 00415 if (find(to_treat.begin(), to_treat.end(), pair_t(*klass, *e)) != 00416 to_treat.end()) 00417 to_treat.push_back(pair_t(twin_[*klass], *e)); 00418 else 00419 if (part[*klass].size() < part[twin_[*klass]].size()) 00420 to_treat.push_back(pair_t(*klass, *e)); 00421 else 00422 to_treat.push_back(pair_t(twin_[*klass], *e)); 00423 } 00424 } 00425 } 00426 00427 for_all_(std::list<unsigned>, klass, met_class_) 00428 { 00429 count_for_[*klass] = 0; 00430 twin_[*klass] = 0; 00431 } 00432 met_class_.clear(); 00433 } 00434 00435 private: 00436 const automaton_t& input_; 00437 const alphabet_t& alphabet_; 00438 class_of_t& class_; 00439 std::vector<unsigned> count_for_; 00440 std::vector<unsigned> twin_; 00441 going_in_t going_in_; 00442 std::list<unsigned> met_class_; 00443 }; 00444 } 00445 } 00446 00447 template <typename A, typename AI1, typename AI2> 00448 void 00449 do_quotient(const AutomataBase<A>&, 00450 const algebra::NumericalSemiring&, 00451 SELECTOR(bool), 00452 Element<A, AI2>& output, 00453 const Element<A, AI1>& input) 00454 { 00455 BENCH_TASK_SCOPED("do_quotient"); 00456 00457 typedef Element<A, AI1> input_t; 00458 typedef Element<A, AI2> output_t; 00459 AUTOMATON_TYPES(input_t); 00460 AUTOMATON_FREEMONOID_TYPES(input_t); 00461 QUOTIENT_TYPES(); 00462 00463 using namespace internal::hopcroft_minimization_undet; 00464 00465 const alphabet_t& alphabet_(input.series().monoid().alphabet()); 00466 unsigned max_states = 0; 00467 00468 for_all_const_states(i, input) 00469 max_states = std::max(unsigned(*i), max_states); 00470 ++max_states; 00471 00472 /*--------------------------. 00473 | To label the subsets of Q | 00474 `--------------------------*/ 00475 unsigned max_partitions = 0; 00476 00477 /*-----------------------------------------. 00478 | To manage efficiently the partition of Q | 00479 `-----------------------------------------*/ 00480 class_of_t class_(max_states); 00481 partition_set_t part(max_states); 00482 00483 /*-------------------------. 00484 | To have a list of (P, a) | 00485 `-------------------------*/ 00486 to_treat_t to_treat; 00487 00488 /*-------------------------. 00489 | Initialize the partition | 00490 `-------------------------*/ 00491 BENCH_TASK_START("initialize partition"); 00492 00493 // In the general case, we have two sets, part[0] and part[1] One 00494 // holds the final states, the other the non-final states. In 00495 // some cases we may have only one set, for instance if we have no 00496 // final states, or if we have only final states. Because we do 00497 // not want to have an empty part[0], we will fill it with the 00498 // first kind of state (final / non-final) we encounter. 00499 unsigned final = 1; 00500 00501 for_all_const_states (p, input) 00502 { 00503 unsigned c; 00504 if (max_partitions == 0) 00505 { 00506 c = 0; 00507 final = !input.is_final(*p); 00508 } 00509 else 00510 { 00511 c = input.is_final(*p) ? final : (1 - final); 00512 } 00513 class_[*p] = c; 00514 part[c].insert(part[c].end(), *p); 00515 max_partitions = std::max(max_partitions, c + 1); 00516 } 00517 00518 BENCH_TASK_STOP(); 00519 00520 /*------------------------------. 00521 | Initialize the list of (P, a) | 00522 `------------------------------*/ 00523 BENCH_TASK_START("initialize partition"); 00524 00525 if (max_partitions > 0) 00526 for_all_const_letters (e, alphabet_) 00527 to_treat.push_back(pair_t(0, *e)); 00528 00529 if (max_partitions > 1) 00530 for_all_const_letters (e, alphabet_) 00531 to_treat.push_back(pair_t(1, *e)); 00532 00533 BENCH_TASK_STOP(); 00534 00535 /*----------. 00536 | Main loop | 00537 `----------*/ 00538 BENCH_TASK_START("main loop"); 00539 { 00540 quotient_splitter<input_t> splitter(input, class_, max_states); 00541 while (!to_treat.empty()) 00542 { 00543 BENCH_TASK_SCOPED("inner loop"); 00544 pair_t c = to_treat.front(); 00545 to_treat.pop_front(); 00546 unsigned p = c.first; 00547 letter_t a = c.second; 00548 00549 if (!splitter.compute_going_in_states(part[p], a)) 00550 continue; 00551 { 00552 BENCH_TASK_SCOPED("splitter.split"); 00553 splitter.split(part, max_partitions); 00554 } 00555 { 00556 BENCH_TASK_SCOPED("splitter.add_new_partitions"); 00557 splitter.add_new_partitions(to_treat, part); 00558 } 00559 } 00560 } 00561 00562 BENCH_TASK_STOP(); 00563 00564 /*------------------------------------. 00565 | Construction of the ouput automaton | 00566 `------------------------------------*/ 00567 BENCH_TASK_START("construct output automaton"); 00568 00569 // Create the states 00570 for (unsigned i = 0; i < max_partitions; ++i) 00571 output.add_state(); 00572 00573 std::set<unsigned> already_linked; 00574 for (unsigned i = 0; i < max_partitions; ++i) 00575 { 00576 // Get the first state of the partition => each state has the 00577 // same behaviour 00578 hstate_t s = part[i].front(); 00579 00580 if (input.is_final(s)) 00581 output.set_final(i); 00582 00583 // Create the transitions 00584 for_all_const_letters (e, alphabet_) 00585 { 00586 already_linked.clear(); 00587 00588 for (delta_iterator t(input.value(), s); ! t.done(); t.next()) 00589 { 00590 monoid_elt_t w(input.series_of(*t).structure().monoid(), *e); 00591 if (input.series_of(*t).get(w) != input.series().semiring().wzero_) 00592 { 00593 hstate_t out = input.dst_of(*t); 00594 unsigned c = class_[out]; 00595 if (already_linked.find(c) == already_linked.end()) 00596 { 00597 already_linked.insert(c); 00598 output.add_letter_transition(i, c, *e); 00599 } 00600 } 00601 } 00602 } 00603 } 00604 00605 // Set initial states. 00606 for_all_const_initial_states(i, input) 00607 output.set_initial(class_[*i]); 00608 00609 BENCH_TASK_STOP(); 00610 } 00611 00612 # undef QUOTIENT_TYPES 00613 00614 00615 /*----------------------------------------. 00616 | Quotient with multiplicities (covering) | 00617 `----------------------------------------*/ 00618 00619 template <class S, class T, 00620 typename A, typename input_t, typename output_t> 00621 void 00622 do_quotient(const AutomataBase<A>& , 00623 const S& , 00624 const T& , 00625 output_t& output, 00626 const input_t& input) 00627 { 00628 AUTOMATON_TYPES(input_t); 00629 AUTOMATON_FREEMONOID_TYPES(input_t); 00630 using namespace std; 00631 00632 /*----------------------------------------. 00633 | Declare data structures and variables. | 00634 `----------------------------------------*/ 00635 00636 typedef set<htransition_t> set_transitions_t; 00637 typedef set<hstate_t> set_states_t; 00638 typedef set<semiring_elt_t> set_semiring_elt_t; 00639 typedef vector<semiring_elt_t> vector_semiring_elt_t; 00640 typedef pair<unsigned, letter_t> pair_class_letter_t; 00641 typedef pair<hstate_t, semiring_elt_t> pair_state_semiring_elt_t; 00642 typedef set<pair_state_semiring_elt_t> set_pair_state_semiring_elt_t; 00643 typedef map<semiring_elt_t, unsigned> map_semiring_elt_t; 00644 00645 series_set_elt_t null_series = input.series().zero_; 00646 semiring_elt_t weight_zero = input.series().semiring().wzero_; 00647 monoid_elt_t monoid_identity = input.series().monoid().VCSN_EMPTY_; 00648 const alphabet_t& alphabet (input.series().monoid().alphabet()); 00649 00650 queue<pair_class_letter_t> the_queue; 00651 00652 set<unsigned> met_classes; 00653 00654 unsigned max_partition = 0; 00655 unsigned max_states = 0; 00656 00657 for_all_const_states(q, input) 00658 max_states = std::max(unsigned (*q), max_states); 00659 ++max_states; 00660 // Avoid special case problem (one initial and final state...) 00661 max_states = std::max(max_states, 2u); 00662 00663 vector< vector<set_pair_state_semiring_elt_t> > inverse (max_states); 00664 00665 map<letter_t, unsigned> pos_of_letter; 00666 00667 unsigned max_pos = 0; 00668 00669 for_all_const_letters(a, alphabet) 00670 pos_of_letter[*a] = max_pos++; 00671 00672 set_states_t states_visited; 00673 set_semiring_elt_t semiring_had_class; 00674 vector<set_states_t> classes (max_states); 00675 vector<unsigned> class_of_state (max_states); 00676 vector_semiring_elt_t old_weight (max_states); 00677 map_semiring_elt_t class_of_weight; 00678 00679 for (unsigned i = 0; i < max_states; ++i) 00680 inverse[i].resize(max_pos); 00681 00682 for_all_const_states(q, input) 00683 for_all_const_letters(a, alphabet) 00684 { 00685 00686 for_all_const_(set_states_t, r, states_visited) 00687 old_weight[*r] = weight_zero; 00688 states_visited.clear(); 00689 00690 for (rdelta_iterator e(input.value(), *q); ! e.done(); e.next()) 00691 { 00692 monoid_elt_t w(input.series_of(*e).structure().monoid(), *a); 00693 if (input.series_of(*e).get(w) != input.series().semiring().wzero_) 00694 { 00695 hstate_t p = input.src_of(*e); 00696 if (states_visited.find(p) != states_visited.end()) 00697 inverse[*q][pos_of_letter[*a]]. 00698 erase(pair_state_semiring_elt_t (p, old_weight[p])); 00699 else 00700 states_visited.insert(p); 00701 series_set_elt_t sd = input.series_of(*e); 00702 monoid_elt_t md (input.structure().series().monoid(), *a); 00703 semiring_elt_t wsd = sd.get(md); 00704 old_weight[p] += wsd; 00705 inverse[*q][pos_of_letter[*a]]. 00706 insert(pair_state_semiring_elt_t (p, old_weight[p])); 00707 } 00708 } 00709 } 00710 00711 /*-----------------------------------------------------------. 00712 | Initialize the partition with as many classes as there are | 00713 | final values. | 00714 `-----------------------------------------------------------*/ 00715 00716 bool empty = true; 00717 unsigned class_non_final (0); 00718 00719 for_all_const_states(q, input) 00720 { 00721 if (not input.is_final(*q)) 00722 { 00723 if (empty == true) 00724 { 00725 empty = false; 00726 class_non_final = max_partition; 00727 max_partition++; 00728 } 00729 classes[class_non_final].insert(*q); 00730 class_of_state[*q] = class_non_final; 00731 } 00732 else 00733 { 00734 semiring_elt_t w = input.get_final(*q).get(monoid_identity); 00735 if (semiring_had_class.find(w) == semiring_had_class.end()) 00736 { 00737 semiring_had_class.insert(w); 00738 classes[max_partition].insert(*q); 00739 class_of_weight[w] = max_partition; 00740 class_of_state[*q] = max_partition; 00741 max_partition++; 00742 } 00743 else 00744 { 00745 classes[class_of_weight[w]].insert(*q); 00746 class_of_state[*q] = class_of_weight[w]; 00747 } 00748 } 00749 } 00750 00751 /*-----------------------------------------------------. 00752 | Initialize the queue with pairs <class_id, letter>. | 00753 `-----------------------------------------------------*/ 00754 00755 for (unsigned i = 0; i < max_partition; i++) 00756 for_all_const_letters(a, alphabet) 00757 the_queue.push(pair_class_letter_t (i, *a)); 00758 00759 /*----------------. 00760 | The main loop. | 00761 `----------------*/ 00762 00763 unsigned old_max_partition = max_partition; 00764 00765 while(not the_queue.empty()) 00766 { 00767 pair_class_letter_t pair = the_queue.front(); 00768 the_queue.pop(); 00769 met_classes.clear(); 00770 vector_semiring_elt_t val (max_states); 00771 00772 // FIXME: Isn't there an easier way to do this? 00773 for_all_const_states(q, input) 00774 val[*q] = 0; 00775 00776 // First, calculate val[state] and not met_classes. 00777 for_all_const_(set_states_t, q, classes[pair.first]) 00778 for_all_const_(set_pair_state_semiring_elt_t, pair_, 00779 inverse[*q][pos_of_letter[pair.second]]) 00780 { 00781 unsigned state = pair_->first; 00782 if (met_classes.find(class_of_state[state]) == 00783 met_classes.end()) 00784 met_classes.insert(class_of_state[state]); 00785 val[state] += pair_->second; 00786 } 00787 00788 // Next, for each met class, do the partition. 00789 for_all_const_(set<unsigned>, class_id, met_classes) 00790 { 00791 if (classes[*class_id].size() == 1) 00792 continue ; 00793 00794 queue<hstate_t> to_erase; 00795 semiring_elt_t next_val; 00796 semiring_elt_t first_val = val[*(classes[*class_id].begin())]; 00797 class_of_weight.clear(); 00798 semiring_had_class.clear(); 00799 00800 for_all_const_(set_states_t, p, classes[*class_id]) 00801 { 00802 next_val = val[*p]; 00803 // This state must be moved to another class! 00804 if (next_val != first_val) 00805 { 00806 if (semiring_had_class.find(next_val) == 00807 semiring_had_class.end()) // Must create a new class 00808 { 00809 classes[max_partition].insert(*p); 00810 class_of_state[*p] = max_partition; 00811 semiring_had_class.insert(next_val); 00812 class_of_weight[next_val] = max_partition; 00813 max_partition++; 00814 } 00815 else 00816 { 00817 classes[class_of_weight[next_val]].insert(*p); 00818 class_of_state[*p] = class_of_weight[next_val]; 00819 } 00820 to_erase.push(*p); 00821 } 00822 } 00823 00824 while(not to_erase.empty()) 00825 { 00826 hstate_t s = to_erase.front(); 00827 to_erase.pop(); 00828 classes[*class_id].erase(s); 00829 } 00830 00831 // Push pairs <new_class_id, letter> into the queue. 00832 for (unsigned i = old_max_partition; i < max_partition; i++) 00833 for_all_const_letters(b, alphabet) 00834 the_queue.push(pair_class_letter_t(i, *b)); 00835 old_max_partition = max_partition; 00836 } 00837 } 00838 00839 /*------------------. 00840 | Form the output. | 00841 `------------------*/ 00842 00843 typedef vector<series_set_elt_t> vector_series_set_elt_t; 00844 00845 std::vector<hstate_t> out_states (max_partition); 00846 00847 // Add states. 00848 for(unsigned i = 0; i < max_partition; i++) 00849 { 00850 out_states[i] = output.add_state(); 00851 hstate_t a_state = *classes[i].begin(); 00852 series_set_elt_t a_serie = null_series; 00853 00854 for_all_const_(set_states_t, state, classes[i]) 00855 if(input.is_initial(*state)) 00856 a_serie += input.get_initial(*state); 00857 00858 output.set_initial(out_states[i] , a_serie); 00859 00860 if (input.is_final(a_state)) 00861 output.set_final(out_states[i] , input.get_final(a_state)); 00862 } 00863 00864 // Add transitions. 00865 vector_series_set_elt_t seriesof (max_partition, null_series); 00866 00867 for(unsigned i = 0; i < max_partition; i++) 00868 { 00869 met_classes.clear(); 00870 00871 for (delta_iterator e(input.value(), *classes[i].begin()); ! e.done(); e.next()) 00872 { 00873 series_set_elt_t se = input.series_of(*e); 00874 unsigned cs = class_of_state[input.dst_of(*e)]; 00875 00876 if (met_classes.find(cs) == met_classes.end()) 00877 { 00878 met_classes.insert(cs); 00879 seriesof[cs] = se; 00880 } 00881 else 00882 seriesof[cs] += se; 00883 } 00884 00885 for_all_const_(set<unsigned>, cs, met_classes) 00886 if (seriesof[*cs] != null_series) 00887 output.add_series_transition(out_states[i], 00888 out_states[*cs], 00889 seriesof[*cs]); 00890 } 00891 } 00892 00893 template<typename A, typename AI> 00894 Element<A, AI> 00895 quotient(const Element<A, AI>& a) 00896 { 00897 BENCH_TASK_SCOPED("quotient"); 00898 precondition(is_realtime(a)); 00899 typedef Element<A, AI> automaton_t; 00900 AUTOMATON_TYPES(automaton_t); 00901 automaton_t output(a.structure()); 00902 do_quotient(a.structure(), a.structure().series().semiring(), 00903 SELECT(semiring_elt_value_t), output, a); 00904 return output; 00905 } 00906 00907 } // vcsn 00908 00909 #endif // ! VCSN_ALGORITHMS_MINIMIZATION_HOPCROFT_HXX