Merge pull request #352 from VeriFIT/uni-inplace

In-place Union

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.

src/nfa/concatenation.cc

@@ -32,21 +32,26 @@ Nfa& Nfa::concatenate(const Nfa& aut) {
         return st + n;
     };
 
+    // copy the information about aut to save the case when this is the same object as aut.
+    utils::SparseSet<mata::nfa::State> aut_initial = aut.initial;
+    utils::SparseSet<mata::nfa::State> aut_final = aut.final;
+    size_t aut_n = aut.num_of_states();
+
     this->delta.allocate(n);
     this->delta.append(aut.delta.renumber_targets(upd_fnc));
 
     // set accepting states
     utils::SparseSet<State> new_fin{};
-    new_fin.reserve(n+aut.num_of_states());
-    for(const State& aut_fin : aut.final) {
+    new_fin.reserve(n+aut_n);
+    for(const State& aut_fin : aut_final) {
         new_fin.insert(upd_fnc(aut_fin));
     }
 
     // connect both parts
-    for(const State& ini : aut.initial) {
+    for(const State& ini : aut_initial) {
         const StatePost& ini_post = this->delta[upd_fnc(ini)];
         // is ini state also final?
-        bool is_final = aut.final[ini];
+        bool is_final = aut_final[ini];
         for(const State& fin : this->final) {
             if(is_final) {
                 new_fin.insert(fin);

src/nfa/operations.cc

@@ -601,37 +601,36 @@ Nfa mata::nfa::minimize(
 }
 
 Nfa mata::nfa::uni(const Nfa &lhs, const Nfa &rhs) {
-    Nfa union_nfa{ rhs };
-
-    StateRenaming lhs_state_renaming;
-    const size_t size = lhs.num_of_states();
-    for (State lhs_state = 0; lhs_state < size; ++lhs_state) {
-        lhs_state_renaming[lhs_state] = union_nfa.add_state();
-    }
-
-    for (State lhs_initial_state : lhs.initial) {
-        union_nfa.initial.insert(lhs_state_renaming[lhs_initial_state]);
-    }
-
-    for (State lhs_final_state : lhs.final) {
-        union_nfa.final.insert(lhs_state_renaming[lhs_final_state]);
-    }
+    Nfa union_nfa{ lhs };
+    return union_nfa.uni(rhs);
+}
 
-    for (State lhs_state = 0; lhs_state < size; ++lhs_state) {
-        State union_state = lhs_state_renaming[lhs_state];
-        for (const SymbolPost &lhs_symbol_post : lhs.delta[lhs_state]) {
+Nfa& Nfa::uni(const Nfa& aut) {
+    size_t n = this->num_of_states();
+    auto upd_fnc = [&](State st) {
+        return st + n;
+    };
 
-            SymbolPost union_symbol_post{ lhs_symbol_post.symbol, StateSet{} };
+    // 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;
 
-            for (State target_state : lhs_symbol_post.targets) {
-                union_symbol_post.insert(lhs_state_renaming[target_state]);
-            }
+    this->delta.allocate(n);
+    this->delta.append(aut.delta.renumber_targets(upd_fnc));
 
-            union_nfa.delta.mutable_state_post(union_state).insert(union_symbol_post);
-        }
+    // set accepting states
+    this->final.reserve(n+aut_states);
+    for(const State& aut_fin : aut_final_copy) {
+        this->final.insert(upd_fnc(aut_fin));
     }
-
-    return union_nfa;
+    // set unitial states
+    this->initial.reserve(n+aut_states);
+    for(const State& aut_ini : aut_initial_copy) {
+        this->initial.insert(upd_fnc(aut_ini));
+    }
+
+    return *this;
 }
 
 Simlib::Util::BinaryRelation mata::nfa::algorithms::compute_relation(const Nfa& aut, const ParameterMap& params) {

tests/nfa/nfa-concatenation.cc

@@ -730,6 +730,24 @@ TEST_CASE("mata::nfa::concatenate() inplace") {
         CHECK(!result.is_lang_empty());
     }
 
+    SECTION("the same automata") {
+        Nfa lhs{};
+
+        lhs.add_state();
+        lhs.initial.insert(0);
+        lhs.final.insert(0);
+        lhs.delta.add(0, 58, 0);
+        lhs.delta.add(0, 65, 0);
+        lhs.delta.add(0, 102, 0);
+        lhs.delta.add(0, 112, 0);
+        lhs.delta.add(0, 115, 0);
+        lhs.delta.add(0, 116, 0);
+
+        size_t lhs_size = lhs.num_of_states();
+        Nfa result = lhs.concatenate(lhs);
+        CHECK(result.num_of_states() == lhs_size * 2);
+    }
+
 }
 
 TEST_CASE("Concat_inplace performance", "[.profiling]") {

tests/nfa/nfa.cc

@@ -2130,6 +2130,37 @@ 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));
+    }
+
+    SECTION("same automata") {
+        size_t lhs_states = lhs.num_of_states();
+        Nfa result = lhs.uni(lhs);
+        REQUIRE(result.num_of_states() == lhs_states * 2);
+    }
+}
+
 TEST_CASE("mata::nfa::remove_final()")
 {
     Nfa aut('q' + 1);