From 77d43524dabfcdbba9d3a1155946a4b467648c33 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Chocholat=C3=BD?= Date: Thu, 4 Jul 2024 13:11:31 +0200 Subject: [PATCH 1/6] fix: Make Nfa::get_words() a const method --- include/mata/nfa/nfa.hh | 2 +- src/nfa/operations.cc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index 013e4842c..12ab26e12 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -350,7 +350,7 @@ public: * you can get all words by calling * get_words(aut.num_of_states()) */ - std::set get_words(unsigned max_length); + std::set get_words(unsigned max_length) const; /** * @brief Get any arbitrary accepted word in the language of the automaton. diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 4cc629041..5e2f8a14d 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -1153,7 +1153,7 @@ Run mata::nfa::encode_word(const Alphabet* alphabet, const std::vectortranslate_word(input) }; } -std::set mata::nfa::Nfa::get_words(unsigned max_length) { +std::set mata::nfa::Nfa::get_words(unsigned max_length) const { std::set result; // contains a pair: a state s and the word with which we got to the state s From 5c026ef2850e7804eb851fb864304d34fd689ec2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Chocholat=C3=BD?= Date: Thu, 4 Jul 2024 13:13:10 +0200 Subject: [PATCH 2/6] feat: Lazily get an arbitrary word from a complement of an NFA --- include/mata/nfa/nfa.hh | 17 ++++++++ src/nfa/operations.cc | 75 +++++++++++++++++++++++++++++++++++ tests/nfa/nfa.cc | 86 ++++++++++++++++++++++++++++++++++++++++- 3 files changed, 177 insertions(+), 1 deletion(-) diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index 12ab26e12..e82b38788 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -359,6 +359,23 @@ public: */ std::optional get_word(Symbol first_epsilon = EPSILON) const; + /** + * @brief Get any arbitrary accepted word in the language of the complement of the automaton. + * + * The automaton is lazily determinized and made complete. The algorithm returns an arbitrary word from the + * complemented NFA constructed until the first macrostate without any final states in the original automaton is + * encountered. + * + * @param[in] alphabet Alphabet to use for computing the complement. If @c nullptr, uses @c this->alphabet when + * defined, otherwise uses @c this->delta.get_used_symbols(). + * + * @pre The automaton does not contain any epsilon transitions. + * TODO: Support lazy epsilon closure? + * @return An arbitrary word from the complemented automaton, or @c std::nullopt if the automaton is universal on + * the chosen set of symbols for the complement. + */ + std::optional get_word_from_complement(const Alphabet* alphabet = nullptr) const; + /** * @brief Make NFA complete in place. * diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 5e2f8a14d..96a69ee57 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -1223,3 +1223,78 @@ std::optional Nfa::get_word(const Symbol first_epsilon) const { } return std::nullopt; } + +std::optional Nfa::get_word_from_complement(const Alphabet* alphabet) const { + if (initial.empty() || final.empty()) { return Word{}; } + + Nfa nfa_complete{}; + const State sink_state{ nfa_complete.add_state() }; + nfa_complete.final.insert(sink_state); + std::vector> worklist{}; + std::unordered_map subset_map{}; + const auto subset_map_end{ subset_map.end() }; + const StateSet initial_states{ initial }; + const State new_initial{ nfa_complete.add_state() }; + nfa_complete.initial.insert(new_initial); + if (!final.intersects_with(initial_states)) { + nfa_complete.final.insert(new_initial); + return nfa_complete.get_word(); + } + subset_map[initial_states] = new_initial; + worklist.emplace_back(new_initial, initial_states); + + using Iterator = mata::utils::OrdVector::const_iterator; + SynchronizedExistentialSymbolPostIterator synchronized_iterator{}; + + bool continue_complementation{ true }; + while (continue_complementation && !worklist.empty()) { + const auto[macrostate, orig_states] = std::move(worklist.back()); + worklist.pop_back(); + + // TODO: shouldn't we also reset first? + for (const State orig_state: orig_states) { mata::utils::push_back(synchronized_iterator, delta[orig_state]); } + bool sync_it_advanced{ synchronized_iterator.advance() }; + for (const Symbol symbol: get_symbols_to_work_with(*this, alphabet)) { + if (!sync_it_advanced) { + nfa_complete.delta.add(macrostate, symbol, sink_state); + continue_complementation = false; + break; + } + + const std::vector& orig_symbol_posts{ synchronized_iterator.get_current() }; + const Symbol symbol_advanced_to{ (*orig_symbol_posts.begin())->symbol }; + if (symbol < symbol_advanced_to) { + nfa_complete.delta.add(macrostate, symbol, sink_state); + continue_complementation = false; + break; + } + if (symbol > symbol_advanced_to) { + throw std::runtime_error( + "Iterating over symbols in the automaton which are missing in the shared alphabet" + ); + } + // From now on, symbol == symbol_advanced_to. + + const StateSet orig_targets{ synchronized_iterator.unify_targets() }; + State target_macrostate; + const auto target_macrostate_it = subset_map.find(orig_targets); + if (target_macrostate_it != subset_map_end) { + target_macrostate = target_macrostate_it->second; + } else { + target_macrostate = nfa_complete.add_state(); + subset_map[orig_targets] = target_macrostate; + worklist.emplace_back(target_macrostate, orig_targets); + if (!final.intersects_with(orig_targets)) { + nfa_complete.final.insert(target_macrostate); + continue_complementation = false; + } + } + nfa_complete.delta.add(macrostate, symbol, target_macrostate); + + if (!continue_complementation) { break; } + + sync_it_advanced = synchronized_iterator.advance(); + } + } + return nfa_complete.get_word(); +} diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc index c2449d885..850958463 100644 --- a/tests/nfa/nfa.cc +++ b/tests/nfa/nfa.cc @@ -425,7 +425,6 @@ TEST_CASE("mata::nfa::is_lang_empty_cex()") } } - TEST_CASE("mata::nfa::determinize()") { Nfa aut(3); @@ -485,6 +484,91 @@ TEST_CASE("mata::nfa::determinize()") } } // }}} +TEST_CASE("mata::nfa::Nfa::get_word_from_complement()") { + Nfa aut{}; + std::optional result; + std::unordered_map subset_map; + EnumAlphabet alphabet{ 'a', 'b', 'c' }; + + SECTION("empty automaton") { + result = aut.get_word_from_complement(); + REQUIRE(result.has_value()); + CHECK(*result == Word{}); + } + + SECTION("simple automaton 1") { + aut.initial = { 0 }; + aut.final = { 0 }; + result = aut.get_word_from_complement(&alphabet); + REQUIRE(result.has_value()); + CHECK(*result == Word{ 'a' }); + } + + SECTION("simple automaton 2") { + aut.initial = { 0 }; + aut.final = { 1 }; + aut.delta.add(0, 'a', 1); + result = aut.get_word_from_complement(); + REQUIRE(result.has_value()); + CHECK(*result == Word{}); + } + + SECTION("simple automaton 2 with epsilon") { + aut.alphabet = &alphabet; + aut.initial = { 0 }; + aut.final = { 0, 1 }; + aut.delta.add(0, 'a', 1); + result = aut.get_word_from_complement(); + REQUIRE(result.has_value()); + CHECK(*result == Word{ 'b' }); + } + + SECTION("nfa accepting \\eps+a+b+c") { + aut.alphabet = &alphabet; + aut.initial = { 0 }; + aut.final = { 0, 1 }; + aut.delta.add(0, 'a', 1); + aut.delta.add(0, 'b', 1); + aut.delta.add(0, 'c', 1); + result = aut.get_word_from_complement(); + REQUIRE(result.has_value()); + CHECK(*result == Word{ 'a', 'a' }); + } + + SECTION("nfa accepting \\eps+a+b+c+aa") { + aut.initial = { 0 }; + aut.final = { 0, 1 }; + aut.delta.add(0, 'a', 1); + aut.delta.add(0, 'b', 1); + aut.delta.add(0, 'c', 1); + result = aut.get_word_from_complement(); + REQUIRE(result.has_value()); + CHECK(*result == Word{ 'a', 'a' }); + } + + SECTION("simple automaton 3") { + aut.initial = { 1 }; + aut.final = { 1, 2, 3, 4, 5 }; + aut.delta.add(1, 'a', 2); + aut.delta.add(2, 'a', 3); + aut.delta.add(2, 'a', 6); + aut.delta.add(6, 'a', 6); + aut.delta.add(3, 'a', 4); + aut.delta.add(4, 'a', 5); + result = aut.get_word_from_complement(); + REQUIRE(result.has_value()); + CHECK(*result == Word{ 'a', 'a','a', 'a', 'a' }); + } + + SECTION("universal language") { + aut.initial = { 1 }; + aut.final = { 1 }; + aut.delta.add(1, 'a', 1); + result = aut.get_word_from_complement(); + CHECK(!result.has_value()); + } +} + TEST_CASE("mata::nfa::minimize() for profiling", "[.profiling],[minimize]") { Nfa aut(4); Nfa result; From fbe9f181e728bf75da30151891405c9b35b32699 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Chocholat=C3=BD?= Date: Thu, 4 Jul 2024 13:14:39 +0200 Subject: [PATCH 3/6] feat: Add callback to determinize() to handle discovery of new macrostates --- include/mata/nfa/nfa.hh | 8 ++++++- src/nfa/operations.cc | 47 ++++++++++++++++++----------------------- 2 files changed, 28 insertions(+), 27 deletions(-) diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index e82b38788..9f1280f76 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -576,9 +576,15 @@ Nfa minimize(const Nfa &aut, const ParameterMap& params = { { "algorithm", "brzo * * @param[in] aut Automaton to determinize. * @param[out] subset_map Map that maps sets of states of input automaton to states of determinized automaton. + * @param[in] macrostate_discover Callback event handler for discovering a new macrostate for the first time. The + * parameters are the determinized NFA constructed so far, the current macrostate, and the set of the original states + * corresponding to the macrostate. Return @c true if the determinization should continue, and @c false if the + * determinization should stop and return only the determinized NFA constructed so far. * @return Determinized automaton. */ -Nfa determinize(const Nfa& aut, std::unordered_map *subset_map = nullptr); +Nfa determinize( + const Nfa& aut, std::unordered_map *subset_map = nullptr, + std::optional> macrostate_discover = std::nullopt); /** * @brief Reduce the size of the automaton. diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 96a69ee57..15eb82068 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -1028,38 +1028,32 @@ Nfa mata::nfa::reduce(const Nfa &aut, StateRenaming *state_renaming, const Param } Nfa mata::nfa::determinize( - const Nfa& aut, - std::unordered_map *subset_map) { - - Nfa result; + const Nfa& aut, std::unordered_map* subset_map, + std::optional> macrostate_discover +) { + Nfa result{}; //assuming all sets targets are non-empty - std::vector> worklist; - bool deallocate_subset_map = false; - if (subset_map == nullptr) { - subset_map = new std::unordered_map(); - deallocate_subset_map = true; - } - - result.clear(); + std::vector> worklist{}; + std::unordered_map subset_map_local{}; + if (subset_map == nullptr) { subset_map = &subset_map_local; } - const StateSet S0 = StateSet(aut.initial); - const State S0id = result.add_state(); + const StateSet S0{ aut.initial }; + const State S0id{ result.add_state() }; result.initial.insert(S0id); if (aut.final.intersects_with(S0)) { result.final.insert(S0id); } worklist.emplace_back(S0id, S0); - (*subset_map)[mata::utils::OrdVector(S0)] = S0id; - - if (aut.delta.empty()) - return result; + if (aut.delta.empty()) { return result; } + if (macrostate_discover.has_value() && !(*macrostate_discover)(result, S0id, S0)) { return result; } using Iterator = mata::utils::OrdVector::const_iterator; SynchronizedExistentialSymbolPostIterator synchronized_iterator; - while (!worklist.empty()) { + bool continue_determinization{ true }; + while (continue_determinization && !worklist.empty()) { const auto Spair = worklist.back(); worklist.pop_back(); const StateSet S = Spair.second; @@ -1076,10 +1070,9 @@ Nfa mata::nfa::determinize( } while (synchronized_iterator.advance()) { - - // extract post from the sychronized_iterator iterator - const std::vector& moves = synchronized_iterator.get_current(); - Symbol currentSymbol = (*moves.begin())->symbol; + // extract post from the synchronized_iterator iterator + const std::vector& symbol_posts = synchronized_iterator.get_current(); + Symbol currentSymbol = (*symbol_posts.begin())->symbol; StateSet T = synchronized_iterator.unify_targets(); const auto existingTitr = subset_map->find(T); @@ -1095,11 +1088,13 @@ Nfa mata::nfa::determinize( worklist.emplace_back(Tid, T); } result.delta.mutable_state_post(Sid).insert(SymbolPost(currentSymbol, Tid)); + if (macrostate_discover.has_value() && existingTitr == subset_map->end() + && !(*macrostate_discover)(result, Tid, T)) { + continue_determinization = false; + break; + } } } - - if (deallocate_subset_map) { delete subset_map; } - return result; } From d670d51ca1bf0205d7cc7a87c0d3f608059ef056 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Chocholat=C3=BD?= Date: Thu, 4 Jul 2024 12:44:30 +0200 Subject: [PATCH 4/6] fix: Reset synchronized iterator after each iteration --- src/nfa/operations.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 15eb82068..beaca90f0 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -249,7 +249,7 @@ namespace { } // add moves of S to the sync ex iterator - // TODO: shouldn't we also reset first? + synchronized_iterator.reset(); for (State q: S) { mata::utils::push_back(synchronized_iterator, aut.delta[q]); } @@ -1064,7 +1064,7 @@ Nfa mata::nfa::determinize( } // add moves of S to the sync ex iterator - // TODO: shouldn't we also reset first? + synchronized_iterator.reset(); for (State q: S) { mata::utils::push_back(synchronized_iterator, aut.delta[q]); } @@ -1246,7 +1246,7 @@ std::optional Nfa::get_word_from_complement(const Alphabet* alphabet const auto[macrostate, orig_states] = std::move(worklist.back()); worklist.pop_back(); - // TODO: shouldn't we also reset first? + synchronized_iterator.reset(); for (const State orig_state: orig_states) { mata::utils::push_back(synchronized_iterator, delta[orig_state]); } bool sync_it_advanced{ synchronized_iterator.advance() }; for (const Symbol symbol: get_symbols_to_work_with(*this, alphabet)) { From f8767f2af8013dbf1ee9ab83d104efaf8d5db626 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Chocholat=C3=BD?= Date: Wed, 10 Jul 2024 09:55:52 +0200 Subject: [PATCH 5/6] feat: Allow passing alphabet missing some symbols in the transition relation --- src/nfa/operations.cc | 61 ++++++++++++++++++++++++------------------- tests/nfa/nfa.cc | 28 ++++++++++++++++++++ 2 files changed, 62 insertions(+), 27 deletions(-) diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index beaca90f0..2705a57d0 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -1241,6 +1241,8 @@ std::optional Nfa::get_word_from_complement(const Alphabet* alphabet using Iterator = mata::utils::OrdVector::const_iterator; SynchronizedExistentialSymbolPostIterator synchronized_iterator{}; + const utils::OrdVector symbols{ get_symbols_to_work_with(*this, alphabet) }; + const auto symbols_end{ symbols.end() }; bool continue_complementation{ true }; while (continue_complementation && !worklist.empty()) { const auto[macrostate, orig_states] = std::move(worklist.back()); @@ -1249,45 +1251,50 @@ std::optional Nfa::get_word_from_complement(const Alphabet* alphabet synchronized_iterator.reset(); for (const State orig_state: orig_states) { mata::utils::push_back(synchronized_iterator, delta[orig_state]); } bool sync_it_advanced{ synchronized_iterator.advance() }; - for (const Symbol symbol: get_symbols_to_work_with(*this, alphabet)) { + auto symbols_it{ symbols.begin() }; + while (sync_it_advanced || symbols_it != symbols_end) { if (!sync_it_advanced) { - nfa_complete.delta.add(macrostate, symbol, sink_state); + assert(symbols_it != symbols_end); + // There are no more transitions from the 'orig_states' but there is a symbol from the 'symbols'. Make + // the complemented NFA complete by adding a transition to a sink state. We can now return the access + // word for the sink state. + nfa_complete.delta.add(macrostate, *symbols_it, sink_state); continue_complementation = false; break; } - + assert(sync_it_advanced); const std::vector& orig_symbol_posts{ synchronized_iterator.get_current() }; const Symbol symbol_advanced_to{ (*orig_symbol_posts.begin())->symbol }; - if (symbol < symbol_advanced_to) { - nfa_complete.delta.add(macrostate, symbol, sink_state); - continue_complementation = false; - break; - } - if (symbol > symbol_advanced_to) { - throw std::runtime_error( - "Iterating over symbols in the automaton which are missing in the shared alphabet" - ); - } - // From now on, symbol == symbol_advanced_to. - const StateSet orig_targets{ synchronized_iterator.unify_targets() }; State target_macrostate; - const auto target_macrostate_it = subset_map.find(orig_targets); - if (target_macrostate_it != subset_map_end) { - target_macrostate = target_macrostate_it->second; - } else { - target_macrostate = nfa_complete.add_state(); - subset_map[orig_targets] = target_macrostate; - worklist.emplace_back(target_macrostate, orig_targets); - if (!final.intersects_with(orig_targets)) { - nfa_complete.final.insert(target_macrostate); - continue_complementation = false; + + if (symbols_it == symbols_end || symbol_advanced_to <= *symbols_it) { + // Continue with the determinization of the NFA. + const auto target_macrostate_it = subset_map.find(orig_targets); + if (target_macrostate_it != subset_map_end) { + target_macrostate = target_macrostate_it->second; + } else { + target_macrostate = nfa_complete.add_state(); + subset_map[orig_targets] = target_macrostate; + worklist.emplace_back(target_macrostate, orig_targets); + if (!final.intersects_with(orig_targets)) { + nfa_complete.final.insert(target_macrostate); + continue_complementation = false; + } } + nfa_complete.delta.add(macrostate, symbol_advanced_to, target_macrostate); + } else { + assert(symbol_advanced_to > *symbols_it); + // There are more transitions from the 'orig_states', but there is a missing transition over + // '*symbols_it'. Make the complemented NFA complete by adding a transition to a sink state. We can now + // return the access word for the sink state. + nfa_complete.delta.add(macrostate, *symbols_it, sink_state); + continue_complementation = false; + break; } - nfa_complete.delta.add(macrostate, symbol, target_macrostate); if (!continue_complementation) { break; } - + if(symbol_advanced_to >= *symbols_it) { ++symbols_it; } sync_it_advanced = synchronized_iterator.advance(); } } diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc index 850958463..9b821ee40 100644 --- a/tests/nfa/nfa.cc +++ b/tests/nfa/nfa.cc @@ -567,6 +567,34 @@ TEST_CASE("mata::nfa::Nfa::get_word_from_complement()") { result = aut.get_word_from_complement(); CHECK(!result.has_value()); } + + SECTION("smaller alphabet symbol") { + aut.initial = { 1 }; + aut.final = { 1 }; + aut.delta.add(1, 'b', 1); + result = aut.get_word_from_complement(&alphabet); + REQUIRE(result.has_value()); + CHECK(*result == Word{ 'a' }); + } + + SECTION("smaller transition symbol") { + aut.initial = { 1 }; + aut.final = { 1 }; + aut.delta.add(1, 'a', 1); + aut.delta.add(1, 0, 2); + result = aut.get_word_from_complement(&alphabet); + REQUIRE(result.has_value()); + CHECK(*result == Word{ 0 }); + } + + SECTION("smaller transition symbol 2") { + aut.initial = { 1 }; + aut.final = { 1 }; + aut.delta.add(1, 0, 2); + result = aut.get_word_from_complement(&alphabet); + REQUIRE(result.has_value()); + CHECK(*result == Word{ 0 }); + } } TEST_CASE("mata::nfa::minimize() for profiling", "[.profiling],[minimize]") { From b1dd80385f2eace3672f7f703461e50c4acfc08f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Chocholat=C3=BD?= Date: Wed, 10 Jul 2024 10:45:25 +0200 Subject: [PATCH 6/6] perf: Minimize number of copies of state sets --- src/nfa/operations.cc | 30 ++++++++++++++---------------- tests/nfa/nfa.cc | 15 +++++++++++++++ 2 files changed, 29 insertions(+), 16 deletions(-) diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index 2705a57d0..28e23c267 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -1220,23 +1220,19 @@ std::optional Nfa::get_word(const Symbol first_epsilon) const { } std::optional Nfa::get_word_from_complement(const Alphabet* alphabet) const { - if (initial.empty() || final.empty()) { return Word{}; } + if (are_disjoint(initial, final)) { return Word{}; } + + std::vector::const_iterator> worklist{}; + std::unordered_map subset_map{}; + const auto subset_map_end{ subset_map.end() }; Nfa nfa_complete{}; const State sink_state{ nfa_complete.add_state() }; nfa_complete.final.insert(sink_state); - std::vector> worklist{}; - std::unordered_map subset_map{}; - const auto subset_map_end{ subset_map.end() }; - const StateSet initial_states{ initial }; const State new_initial{ nfa_complete.add_state() }; nfa_complete.initial.insert(new_initial); - if (!final.intersects_with(initial_states)) { - nfa_complete.final.insert(new_initial); - return nfa_complete.get_word(); - } - subset_map[initial_states] = new_initial; - worklist.emplace_back(new_initial, initial_states); + auto subset_map_it{ subset_map.emplace(initial, new_initial).first }; + worklist.emplace_back(subset_map_it); using Iterator = mata::utils::OrdVector::const_iterator; SynchronizedExistentialSymbolPostIterator synchronized_iterator{}; @@ -1245,11 +1241,13 @@ std::optional Nfa::get_word_from_complement(const Alphabet* alphabet const auto symbols_end{ symbols.end() }; bool continue_complementation{ true }; while (continue_complementation && !worklist.empty()) { - const auto[macrostate, orig_states] = std::move(worklist.back()); + const auto curr_state_set_it{ worklist.back() }; + const State macrostate{ curr_state_set_it->second }; + const StateSet& curr_state_set{ curr_state_set_it->first }; worklist.pop_back(); synchronized_iterator.reset(); - for (const State orig_state: orig_states) { mata::utils::push_back(synchronized_iterator, delta[orig_state]); } + for (const State orig_state: curr_state_set) { mata::utils::push_back(synchronized_iterator, delta[orig_state]); } bool sync_it_advanced{ synchronized_iterator.advance() }; auto symbols_it{ symbols.begin() }; while (sync_it_advanced || symbols_it != symbols_end) { @@ -1265,7 +1263,7 @@ std::optional Nfa::get_word_from_complement(const Alphabet* alphabet assert(sync_it_advanced); const std::vector& orig_symbol_posts{ synchronized_iterator.get_current() }; const Symbol symbol_advanced_to{ (*orig_symbol_posts.begin())->symbol }; - const StateSet orig_targets{ synchronized_iterator.unify_targets() }; + StateSet orig_targets{ synchronized_iterator.unify_targets() }; State target_macrostate; if (symbols_it == symbols_end || symbol_advanced_to <= *symbols_it) { @@ -1275,12 +1273,12 @@ std::optional Nfa::get_word_from_complement(const Alphabet* alphabet target_macrostate = target_macrostate_it->second; } else { target_macrostate = nfa_complete.add_state(); - subset_map[orig_targets] = target_macrostate; - worklist.emplace_back(target_macrostate, orig_targets); if (!final.intersects_with(orig_targets)) { nfa_complete.final.insert(target_macrostate); continue_complementation = false; } + subset_map_it = subset_map.emplace(std::move(orig_targets), target_macrostate).first; + worklist.emplace_back(subset_map_it); } nfa_complete.delta.add(macrostate, symbol_advanced_to, target_macrostate); } else { diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc index 9b821ee40..d764939ad 100644 --- a/tests/nfa/nfa.cc +++ b/tests/nfa/nfa.cc @@ -496,6 +496,21 @@ TEST_CASE("mata::nfa::Nfa::get_word_from_complement()") { CHECK(*result == Word{}); } + SECTION("empty automaton 2") { + aut.initial = { 0 }; + result = aut.get_word_from_complement(); + REQUIRE(result.has_value()); + CHECK(*result == Word{}); + } + + SECTION("empty automaton 3") { + aut.initial = { 0 }; + aut.final = { 1 }; + result = aut.get_word_from_complement(); + REQUIRE(result.has_value()); + CHECK(*result == Word{}); + } + SECTION("simple automaton 1") { aut.initial = { 0 }; aut.final = { 0 };