diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc index d885dfffa..abbfe9a2d 100644 --- a/src/tgbaalgos/dupexp.cc +++ b/src/tgbaalgos/dupexp.cc @@ -73,10 +73,7 @@ namespace spot class dupexp_iter_save: public dupexp_iter { public: - dupexp_iter_save(const tgba* a, - std::map& relation) + dupexp_iter_save(const tgba* a, std::vector& relation) : dupexp_iter(a), relation_(relation) { } @@ -84,12 +81,12 @@ namespace spot virtual void end() { + relation_.resize(this->seen.size()); for (auto s: this->seen) - relation_[this->out_->state_from_number(s.second - 1)] - = const_cast(s.first); + relation_[s.second - 1] = const_cast(s.first); } - std::map& relation_; + std::vector& relation_; }; } // anonymous @@ -111,23 +108,17 @@ namespace spot } tgba_digraph* - tgba_dupexp_bfs(const tgba* aut, - std::map& rel) + tgba_dupexp_bfs(const tgba* aut, std::vector& rel) { - dupexp_iter_save di(aut, - rel); + dupexp_iter_save di(aut, rel); di.run(); return di.result(); } tgba_digraph* - tgba_dupexp_dfs(const tgba* aut, - std::map& rel) + tgba_dupexp_dfs(const tgba* aut, std::vector& rel) { - dupexp_iter_save di(aut, - rel); + dupexp_iter_save di(aut, rel); di.run(); return di.result(); } diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh index f50d4ef85..a0aedce66 100644 --- a/src/tgbaalgos/dupexp.hh +++ b/src/tgbaalgos/dupexp.hh @@ -41,17 +41,20 @@ namespace spot /// \ingroup tgba_misc /// \brief Build an explicit automaton from all states of \a aut, /// numbering states in bread first order as they are processed. + /// \a aut the automaton to duplicate + /// \a relation a map of all the new states (represented by + /// their number) to the old states. SPOT_API tgba_digraph* - tgba_dupexp_bfs(const tgba* aut, - std::map& relation); + tgba_dupexp_bfs(const tgba* aut, std::vector& relation); + /// \ingroup tgba_misc /// \brief Build an explicit automata from all states of \a aut, /// numbering states in depth first order as they are processed. + /// \a aut the automaton to duplicate + /// \a relation a map of all the new states (represented by + /// their number) to the old states. SPOT_API tgba_digraph* - tgba_dupexp_dfs(const tgba* aut, - std::map& relation); + tgba_dupexp_dfs(const tgba* aut, std::vector& relation); } #endif // SPOT_TGBAALGOS_DUPEXP_HH diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 8397ddf05..ad2ee2b04 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -98,9 +98,6 @@ namespace spot state_ptr_equal> map_state_bdd; typedef std::vector vector_state_bdd; - typedef std::map map_state_state; - typedef std::vector vector_state_state; @@ -393,15 +390,12 @@ namespace spot bdd acc = bddtrue; map_constraint::const_iterator it; - // We are using - // new_original_[old_a_->state_from_number(...)] because - // we have the constraints in the original automaton which - // has been duplicated twice to get the current automaton. + // Check if we have a constraint about this edge in the + // original automaton. if (map_cst_ && ((it = map_cst_ - ->find(std::make_pair - (new_original_[old_a_->state_from_number(src)], - new_original_[old_a_->state_from_number(t.dst)]))) + ->find(std::make_pair(new_original_[src], + new_original_[t.dst]))) != map_cst_->end())) { acc = it->second; @@ -798,11 +792,7 @@ namespace spot automaton_size stat; scc_map* scc_map_; - map_state_state new_original_; - - // This table link a state in the current automaton with a state - // in the original one. - map_state_state old_old_name_; + std::vector new_original_; const map_constraint* map_cst_; @@ -1019,10 +1009,9 @@ namespace spot { assert(src_right != dst_right); - constraint.emplace_back - (new_original_[old_a_->state_from_number(src_right_n)], - new_original_[old_a_->state_from_number(dst_right_n)], - add); + constraint.emplace_back(new_original_[src_right_n], + new_original_[dst_right_n], + add); } } else if (out_scc_left && !out_scc_right) @@ -1035,10 +1024,9 @@ namespace spot { assert(src_left != dst_left); - constraint.emplace_back - (new_original_[old_a_->state_from_number(src_left_n)], - new_original_[old_a_->state_from_number(dst_left_n)], - add); + constraint.emplace_back(new_original_[src_left_n], + new_original_[dst_left_n], + add); } } else if (out_scc_left && out_scc_right) @@ -1051,14 +1039,12 @@ namespace spot { assert(src_left != dst_left && src_right != dst_right); // FIXME: cas pas compris. - constraint.emplace_back - (new_original_[old_a_->state_from_number(src_left_n)], - new_original_[old_a_->state_from_number(dst_left_n)], - add); - constraint.emplace_back - (new_original_[old_a_->state_from_number(src_right_n)], - new_original_[old_a_->state_from_number(dst_right_n)], - add); + constraint.emplace_back(new_original_[src_left_n], + new_original_[dst_left_n], + add); + constraint.emplace_back(new_original_[src_right_n], + new_original_[dst_right_n], + add); } }