From db4693b30392f8c27713cb2dc4a5787ed268b56b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 2 May 2012 17:57:38 +0200 Subject: [PATCH] Downcase a couple of misnamed class names. * src/misc/acccompl.hh, src/misc/acccompl.cc (AccCompl): Rename to acc_compl. * src/tgbaalgos/simulation.cc (AccComplAutomaton, Simulation): Rename to acc_compl_automaton and direct_simulation. At the same time, reindent the whole file. * src/sanity/style.test: Detect capitalized class names. * src/kripke/kripkeexplicit.hh (KripkePrint): Remove useless predeclaration. * src/tgbaalgos/simulation.hh: Typo in comment. --- src/kripke/kripkeexplicit.hh | 8 +- src/misc/acccompl.cc | 4 +- src/misc/acccompl.hh | 12 +- src/sanity/style.test | 3 + src/tgbaalgos/simulation.cc | 626 ++++++++++++++++++----------------- src/tgbaalgos/simulation.hh | 2 +- 6 files changed, 329 insertions(+), 326 deletions(-) diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh index ba33f1b6f..bc09beccd 100644 --- a/src/kripke/kripkeexplicit.hh +++ b/src/kripke/kripkeexplicit.hh @@ -1,4 +1,5 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -29,10 +30,7 @@ namespace spot { - // Define in kripkeprint.hh - class KripkeVisitor; - -/// \brief Concrete class for kripke states. + /// \brief Concrete class for kripke states. class state_kripke : public state { friend class kripke_explicit; diff --git a/src/misc/acccompl.cc b/src/misc/acccompl.cc index 4434377b0..cb2156c6f 100644 --- a/src/misc/acccompl.cc +++ b/src/misc/acccompl.cc @@ -34,7 +34,7 @@ namespace spot // we need to know wich one is go to one when true. So we are looping // through the conditions until bdd_high is true. // Once found, we keep only it. - bdd AccCompl::complement(const bdd acc) + bdd acc_compl::complement(const bdd acc) { bdd_cache_t::const_iterator it = cache_.find(acc); if (it != cache_.end()) @@ -70,7 +70,7 @@ namespace spot } - bdd AccCompl::reverse_complement(const bdd acc) + bdd acc_compl::reverse_complement(const bdd acc) { // We are sure that if we have no acceptance condition // the result is all_. diff --git a/src/misc/acccompl.hh b/src/misc/acccompl.hh index 9a14a209a..43315dbc2 100644 --- a/src/misc/acccompl.hh +++ b/src/misc/acccompl.hh @@ -30,14 +30,14 @@ namespace spot { - /// \brief Help class to convert a bdd of an automaton into - /// its complement. - /// This is used when you need to complement all the acceptance - /// conditions in an automaton. For example in the simulation. - class AccCompl + /// \brief Helper class to convert acceptance conditions into promises + /// + /// A set of acceptance conditions represented by the sum "à la Spot", + /// is converted into a product of promises. + class acc_compl { public: - AccCompl(bdd all, bdd neg) + acc_compl(bdd all, bdd neg) : all_(all), neg_(neg) { diff --git a/src/sanity/style.test b/src/sanity/style.test index 8c98c91a6..509cb68ed 100755 --- a/src/sanity/style.test +++ b/src/sanity/style.test @@ -67,6 +67,9 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do case $file in *.test);; *) + grep -E '[^<]class[ \t]+[A-Z]' $tmp && + diag 'Use lower case class names.' + grep '[ ]if(' $tmp && diag 'Missing space after "if"' diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 58dbbebd3..9b6306f60 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -60,7 +60,7 @@ // state. This function is `update_sig'. // - Enter in a double loop to adapt the partial order, and set // 'relation_' accordingly. This function is `update_po'. -// 3. Rename the class (to actualize the name in the previous_it_class and +// 3. Rename the class (to actualize the name in the previous_class and // in relation_). // 4. Building an automaton with the result, with the condition: // "a transition in the original automaton appears in the simulated one @@ -99,20 +99,20 @@ namespace spot bdd_less_than> map_bdd_lstate; - // This class takes an automaton and creates a copy with all - // acceptance conditions complemented. - class AccComplAutomaton: + // This class takes an automaton and creates a copy with all + // acceptance conditions complemented. + class acc_compl_automaton: public tgba_reachable_iterator_depth_first - { + { public: - AccComplAutomaton(const tgba* a) - : tgba_reachable_iterator_depth_first(a), - size(0), - out_(new tgba_explicit_number(a->get_dict())), - ea_(a), - ac_(ea_->all_acceptance_conditions(), - ea_->neg_acceptance_conditions()), - current_max(0) + acc_compl_automaton(const tgba* a) + : tgba_reachable_iterator_depth_first(a), + size(0), + out_(new tgba_explicit_number(a->get_dict())), + ea_(a), + ac_(ea_->all_acceptance_conditions(), + ea_->neg_acceptance_conditions()), + current_max(0) { init_ = ea_->get_init_state(); out_->set_init_state(get_state(init_)); @@ -122,10 +122,10 @@ namespace spot get_state(const state* s) { if (state2int.find(s) == state2int.end()) - { - state2int[s] = ++current_max; - previous_it_class_[out_->add_state(current_max)] = bddfalse; - } + { + state2int[s] = ++current_max; + previous_class_[out_->add_state(current_max)] = bddfalse; + } return state2int[s]; } @@ -155,7 +155,7 @@ namespace spot ++size; } - ~AccComplAutomaton() + ~acc_compl_automaton() { init_->destroy(); } @@ -163,128 +163,128 @@ namespace spot public: size_t size; tgba_explicit_number* out_; - map_state_bdd previous_it_class_; + map_state_bdd previous_class_; private: const tgba* ea_; - AccCompl ac_; + acc_compl ac_; map_state_unsigned state2int; unsigned current_max; state* init_; - }; + }; - class Simulation + class direct_simulation { - // Shortcut used in update_po and go_to_next_it. - typedef std::map map_bdd_bdd; - public: - Simulation(const tgba* t) - : a_(0), - po_size_(0), - all_class_var_(bddtrue) - { - AccComplAutomaton - acc_compl(t); + // Shortcut used in update_po and go_to_next_it. + typedef std::map map_bdd_bdd; + public: + direct_simulation(const tgba* t) + : a_(0), + po_size_(0), + all_class_var_(bddtrue) + { + acc_compl_automaton + acc_compl(t); - // We'll start our work by replacing all the acceptance - // conditions by their complement. - acc_compl.run(); + // We'll start our work by replacing all the acceptance + // conditions by their complement. + acc_compl.run(); - a_ = acc_compl.out_; + a_ = acc_compl.out_; - // We use the previous run to know the size of the - // automaton, and to class all the reachable states in the - // map previous_it_class_. - size_a_ = acc_compl.size; + // We use the previous run to know the size of the + // automaton, and to class all the reachable states in the + // map previous_class_. + size_a_ = acc_compl.size; - // Now, we have to get the bdd which will represent the - // class. We register one bdd by state, because in the worst - // case, |Class| == |State|. - unsigned set_num = a_->get_dict() - ->register_anonymous_variables(size_a_, a_); - bdd init = bdd_ithvar(set_num); + // Now, we have to get the bdd which will represent the + // class. We register one bdd by state, because in the worst + // case, |Class| == |State|. + unsigned set_num = a_->get_dict() + ->register_anonymous_variables(size_a_, a_); + bdd init = bdd_ithvar(set_num); - // Because we have already take the first element which is init. - ++set_num; + // Because we have already take the first element which is init. + ++set_num; - used_var_.push_back(init); - all_class_var_ = init; + used_var_.push_back(init); + all_class_var_ = init; - // We fetch the result the run of AccComplAutomaton which - // has recorded all the state in a hash table, and we set all - // to init. - for (map_state_bdd::iterator it - = acc_compl.previous_it_class_.begin(); - it != acc_compl.previous_it_class_.end(); - ++it) + // We fetch the result the run of acc_compl_automaton which + // has recorded all the state in a hash table, and we set all + // to init. + for (map_state_bdd::iterator it + = acc_compl.previous_class_.begin(); + it != acc_compl.previous_class_.end(); + ++it) { - previous_it_class_[it->first] = init; + previous_class_[it->first] = init; } - // Put all the anonymous variable in a queue, and record all - // of these in a variable all_class_var_ which will be used - // to understand the destination part in the signature when - // building the resulting automaton. - for (unsigned i = set_num; i < set_num + size_a_ - 1; ++i) + // Put all the anonymous variable in a queue, and record all + // of these in a variable all_class_var_ which will be used + // to understand the destination part in the signature when + // building the resulting automaton. + for (unsigned i = set_num; i < set_num + size_a_ - 1; ++i) { free_var_.push(i); all_class_var_ &= bdd_ithvar(i); } - relation_[init] = init; - } + relation_[init] = init; + } - // Reverse all the acceptance condition at the destruction of - // this object, because it occurs after the return of the - // function simulation. - ~Simulation() - { - delete a_; - } + // Reverse all the acceptance condition at the destruction of + // this object, because it occurs after the return of the + // function simulation. + ~direct_simulation() + { + delete a_; + } - // We update the name of the class. - void update_previous_it_class() - { - std::list::iterator it_bdd = used_var_.begin(); + // We update the name of the class. + void update_previous_class() + { + std::list::iterator it_bdd = used_var_.begin(); - // We run through the map bdd/list, and we update - // the previous_it_class_ with the new data. - it_bdd = used_var_.begin(); - for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); - it != bdd_lstate_.end(); - ++it) + // We run through the map bdd/list, and we update + // the previous_class_ with the new data. + it_bdd = used_var_.begin(); + for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); + it != bdd_lstate_.end(); + ++it) { for (std::list::iterator it_s = it->second.begin(); it_s != it->second.end(); ++it_s) - { - // If the signature of a state is bddfalse (which is - // roughly equivalent to no transition) the class of - // this state is bddfalse instead of an anonymous - // variable. It allows simplifications in the signature - // by removing a transition which has as a destination a - // state with no outgoing transition. - if (it->first == bddfalse) - previous_it_class_[*it_s] = bddfalse; - else - previous_it_class_[*it_s] = *it_bdd; - } + { + // If the signature of a state is bddfalse (which is + // roughly equivalent to no transition) the class of + // this state is bddfalse instead of an anonymous + // variable. It allows simplifications in the signature + // by removing a transition which has as a destination a + // state with no outgoing transition. + if (it->first == bddfalse) + previous_class_[*it_s] = bddfalse; + else + previous_class_[*it_s] = *it_bdd; + } ++it_bdd; } - } + } - // The core loop of the algorithm. - tgba* run() - { - unsigned int nb_partition_before = 0; - unsigned int nb_po_before = po_size_ - 1; - while (nb_partition_before != bdd_lstate_.size() - || nb_po_before != po_size_) + // The core loop of the algorithm. + tgba* run() + { + unsigned int nb_partition_before = 0; + unsigned int nb_po_before = po_size_ - 1; + while (nb_partition_before != bdd_lstate_.size() + || nb_po_before != po_size_) { - update_previous_it_class(); + update_previous_class(); nb_partition_before = bdd_lstate_.size(); bdd_lstate_.clear(); nb_po_before = po_size_; @@ -293,17 +293,17 @@ namespace spot go_to_next_it(); } - update_previous_it_class(); - return build_result(); - } + update_previous_class(); + return build_result(); + } - // Take a state and compute its signature. - bdd compute_sig(const state* src) - { - tgba_succ_iterator* sit = a_->succ_iter(src); - bdd res = bddfalse; + // Take a state and compute its signature. + bdd compute_sig(const state* src) + { + tgba_succ_iterator* sit = a_->succ_iter(src); + bdd res = bddfalse; - for (sit->first(); !sit->done(); sit->next()) + for (sit->first(); !sit->done(); sit->next()) { const state* dst = sit->current_state(); bdd acc = sit->current_acceptance_conditions(); @@ -312,65 +312,65 @@ namespace spot // the label of the transition and the class of the // destination and all the class it implies. bdd to_add = acc & sit->current_condition() - & relation_[previous_it_class_[dst]]; + & relation_[previous_class_[dst]]; res |= to_add; dst->destroy(); } - delete sit; - return res; - } + delete sit; + return res; + } - void update_sig() - { - // At this time, current_class_ must be empty. It implies - // that the "previous_it_class_ = current_class_" must be - // done before. - assert(current_class_.empty()); + void update_sig() + { + // At this time, current_class_ must be empty. It implies + // that the "previous_class_ = current_class_" must be + // done before. + assert(current_class_.empty()); - // Here we suppose that previous_it_class_ always contains - // all the reachable states of this automaton. We do not - // have to make (again) a traversal. We just have to run - // through this map. - for (map_state_bdd::iterator it = previous_it_class_.begin(); - it != previous_it_class_.end(); - ++it) + // Here we suppose that previous_class_ always contains + // all the reachable states of this automaton. We do not + // have to make (again) a traversal. We just have to run + // through this map. + for (map_state_bdd::iterator it = previous_class_.begin(); + it != previous_class_.end(); + ++it) { const state* src = it->first; bdd_lstate_[compute_sig(src)].push_back(src); } - } + } - // This method rename the color set, update the partial order. - void go_to_next_it() - { - int nb_new_color = bdd_lstate_.size() - used_var_.size(); + // This method rename the color set, update the partial order. + void go_to_next_it() + { + int nb_new_color = bdd_lstate_.size() - used_var_.size(); - for (int i = 0; i < nb_new_color; ++i) + for (int i = 0; i < nb_new_color; ++i) { assert(!free_var_.empty()); used_var_.push_back(bdd_ithvar(free_var_.front())); free_var_.pop(); } - assert(bdd_lstate_.size() == used_var_.size()); + assert(bdd_lstate_.size() == used_var_.size()); - // Now we make a temporary hash_table which links the tuple - // "C^(i-1), N^(i-1)" to the new class coloring. If we - // rename the class before updating the partial order, we - // loose the information, and if we make it after, I can't - // figure out how to apply this renaming on rel_. - // It adds a data structure but it solves our problem. - map_bdd_bdd now_to_next; + // Now we make a temporary hash_table which links the tuple + // "C^(i-1), N^(i-1)" to the new class coloring. If we + // rename the class before updating the partial order, we + // loose the information, and if we make it after, I can't + // figure out how to apply this renaming on rel_. + // It adds a data structure but it solves our problem. + map_bdd_bdd now_to_next; - std::list::iterator it_bdd = used_var_.begin(); + std::list::iterator it_bdd = used_var_.begin(); - for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); - it != bdd_lstate_.end(); - ++it) + for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); + it != bdd_lstate_.end(); + ++it) { // If the signature of a state is bddfalse (which is // roughly equivalent to no transition) the class of @@ -385,85 +385,85 @@ namespace spot ++it_bdd; } - update_po(now_to_next); - } + update_po(now_to_next); + } - // This function computes the new po with previous_it_class_ - // and the argument. `now_to_next' contains the relation - // between the signature and the future name of the class. - void update_po(const map_bdd_bdd& now_to_next) - { - // This loop follows the pattern given by the paper. - // foreach class do - // | foreach class do - // | | update po if needed - // | od - // od + // This function computes the new po with previous_class_ + // and the argument. `now_to_next' contains the relation + // between the signature and the future name of the class. + void update_po(const map_bdd_bdd& now_to_next) + { + // This loop follows the pattern given by the paper. + // foreach class do + // | foreach class do + // | | update po if needed + // | od + // od - for (map_bdd_bdd::const_iterator it1 = now_to_next.begin(); - it1 != now_to_next.end(); - ++it1) + for (map_bdd_bdd::const_iterator it1 = now_to_next.begin(); + it1 != now_to_next.end(); + ++it1) { bdd accu = it1->second; for (map_bdd_bdd::const_iterator it2 = now_to_next.begin(); it2 != now_to_next.end(); ++it2) - { - // Skip the case managed by the initialization of accu. - if (it1 == it2) - continue; + { + // Skip the case managed by the initialization of accu. + if (it1 == it2) + continue; - // We detect that "a&b -> a" by testing "a&b = a". - if ((it1->first & it2->first) == (it1->first)) - { - accu &= it2->second; - ++po_size_; - } - } + // We detect that "a&b -> a" by testing "a&b = a". + if ((it1->first & it2->first) == (it1->first)) + { + accu &= it2->second; + ++po_size_; + } + } relation_[it1->second] = accu; } - } + } - // Build the minimal resulting automaton. - tgba* build_result() - { - // Now we need to create a state per partition. But the - // problem is that we don't know exactly the class. We know - // that it is a combination of the acceptance condition - // contained in all_class_var_. So we need to make a little - // workaround. We will create a map which will associate bdd - // and unsigned. - std::map bdd2state; - unsigned int current_max = 0; + // Build the minimal resulting automaton. + tgba* build_result() + { + // Now we need to create a state per partition. But the + // problem is that we don't know exactly the class. We know + // that it is a combination of the acceptance condition + // contained in all_class_var_. So we need to make a little + // workaround. We will create a map which will associate bdd + // and unsigned. + std::map bdd2state; + unsigned int current_max = 0; - bdd all_acceptance_conditions - = a_->all_acceptance_conditions(); + bdd all_acceptance_conditions + = a_->all_acceptance_conditions(); - // We have all the a_'s acceptances conditions - // complemented. So we need to complement it when adding a - // transition. We *must* keep the complemented because it - // is easy to know if an acceptance condition is maximal or - // not. - AccCompl reverser(all_acceptance_conditions, - a_->neg_acceptance_conditions()); + // We have all the a_'s acceptances conditions + // complemented. So we need to complement it when adding a + // transition. We *must* keep the complemented because it + // is easy to know if an acceptance condition is maximal or + // not. + acc_compl reverser(all_acceptance_conditions, + a_->neg_acceptance_conditions()); - typedef tgba_explicit_number::transition trs; - tgba_explicit_number* res - = new tgba_explicit_number(a_->get_dict()); - res->set_acceptance_conditions - (all_acceptance_conditions); + typedef tgba_explicit_number::transition trs; + tgba_explicit_number* res + = new tgba_explicit_number(a_->get_dict()); + res->set_acceptance_conditions + (all_acceptance_conditions); - bdd sup_all_acc = bdd_support(all_acceptance_conditions); - // Non atomic propositions variables (= acc and class) - bdd nonapvars = sup_all_acc & bdd_support(all_class_var_); + bdd sup_all_acc = bdd_support(all_acceptance_conditions); + // Non atomic propositions variables (= acc and class) + bdd nonapvars = sup_all_acc & bdd_support(all_class_var_); - // Create one state per partition. - for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); - it != bdd_lstate_.end(); ++it) + // Create one state per partition. + for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); + it != bdd_lstate_.end(); ++it) { res->add_state(++current_max); - bdd part = previous_it_class_[*it->second.begin()]; + bdd part = previous_class_[*it->second.begin()]; // The difference between the two next lines is: // the first says "if you see A", the second "if you @@ -472,11 +472,11 @@ namespace spot bdd2state[relation_[part]] = current_max; } - // For each partition, we will create - // all the transitions between the states. - for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); - it != bdd_lstate_.end(); - ++it) + // For each partition, we will create + // all the transitions between the states. + for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); + it != bdd_lstate_.end(); + ++it) { // Get the signature. bdd sig = compute_sig(*(it->second.begin())); @@ -494,80 +494,82 @@ namespace spot // First loop over all possible valuations atomic properties. while (all_atomic_prop != bddfalse) - { - bdd one = bdd_satoneset(all_atomic_prop, - sup_all_atomic_prop, - bddtrue); - all_atomic_prop -= one; + { + bdd one = bdd_satoneset(all_atomic_prop, + sup_all_atomic_prop, + bddtrue); + all_atomic_prop -= one; - // For each possible valuation, iterator over all possible - // destination classes. We use minato_isop here, because - // if the same valuation of atomic properties can go - // to two different classes C1 and C2, iterating on - // C1 + C2 with the above bdd_satoneset loop will see - // C1 then (!C1)C2, instead of C1 then C2. - // With minatop_isop, we ensure that the no negative - // class variable will be seen (likewise for promises). - minato_isop isop(sig & one); + // For each possible valuation, iterator over all possible + // destination classes. We use minato_isop here, because + // if the same valuation of atomic properties can go + // to two different classes C1 and C2, iterating on + // C1 + C2 with the above bdd_satoneset loop will see + // C1 then (!C1)C2, instead of C1 then C2. + // With minatop_isop, we ensure that the no negative + // class variable will be seen (likewise for promises). + minato_isop isop(sig & one); - bdd cond_acc_dest; - while ((cond_acc_dest = isop.next()) != bddfalse) - { - // Take the transition, and keep only the variable which - // are used to represent the class. - bdd dest = bdd_existcomp(cond_acc_dest, - all_class_var_); + bdd cond_acc_dest; + while ((cond_acc_dest = isop.next()) != bddfalse) + { + // Take the transition, and keep only the variable which + // are used to represent the class. + bdd dest = bdd_existcomp(cond_acc_dest, + all_class_var_); - // Keep only ones who are acceptance condition. - bdd acc = bdd_existcomp(cond_acc_dest, sup_all_acc); + // Keep only ones who are acceptance condition. + bdd acc = bdd_existcomp(cond_acc_dest, sup_all_acc); - // Keep the other ! - bdd cond = bdd_existcomp(cond_acc_dest, sup_all_atomic_prop); + // Keep the other ! + bdd cond = bdd_existcomp(cond_acc_dest, + sup_all_atomic_prop); - // Because we have complemented all the acceptance condition - // on the input automaton, we must re invert them to create - // a new transition. - acc = reverser.reverse_complement(acc); + // Because we have complemented all the acceptance + // condition on the input automaton, we must re + // invert them to create a new transition. + acc = reverser.reverse_complement(acc); - // Take the id of the source and destination. - // To know the source, we must take a random state in the - // list which is in the class we currently work on. - int src = bdd2state[previous_it_class_[*it->second.begin()]]; - int dst = bdd2state[dest]; + // Take the id of the source and destination. To + // know the source, we must take a random state in + // the list which is in the class we currently + // work on. + int src = bdd2state[previous_class_[*it->second.begin()]]; + int dst = bdd2state[dest]; - // src or dst == 0 means "dest" or "prev..." isn't in the map. - // so it is a bug. - assert(src != 0); - assert(dst != 0); + // src or dst == 0 means "dest" or "prev..." isn't + // in the map. so it is a bug. + assert(src != 0); + assert(dst != 0); - // Create the transition, add the condition and the - // acceptance condition. - tgba_explicit_number::transition* t - = res->create_transition(src , dst); - res->add_conditions(t, cond); - res->add_acceptance_conditions(t, acc); - } - } + // Create the transition, add the condition and the + // acceptance condition. + tgba_explicit_number::transition* t + = res->create_transition(src , dst); + res->add_conditions(t, cond); + res->add_acceptance_conditions(t, acc); + } + } } - res->set_init_state(bdd2state[previous_it_class_ - [a_->get_init_state()]]); - res->merge_transitions(); - return res; - } + res->set_init_state(bdd2state[previous_class_ + [a_->get_init_state()]]); + res->merge_transitions(); + return res; + } - // Debug: - // In a first time, print the signature, and the print a list - // of each state in this partition. - // In a second time, print foreach state, who is where, - // where is the new class name. - void print_partition() - { - for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); - it != bdd_lstate_.end(); - ++it) + // Debug: + // In a first time, print the signature, and the print a list + // of each state in this partition. + // In a second time, print foreach state, who is where, + // where is the new class name. + void print_partition() + { + for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); + it != bdd_lstate_.end(); + ++it) { std::cerr << "partition: " << bdd_format_set(a_->get_dict(), it->first) << std::endl; @@ -575,70 +577,70 @@ namespace spot for (std::list::iterator it_s = it->second.begin(); it_s != it->second.end(); ++it_s) - { - std::cerr << " - " - << a_->format_state(*it_s) << std::endl; - } + { + std::cerr << " - " + << a_->format_state(*it_s) << std::endl; + } } - std::cerr << "\nPrevious iteration\n" << std::endl; + std::cerr << "\nPrevious iteration\n" << std::endl; - for (map_state_bdd::const_iterator it = previous_it_class_.begin(); - it != previous_it_class_.end(); - ++it) + for (map_state_bdd::const_iterator it = previous_class_.begin(); + it != previous_class_.end(); + ++it) { std::cerr << a_->format_state(it->first) << " was in " << bdd_format_set(a_->get_dict(), it->second) << std::endl; } - } + } - private: - // The automaton which is simulated. - tgba_explicit_number* a_; + private: + // The automaton which is simulated. + tgba_explicit_number* a_; - // Relation is aimed to represent the same thing than - // rel_. The difference is in the way it does. - // If A => A /\ A => B, rel will be (!A U B), but relation_ - // will have A /\ B at the key A. This trick is due to a problem - // with the computation of the resulting automaton with the signature. - // rel_ will pollute the meaning of the signature. - map_bdd_bdd relation_; + // Relation is aimed to represent the same thing than + // rel_. The difference is in the way it does. + // If A => A /\ A => B, rel will be (!A U B), but relation_ + // will have A /\ B at the key A. This trick is due to a problem + // with the computation of the resulting automaton with the signature. + // rel_ will pollute the meaning of the signature. + map_bdd_bdd relation_; - // Represent the class of each state at the previous iteration. - map_state_bdd previous_it_class_; + // Represent the class of each state at the previous iteration. + map_state_bdd previous_class_; - // The class at the current iteration. - map_state_bdd current_class_; + // The class at the current iteration. + map_state_bdd current_class_; - // The list of state for each class at the current_iteration. - // Computed in `update_sig'. - map_bdd_lstate bdd_lstate_; + // The list of state for each class at the current_iteration. + // Computed in `update_sig'. + map_bdd_lstate bdd_lstate_; - // The queue of free bdd. They will be used as the identifier - // for the class. - std::queue free_var_; + // The queue of free bdd. They will be used as the identifier + // for the class. + std::queue free_var_; - // The list of used bdd. They are in used as identifier for class. - std::list used_var_; + // The list of used bdd. They are in used as identifier for class. + std::list used_var_; - // Size of the automaton. - unsigned int size_a_; + // Size of the automaton. + unsigned int size_a_; - // Used to know when there is no evolution in the po. Updated - // in the `update_po' method. - unsigned int po_size_; + // Used to know when there is no evolution in the po. Updated + // in the `update_po' method. + unsigned int po_size_; - // All the class variable: - bdd all_class_var_; + // All the class variable: + bdd all_class_var_; }; } // End namespace anonymous. tgba* simulation(const tgba* t) { - Simulation simul(t); + direct_simulation simul(t); return simul.run(); } diff --git a/src/tgbaalgos/simulation.hh b/src/tgbaalgos/simulation.hh index 40301845d..6373039b6 100644 --- a/src/tgbaalgos/simulation.hh +++ b/src/tgbaalgos/simulation.hh @@ -35,7 +35,7 @@ namespace spot /// When the language recognized by one state is included in the /// language recognized by an another one, the first one is merged /// with the second. The algorithm is based on the following - /// paper, but generalized to handled TGBA directly. + /// paper, but generalized to handle TGBA directly. /// /// \verbatim /// @InProceedings{ etessami.00.concur,