From ef9690cc5c7f13a8bc62e89dee07120df9a72b0d Mon Sep 17 00:00:00 2001 From: jurajsic Date: Thu, 17 Aug 2023 17:04:03 +0200 Subject: [PATCH 1/8] implemented function that gets all one symbol words from nfa --- include/mata/nfa/strings.hh | 5 ++++ src/strings/nfa-strings.cc | 11 ++++++++ tests/strings/nfa-string-solving.cc | 40 +++++++++++++++++++++++++++++ 3 files changed, 56 insertions(+) diff --git a/include/mata/nfa/strings.hh b/include/mata/nfa/strings.hh index 3d8523fd5..815ff0c5e 100644 --- a/include/mata/nfa/strings.hh +++ b/include/mata/nfa/strings.hh @@ -113,6 +113,11 @@ private: */ std::set get_shortest_words(const Nfa& nfa); +/** + * @brief Get all the symbols accepted by @p nfa. + */ +std::set get_one_symbol_words(const Nfa::Nfa& nfa); + /** * @brief Get the lengths of all words in the automaton @p aut. The function returns a set of pairs where for each * such a pair there is a word with length u+k*v for all ks. The disjunction of such formulae of all pairs hence precisely diff --git a/src/strings/nfa-strings.cc b/src/strings/nfa-strings.cc index f7d9c3c91..a5df370a4 100644 --- a/src/strings/nfa-strings.cc +++ b/src/strings/nfa-strings.cc @@ -144,6 +144,17 @@ void ShortestWordsMap::update_current_words(LengthWordsPair& act, const LengthWo act.first = dst.first + 1; } +std::set Mata::Strings::get_one_symbol_words(const Nfa::Nfa& nfa) { + std::set one_symbol_words; + for (State init : nfa.initial) { + for (const auto& move_from_init : nfa.delta[init]) { + if (!one_symbol_words.contains(move_from_init.symbol) && nfa.final.intersects_with(move_from_init.targets)) { + one_symbol_words.insert(move_from_init.symbol); + } + } + } + return one_symbol_words; +} std::set> mata::strings::get_word_lengths(const Nfa& aut) { Nfa one_letter; diff --git a/tests/strings/nfa-string-solving.cc b/tests/strings/nfa-string-solving.cc index 385af77a9..c6a0a4dd4 100644 --- a/tests/strings/nfa-string-solving.cc +++ b/tests/strings/nfa-string-solving.cc @@ -339,3 +339,43 @@ TEST_CASE("mata::nfa::create_single_word_nfa()") { } } } + +TEST_CASE("Mata::Strings::get_one_symbol_words()") { + Nfa x; + std::set symbols; + + SECTION("basic") { + create_nfa(&x, "a|bc"); + symbols = {'a'}; + CHECK(get_one_symbol_words(x) == symbols); + } + + SECTION("basic 2") { + create_nfa(&x, ""); + CHECK(get_one_symbol_words(x).empty()); + } + + SECTION("basic 3") { + CHECK(get_one_symbol_words(x).empty()); + } + + SECTION("advanced 1") { + create_nfa(&x, "a*|c+|(db)*"); + symbols = {'a', 'c'}; + CHECK(get_one_symbol_words(x) == symbols); + } + + SECTION("advanced 2") { + x.delta.add(0, 'a', 1); + x.delta.add(0, 'b', 1); + x.delta.add(2, 'c', 3); + x.delta.add(2, 'd', 4); + x.delta.add(4, 'e', 2); + x.delta.add(2, 'f', 2); + x.delta.add(5, 'g', 1); + x.initial = {0, 2, 4}; + x.final = {1, 3, 2}; + symbols = {'a', 'b', 'c', 'e', 'f'}; + CHECK(get_one_symbol_words(x) == symbols); + } +} From 3f6d7dba0be3b3d4e96e591afff673adbc064082 Mon Sep 17 00:00:00 2001 From: jurajsic Date: Mon, 18 Sep 2023 18:21:35 +0200 Subject: [PATCH 2/8] update to newest mata --- include/mata/nfa/strings.hh | 2 +- src/strings/nfa-strings.cc | 4 ++-- tests/strings/nfa-string-solving.cc | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/include/mata/nfa/strings.hh b/include/mata/nfa/strings.hh index 815ff0c5e..9b2423683 100644 --- a/include/mata/nfa/strings.hh +++ b/include/mata/nfa/strings.hh @@ -116,7 +116,7 @@ std::set get_shortest_words(const Nfa& nfa); /** * @brief Get all the symbols accepted by @p nfa. */ -std::set get_one_symbol_words(const Nfa::Nfa& nfa); +std::set get_one_symbol_words(const Nfa& nfa); /** * @brief Get the lengths of all words in the automaton @p aut. The function returns a set of pairs where for each diff --git a/src/strings/nfa-strings.cc b/src/strings/nfa-strings.cc index a5df370a4..cc4fe2231 100644 --- a/src/strings/nfa-strings.cc +++ b/src/strings/nfa-strings.cc @@ -144,8 +144,8 @@ void ShortestWordsMap::update_current_words(LengthWordsPair& act, const LengthWo act.first = dst.first + 1; } -std::set Mata::Strings::get_one_symbol_words(const Nfa::Nfa& nfa) { - std::set one_symbol_words; +std::set mata::strings::get_one_symbol_words(const Nfa& nfa) { + std::set one_symbol_words; for (State init : nfa.initial) { for (const auto& move_from_init : nfa.delta[init]) { if (!one_symbol_words.contains(move_from_init.symbol) && nfa.final.intersects_with(move_from_init.targets)) { diff --git a/tests/strings/nfa-string-solving.cc b/tests/strings/nfa-string-solving.cc index c6a0a4dd4..9a0006d69 100644 --- a/tests/strings/nfa-string-solving.cc +++ b/tests/strings/nfa-string-solving.cc @@ -340,9 +340,9 @@ TEST_CASE("mata::nfa::create_single_word_nfa()") { } } -TEST_CASE("Mata::Strings::get_one_symbol_words()") { +TEST_CASE("mata::strings::get_one_symbol_words()") { Nfa x; - std::set symbols; + std::set symbols; SECTION("basic") { create_nfa(&x, "a|bc"); From ae735eb60704720a39e30469146c0dfcd95823a8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Juraj=20S=C3=AD=C4=8D?= Date: Tue, 19 Sep 2023 12:54:15 +0200 Subject: [PATCH 3/8] Small clarification MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: David Chocholatý --- include/mata/nfa/strings.hh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/mata/nfa/strings.hh b/include/mata/nfa/strings.hh index 9b2423683..e57b7101d 100644 --- a/include/mata/nfa/strings.hh +++ b/include/mata/nfa/strings.hh @@ -114,7 +114,7 @@ private: std::set get_shortest_words(const Nfa& nfa); /** - * @brief Get all the symbols accepted by @p nfa. + * @brief Get all the one symbol words accepted by @p nfa. */ std::set get_one_symbol_words(const Nfa& nfa); From ab12dd3e63d7fe0aa22d2b67f93b0fd0d68f561d Mon Sep 17 00:00:00 2001 From: jurajsic Date: Tue, 19 Sep 2023 14:29:07 +0200 Subject: [PATCH 4/8] renamed move to symbol post --- src/strings/nfa-strings.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/strings/nfa-strings.cc b/src/strings/nfa-strings.cc index cc4fe2231..236496796 100644 --- a/src/strings/nfa-strings.cc +++ b/src/strings/nfa-strings.cc @@ -147,9 +147,9 @@ void ShortestWordsMap::update_current_words(LengthWordsPair& act, const LengthWo std::set mata::strings::get_one_symbol_words(const Nfa& nfa) { std::set one_symbol_words; for (State init : nfa.initial) { - for (const auto& move_from_init : nfa.delta[init]) { - if (!one_symbol_words.contains(move_from_init.symbol) && nfa.final.intersects_with(move_from_init.targets)) { - one_symbol_words.insert(move_from_init.symbol); + for (const SymbolPost& symbol_post_init : nfa.delta[init]) { + if (!one_symbol_words.contains(symbol_post_init.symbol) && nfa.final.intersects_with(symbol_post_init.targets)) { + one_symbol_words.insert(symbol_post_init.symbol); } } } From dc53e3b85553233afb6163ad4abf4f3e6a59d506 Mon Sep 17 00:00:00 2001 From: jurajsic Date: Tue, 19 Sep 2023 15:41:13 +0200 Subject: [PATCH 5/8] rename function --- include/mata/nfa/strings.hh | 2 +- src/strings/nfa-strings.cc | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/include/mata/nfa/strings.hh b/include/mata/nfa/strings.hh index e57b7101d..a66b28936 100644 --- a/include/mata/nfa/strings.hh +++ b/include/mata/nfa/strings.hh @@ -116,7 +116,7 @@ std::set get_shortest_words(const Nfa& nfa); /** * @brief Get all the one symbol words accepted by @p nfa. */ -std::set get_one_symbol_words(const Nfa& nfa); +std::set get_accepted_symbols(const Nfa& nfa); /** * @brief Get the lengths of all words in the automaton @p aut. The function returns a set of pairs where for each diff --git a/src/strings/nfa-strings.cc b/src/strings/nfa-strings.cc index 236496796..a5a7aabf8 100644 --- a/src/strings/nfa-strings.cc +++ b/src/strings/nfa-strings.cc @@ -144,16 +144,16 @@ void ShortestWordsMap::update_current_words(LengthWordsPair& act, const LengthWo act.first = dst.first + 1; } -std::set mata::strings::get_one_symbol_words(const Nfa& nfa) { - std::set one_symbol_words; +std::set mata::strings::get_accepted_symbols(const Nfa& nfa) { + std::set accepted_symbols; for (State init : nfa.initial) { for (const SymbolPost& symbol_post_init : nfa.delta[init]) { - if (!one_symbol_words.contains(symbol_post_init.symbol) && nfa.final.intersects_with(symbol_post_init.targets)) { - one_symbol_words.insert(symbol_post_init.symbol); + if (!accepted_symbols.contains(symbol_post_init.symbol) && nfa.final.intersects_with(symbol_post_init.targets)) { + accepted_symbols.insert(symbol_post_init.symbol); } } } - return one_symbol_words; + return accepted_symbols; } std::set> mata::strings::get_word_lengths(const Nfa& aut) { From 36745291088854ed07f79348fcd20bf7da20b85c Mon Sep 17 00:00:00 2001 From: jurajsic Date: Tue, 19 Sep 2023 15:52:50 +0200 Subject: [PATCH 6/8] fix tests --- tests/strings/nfa-string-solving.cc | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/strings/nfa-string-solving.cc b/tests/strings/nfa-string-solving.cc index 9a0006d69..3488a539b 100644 --- a/tests/strings/nfa-string-solving.cc +++ b/tests/strings/nfa-string-solving.cc @@ -340,29 +340,29 @@ TEST_CASE("mata::nfa::create_single_word_nfa()") { } } -TEST_CASE("mata::strings::get_one_symbol_words()") { +TEST_CASE("mata::strings::get_accepted_symbols()") { Nfa x; std::set symbols; SECTION("basic") { create_nfa(&x, "a|bc"); symbols = {'a'}; - CHECK(get_one_symbol_words(x) == symbols); + CHECK(get_accepted_symbols(x) == symbols); } SECTION("basic 2") { create_nfa(&x, ""); - CHECK(get_one_symbol_words(x).empty()); + CHECK(get_accepted_symbols(x).empty()); } SECTION("basic 3") { - CHECK(get_one_symbol_words(x).empty()); + CHECK(get_accepted_symbols(x).empty()); } SECTION("advanced 1") { create_nfa(&x, "a*|c+|(db)*"); symbols = {'a', 'c'}; - CHECK(get_one_symbol_words(x) == symbols); + CHECK(get_accepted_symbols(x) == symbols); } SECTION("advanced 2") { @@ -376,6 +376,6 @@ TEST_CASE("mata::strings::get_one_symbol_words()") { x.initial = {0, 2, 4}; x.final = {1, 3, 2}; symbols = {'a', 'b', 'c', 'e', 'f'}; - CHECK(get_one_symbol_words(x) == symbols); + CHECK(get_accepted_symbols(x) == symbols); } } From b4bf3abf5f1d74a6659abd5c056c4f4e3eb9b897 Mon Sep 17 00:00:00 2001 From: jurajsic Date: Wed, 20 Sep 2023 14:01:32 +0200 Subject: [PATCH 7/8] optimization --- include/mata/nfa/strings.hh | 2 +- src/strings/nfa-strings.cc | 6 ++++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/include/mata/nfa/strings.hh b/include/mata/nfa/strings.hh index a66b28936..3739f80d0 100644 --- a/include/mata/nfa/strings.hh +++ b/include/mata/nfa/strings.hh @@ -116,7 +116,7 @@ std::set get_shortest_words(const Nfa& nfa); /** * @brief Get all the one symbol words accepted by @p nfa. */ -std::set get_accepted_symbols(const Nfa& nfa); +std::set get_accepted_symbols(const Nfa& nfa); /** * @brief Get the lengths of all words in the automaton @p aut. The function returns a set of pairs where for each diff --git a/src/strings/nfa-strings.cc b/src/strings/nfa-strings.cc index a5a7aabf8..9d6cf43ea 100644 --- a/src/strings/nfa-strings.cc +++ b/src/strings/nfa-strings.cc @@ -148,8 +148,10 @@ std::set mata::strings::get_accepted_symbols(const Nfa& nfa) { std::set accepted_symbols; for (State init : nfa.initial) { for (const SymbolPost& symbol_post_init : nfa.delta[init]) { - if (!accepted_symbols.contains(symbol_post_init.symbol) && nfa.final.intersects_with(symbol_post_init.targets)) { - accepted_symbols.insert(symbol_post_init.symbol); + mata::Symbol sym = symbol_post_init.symbol; + auto symbol_it = accepted_symbols.lower_bound(sym); + if (*symbol_it != sym && nfa.final.intersects_with(symbol_post_init.targets)) { + accepted_symbols.insert(symbol_it, sym); } } } From 3380500a72261be551cbff6452621db05045e5ca Mon Sep 17 00:00:00 2001 From: jurajsic Date: Wed, 20 Sep 2023 14:06:22 +0200 Subject: [PATCH 8/8] fix lower_bound can return end() --- src/strings/nfa-strings.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/strings/nfa-strings.cc b/src/strings/nfa-strings.cc index 9d6cf43ea..38c88bfb4 100644 --- a/src/strings/nfa-strings.cc +++ b/src/strings/nfa-strings.cc @@ -150,7 +150,8 @@ std::set mata::strings::get_accepted_symbols(const Nfa& nfa) { for (const SymbolPost& symbol_post_init : nfa.delta[init]) { mata::Symbol sym = symbol_post_init.symbol; auto symbol_it = accepted_symbols.lower_bound(sym); - if (*symbol_it != sym && nfa.final.intersects_with(symbol_post_init.targets)) { + if ((symbol_it == accepted_symbols.end() || *symbol_it != sym) + && nfa.final.intersects_with(symbol_post_init.targets)) { accepted_symbols.insert(symbol_it, sym); } }