in-place union in the concat style

VeriFIT · Sep 28, 2023 · 8c44493 · 8c44493
1 parent 0c0bbfb
commit 8c44493
Show file tree

Hide file tree

Showing 3 changed files with 53 additions and 0 deletions.
diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh
@@ -199,6 +199,11 @@ public:
      */
     Nfa& concatenate(const Nfa& aut);
 
+    /**
+     * @brief In-place union
+     */
+    Nfa& uni(const Nfa &aut);
+
     /**
      * Unify transitions to create a directed graph with at most a single transition between two states.
      * @param[in] abstract_symbol Abstract symbol to use for transitions in digraph.

diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc
@@ -634,6 +634,29 @@ Nfa mata::nfa::uni(const Nfa &lhs, const Nfa &rhs) {
     return union_nfa;
 }
 
+Nfa& Nfa::uni(const Nfa& aut) {
+    size_t n = this->num_of_states();
+    auto upd_fnc = [&](State st) {
+        return st + n;
+    };
+
+    this->delta.allocate(n);
+    this->delta.append(aut.delta.renumber_targets(upd_fnc));
+
+    // set accepting states
+    this->final.reserve(n+aut.num_of_states());
+    for(const State& aut_fin : aut.final) {
+        this->final.insert(upd_fnc(aut_fin));
+    }
+    // set unitial states
+    this->initial.reserve(n+aut.num_of_states());
+    for(const State& aut_ini : aut.initial) {
+        this->initial.insert(upd_fnc(aut_ini));
+    }
+
+    return *this;
+}
+
 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__) +

diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc
@@ -2130,6 +2130,31 @@ TEST_CASE("mata::nfa::union_norename()") {
     }
 }
 
+TEST_CASE("mata::nfa::union_inplace") {
+    Run one{{1},{}};
+    Run zero{{0}, {}};
+
+    Nfa lhs(2);
+    lhs.initial.insert(0);
+    lhs.delta.add(0, 0, 1);
+    lhs.final.insert(1);
+    REQUIRE(!lhs.is_in_lang(one));
+    REQUIRE(lhs.is_in_lang(zero));
+
+    Nfa rhs(2);
+    rhs.initial.insert(0);
+    rhs.delta.add(0, 1, 1);
+    rhs.final.insert(1);
+    REQUIRE(rhs.is_in_lang(one));
+    REQUIRE(!rhs.is_in_lang(zero));
+
+    SECTION("failing minimal scenario") {
+        Nfa result = lhs.uni(rhs);
+        REQUIRE(result.is_in_lang(one));
+        REQUIRE(result.is_in_lang(zero));
+    }
+}
+
 TEST_CASE("mata::nfa::remove_final()")
 {
     Nfa aut('q' + 1);