From 92c4b39efed853023be2c76925927d629e14c83c Mon Sep 17 00:00:00 2001 From: Lukas Holik Date: Sun, 24 Sep 2023 11:45:32 +0200 Subject: [PATCH 1/3] refactoring intersection, version 0 (refactored version without e, matrix) --- CMakeLists.txt | 5 + include/mata/nfa/algorithms.hh | 2 + include/mata/nfa/nfa.hh | 4 + src/nfa/delta.cc | 1 + src/nfa/intersection.cc | 174 +++++++++++++++++- .../src/bench-bool-comb-cox-inter.cc | 15 +- tests-integration/src/utils/utils.cc | 2 +- 7 files changed, 193 insertions(+), 10 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index e61b668f8..d07bddd02 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -91,6 +91,11 @@ set(MATA_CLANG_WARNINGS -Wno-system-headers ) +# set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -O0") +# set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -O0") +# add_compile_options(-fno-omit-frame-pointer -mno-omit-leaf-frame-pointer) +# add_compile_options(-DNDEBUG -g) + # Set whether to treat warnings as errors. if (MATA_WERROR) message("-- Treating warnings in mata as errors") diff --git a/include/mata/nfa/algorithms.hh b/include/mata/nfa/algorithms.hh index 0dc296db6..819855f8a 100644 --- a/include/mata/nfa/algorithms.hh +++ b/include/mata/nfa/algorithms.hh @@ -115,6 +115,8 @@ Simlib::Util::BinaryRelation compute_relation( Nfa intersection_eps(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, const std::set& epsilons, std::unordered_map, State> *prod_map = nullptr); +Nfa intersection_eps2(const Nfa& lhs_nfa, const Nfa& rhs_nfa, bool preserve_epsilon, const std::set& epsilons, + std::unordered_map, State> *prod_map = nullptr); /** * @brief Concatenate two NFAs. * diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index b9962f846..60281e4d8 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -427,6 +427,10 @@ Nfa uni(const Nfa &lhs, const Nfa &rhs); Nfa intersection(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon = false, std::unordered_map, State> *prod_map = nullptr); +Nfa intersection2(const Nfa& lhs, const Nfa& rhs, + bool preserve_epsilon = false, std::unordered_map, State> *prod_map = nullptr); + + /** * @brief Concatenate two NFAs. * diff --git a/src/nfa/delta.cc b/src/nfa/delta.cc index a0e8ec66e..fa0458cc7 100644 --- a/src/nfa/delta.cc +++ b/src/nfa/delta.cc @@ -39,6 +39,7 @@ void SymbolPost::insert(State s) { } } +//TODO: slow! This should be doing merge, not inserting one by one. void SymbolPost::insert(const StateSet& states) { for (State s : states) { insert(s); diff --git a/src/nfa/intersection.cc b/src/nfa/intersection.cc index 8519a70be..77b868ec4 100644 --- a/src/nfa/intersection.cc +++ b/src/nfa/intersection.cc @@ -14,6 +14,7 @@ */ // MATA headers +#include #include "mata/nfa/nfa.hh" #include "mata/nfa/algorithms.hh" @@ -21,6 +22,10 @@ using namespace mata::nfa; namespace { + //using pair_to_state_t = std::vector>; + using pair_to_state_t = std::vector>; + using state_map_t = std::unordered_map,State>; + /** * Add transition to the product. * @param[out] product Created product automaton. @@ -28,20 +33,30 @@ namespace { * @param[in] pair_to_process Currently processed pair of original states. * @param[in] intersection_transition State transitions to add to the product. */ -void add_product_transition(Nfa& product, std::unordered_map, State>& product_map, +void add_product_transition(Nfa& product, state_map_t& product_map, const std::pair& pair_to_process, SymbolPost& intersection_transition) { if (intersection_transition.empty()) { return; } - auto& intersect_state_transitions{ product.delta.mutable_state_post(product_map[pair_to_process]) }; + StatePost& intersect_state_transitions{ product.delta.mutable_state_post(product_map[pair_to_process]) }; auto intersection_move_iter{ intersect_state_transitions.find(intersection_transition) }; if (intersection_move_iter == intersect_state_transitions.end()) { intersect_state_transitions.insert(intersection_transition); } else { + if (++intersection_move_iter != intersect_state_transitions.end()) + std::cout<<"fuck"; // Product already has some target states for the given symbol from the current product state. intersection_move_iter->insert(intersection_transition.targets); } } +void add_product_symbol_post2(Nfa& product, pair_to_state_t & pair_to_state, + const State lhs, const State rhs, SymbolPost& intersection_transition) { + if (intersection_transition.empty()) { return; } + + StatePost& intersect_state_transitions{ product.delta.mutable_state_post(pair_to_state[lhs][rhs]) }; + intersect_state_transitions.push_back(std::move(intersection_transition)); +} + /** * Create product state and its transitions. * @param[out] product Created product automaton. @@ -53,7 +68,7 @@ void add_product_transition(Nfa& product, std::unordered_map, State>& product_map, + state_map_t& product_map, const Nfa& lhs, const Nfa& rhs, std::deque>& pairs_to_process, @@ -76,24 +91,63 @@ void create_product_state_and_trans( } intersect_transitions.insert(intersect_state_to); } +void create_product_state_and_transition2( + Nfa& product_nfa, + pair_to_state_t & pair_to_state, + const Nfa& lhs_nfa, + const Nfa& rhs_nfa, + std::deque& pairs_to_process, + const State lhs_target, + const State rhs_target, + SymbolPost& product_symbol_post +) { + State intersect_target; + if (pair_to_state[lhs_target][rhs_target] == 1000000) { + //if (pair_to_state[intersect_state_pair_to.first].find(intersect_state_pair_to.second) == pair_to_state[intersect_state_pair_to.first].end()) { + //if (product_map.find(intersect_state_pair_to) == product_map.end()) { + intersect_target = product_nfa.add_state(); + //product_map[intersect_state_pair_to] = intersect_state_to; + pair_to_state[lhs_target][rhs_target] = intersect_target; + pairs_to_process.push_back(lhs_target); + pairs_to_process.push_back(rhs_target); + + if (lhs_nfa.final[lhs_target] && rhs_nfa.final[rhs_target]) { + product_nfa.final.insert(intersect_target); + } + } else { + //intersect_state_to = product_map[intersect_state_pair_to]; + intersect_target = pair_to_state[lhs_target][rhs_target]; + } + //TODO: would push_back and sort at the end be faster? + product_symbol_post.insert(intersect_target); +} + } // Anonymous namespace. namespace mata::nfa { Nfa intersection(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, - std::unordered_map, State> *prod_map) { + state_map_t *prod_map) { const std::set epsilons({EPSILON}); return algorithms::intersection_eps(lhs, rhs, preserve_epsilon, epsilons, prod_map); } +Nfa intersection2(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, + state_map_t *prod_map) { + + const std::set epsilons({EPSILON}); + return algorithms::intersection_eps2(lhs, rhs, preserve_epsilon, epsilons, prod_map); +} + + Nfa mata::nfa::algorithms::intersection_eps( const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, const std::set& epsilons, std::unordered_map, State> *prod_map) { Nfa product{}; // Product of the intersection. // Product map for the generated intersection mapping original state pairs to new product states. - std::unordered_map, State> product_map{}; + state_map_t product_map{}; std::pair pair_to_process{}; // State pair of original states currently being processed. std::deque> pairs_to_process{}; // Set of state pairs of original states to process. @@ -190,4 +244,114 @@ Nfa mata::nfa::algorithms::intersection_eps( return product; } // intersection(). +Nfa mata::nfa::algorithms::intersection_eps2( + const Nfa& lhs_nfa, const Nfa& rhs_nfa, bool preserve_epsilon, const std::set& epsilons, + std::unordered_map, State> *prod_map) { + Nfa product_nfa{}; // Product of the intersection. + // Product map for the generated intersection mapping original state pairs to new product states. + state_map_t product_map{}; + std::deque pairs_to_process{}; // Set of state pairs of original states to process. + + //pair_to_state_t pair_to_state(lhs.num_of_states()); + pair_to_state_t pair_to_state(lhs_nfa.num_of_states(), std::vector(rhs_nfa.num_of_states(), 1000000)); + + // Initialize pairs to process with initial state pairs. + for (const State lhs_initial_state : lhs_nfa.initial) { + for (const State rhs_initial_state : rhs_nfa.initial) { + // Update product with initial state pairs. + const State new_intersection_state = product_nfa.add_state(); + + //product_map[this_and_other_initial_state_pair] = new_intersection_state; + pair_to_state[lhs_initial_state][rhs_initial_state] = new_intersection_state; + pairs_to_process.push_back(lhs_initial_state); + pairs_to_process.push_back(rhs_initial_state); + + product_nfa.initial.insert(new_intersection_state); + } + } + + while (!pairs_to_process.empty()) { + State rhs_source = pairs_to_process.back();; + pairs_to_process.pop_back(); + State lhs_source = pairs_to_process.back();; + pairs_to_process.pop_back(); + // Compute classic product for current state pair. + + mata::utils::SynchronizedUniversalIterator::const_iterator> sync_iterator(2); + mata::utils::push_back(sync_iterator, lhs_nfa.delta[lhs_source]); + mata::utils::push_back(sync_iterator, rhs_nfa.delta[rhs_source]); + + while (sync_iterator.advance()) { + std::vector same_symbol_posts = sync_iterator.get_current(); + assert(same_symbol_posts.size() == 2); // One move per state in the pair. + + // Compute product for state transitions with same symbols. + // Find all transitions that have the same symbol for first and the second state in the pair_to_process. + // Create transition from the pair_to_process to all pairs between states to which first transition goes + // and states to which second one goes. + SymbolPost product_symbol_post{same_symbol_posts[0]->symbol }; + for (const State lhs_target: same_symbol_posts[0]->targets) + { + for (const State rhs_target: same_symbol_posts[1]->targets) + { + create_product_state_and_transition2( + product_nfa, pair_to_state, lhs_nfa, rhs_nfa, pairs_to_process, + lhs_target, rhs_target, product_symbol_post + ); + } + } + add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source, product_symbol_post); + } + + if (preserve_epsilon) { + // Add transitions of the current state pair for an epsilon preserving product. + + // Check for lhs epsilon transitions. + const StatePost& lhs_state_post{lhs_nfa.delta[lhs_source] }; + if (!lhs_state_post.empty()) { + //TODO: does this copy the symbol post? + const SymbolPost& lhs_last_symbol_post{lhs_state_post.back() }; + if (epsilons.find(lhs_last_symbol_post.symbol) != epsilons.end()) { + // Compute product for state transitions with lhs state epsilon transition. + // Create transition from the pair_to_process to all pairs between states to which first transition + // goes and states to which second one goes. + SymbolPost lhs_symbol_post{lhs_last_symbol_post.symbol }; + for (const State lhs_state_to: lhs_last_symbol_post.targets) { + create_product_state_and_transition2(product_nfa, pair_to_state, lhs_nfa, rhs_nfa, + pairs_to_process, + lhs_state_to, rhs_source, + lhs_symbol_post); + } + add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source, + lhs_symbol_post); + } + } + + // Check for rhs epsilon transitions in case only rhs has any transitions and add them. + const StatePost& rhs_post{rhs_nfa.delta[rhs_source]}; + if (!rhs_post.empty()) { + const auto& rhs_state_last_transitions{ rhs_post.back()}; + if (epsilons.find(rhs_state_last_transitions.symbol) != epsilons.end()) { + // Compute product for state transitions with rhs state epsilon transition. + // Create transition from the pair_to_process to all pairs between states to which first transition + // goes and states to which second one goes. + SymbolPost intersection_transition{ rhs_state_last_transitions.symbol }; + for (const State rhs_state_to: rhs_state_last_transitions.targets) { + create_product_state_and_transition2(product_nfa, pair_to_state, lhs_nfa, rhs_nfa, + pairs_to_process, + lhs_source, rhs_state_to, + intersection_transition); + } + add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source, + intersection_transition); + } + } + } + } + + if (prod_map != nullptr) { *prod_map = product_map; } + return product_nfa; +} // intersection(). + + } // namespace mata::nfa. diff --git a/tests-integration/src/bench-bool-comb-cox-inter.cc b/tests-integration/src/bench-bool-comb-cox-inter.cc index 2118b8de8..531eebb14 100644 --- a/tests-integration/src/bench-bool-comb-cox-inter.cc +++ b/tests-integration/src/bench-bool-comb-cox-inter.cc @@ -32,10 +32,17 @@ int main(int argc, char *argv[]) { // Setting precision of the times to fixed points and 4 decimal places std::cout << std::fixed << std::setprecision(4); - TIME_BEGIN(emptiness_check); - Nfa intersect_aut = intersection(lhs, rhs); - intersect_aut.is_lang_empty(); - TIME_END(emptiness_check); + // TIME_BEGIN(intersection); + // Nfa intersect_aut = intersection(lhs, rhs); + // TIME_END(intersection); + + TIME_BEGIN(intersection2); + Nfa intersect_aut2 = intersection2(lhs, rhs); + TIME_END(intersection2); + +// TIME_BEGIN(emptiness_check); +// intersect_aut.is_lang_empty(); +// TIME_END(emptiness_check); return EXIT_SUCCESS; } diff --git a/tests-integration/src/utils/utils.cc b/tests-integration/src/utils/utils.cc index e85f8fd47..04ddce8f3 100644 --- a/tests-integration/src/utils/utils.cc +++ b/tests-integration/src/utils/utils.cc @@ -62,7 +62,7 @@ int load_automata( std::vector mintermized = mintermization.mintermize(inter_auts); TIME_END(mintermization); for (mata::IntermediateAut& inter_aut : mintermized) { - assert(inter_aut.alphabet_type == mata::IntermediateAut::AlphabetType::BITVECTOR); + //assert(inter_aut.alphabet_type == mata::IntermediateAut::AlphabetType::BITVECTOR); auts.push_back(mata::nfa::builder::construct(inter_aut, &alphabet)); } } From 85320764fd181b720feae3819b05f330b619e857 Mon Sep 17 00:00:00 2001 From: Lukas Holik Date: Sun, 24 Sep 2023 22:52:25 +0200 Subject: [PATCH 2/3] segfaoult --- include/mata/nfa/algorithms.hh | 2 - include/mata/nfa/delta.hh | 2 + include/mata/nfa/nfa.hh | 8 +- include/mata/nfa/plumbing.hh | 2 +- src/nfa/complement.cc | 1 + src/nfa/delta.cc | 13 ++ src/nfa/inclusion.cc | 2 +- src/nfa/intersection.cc | 135 ++++++++---------- src/strings/nfa-noodlification.cc | 4 +- .../src/bench-bool-comb-cox-inter.cc | 2 +- tests/nfa/nfa-intersection.cc | 12 +- tests/strings/nfa-noodlification.cc | 2 +- 12 files changed, 95 insertions(+), 90 deletions(-) diff --git a/include/mata/nfa/algorithms.hh b/include/mata/nfa/algorithms.hh index 819855f8a..0dc296db6 100644 --- a/include/mata/nfa/algorithms.hh +++ b/include/mata/nfa/algorithms.hh @@ -115,8 +115,6 @@ Simlib::Util::BinaryRelation compute_relation( Nfa intersection_eps(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, const std::set& epsilons, std::unordered_map, State> *prod_map = nullptr); -Nfa intersection_eps2(const Nfa& lhs_nfa, const Nfa& rhs_nfa, bool preserve_epsilon, const std::set& epsilons, - std::unordered_map, State> *prod_map = nullptr); /** * @brief Concatenate two NFAs. * diff --git a/include/mata/nfa/delta.hh b/include/mata/nfa/delta.hh index faa1ab316..8a3f74a59 100644 --- a/include/mata/nfa/delta.hh +++ b/include/mata/nfa/delta.hh @@ -123,6 +123,8 @@ public: iterator find(const Symbol symbol) { return super::find({ symbol, {} }); } const_iterator find(const Symbol symbol) const { return super::find({ symbol, {} }); } + const_iterator first_epsilon_it(Symbol first_epsilon) const; + /** * @brief Iterator over moves represented as @c Move instances. * diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index 60281e4d8..6ecf1c62c 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -424,11 +424,13 @@ Nfa uni(const Nfa &lhs, const Nfa &rhs); * @param[out] prod_map Mapping of pairs of the original states (lhs_state, rhs_state) to new product states. * @return NFA as a product of NFAs @p lhs and @p rhs with ε-transitions preserved. */ -Nfa intersection(const Nfa& lhs, const Nfa& rhs, +Nfa intersection_old(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon = false, std::unordered_map, State> *prod_map = nullptr); -Nfa intersection2(const Nfa& lhs, const Nfa& rhs, - bool preserve_epsilon = false, std::unordered_map, State> *prod_map = nullptr); +Nfa intersection( + const Nfa& lhs_nfa, const Nfa& rhs_nfa, + std::unordered_map, State> *prod_map_ptr = nullptr, + Symbol first_epsilon = Limits::max_symbol); /** diff --git a/include/mata/nfa/plumbing.hh b/include/mata/nfa/plumbing.hh index 200472028..1800d6404 100644 --- a/include/mata/nfa/plumbing.hh +++ b/include/mata/nfa/plumbing.hh @@ -88,7 +88,7 @@ inline void uni(Nfa *unionAutomaton, const Nfa &lhs, const Nfa &rhs) { *unionAut inline void intersection(Nfa* res, const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon = false, std::unordered_map, State> *prod_map = nullptr) { - *res = intersection(lhs, rhs, preserve_epsilon, prod_map); + *res = intersection(lhs, rhs, prod_map); } /** diff --git a/src/nfa/complement.cc b/src/nfa/complement.cc index a8fc509d7..9b1b8415c 100644 --- a/src/nfa/complement.cc +++ b/src/nfa/complement.cc @@ -74,6 +74,7 @@ Nfa mata::nfa::complement(const Nfa& aut, const mata::utils::OrdVectorsymbol < first_epsilon) { + ++it; + return it; + } + } + return end(); +} + StatePost::Moves StatePost::moves_epsilons(const Symbol first_epsilon) const { const StatePost::const_iterator symbol_post_begin{ cbegin() }; const StatePost::const_iterator symbol_post_end{ cend() }; @@ -479,6 +491,7 @@ StatePost::Moves StatePost::moves_epsilons(const Symbol first_epsilon) const { return { *this, symbol_post_begin, symbol_post_end }; } + //TODO: some comments, my brain hurts. Can we use first_epsilon_it above (or rewrite its code as below) StatePost::const_iterator previous_symbol_post_it{ std::prev(symbol_post_end) }; StatePost::const_iterator symbol_post_it{ previous_symbol_post_it }; while (previous_symbol_post_it != symbol_post_begin && first_epsilon < previous_symbol_post_it->symbol) { diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc index 38f00774f..07e602103 100644 --- a/src/nfa/inclusion.cc +++ b/src/nfa/inclusion.cc @@ -35,7 +35,7 @@ bool mata::nfa::algorithms::is_included_naive( } else { bigger_cmpl = complement(bigger, *alphabet); } - Nfa nfa_isect = intersection(smaller, bigger_cmpl, false, nullptr); + Nfa nfa_isect = intersection(smaller, bigger_cmpl); return nfa_isect.is_lang_empty(cex); } // is_included_naive }}} diff --git a/src/nfa/intersection.cc b/src/nfa/intersection.cc index 77b868ec4..b2cf97cd0 100644 --- a/src/nfa/intersection.cc +++ b/src/nfa/intersection.cc @@ -24,7 +24,7 @@ namespace { //using pair_to_state_t = std::vector>; using pair_to_state_t = std::vector>; - using state_map_t = std::unordered_map,State>; + using product_map_t = std::unordered_map,State>; /** * Add transition to the product. @@ -33,7 +33,7 @@ namespace { * @param[in] pair_to_process Currently processed pair of original states. * @param[in] intersection_transition State transitions to add to the product. */ -void add_product_transition(Nfa& product, state_map_t& product_map, +void add_product_transition(Nfa& product, product_map_t& product_map, const std::pair& pair_to_process, SymbolPost& intersection_transition) { if (intersection_transition.empty()) { return; } @@ -68,7 +68,7 @@ void add_product_symbol_post2(Nfa& product, pair_to_state_t & pair_to_state, */ void create_product_state_and_trans( Nfa& product, - state_map_t& product_map, + product_map_t& product_map, const Nfa& lhs, const Nfa& rhs, std::deque>& pairs_to_process, @@ -91,9 +91,10 @@ void create_product_state_and_trans( } intersect_transitions.insert(intersect_state_to); } -void create_product_state_and_transition2( +void create_product_state_and_move2( Nfa& product_nfa, pair_to_state_t & pair_to_state, + product_map_t * prod_map, const Nfa& lhs_nfa, const Nfa& rhs_nfa, std::deque& pairs_to_process, @@ -102,12 +103,14 @@ void create_product_state_and_transition2( SymbolPost& product_symbol_post ) { State intersect_target; - if (pair_to_state[lhs_target][rhs_target] == 1000000) { + if (pair_to_state[lhs_target][rhs_target] == Limits::max_state) { //if (pair_to_state[intersect_state_pair_to.first].find(intersect_state_pair_to.second) == pair_to_state[intersect_state_pair_to.first].end()) { //if (product_map.find(intersect_state_pair_to) == product_map.end()) { intersect_target = product_nfa.add_state(); //product_map[intersect_state_pair_to] = intersect_state_to; pair_to_state[lhs_target][rhs_target] = intersect_target; + if (prod_map != nullptr) //this is here to appease tests + (*prod_map)[std::pair(lhs_target,rhs_target)] = intersect_target; pairs_to_process.push_back(lhs_target); pairs_to_process.push_back(rhs_target); @@ -127,27 +130,19 @@ void create_product_state_and_transition2( namespace mata::nfa { -Nfa intersection(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, - state_map_t *prod_map) { +Nfa intersection_old(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, + product_map_t *prod_map) { const std::set epsilons({EPSILON}); return algorithms::intersection_eps(lhs, rhs, preserve_epsilon, epsilons, prod_map); } -Nfa intersection2(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, - state_map_t *prod_map) { - - const std::set epsilons({EPSILON}); - return algorithms::intersection_eps2(lhs, rhs, preserve_epsilon, epsilons, prod_map); -} - - Nfa mata::nfa::algorithms::intersection_eps( const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, const std::set& epsilons, std::unordered_map, State> *prod_map) { Nfa product{}; // Product of the intersection. // Product map for the generated intersection mapping original state pairs to new product states. - state_map_t product_map{}; + product_map_t product_map{}; std::pair pair_to_process{}; // State pair of original states currently being processed. std::deque> pairs_to_process{}; // Set of state pairs of original states to process. @@ -244,29 +239,32 @@ Nfa mata::nfa::algorithms::intersection_eps( return product; } // intersection(). -Nfa mata::nfa::algorithms::intersection_eps2( - const Nfa& lhs_nfa, const Nfa& rhs_nfa, bool preserve_epsilon, const std::set& epsilons, - std::unordered_map, State> *prod_map) { +Nfa mata::nfa::intersection( + const Nfa& lhs_nfa, const Nfa& rhs_nfa, + std::unordered_map, State> *prod_map_ptr/* = nullptr*/, + Symbol first_epsilon/* = Limits::max_symbol*/) { + Nfa product_nfa{}; // Product of the intersection. // Product map for the generated intersection mapping original state pairs to new product states. - state_map_t product_map{}; std::deque pairs_to_process{}; // Set of state pairs of original states to process. //pair_to_state_t pair_to_state(lhs.num_of_states()); - pair_to_state_t pair_to_state(lhs_nfa.num_of_states(), std::vector(rhs_nfa.num_of_states(), 1000000)); + pair_to_state_t pair_to_state(lhs_nfa.num_of_states(), std::vector(rhs_nfa.num_of_states(), Limits::max_state/100)); // Initialize pairs to process with initial state pairs. for (const State lhs_initial_state : lhs_nfa.initial) { for (const State rhs_initial_state : rhs_nfa.initial) { // Update product with initial state pairs. - const State new_intersection_state = product_nfa.add_state(); + const State product_initial_state = product_nfa.add_state(); //product_map[this_and_other_initial_state_pair] = new_intersection_state; - pair_to_state[lhs_initial_state][rhs_initial_state] = new_intersection_state; + pair_to_state[lhs_initial_state][rhs_initial_state] = product_initial_state; + if (prod_map_ptr != nullptr) //this is here to appease tests + (*prod_map_ptr)[std::pair(lhs_initial_state, rhs_initial_state)] = product_initial_state; pairs_to_process.push_back(lhs_initial_state); pairs_to_process.push_back(rhs_initial_state); - product_nfa.initial.insert(new_intersection_state); + product_nfa.initial.insert(product_initial_state); } } @@ -289,67 +287,58 @@ Nfa mata::nfa::algorithms::intersection_eps2( // Find all transitions that have the same symbol for first and the second state in the pair_to_process. // Create transition from the pair_to_process to all pairs between states to which first transition goes // and states to which second one goes. - SymbolPost product_symbol_post{same_symbol_posts[0]->symbol }; - for (const State lhs_target: same_symbol_posts[0]->targets) - { - for (const State rhs_target: same_symbol_posts[1]->targets) - { - create_product_state_and_transition2( - product_nfa, pair_to_state, lhs_nfa, rhs_nfa, pairs_to_process, - lhs_target, rhs_target, product_symbol_post - ); + Symbol symbol = same_symbol_posts[0]->symbol; + if (symbol < first_epsilon) { + SymbolPost product_symbol_post{symbol}; + for (const State lhs_target: same_symbol_posts[0]->targets) { + for (const State rhs_target: same_symbol_posts[1]->targets) { + create_product_state_and_move2( + product_nfa, pair_to_state, prod_map_ptr, lhs_nfa, rhs_nfa, pairs_to_process, + lhs_target, rhs_target, product_symbol_post + ); + } } + add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source, product_symbol_post); } - add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source, product_symbol_post); + else + break; } - if (preserve_epsilon) { - // Add transitions of the current state pair for an epsilon preserving product. - - // Check for lhs epsilon transitions. - const StatePost& lhs_state_post{lhs_nfa.delta[lhs_source] }; - if (!lhs_state_post.empty()) { - //TODO: does this copy the symbol post? - const SymbolPost& lhs_last_symbol_post{lhs_state_post.back() }; - if (epsilons.find(lhs_last_symbol_post.symbol) != epsilons.end()) { - // Compute product for state transitions with lhs state epsilon transition. - // Create transition from the pair_to_process to all pairs between states to which first transition - // goes and states to which second one goes. - SymbolPost lhs_symbol_post{lhs_last_symbol_post.symbol }; - for (const State lhs_state_to: lhs_last_symbol_post.targets) { - create_product_state_and_transition2(product_nfa, pair_to_state, lhs_nfa, rhs_nfa, - pairs_to_process, - lhs_state_to, rhs_source, - lhs_symbol_post); - } - add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source, - lhs_symbol_post); + // Add epsilon transitions, from lhs e-transitions. + const StatePost& lhs_state_post{lhs_nfa.delta[lhs_source] }; + auto lhs_first_epsilon_it = lhs_state_post.first_epsilon_it(first_epsilon); + if (lhs_first_epsilon_it != lhs_state_post.end()) { + for (auto lhs_symbol_post = lhs_first_epsilon_it; lhs_symbol_post < lhs_state_post.end(); lhs_symbol_post++) { + SymbolPost prod_symbol_post{lhs_symbol_post->symbol }; + for (const State lhs_target: lhs_symbol_post->targets) { + create_product_state_and_move2(product_nfa, pair_to_state, prod_map_ptr, lhs_nfa, rhs_nfa, + pairs_to_process, + lhs_target, rhs_source, + prod_symbol_post); } + add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source, + prod_symbol_post); } + } - // Check for rhs epsilon transitions in case only rhs has any transitions and add them. - const StatePost& rhs_post{rhs_nfa.delta[rhs_source]}; - if (!rhs_post.empty()) { - const auto& rhs_state_last_transitions{ rhs_post.back()}; - if (epsilons.find(rhs_state_last_transitions.symbol) != epsilons.end()) { - // Compute product for state transitions with rhs state epsilon transition. - // Create transition from the pair_to_process to all pairs between states to which first transition - // goes and states to which second one goes. - SymbolPost intersection_transition{ rhs_state_last_transitions.symbol }; - for (const State rhs_state_to: rhs_state_last_transitions.targets) { - create_product_state_and_transition2(product_nfa, pair_to_state, lhs_nfa, rhs_nfa, - pairs_to_process, - lhs_source, rhs_state_to, - intersection_transition); - } - add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source, - intersection_transition); + // Add epsilon transitions, from rhs e-transitions. + const StatePost& rhs_state_post{rhs_nfa.delta[rhs_source] }; + auto rhs_first_epsilon_it = rhs_state_post.first_epsilon_it(first_epsilon); + if (rhs_first_epsilon_it != rhs_state_post.end()) { + for (auto rhs_symbol_post = rhs_first_epsilon_it; rhs_symbol_post < rhs_state_post.end(); rhs_symbol_post++) { + SymbolPost prod_symbol_post{rhs_symbol_post->symbol }; + for (const State rhs_target: rhs_symbol_post->targets) { + create_product_state_and_move2(product_nfa, pair_to_state, prod_map_ptr, lhs_nfa, rhs_nfa, + pairs_to_process, + lhs_source, rhs_target, + prod_symbol_post); } + add_product_symbol_post2(product_nfa, pair_to_state, lhs_source, rhs_source, + prod_symbol_post); } } } - if (prod_map != nullptr) { *prod_map = product_map; } return product_nfa; } // intersection(). diff --git a/src/strings/nfa-noodlification.cc b/src/strings/nfa-noodlification.cc index 09820ac9b..7ebdbcf22 100644 --- a/src/strings/nfa-noodlification.cc +++ b/src/strings/nfa-noodlification.cc @@ -279,7 +279,7 @@ std::vector seg_nfa::noodlify_for_equation( } auto product_pres_eps_trans{ - intersection(concatenated_lhs, rhs_automaton, true).trim() }; + intersection(concatenated_lhs, rhs_automaton).trim() }; if (product_pres_eps_trans.is_lang_empty()) { return {}; } @@ -328,7 +328,7 @@ std::vector seg_nfa::noodlify_for_equation( } auto product_pres_eps_trans{ - intersection(concatenated_lhs, rhs_automaton, true).trim() }; + intersection(concatenated_lhs, rhs_automaton).trim() }; if (product_pres_eps_trans.is_lang_empty()) { return {}; } diff --git a/tests-integration/src/bench-bool-comb-cox-inter.cc b/tests-integration/src/bench-bool-comb-cox-inter.cc index 531eebb14..b17d759b1 100644 --- a/tests-integration/src/bench-bool-comb-cox-inter.cc +++ b/tests-integration/src/bench-bool-comb-cox-inter.cc @@ -37,7 +37,7 @@ int main(int argc, char *argv[]) { // TIME_END(intersection); TIME_BEGIN(intersection2); - Nfa intersect_aut2 = intersection2(lhs, rhs); + Nfa intersect_aut2 = intersection(lhs, rhs); TIME_END(intersection2); // TIME_BEGIN(emptiness_check); diff --git a/tests/nfa/nfa-intersection.cc b/tests/nfa/nfa-intersection.cc index ffa35c1e5..2fa054216 100644 --- a/tests/nfa/nfa-intersection.cc +++ b/tests/nfa/nfa-intersection.cc @@ -75,7 +75,7 @@ TEST_CASE("mata::nfa::intersection()") SECTION("Intersection of empty automata") { - res = intersection(a, b, false, &prod_map); + res = intersection(a, b, &prod_map); REQUIRE(res.initial.empty()); REQUIRE(res.final.empty()); @@ -108,7 +108,7 @@ TEST_CASE("mata::nfa::intersection()") REQUIRE(!a.final.empty()); REQUIRE(!b.final.empty()); - res = intersection(a, b, false, &prod_map); + res = intersection(a, b, &prod_map); REQUIRE(!res.initial.empty()); REQUIRE(!res.final.empty()); @@ -127,7 +127,7 @@ TEST_CASE("mata::nfa::intersection()") FILL_WITH_AUT_A(a); FILL_WITH_AUT_B(b); - res = intersection(a, b, false, &prod_map); + res = intersection(a, b, &prod_map); REQUIRE(res.initial[prod_map[{1, 4}]]); REQUIRE(res.initial[prod_map[{3, 4}]]); @@ -178,7 +178,7 @@ TEST_CASE("mata::nfa::intersection()") FILL_WITH_AUT_B(b); b.final = {12}; - res = intersection(a, b, false, &prod_map); + res = intersection(a, b, &prod_map); REQUIRE(res.initial[prod_map[{1, 4}]]); REQUIRE(res.initial[prod_map[{3, 4}]]); @@ -215,7 +215,7 @@ TEST_CASE("mata::nfa::intersection() with preserving epsilon transitions") b.delta.add(6, 'a', 9); b.delta.add(6, 'b', 7); - Nfa result{intersection(a, b, true, &prod_map) }; + Nfa result{intersection(a, b, &prod_map) }; // Check states. CHECK(result.is_state(prod_map[{0, 0}])); @@ -315,7 +315,7 @@ TEST_CASE("mata::nfa::intersection() for profiling", "[.profiling],[intersection b.delta.add(6, 'b', 7); for (size_t i{ 0 }; i < 10000; ++i) { - Nfa result{intersection(a, b, true) }; + Nfa result{intersection(a, b) }; } } diff --git a/tests/strings/nfa-noodlification.cc b/tests/strings/nfa-noodlification.cc index c974bafb9..87ed8ea34 100644 --- a/tests/strings/nfa-noodlification.cc +++ b/tests/strings/nfa-noodlification.cc @@ -191,7 +191,7 @@ TEST_CASE("mata::nfa::SegNfa::noodlify_for_equation()") { noodle.delta.add(0, 0, 1); noodle.final.insert(1); auto result{ seg_nfa::noodlify_for_equation({ left1, left2 }, right) }; - REQUIRE(result.size() == 1); + REQUIRE(result.size() == 1); } SECTION("Larger automata") { From f0a51ba85e1f4e748aece38639ce3c3070f87c0c Mon Sep 17 00:00:00 2001 From: Lukas Holik Date: Sun, 24 Sep 2023 23:01:41 +0200 Subject: [PATCH 3/3] only one version --- include/mata/nfa/algorithms.hh | 12 --- include/mata/nfa/nfa.hh | 3 - src/nfa/intersection.cc | 150 ------------------------------ src/strings/nfa-noodlification.cc | 2 +- 4 files changed, 1 insertion(+), 166 deletions(-) diff --git a/include/mata/nfa/algorithms.hh b/include/mata/nfa/algorithms.hh index 0dc296db6..f4a9b3ecc 100644 --- a/include/mata/nfa/algorithms.hh +++ b/include/mata/nfa/algorithms.hh @@ -102,18 +102,6 @@ Simlib::Util::BinaryRelation compute_relation( const Nfa& aut, const ParameterMap& params = {{ "relation", "simulation"}, { "direction", "forward"}}); -/** - * @brief Compute intersection of two NFAs with a possibility of using multiple epsilons. - * - * @param[in] lhs First NFA to compute intersection for. - * @param[in] rhs Second NFA to compute intersection for. - * @param[in] preserve_epsilon Whether to compute intersection preserving epsilon transitions. - * @param[in] epsilons Set of symbols to be considered as epsilons - * @param[out] prod_map Mapping of pairs of the original states (lhs_state, rhs_state) to new product states. - * @return NFA as a product of NFAs @p lhs and @p rhs with ε-transitions preserved. - */ -Nfa intersection_eps(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, const std::set& epsilons, - std::unordered_map, State> *prod_map = nullptr); /** * @brief Concatenate two NFAs. diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index 6ecf1c62c..3b41f756f 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -424,15 +424,12 @@ Nfa uni(const Nfa &lhs, const Nfa &rhs); * @param[out] prod_map Mapping of pairs of the original states (lhs_state, rhs_state) to new product states. * @return NFA as a product of NFAs @p lhs and @p rhs with ε-transitions preserved. */ -Nfa intersection_old(const Nfa& lhs, const Nfa& rhs, - bool preserve_epsilon = false, std::unordered_map, State> *prod_map = nullptr); Nfa intersection( const Nfa& lhs_nfa, const Nfa& rhs_nfa, std::unordered_map, State> *prod_map_ptr = nullptr, Symbol first_epsilon = Limits::max_symbol); - /** * @brief Concatenate two NFAs. * diff --git a/src/nfa/intersection.cc b/src/nfa/intersection.cc index b2cf97cd0..67971a381 100644 --- a/src/nfa/intersection.cc +++ b/src/nfa/intersection.cc @@ -33,22 +33,6 @@ namespace { * @param[in] pair_to_process Currently processed pair of original states. * @param[in] intersection_transition State transitions to add to the product. */ -void add_product_transition(Nfa& product, product_map_t& product_map, - const std::pair& pair_to_process, SymbolPost& intersection_transition) { - if (intersection_transition.empty()) { return; } - - StatePost& intersect_state_transitions{ product.delta.mutable_state_post(product_map[pair_to_process]) }; - auto intersection_move_iter{ intersect_state_transitions.find(intersection_transition) }; - if (intersection_move_iter == intersect_state_transitions.end()) { - intersect_state_transitions.insert(intersection_transition); - } else { - if (++intersection_move_iter != intersect_state_transitions.end()) - std::cout<<"fuck"; - // Product already has some target states for the given symbol from the current product state. - intersection_move_iter->insert(intersection_transition.targets); - } -} - void add_product_symbol_post2(Nfa& product, pair_to_state_t & pair_to_state, const State lhs, const State rhs, SymbolPost& intersection_transition) { if (intersection_transition.empty()) { return; } @@ -66,31 +50,6 @@ void add_product_symbol_post2(Nfa& product, pair_to_state_t & pair_to_state, * @param[in] rhs_state_to Target state in NFA @c rhs. * @param[out] intersect_transitions Transitions of the product state. */ -void create_product_state_and_trans( - Nfa& product, - product_map_t& product_map, - const Nfa& lhs, - const Nfa& rhs, - std::deque>& pairs_to_process, - const State lhs_state_to, - const State rhs_state_to, - SymbolPost& intersect_transitions -) { - const std::pair intersect_state_pair_to(lhs_state_to, rhs_state_to); - State intersect_state_to; - if (product_map.find(intersect_state_pair_to) == product_map.end()) { - intersect_state_to = product.add_state(); - product_map[intersect_state_pair_to] = intersect_state_to; - pairs_to_process.push_back(intersect_state_pair_to); - - if (lhs.final[lhs_state_to] && rhs.final[rhs_state_to]) { - product.final.insert(intersect_state_to); - } - } else { - intersect_state_to = product_map[intersect_state_pair_to]; - } - intersect_transitions.insert(intersect_state_to); -} void create_product_state_and_move2( Nfa& product_nfa, pair_to_state_t & pair_to_state, @@ -130,115 +89,6 @@ void create_product_state_and_move2( namespace mata::nfa { -Nfa intersection_old(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, - product_map_t *prod_map) { - - const std::set epsilons({EPSILON}); - return algorithms::intersection_eps(lhs, rhs, preserve_epsilon, epsilons, prod_map); -} - -Nfa mata::nfa::algorithms::intersection_eps( - const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, const std::set& epsilons, - std::unordered_map, State> *prod_map) { - Nfa product{}; // Product of the intersection. - // Product map for the generated intersection mapping original state pairs to new product states. - product_map_t product_map{}; - std::pair pair_to_process{}; // State pair of original states currently being processed. - std::deque> pairs_to_process{}; // Set of state pairs of original states to process. - - // Initialize pairs to process with initial state pairs. - for (const State lhs_initial_state : lhs.initial) { - for (const State rhs_initial_state : rhs.initial) { - // Update product with initial state pairs. - const std::pair this_and_other_initial_state_pair(lhs_initial_state, rhs_initial_state); - const State new_intersection_state = product.add_state(); - - product_map[this_and_other_initial_state_pair] = new_intersection_state; - pairs_to_process.push_back(this_and_other_initial_state_pair); - - product.initial.insert(new_intersection_state); - if (lhs.final[lhs_initial_state] && rhs.final[rhs_initial_state]) { - product.final.insert(new_intersection_state); - } - } - } - - while (!pairs_to_process.empty()) { - pair_to_process = pairs_to_process.back(); - pairs_to_process.pop_back(); - // Compute classic product for current state pair. - - mata::utils::SynchronizedUniversalIterator::const_iterator> sync_iterator(2); - mata::utils::push_back(sync_iterator, lhs.delta[pair_to_process.first]); - mata::utils::push_back(sync_iterator, rhs.delta[pair_to_process.second]); - - while (sync_iterator.advance()) { - std::vector moves = sync_iterator.get_current(); - assert(moves.size() == 2); // One move per state in the pair. - - // Compute product for state transitions with same symbols. - // Find all transitions that have the same symbol for first and the second state in the pair_to_process. - // Create transition from the pair_to_process to all pairs between states to which first transition goes - // and states to which second one goes. - SymbolPost intersection_transition{ moves[0]->symbol }; - for (const State this_state_to: moves[0]->targets) - { - for (const State other_state_to: moves[1]->targets) - { - create_product_state_and_trans( - product, product_map, lhs, rhs, pairs_to_process, - this_state_to, other_state_to, intersection_transition - ); - } - } - add_product_transition(product, product_map, pair_to_process, intersection_transition); - } - - if (preserve_epsilon) { - // Add transitions of the current state pair for an epsilon preserving product. - - // Check for lhs epsilon transitions. - const StatePost& lhs_post{ lhs.delta[pair_to_process.first] }; - if (!lhs_post.empty()) { - const auto& lhs_state_last_transitions{ lhs_post.back() }; - if (epsilons.find(lhs_state_last_transitions.symbol) != epsilons.end()) { - // Compute product for state transitions with lhs state epsilon transition. - // Create transition from the pair_to_process to all pairs between states to which first transition - // goes and states to which second one goes. - SymbolPost intersection_transition{ lhs_state_last_transitions.symbol }; - for (const State lhs_state_to: lhs_state_last_transitions.targets) { - create_product_state_and_trans(product, product_map, lhs, rhs, pairs_to_process, - lhs_state_to, pair_to_process.second, - intersection_transition); - } - add_product_transition(product, product_map, pair_to_process, intersection_transition); - } - } - - // Check for rhs epsilon transitions in case only rhs has any transitions and add them. - const StatePost& rhs_post{ rhs.delta[pair_to_process.second]}; - if (!rhs_post.empty()) { - const auto& rhs_state_last_transitions{ rhs_post.back()}; - if (epsilons.find(rhs_state_last_transitions.symbol) != epsilons.end()) { - // Compute product for state transitions with rhs state epsilon transition. - // Create transition from the pair_to_process to all pairs between states to which first transition - // goes and states to which second one goes. - SymbolPost intersection_transition{ rhs_state_last_transitions.symbol }; - for (const State rhs_state_to: rhs_state_last_transitions.targets) { - create_product_state_and_trans(product, product_map, lhs, rhs, pairs_to_process, - pair_to_process.first, rhs_state_to, - intersection_transition); - } - add_product_transition(product, product_map, pair_to_process, intersection_transition); - } - } - } - } - - if (prod_map != nullptr) { *prod_map = product_map; } - return product; -} // intersection(). - Nfa mata::nfa::intersection( const Nfa& lhs_nfa, const Nfa& rhs_nfa, std::unordered_map, State> *prod_map_ptr/* = nullptr*/, diff --git a/src/strings/nfa-noodlification.cc b/src/strings/nfa-noodlification.cc index 7ebdbcf22..e49de6e85 100644 --- a/src/strings/nfa-noodlification.cc +++ b/src/strings/nfa-noodlification.cc @@ -386,7 +386,7 @@ std::vector seg_nfa::noodlify_for_equation( const std::set epsilons({EPSILON, EPSILON-1}); auto product_pres_eps_trans{ - intersection_eps(concatenated_lhs, concatenated_rhs, true, epsilons).trim() }; + intersection(concatenated_lhs, concatenated_rhs, nullptr, EPSILON-1).trim() }; if (product_pres_eps_trans.is_lang_empty()) { return {};