diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index c50134d39..eb2300c60 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -404,7 +404,11 @@ OnTheFlyAlphabet create_alphabet(const std::vector& nfas); */ OnTheFlyAlphabet create_alphabet(const std::vector& nfas); -Nfa uni(const Nfa &lhs, const Nfa &rhs); +///Non-deterministic union. (does not add e-transitions, just unites initial and final states). +Nfa union_nondet(const Nfa &lhs, const Nfa &rhs); + +///Union by product construction, preserves determinism. +Nfa union_product(const Nfa &lhs, const Nfa &rhs, const Symbol first_epsilon = EPSILON, std::unordered_map,State> *prod_map = nullptr); /** * @brief Compute intersection of two NFAs. diff --git a/include/mata/nfa/plumbing.hh b/include/mata/nfa/plumbing.hh index 9b4122069..25bc0b511 100644 --- a/include/mata/nfa/plumbing.hh +++ b/include/mata/nfa/plumbing.hh @@ -71,7 +71,7 @@ void construct(Nfa* result, const ParsedObject& parsed, Alphabet* alphabet = nul *result = builder::construct(parsed, alphabet, state_map); } -inline void uni(Nfa *unionAutomaton, const Nfa &lhs, const Nfa &rhs) { *unionAutomaton = uni(lhs, rhs); } +inline void uni(Nfa *unionAutomaton, const Nfa &lhs, const Nfa &rhs) { *unionAutomaton = union_nondet(lhs, rhs); } /** * @brief Compute intersection of two NFAs. diff --git a/src/nfa/intersection.cc b/src/nfa/intersection.cc index e03028217..b2b3eca62 100644 --- a/src/nfa/intersection.cc +++ b/src/nfa/intersection.cc @@ -34,18 +34,6 @@ using InvertedProductStorage = std::vector; namespace mata::nfa { -Nfa intersection(const Nfa& lhs, const Nfa& rhs, const Symbol first_epsilon, ProductMap *prod_map) { - - auto both_final = [&](const State lhs_state,const State rhs_state) { - return lhs.final.contains(lhs_state) && rhs.final.contains(rhs_state); - }; - - if (lhs.final.empty() || lhs.initial.empty() || rhs.initial.empty() || rhs.final.empty()) - return Nfa{}; - - return algorithms::product(lhs, rhs, both_final, first_epsilon, prod_map); -} - //TODO: move this method to nfa.hh? It is something one might want to use (e.g. for union, inclusion, equivalence of DFAs). Nfa mata::nfa::algorithms::product( const Nfa& lhs, const Nfa& rhs, const std::function&& final_condition, diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index b8a5318fb..30332e1eb 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -600,7 +600,36 @@ Nfa mata::nfa::minimize( return algo(aut); } -Nfa mata::nfa::uni(const Nfa &lhs, const Nfa &rhs) { +Nfa mata::nfa::intersection(const Nfa& lhs, const Nfa& rhs, const Symbol first_epsilon, std::unordered_map, State> *prod_map) { + + auto both_final = [&](const State lhs_state,const State rhs_state) { + return lhs.final.contains(lhs_state) && rhs.final.contains(rhs_state); + }; + + if (lhs.final.empty() || lhs.initial.empty() || rhs.initial.empty() || rhs.final.empty()) + return Nfa{}; + + return algorithms::product(lhs, rhs, both_final, first_epsilon, prod_map); +} + +Nfa mata::nfa::union_product(const Nfa &lhs, const Nfa &rhs, const Symbol first_epsilon, std::unordered_map,State> *prod_map) { + auto one_final = [&](const State lhs_state,const State rhs_state) { + return lhs.final.contains(lhs_state) || rhs.final.contains(rhs_state); + }; + + if ( lhs.final.empty() || lhs.initial.empty() ) { + Nfa result = rhs; + return result; + } + if ( rhs.final.empty() || rhs.initial.empty() ) { + Nfa result = lhs; + return result; + } + + return algorithms::product(lhs, rhs, one_final, first_epsilon, prod_map); +} + +Nfa mata::nfa::union_nondet(const Nfa &lhs, const Nfa &rhs) { Nfa union_nfa{ rhs }; StateRenaming lhs_state_renaming; diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index c7a0a17e6..c8fe94251 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -11,7 +11,7 @@ add_executable(tests nfa/nfa.cc nfa/builder.cc nfa/nfa-concatenation.cc - nfa/nfa-intersection.cc + nfa/nfa-product.cc nfa/nfa-profiling.cc nfa/nfa-plumbing.cc strings/nfa-noodlification.cc diff --git a/tests/nfa/nfa-intersection.cc b/tests/nfa/nfa-product.cc similarity index 100% rename from tests/nfa/nfa-intersection.cc rename to tests/nfa/nfa-product.cc diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc index 653f112a0..bccf7692e 100644 --- a/tests/nfa/nfa.cc +++ b/tests/nfa/nfa.cc @@ -2124,7 +2124,7 @@ TEST_CASE("mata::nfa::union_norename()") { REQUIRE(!rhs.is_in_lang(zero)); SECTION("failing minimal scenario") { - Nfa result = uni(lhs, rhs); + Nfa result = union_nondet(lhs, rhs); REQUIRE(result.is_in_lang(one)); REQUIRE(result.is_in_lang(zero)); }