From 8c444933ea7d14342e6665e8793ad89edcbe3952 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 28 Sep 2023 21:34:58 +0200 Subject: [PATCH 1/4] in-place union in the concat style --- include/mata/nfa/nfa.hh | 5 +++++ src/nfa/operations.cc | 23 +++++++++++++++++++++++ tests/nfa/nfa.cc | 25 +++++++++++++++++++++++++ 3 files changed, 53 insertions(+) diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index c50134d39..469593846 100644 --- 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 index b8a5318fb..10280cc85 100644 --- 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 index 653f112a0..ea0753412 100644 --- 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); From b71fac0f4cbf2d28be3232e4c9f8204f496a4ce9 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Fri, 29 Sep 2023 14:47:07 +0200 Subject: [PATCH 2/4] uni: fixing the case when aut == this --- src/nfa/operations.cc | 13 +++++++++---- tests/nfa/nfa.cc | 6 ++++++ 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 10280cc85..67c328dd0 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -640,17 +640,22 @@ Nfa& Nfa::uni(const Nfa& aut) { return st + n; }; + // 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 aut_final_copy = aut.final; + SparseSet aut_initial_copy = aut.initial; + 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.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.num_of_states()); - for(const State& aut_ini : aut.initial) { + this->initial.reserve(n+aut_states); + for(const State& aut_ini : aut_initial_copy) { this->initial.insert(upd_fnc(aut_ini)); } diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc index ea0753412..c54e5f878 100644 --- a/tests/nfa/nfa.cc +++ b/tests/nfa/nfa.cc @@ -2153,6 +2153,12 @@ TEST_CASE("mata::nfa::union_inplace") { 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()") From fed60162ce0ef8c69120df6b225dab1a8370b224 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Fri, 29 Sep 2023 14:49:50 +0200 Subject: [PATCH 3/4] uni: function now call the method --- src/nfa/operations.cc | 33 ++------------------------------- 1 file changed, 2 insertions(+), 31 deletions(-) diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 67c328dd0..e311110b5 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -601,37 +601,8 @@ 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]); - } - - 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]) { - - SymbolPost union_symbol_post{ lhs_symbol_post.symbol, StateSet{} }; - - for (State target_state : lhs_symbol_post.targets) { - union_symbol_post.insert(lhs_state_renaming[target_state]); - } - - union_nfa.delta.mutable_state_post(union_state).insert(union_symbol_post); - } - } - - return union_nfa; + Nfa union_nfa{ lhs }; + return union_nfa.uni(rhs); } Nfa& Nfa::uni(const Nfa& aut) { From 5143cde0aa40b751680d447bc3b0c52f1cebc9ee Mon Sep 17 00:00:00 2001 From: vhavlena Date: Fri, 29 Sep 2023 16:33:52 +0200 Subject: [PATCH 4/4] concat: fix when this == aut --- src/nfa/concatenation.cc | 13 +++++++++---- tests/nfa/nfa-concatenation.cc | 18 ++++++++++++++++++ 2 files changed, 27 insertions(+), 4 deletions(-) diff --git a/src/nfa/concatenation.cc b/src/nfa/concatenation.cc index 31d2ae772..f522994e1 100644 --- a/src/nfa/concatenation.cc +++ b/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 aut_initial = aut.initial; + utils::SparseSet 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 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); diff --git a/tests/nfa/nfa-concatenation.cc b/tests/nfa/nfa-concatenation.cc index 8bc8f831f..9e1f72ee6 100644 --- a/tests/nfa/nfa-concatenation.cc +++ b/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]") {