Merge pull request #412 from VeriFIT/renamed_union

Renamed union

bindings/python/libmata/nfa/nfa.pxd

@@ -161,7 +161,7 @@ cdef extern from "mata/nfa/nfa.hh" namespace "mata::nfa":
         void print_to_DOT(ostream)
         CNfa& trim(StateRenaming*)
         CNfa& concatenate(CNfa&)
-        CNfa& uni(CNfa&)
+        CNfa& unite_nondet_with(CNfa&)
         void get_one_letter_aut(CNfa&)
         bool is_epsilon(Symbol)
         CBoolVector get_useful_states()
@@ -198,7 +198,7 @@ cdef extern from "mata/nfa/algorithms.hh" namespace "mata::nfa::algorithms":
 cdef extern from "mata/nfa/plumbing.hh" namespace "mata::nfa::plumbing":
     cdef void get_elements(StateSet*, CBoolVector)
     cdef void c_determinize "mata::nfa::plumbing::determinize" (CNfa*, CNfa&, umap[StateSet, State]*)
-    cdef void c_uni "mata::nfa::plumbing::uni" (CNfa*, CNfa&, CNfa&)
+    cdef void c_union_nondet "mata::nfa::plumbing::union_nondet" (CNfa*, CNfa&, CNfa&)
     cdef void c_intersection "mata::nfa::plumbing::intersection" (CNfa*, CNfa&, CNfa&, Symbol, umap[pair[State, State], State]*)
     cdef void c_concatenate "mata::nfa::plumbing::concatenate" (CNfa*, CNfa&, CNfa&, bool, StateRenaming*, StateRenaming*)
     cdef void c_complement "mata::nfa::plumbing::complement" (CNfa*, CNfa&, CAlphabet&, ParameterMap&) except +

bindings/python/libmata/nfa/nfa.pyx

@@ -546,7 +546,7 @@ cdef class Nfa:
 
         :return: Self
         """
-        self.thisptr.get().uni(dereference(other.thisptr.get()))
+        self.thisptr.get().unite_nondet_with(dereference(other.thisptr.get()))
         return self
 
     def is_lang_empty(self, Run run = None):
@@ -833,7 +833,7 @@ def union(Nfa lhs, Nfa rhs):
     :return: union of lhs and rhs
     """
     result = Nfa()
-    mata_nfa.c_uni(
+    mata_nfa.c_union_nondet(
         result.thisptr.get(), dereference(lhs.thisptr.get()), dereference(rhs.thisptr.get())
     )
     return result

bindings/python/setup.py

@@ -219,7 +219,7 @@ def run_safely_external_command(cmd: str, check_results=True, quiet=True, timeou
                 "David Chocholatý <[email protected]>, "
                 "Juraj Síč <[email protected]>, "
                 "Tomáš Vojnar <[email protected]>",
-    author_email="lengal@fit.vutbr.cz",
+    author_email="holik@fit.vutbr.cz",
     long_description=README_MD,
     long_description_content_type="text/markdown",
     keywords="automata, finite automata, alternating automata",

include/mata/nfa/nfa.hh

@@ -218,9 +218,11 @@ public:
     Nfa& concatenate(const Nfa& aut);
 
     /**
-     * @brief In-place union
+     * @brief In-place nondeterministic union with @p aut.
+     *
+     * Does not add epsilon transitions, just unites initial and final states.
      */
-    Nfa& uni(const Nfa &aut);
+    Nfa& unite_nondet_with(const Nfa &aut);
 
     /**
      * Unify transitions to create a directed graph with at most a single transition between two states.
@@ -467,7 +469,24 @@ 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);
+/**
+ * @brief Compute non-deterministic union.
+ *
+ * Does not add epsilon transitions, just unites initial and final states.
+ * @return Non-deterministic union of @p lhs and @p rhs.
+ */
+Nfa union_nondet(const Nfa &lhs, const Nfa &rhs);
+
+/**
+ * @brief Compute union by product construction.
+ *
+ * Preserves determinism.
+ * @param[in] first_epsilon The first symbol to handle as an epsilon.
+ * @param[out] prod_map Map mapping product states to the original states.
+ * @return Union by product construction of @p lhs and @p rhs.
+ */
+Nfa union_product(const Nfa &lhs, const Nfa &rhs, Symbol first_epsilon = EPSILON,
+                  std::unordered_map<std::pair<State,State>,State> *prod_map = nullptr);
 
 /**
  * @brief Compute intersection of two NFAs.

include/mata/nfa/plumbing.hh

@@ -59,7 +59,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 union_nondet(Nfa *unionAutomaton, const Nfa &lhs, const Nfa &rhs) { *unionAutomaton = union_nondet(lhs, rhs); }
 
 /**
  * @brief Compute intersection of two NFAs.

src/CMakeLists.txt

@@ -13,7 +13,7 @@ add_library(libmata STATIC
 	nfa/inclusion.cc
 	nfa/universal.cc
 	nfa/complement.cc
-	nfa/intersection.cc
+	nfa/product.cc
 	nfa/concatenation.cc
 	strings/nfa-noodlification.cc
 	strings/nfa-segmentation.cc

src/nfa/nfa.cc

@@ -566,3 +566,38 @@ Nfa& Nfa::complement_deterministic(const OrdVector<Symbol>& symbols, std::option
     swap_final_nonfinal();
     return *this;
 }
+
+Nfa& Nfa::unite_nondet_with(const mata::nfa::Nfa& aut) {
+    const size_t num_of_states{ this->num_of_states() };
+    const size_t aut_num_of_states{ aut.num_of_states() };
+    const size_t new_num_of_states{ num_of_states + aut_num_of_states };
+
+    if (this == &aut) {
+        return *this;
+    }
+
+    if (final.empty() || initial.empty()) { *this = aut; return *this; }
+    if (aut.final.empty() || aut.initial.empty()) { return *this; }
+
+    this->delta.reserve(new_num_of_states);
+    // Allocate space for initial and final states from 'this' which might be missing in Delta.
+    this->delta.allocate(num_of_states);
+
+    auto renumber_states = [&](State st) {
+        return st + num_of_states;
+    };
+    this->delta.append(aut.delta.renumber_targets(renumber_states));
+
+    // Set accepting states.
+    this->final.reserve(new_num_of_states);
+    for(const State& aut_fin: aut.final) {
+        this->final.insert(renumber_states(aut_fin));
+    }
+    // Set initial states.
+    this->initial.reserve(new_num_of_states);
+    for(const State& aut_ini: aut.initial) {
+        this->initial.insert(renumber_states(aut_ini));
+    }
+
+    return *this;
+}

src/nfa/operations.cc

@@ -943,39 +943,30 @@ Nfa mata::nfa::minimize(
     return algo(aut);
 }
 
-Nfa mata::nfa::uni(const Nfa &lhs, const Nfa &rhs) {
-    Nfa union_nfa{ lhs };
-    return union_nfa.uni(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) {
 
-Nfa& Nfa::uni(const Nfa& aut) {
-    size_t n = this->num_of_states();
-    auto upd_fnc = [&](State st) {
-        return st + n;
+    auto both_final = [&](const State lhs_state,const State rhs_state) {
+        return lhs.final.contains(lhs_state) && rhs.final.contains(rhs_state);
     };
 
-    // copy the information about aut to save the case when this is the same object as aut.
-    size_t aut_states = aut.num_of_states();
-    SparseSet<mata::nfa::State> aut_final_copy = aut.final;
-    SparseSet<mata::nfa::State> aut_initial_copy = aut.initial;
+    if (lhs.final.empty() || lhs.initial.empty() || rhs.initial.empty() || rhs.final.empty())
+        return Nfa{};
 
-    this->delta.allocate(n);
-    this->delta.append(aut.delta.renumber_targets(upd_fnc));
+    return algorithms::product(lhs, rhs, both_final, first_epsilon, prod_map);
+}
 
-    // set accepting states
-    this->final.reserve(n+aut_states);
-    for(const State& aut_fin : aut_final_copy) {
-        this->final.insert(upd_fnc(aut_fin));
-    }
-    // set unitial states
-    this->initial.reserve(n+aut_states);
-    for(const State& aut_ini : aut_initial_copy) {
-        this->initial.insert(upd_fnc(aut_ini));
-    }
+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);
+    };
 
-    return *this;
+    if (lhs.final.empty() || lhs.initial.empty()) { return rhs; }
+    if (rhs.final.empty() || rhs.initial.empty()) { return lhs; }
+    return algorithms::product(lhs, rhs, one_final, first_epsilon, prod_map);
 }
 
+Nfa mata::nfa::union_nondet(const Nfa &lhs, const Nfa &rhs) { return Nfa{ lhs }.unite_nondet_with(rhs); }
+
 Simlib::Util::BinaryRelation mata::nfa::algorithms::compute_relation(const Nfa& aut, const ParameterMap& params) {
     if (!haskey(params, "relation")) {
         throw std::runtime_error(std::to_string(__func__) +

src/nfa/intersection.cc → src/nfa/product.cc

@@ -22,18 +22,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,

tests-integration/src/binary-operations.cc

@@ -38,7 +38,7 @@ int main(int argc, char *argv[]) {
 
     Nfa union_aut;
     TIME_BEGIN(union);
-    mata::nfa::plumbing::uni(&union_aut, lhs, rhs);
+    mata::nfa::plumbing::union_nondet(&union_aut, lhs, rhs);
     TIME_END(union);
 
     TIME_BEGIN(naive_inclusion);

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

tests/nfa/nfa-plumbing.cc

@@ -74,10 +74,10 @@ TEST_CASE("Mata::nfa::Plumbing") {
         CHECK(result.is_lang_empty());
     }
 
-    SECTION("Mata::nfa::Plumbing::union") {
+    SECTION("Mata::nfa::Plumbing::union_nondet") {
         FILL_WITH_AUT_A(lhs);
         FILL_WITH_AUT_B(lhs);
-        mata::nfa::plumbing::uni(&result, lhs, rhs);
+        mata::nfa::plumbing::union_nondet(&result, lhs, rhs);
         CHECK(!result.is_lang_empty());
     }
 

tests/nfa/nfa.cc

@@ -2471,7 +2471,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));
     }
@@ -2496,15 +2496,53 @@ TEST_CASE("mata::nfa::union_inplace") {
     REQUIRE(!rhs.is_in_lang(zero));
 
     SECTION("failing minimal scenario") {
-        Nfa result = lhs.uni(rhs);
+        Nfa result = lhs.unite_nondet_with(rhs);
         REQUIRE(result.is_in_lang(one));
         REQUIRE(result.is_in_lang(zero));
     }
 
     SECTION("same automata") {
-        size_t lhs_states = lhs.num_of_states();
-        Nfa result = lhs.uni(lhs);
-        REQUIRE(result.num_of_states() == lhs_states * 2);
+        const Nfa lhs_copy{ lhs };
+        CHECK(are_equivalent(lhs.unite_nondet_with(lhs), lhs_copy));
+    }
+}
+
+TEST_CASE("mata::nfa::union_product()") {
+    Run one{ { 1 },{} };
+    Run zero{{ 0 }, {} };
+    Run two{ { 2 },{} };
+    Run two_three{ { 2, 3 },{} };
+
+    Nfa lhs(4);
+    lhs.initial.insert(0);
+    lhs.delta.add(0, 0, 1);
+    lhs.delta.add(0, 2, 2);
+    lhs.delta.add(2, 3, 3);
+    lhs.final.insert(1);
+    lhs.final.insert(3);
+    REQUIRE(!lhs.is_in_lang(one));
+    REQUIRE(lhs.is_in_lang(zero));
+    REQUIRE(!lhs.is_in_lang(two));
+    REQUIRE(lhs.is_in_lang(two_three));
+
+    Nfa rhs(4);
+    rhs.initial.insert(0);
+    rhs.delta.add(0, 1, 1);
+    rhs.delta.add(0, 2, 2);
+    rhs.delta.add(2, 3, 3);
+    rhs.final.insert(1);
+    rhs.final.insert(2);
+    REQUIRE(rhs.is_in_lang(one));
+    REQUIRE(!rhs.is_in_lang(zero));
+    REQUIRE(rhs.is_in_lang(two));
+    REQUIRE(!rhs.is_in_lang(two_three));
+
+    SECTION("Minimal example") {
+        Nfa result = mata::nfa::union_product(lhs, rhs);
+        CHECK(!result.is_in_lang(one));
+        CHECK(!result.is_in_lang(zero));
+        CHECK(result.is_in_lang(two));
+        CHECK(result.is_in_lang(two_three));
     }
 }