Get a single arbitrary word accepted bt the NFA using DFS

VeriFIT · Jun 26, 2024 · 409df0a · 409df0a
1 parent b0dfdbc
commit 409df0a
Show file tree

Hide file tree

Showing 3 changed files with 105 additions and 0 deletions.
diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh
@@ -345,6 +345,13 @@ public:
      */
     std::set<Word> get_words(unsigned max_length, Symbol first_epsilon = EPSILON);
 
+    /**
+     * @brief Get any arbitrary accepted word in the language of the automaton.
+     *
+     * The automaton is searched using DFS, returning a word for the first reached final state.
+     */
+    std::optional<Word> get_word(Symbol first_epsilon = EPSILON) const;
+
     /**
      * @brief Make NFA complete in place.
      *

diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc
@@ -1200,3 +1200,28 @@ std::set<mata::Word> mata::nfa::Nfa::get_words(unsigned max_length, const Symbol
 
     return result;
 }
+
+std::optional<mata::Word> Nfa::get_word(const Symbol first_epsilon) const {
+    if (initial.empty() || final.empty()) { return std::nullopt; }
+
+    std::vector<std::pair<State, Word>> worklist{};
+    for (const State initial_state: initial) {
+        if (final.contains(initial_state)) { return Word{}; }
+        worklist.emplace_back(initial_state, Word{});
+    }
+    std::vector<bool> searched(num_of_states());
+
+    while (!worklist.empty()) {
+        auto [state, word]{ std::move(worklist.back()) };
+        worklist.pop_back();
+        for (const Move move: delta[state].moves()) {
+            if (searched[move.target]) { continue; }
+            Word target_word{ word };
+            if (move.symbol < first_epsilon) { target_word.push_back(move.symbol); }
+            if (final.contains(move.target)) { return target_word; }
+            worklist.emplace_back(move.target, target_word);
+            searched[move.target] = true;
+        }
+    }
+    return std::nullopt;
+}
diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc
@@ -3299,3 +3299,76 @@ TEST_CASE("mata::nfa::Nfa::get_words()") {
         CHECK(aut.get_words(5) == std::set<mata::Word>{{}, {}, {1}, {1}, {1}, {1}, {1,1}, {1,1}, {1,1}, {1,1}, {1,1,1}});
     }
 }
+
+TEST_CASE("mata::nfa::Nfa::get_word()") {
+    SECTION("empty") {
+        Nfa aut;
+        CHECK(aut.get_word(0) == std::nullopt);
+    }
+
+    SECTION("empty word") {
+        Nfa aut(1, { 0 }, { 0 });
+        CHECK(aut.get_word() == Word{});
+    }
+
+    SECTION("noodle - one final") {
+        Nfa aut(3, { 0 }, { 2 });
+        aut.delta.add(0, 0, 1);
+        aut.delta.add(1, 1, 2);
+        CHECK(aut.get_word() == Word{ 0, 1 });
+    }
+
+    SECTION("noodle - two finals") {
+        Nfa aut(3, { 0 }, { 1, 2 });
+        aut.delta.add(0, 0, 1);
+        aut.delta.add(1, 1, 2);
+        CHECK(aut.get_word() == Word{ 0 });
+    }
+
+    SECTION("noodle - three finals") {
+        Nfa aut(3, { 0 }, { 0, 1, 2 });
+        aut.delta.add(0, 0, 1);
+        aut.delta.add(1, 1, 2);
+        CHECK(aut.get_word() == Word{});
+    }
+
+    SECTION("more complex initial final") {
+        Nfa aut(6, { 0, 1 }, { 1, 3, 4, 5 });
+        aut.delta.add(0, 0, 3);
+        aut.delta.add(3, 1, 4);
+        aut.delta.add(0, 2, 2);
+        aut.delta.add(3, 3, 2);
+        aut.delta.add(1, 4, 2);
+        aut.delta.add(2, 5, 5);
+        CHECK(aut.get_word() == Word{});
+    }
+
+    SECTION("more complex") {
+        Nfa aut(6, { 0, 1 }, { 5 });
+        aut.delta.add(0, 0, 3);
+        aut.delta.add(3, 1, 4);
+        aut.delta.add(0, 2, 2);
+        aut.delta.add(3, 3, 2);
+        aut.delta.add(1, 4, 2);
+        aut.delta.add(2, 5, 5);
+        CHECK(aut.get_word() == Word{ 4, 5 });
+    }
+
+    SECTION("cycle") {
+        Nfa aut(6, { 0, 2 }, { 4 });
+        aut.delta.add(2, 2, 3);
+        aut.delta.add(3, 3, 2);
+        aut.delta.add(0, 0, 1);
+        aut.delta.add(1, 1, 4);
+        CHECK(aut.get_word() == Word{ 0, 1 });
+    }
+
+    SECTION("epsilons") {
+        Nfa aut(6, { 0, 2 }, { 4 });
+        aut.delta.add(2, 2, 3);
+        aut.delta.add(3, 3, 2);
+        aut.delta.add(0, EPSILON, 1);
+        aut.delta.add(1, 1, 4);
+        CHECK(aut.get_word() == Word{ 1 });
+    }
+}