renaming uni to union_nondet, adding union_product,

and also moving definition of intersection and renaming intersection.cc to product.cc
VeriFIT · Sep 29, 2023 · 80f4e82 · 80f4e82
1 parent 0c0bbfb
commit 80f4e82
Show file tree

Hide file tree

Showing 7 changed files with 38 additions and 17 deletions.
diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh
@@ -404,7 +404,11 @@ OnTheFlyAlphabet create_alphabet(const std::vector<Nfa*>& nfas);
  */
 OnTheFlyAlphabet create_alphabet(const std::vector<const Nfa*>& 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<std::pair<State,State>,State> *prod_map = nullptr);
 
 /**
  * @brief Compute intersection of two NFAs.

diff --git 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
@@ -34,18 +34,6 @@ using InvertedProductStorage = std::vector<State>;
 
 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<bool(State,State)>&& final_condition,

diff --git 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<std::pair<State, State>, 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<std::pair<State,State>,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
@@ -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 → tests/nfa/nfa-product.cc b/tests/nfa/nfa-intersection.cc → tests/nfa/nfa-product.cc
diff --git 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));
     }