feat: Add function to get arbitrary word from language difference lazily

include/mata/nfa/nfa.hh

@@ -501,10 +501,9 @@ Nfa union_product(const Nfa &lhs, const Nfa &rhs, Symbol first_epsilon = EPSILON
  *
  * @param[in] nfa_included NFA to include in the difference.
  * @param[in] nfa_excluded NFA to exclude from the difference.
- * @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.
+ * @param[in] macrostate_discover Callback event handler for discovering a new macrostate in the language difference
+ *  automaton for the first time. Return @c true if the computation should continue, and @c false if the computation
+ *  should stop and return only the NFA for the language difference constructed so far.
  *  The parameters are:
         const Nfa& nfa_included,
         const Nfa& nfa_excluded,
@@ -728,6 +727,23 @@ Run encode_word(const Alphabet* alphabet, const std::vector<std::string>& input)
  */
 utils::OrdVector<Symbol> get_symbols_to_work_with(const nfa::Nfa& nfa, const Alphabet* const shared_alphabet = nullptr);
 
+/**
+ * @brief Get any arbitrary accepted word in the language difference of @p nfa_included without @p nfa_excluded.
+ *
+ * The language difference automaton is lazily constructed without computing the whole determinized automata and the
+ *  complememt of @p nfa_excluded. The algorithm returns an arbitrary word from the language difference constructed
+ *  until the first macrostate with a final state in the original states in @p nfa_included and without any
+ *  corresponding final states in @p nfa_excluded is encountered.
+ *
+ * @pre The automaton does not contain any epsilon transitions.
+ * @param[in] nfa_included NFA to include in the language difference.
+ * @param[in] nfa_excluded NFA to exclude in the language difference.
+ * TODO: Support lazy epsilon closure?
+ * @return An arbitrary word from the language difference, or @c std::nullopt if the language difference automaton
+ *  is universal on the set of symbols from transitions of @p nfa_included.
+ */
+std::optional<Word> get_word_from_lang_difference(const Nfa &nfa_included, const Nfa &nfa_excluded);
+
 } // namespace mata::nfa.
 
 namespace std {

src/nfa/operations.cc

@@ -1403,3 +1403,15 @@ Nfa mata::nfa::lang_difference(
     }
     return nfa_lang_difference;
 }
+
+std::optional<mata::Word> mata::nfa::get_word_from_lang_difference(const Nfa & nfa_included, const Nfa & nfa_excluded) {
+    return lang_difference(nfa_included, nfa_excluded,
+        [&](const Nfa& nfa_included, const Nfa& nfa_excluded,
+            const StateSet& macrostate_included_state_set, const StateSet& macrostate_excluded_state_set,
+            const State macrostate, const Nfa& nfa_lang_difference) {
+            (void)nfa_included, (void)nfa_excluded;
+            (void)macrostate_included_state_set, (void)macrostate_excluded_state_set;
+            (void)macrostate;
+            return nfa_lang_difference.final.empty();
+        }).get_word();
+}

tests/nfa/nfa.cc

@@ -778,6 +778,159 @@ TEST_CASE("mata::nfa::lang_difference()") {
     }
 }
 
+TEST_CASE("mata::nfa::Nfa::get_word_from_lang_difference()") {
+    Nfa nfa_included{};
+    Nfa nfa_excluded{};
+    std::optional<Word> result{};
+    Nfa expected{};
+
+    SECTION("empty automata") {
+        result = get_word_from_lang_difference(nfa_included, nfa_excluded);
+        CHECK(!result.has_value());
+    }
+
+    SECTION("empty included") {
+        nfa_excluded.initial = { 0 };
+        nfa_excluded.final = { 0 };
+        result = get_word_from_lang_difference(nfa_included, nfa_excluded);
+        CHECK(!result.has_value());
+    }
+
+    SECTION("empty excluded") {
+        nfa_included.initial = { 0 };
+        nfa_included.final = { 0 };
+        result = get_word_from_lang_difference(nfa_included, nfa_excluded);
+        REQUIRE(result.has_value());
+        CHECK(*result == Word{});
+    }
+
+    SECTION("included { '', 'a' }, excluded { '' }") {
+        nfa_included.initial = { 0 };
+        nfa_included.delta.add(0, 'a', 1);
+        nfa_included.final = { 0, 1 };
+
+        nfa_excluded.initial = { 0 };
+        nfa_excluded.final = { 0 };
+
+        result = get_word_from_lang_difference(nfa_included, nfa_excluded);
+        REQUIRE(result.has_value());
+        CHECK(*result == Word{ 'a' });
+    }
+
+    SECTION("included { '', 'a' }, excluded { 'a' }") {
+        nfa_included.initial = { 0 };
+        nfa_included.delta.add(0, 'a', 1);
+        nfa_included.final = { 0 };
+
+        nfa_excluded.initial = { 0 };
+        nfa_excluded.delta.add(0, 'a', 1);
+        nfa_excluded.final = { 1 };
+
+        result = get_word_from_lang_difference(nfa_included, nfa_excluded);
+        REQUIRE(result.has_value());
+        CHECK(*result == Word{});
+    }
+
+    SECTION("included { '', 'a' }, excluded { '', 'a' }") {
+        nfa_included.initial = { 0 };
+        nfa_included.delta.add(0, 'a', 1);
+        nfa_included.final = { 0, 1 };
+
+        nfa_excluded.initial = { 0 };
+        nfa_excluded.delta.add(0, 'a', 1);
+        nfa_excluded.final = { 0, 1 };
+
+        result = get_word_from_lang_difference(nfa_included, nfa_excluded);
+        CHECK(!result.has_value());
+    }
+
+    SECTION("included { '', 'a', 'ab' }, excluded { '', 'ab' }") {
+        nfa_included.initial = { 0 };
+        nfa_included.delta.add(0, 'a', 1);
+        nfa_included.delta.add(1, 'b', 2);
+        nfa_included.final = { 0, 1, 2 };
+
+        nfa_excluded.initial = { 0 };
+        nfa_excluded.delta.add(0, 'a', 1);
+        nfa_excluded.delta.add(1, 'b', 2);
+        nfa_excluded.final = { 0, 2 };
+
+        result = get_word_from_lang_difference(nfa_included, nfa_excluded);
+        REQUIRE(result.has_value());
+        CHECK(*result == Word{ 'a' });
+    }
+
+    SECTION("included { '', 'a+', 'a+b' }, excluded { '', 'ab' }") {
+        nfa_included.initial = { 0 };
+        nfa_included.delta.add(0, 'a', 1);
+        nfa_included.delta.add(1, 'a', 1);
+        nfa_included.delta.add(1, 'b', 2);
+        nfa_included.final = { 0, 1, 2 };
+
+        nfa_excluded.initial = { 0 };
+        nfa_excluded.delta.add(0, 'a', 1);
+        nfa_excluded.delta.add(1, 'b', 2);
+        nfa_excluded.final = { 0, 2 };
+
+        expected.initial = { 0 };
+        expected.delta.add(0, 'a', 1);
+        expected.delta.add(1, 'a', 1);
+        expected.delta.add(1, 'a', 2);
+        expected.delta.add(2, 'b', 3);
+        expected.final = { 1, 3 };
+
+        result = get_word_from_lang_difference(nfa_included, nfa_excluded);
+        REQUIRE(result.has_value());
+        CHECK(expected.is_in_lang(*result));
+    }
+
+    SECTION("included { '', 'ab' }, excluded { '', 'a+', 'a+b' }") {
+        nfa_included.initial = { 0 };
+        nfa_included.delta.add(0, 'a', 1);
+        nfa_included.delta.add(1, 'b', 2);
+        nfa_included.final = { 0, 2 };
+
+        nfa_excluded.initial = { 0 };
+        nfa_excluded.delta.add(0, 'a', 1);
+        nfa_excluded.delta.add(1, 'a', 1);
+        nfa_excluded.delta.add(1, 'b', 2);
+        nfa_excluded.final = { 0, 1, 2 };
+
+        result = get_word_from_lang_difference(nfa_included, nfa_excluded);
+        CHECK(!result.has_value());
+    }
+
+    SECTION("included { 'a', 'ab', '(abc)+a', '(abc)+ab' }, excluded { 'a', 'ab' }") {
+        nfa_included.initial = { 0 };
+        nfa_included.delta.add(0, 'a', 1);
+        nfa_included.delta.add(0, 'a', 2);
+        nfa_included.delta.add(0, 'a', 3);
+        nfa_included.delta.add(3, 'b', 4);
+        nfa_included.delta.add(2, 'b', 5);
+        nfa_included.delta.add(1, 'b', 6);
+        nfa_included.delta.add(6, 'c', 0);
+        nfa_included.final = { 2, 6 };
+
+        nfa_excluded.initial = { 0 };
+        nfa_excluded.delta.add(0, 'a', 1);
+        nfa_excluded.delta.add(1, 'b', 2);
+        nfa_excluded.final = { 0, 1, 2 };
+
+        expected.initial = { 0 };
+        expected.delta.add(0, 'a', 1);
+        expected.delta.add(1, 'b', 2);
+        expected.delta.add(2, 'c', 3);
+        expected.delta.add(3, 'a', 4);
+        expected.delta.add(4, 'b', 5);
+        expected.delta.add(5, 'c', 3);
+        expected.final = { 4, 5 };
+
+        result = get_word_from_lang_difference(nfa_included, nfa_excluded);
+        REQUIRE(result.has_value());
+        CHECK(expected.is_in_lang(*result));
+    }
+}
+
 TEST_CASE("mata::nfa::minimize() for profiling", "[.profiling],[minimize]") {
     Nfa aut(4);
     Nfa result;