Merge pull request #301 from VeriFIT/one_symbol_words

Get all one symbol words from NFA #patch
VeriFIT · Sep 20, 2023 · 40ca1cd · 40ca1cd
2 parents 2b84311 + 3380500
commit 40ca1cd
Show file tree

Hide file tree

Showing 3 changed files with 59 additions and 0 deletions.
diff --git a/include/mata/nfa/strings.hh b/include/mata/nfa/strings.hh
@@ -113,6 +113,11 @@ private:
  */
 std::set<Word> get_shortest_words(const Nfa& nfa);
 
+/**
+ * @brief Get all the one symbol words accepted by @p nfa.
+ */
+std::set<Symbol> 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 <u,v> 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
@@ -144,6 +144,20 @@ void ShortestWordsMap::update_current_words(LengthWordsPair& act, const LengthWo
     act.first = dst.first + 1;
 }
 
+std::set<mata::Symbol> mata::strings::get_accepted_symbols(const Nfa& nfa) {
+    std::set<mata::Symbol> accepted_symbols;
+    for (State init : nfa.initial) {
+        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 == accepted_symbols.end() || *symbol_it != sym)
+                 && nfa.final.intersects_with(symbol_post_init.targets)) {
+                accepted_symbols.insert(symbol_it, sym);
+            }
+        }
+    }
+    return accepted_symbols;
+}
 
 std::set<std::pair<int, int>> 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
@@ -339,3 +339,43 @@ TEST_CASE("mata::nfa::create_single_word_nfa()") {
         }
     }
 }
+
+TEST_CASE("mata::strings::get_accepted_symbols()") {
+    Nfa x;
+    std::set<mata::Symbol> symbols;
+
+    SECTION("basic") {
+        create_nfa(&x, "a|bc");
+        symbols = {'a'};
+        CHECK(get_accepted_symbols(x) == symbols);
+    }
+
+    SECTION("basic 2") {
+        create_nfa(&x, "");
+        CHECK(get_accepted_symbols(x).empty());
+    }
+
+    SECTION("basic 3") {
+        CHECK(get_accepted_symbols(x).empty());
+    }
+
+    SECTION("advanced 1") {
+        create_nfa(&x, "a*|c+|(db)*");
+        symbols = {'a', 'c'};
+        CHECK(get_accepted_symbols(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_accepted_symbols(x) == symbols);
+    }
+}