Merge pull request VeriFIT#375 from VeriFIT/get_all_words

Added function that gets all words of an automaton
notValord · Jan 25, 2024 · 2cddb2f · 2cddb2f
2 parents b5527ca + 77da58f
commit 2cddb2f
Show file tree

Hide file tree

Showing 3 changed files with 126 additions and 0 deletions.
diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh
@@ -335,6 +335,15 @@ public:
 
     std::pair<Run, bool> get_word_for_path(const Run& run) const;
 
+    /**
+     * @brief Get the set of all words in the language of the automaton whose length is <= @p max_length
+     * 
+     * If you have an automaton with finite language (can be checked using @ref is_acyclic),
+     * you can get all words by calling
+     *      get_words(aut.num_of_states())
+     */
+    std::set<Word> get_words(unsigned max_length);
+
     /**
      * @brief Make NFA complete in place.
      *

diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc
@@ -787,3 +787,43 @@ mata::OnTheFlyAlphabet mata::nfa::create_alphabet(const std::vector<Nfa*>& nfas)
 Run mata::nfa::encode_word(const Alphabet* alphabet, const std::vector<std::string>& input) {
     return { .word = alphabet->translate_word(input) };
 }
+
+std::set<mata::Word> mata::nfa::Nfa::get_words(unsigned max_length) {
+    std::set<mata::Word> result;
+
+    // contains a pair: a state s and the word with which we got to the state s
+    std::vector<std::pair<State, mata::Word>> worklist;
+    // initializing worklist
+    for (State init_state : initial) {
+        worklist.push_back({init_state, {}});
+        if (final.contains(init_state)) {
+            result.insert(mata::Word());
+        }
+    }
+
+    // will be used during the loop
+    std::vector<std::pair<State, mata::Word>> new_worklist;
+
+    unsigned cur_length = 0;
+    while (!worklist.empty() && cur_length < max_length) {
+        new_worklist.clear();
+        for (const auto& state_and_word : worklist) {
+            State s_from = state_and_word.first;
+            const mata::Word& word = state_and_word.second;
+            for (const SymbolPost& sp : delta[s_from]) {
+                mata::Word new_word = word;
+                new_word.push_back(sp.symbol);
+                for (State s_to : sp.targets) {
+                    new_worklist.push_back({s_to, new_word});
+                    if (final.contains(s_to)) {
+                        result.insert(new_word);
+                    }
+                }
+            }
+        }
+        worklist.swap(new_worklist);
+        ++cur_length;
+    }
+
+    return result;
+}
diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc
@@ -2907,3 +2907,80 @@ TEST_CASE("mata::nfa::get_useful_states_tarjan") {
         CHECK(aut.get_useful_states() == mata::BoolVector{ 1, 1, 1, 1});
     }
 }
+
+TEST_CASE("mata::nfa::Nfa::get_words") {
+    SECTION("empty") {
+        Nfa aut;
+        CHECK(aut.get_words(0) == std::set<mata::Word>());
+        CHECK(aut.get_words(1) == std::set<mata::Word>());
+        CHECK(aut.get_words(5) == std::set<mata::Word>());
+    }
+
+    SECTION("empty word") {
+        Nfa aut(1, {0}, {0});
+        CHECK(aut.get_words(0) == std::set<mata::Word>{{}});
+        CHECK(aut.get_words(1) == std::set<mata::Word>{{}});
+        CHECK(aut.get_words(5) == std::set<mata::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_words(0) == std::set<mata::Word>{});
+        CHECK(aut.get_words(1) == std::set<mata::Word>{});
+        CHECK(aut.get_words(2) == std::set<mata::Word>{{0, 1}});
+        CHECK(aut.get_words(3) == std::set<mata::Word>{{0, 1}});
+        CHECK(aut.get_words(5) == std::set<mata::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_words(0) == std::set<mata::Word>{});
+        CHECK(aut.get_words(1) == std::set<mata::Word>{{0}});
+        CHECK(aut.get_words(2) == std::set<mata::Word>{{0}, {0, 1}});
+        CHECK(aut.get_words(3) == std::set<mata::Word>{{0}, {0, 1}});
+        CHECK(aut.get_words(5) == std::set<mata::Word>{{0}, {0, 1}});
+    }
+
+    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_words(0) == std::set<mata::Word>{{}});
+        CHECK(aut.get_words(1) == std::set<mata::Word>{{}, {0}});
+        CHECK(aut.get_words(2) == std::set<mata::Word>{{}, {0}, {0, 1}});
+        CHECK(aut.get_words(3) == std::set<mata::Word>{{}, {0}, {0, 1}});
+        CHECK(aut.get_words(5) == std::set<mata::Word>{{}, {0}, {0, 1}});
+    }
+
+    SECTION("more complex") {
+        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_words(0) == std::set<mata::Word>{{}});
+        CHECK(aut.get_words(1) == std::set<mata::Word>{{}, {0}});
+        CHECK(aut.get_words(2) == std::set<mata::Word>{{}, {0}, {0, 1}, {2,5}, {4,5}});
+        CHECK(aut.get_words(3) == std::set<mata::Word>{{}, {0}, {0, 1}, {2,5}, {4,5}, {0,3,5}});
+        CHECK(aut.get_words(4) == std::set<mata::Word>{{}, {0}, {0, 1}, {2,5}, {4,5}, {0,3,5}});
+        CHECK(aut.get_words(5) == std::set<mata::Word>{{}, {0}, {0, 1}, {2,5}, {4,5}, {0,3,5}});
+    }
+
+    SECTION("cycle") {
+        Nfa aut(6, {0,1}, {0,1});
+        aut.delta.add(0, 0, 1);
+        aut.delta.add(1, 1, 0);
+        CHECK(aut.get_words(0) == std::set<mata::Word>{{}});
+        CHECK(aut.get_words(1) == std::set<mata::Word>{{}, {0}, {1}});
+        CHECK(aut.get_words(2) == std::set<mata::Word>{{}, {0}, {1}, {0, 1}, {1, 0}});
+        CHECK(aut.get_words(3) == std::set<mata::Word>{{}, {0}, {1}, {0, 1}, {1, 0}, {0,1,0}, {1,0,1}});
+        CHECK(aut.get_words(4) == std::set<mata::Word>{{}, {0}, {1}, {0, 1}, {1, 0}, {0,1,0}, {1,0,1}, {0,1,0,1}, {1,0,1,0}});
+        CHECK(aut.get_words(5) == std::set<mata::Word>{{}, {0}, {1}, {0, 1}, {1, 0}, {0,1,0}, {1,0,1}, {0,1,0,1}, {1,0,1,0}, {0,1,0,1,0}, {1,0,1,0,1}});
+    }
+}