Merge pull request #403 from VeriFIT/apply

Apply NFA to NFT

include/mata/nft/builder.hh

@@ -100,11 +100,12 @@ Nft parse_from_mata(const std::filesystem::path& nft_file);
 /**
  * Create NFT from NFA.
  * @param nfa_state NFA to create NFT from.
- * @param level_cnt Number of levels of NFT.
+ * @param num_of_levels Number of levels of NFT.
+ * @param next_level_symbol Symbol to use on non-NFA levels. std::nullopt means using the same symbol on all levels.
  * @param epsilons Which symbols handle as epsilons.
- * @return NFT representing @p nfa_state with @p level_cnt number of levels.
+ * @return NFT representing @p nfa_state with @p num_of_levels number of levels.
  */
-Nft create_from_nfa(const mata::nfa::Nfa& nfa_state, Level level_cnt = 2, std::optional<Symbol> next_level_symbol = {}, const std::set<Symbol>& epsilons = { EPSILON });
+Nft create_from_nfa(const mata::nfa::Nfa& nfa_state, size_t num_of_levels = 2, std::optional<Symbol> next_level_symbol = {}, const std::set<Symbol>& epsilons = { EPSILON });
 
 } // namespace mata::nft::builder.
 

include/mata/nft/nft.hh

@@ -370,6 +370,67 @@ public:
      */
     std::set<Word> get_words(size_t max_length) const;
 
+    /**
+     * @brief Apply @p nfa to @c this.
+     *
+     * Identical to `Id(nfa) || this`.
+     * @param nfa NFA to apply.
+     * @param level_to_apply_on Which level to apply the @p nfa on.
+     * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+     *  is interpreted as a sequence repeating the same symbol, or as a single instance of the symbol followed by a
+     *  sequence of @c DONT_CARE symbols.
+     * @return
+     */
+    Nft apply(
+        const nfa::Nfa& nfa, Level level_to_apply_on = 0,
+        JumpMode jump_mode = JumpMode::RepeatSymbol) const;
+
+    /**
+     * @brief Copy NFT as NFA.
+     *
+     * Transitions are not updated to only have one level.
+     * @return A newly created NFA with copied members from NFT.
+     */
+    Nfa to_nfa_copy() const { return Nfa{ delta, initial, final, alphabet }; }
+
+    /**
+     * @brief Move NFT as NFA.
+     *
+     * The NFT can no longer be used.
+     * Transitions are not updated to only have one level.
+     * @return A newly created NFA with moved members from NFT.
+     */
+    Nfa to_nfa_move() { return Nfa{ std::move(delta), std::move(initial), std::move(final), alphabet }; }
+
+    /**
+     * @brief Copy NFT as NFA updating the transitions to have one level only.
+     *
+     * @param[in] dont_care_symbol_replacements Vector of symbols to replace @c DONT_CARE symbols with.
+     * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+     * is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence
+     * of @c DONT_CARE symbols.
+     * @return A newly created NFA with copied members from NFT with updated transitions.
+     */
+    Nfa to_nfa_update_copy(
+        const utils::OrdVector<Symbol>& dont_care_symbol_replacements = { DONT_CARE },
+        JumpMode jump_mode = JumpMode::RepeatSymbol
+    ) const;
+
+    /**
+     * @brief Move NFT as NFA updating the transitions to have one level only.
+     *
+     * The NFT can no longer be used.
+     * @param[in] dont_care_symbol_replacements Vector of symbols to replace @c DONT_CARE symbols with.
+     * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1)
+     * is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence
+     * of @c DONT_CARE symbols.
+     * @return A newly created NFA with moved members from NFT with updated transitions.
+     */
+    Nfa to_nfa_update_move(
+        const utils::OrdVector<Symbol>& dont_care_symbol_replacements = { DONT_CARE },
+        JumpMode jump_mode = JumpMode::RepeatSymbol
+    );
+
 }; // class Nft.
 
 // Allow variadic number of arguments of the same type.

src/nft/builder.cc

@@ -296,11 +296,11 @@ Nft builder::parse_from_mata(const std::string& nft_in_mata) {
     return parse_from_mata(nft_stream);
 }
 
-Nft builder::create_from_nfa(const mata::nfa::Nfa& nfa, Level level_cnt, std::optional<Symbol> next_level_symbol, const std::set<Symbol>& epsilons) {
-    const Level num_of_additional_states_per_nfa_trans{ level_cnt - 1 };
+Nft builder::create_from_nfa(const mata::nfa::Nfa& nfa, const size_t num_of_levels, std::optional<Symbol> next_level_symbol, const std::set<Symbol>& epsilons) {
+    const Level num_of_additional_states_per_nfa_trans{ static_cast<Level>(num_of_levels) - 1 };
     Nft nft{};
     size_t nfa_num_of_states{ nfa.num_of_states() };
-    nft.num_of_levels = level_cnt;
+    nft.num_of_levels = num_of_levels;
     nft.levels.resize(nfa_num_of_states + nfa.delta.num_of_transitions() * num_of_additional_states_per_nfa_trans);
     std::unordered_map<State, State> state_mapping{};
     state_mapping.reserve(nfa_num_of_states);

src/nft/nft.cc

@@ -403,6 +403,7 @@ void Nft::insert_identity(const State state, const std::vector<Symbol> &symbols,
 }
 
 void Nft::insert_identity(const State state, const Symbol symbol, const JumpMode jump_mode) {
+    (void)jump_mode;
     // TODO(nft): Evaluate the performance difference between adding a jump transition and inserting a transition for each level.
     // FIXME(nft): Allow symbol jump transitions?
 //    if (jump_mode == JumpMode::RepeatSymbol) {
@@ -427,3 +428,14 @@ Levels& Levels::set(State state, Level level) {
     (*this)[state] = level;
     return *this;
 }
+
+mata::nfa::Nfa Nft::to_nfa_update_copy(
+    const utils::OrdVector<Symbol>& dont_care_symbol_replacements, const JumpMode jump_mode) const {
+    return get_one_level_aut(dont_care_symbol_replacements, jump_mode).to_nfa_copy();
+}
+
+mata::nfa::Nfa Nft::to_nfa_update_move(
+    const utils::OrdVector<Symbol>& dont_care_symbol_replacements, const JumpMode jump_mode) {
+    make_one_level_aut(dont_care_symbol_replacements, jump_mode);
+    return to_nfa_move();
+}

src/nft/operations.cc

@@ -13,12 +13,15 @@
 #include "mata/nft/nft.hh"
 #include "mata/nft/algorithms.hh"
 #include "mata/nft/builder.hh"
+#include "mata/nft/strings.hh"
 #include <mata/simlib/explicit_lts.hh>
 
 using std::tie;
 
 using namespace mata::utils;
 using namespace mata::nft;
+using namespace mata::nfa;
+using namespace mata;
 using mata::Symbol;
 
 using StateBoolArray = std::vector<bool>; ///< Bool array for states in the automaton.
@@ -344,6 +347,12 @@ Nft mata::nft::project_to(const Nft& nft, Level level_to_project, const JumpMode
     return project_to(nft, OrdVector<Level>{ level_to_project }, jump_mode);
 }
 
+Nft Nft::apply(const nfa::Nfa& nfa, Level level_to_apply_on, JumpMode jump_mode) const {
+    Nft nft_from_nfa{ nft::builder::create_from_nfa(nfa, this->num_of_levels) };
+    return compose(nft_from_nfa, *this, static_cast<Level>(this->num_of_levels) - 1, level_to_apply_on, jump_mode);
+}
+
+
 Nft mata::nft::insert_levels(const Nft& nft, const BoolVector& new_levels_mask, const JumpMode jump_mode) {
     assert(0 < nft.num_of_levels);
     assert(nft.num_of_levels <= new_levels_mask.size());

tests/nft/nft.cc

@@ -14,6 +14,7 @@
 #include "mata/nft/builder.hh"
 #include "mata/nft/plumbing.hh"
 #include "mata/nft/algorithms.hh"
+#include "mata/nfa/nfa.hh"
 #include "mata/parser/re2parser.hh"
 
 using namespace mata;
@@ -4883,3 +4884,41 @@ TEST_CASE("mata::nft::Nft::insert_word_by_parts()") {
         }
     }
 }
+
+TEST_CASE("mata::nft::Nft::apply()") {
+    SECTION("replace reluctant regex NFT") {
+        Nfa nfa{};
+        parser::create_nfa(&nfa, "da+b+ce");
+        mata::EnumAlphabet alphabet{ 'a', 'b', 'c', 'd', 'e', 'f' };
+        Nft nft{ nft::strings::replace_reluctant_regex("a+b+c", { 'f' }, &alphabet) };
+        Nft nft_applied_nfa{ nft.apply(nfa, 0) };
+        Nfa result{ project_to(nft_applied_nfa, 1).to_nfa_move() };
+        result.remove_epsilon();
+        result.trim();
+        Nfa expected{};
+        expected.initial.insert(0);
+        expected.delta.add(0, 'd', 1);
+        expected.delta.add(1, 'f', 2);
+        expected.delta.add(2, 'e', 3);
+        expected.final.insert(3);
+        CHECK(nfa::are_equivalent(result, expected));
+    }
+
+    SECTION("replace reluctant literal NFT") {
+        Nfa nfa{};
+        parser::create_nfa(&nfa, "dabce");
+        mata::EnumAlphabet alphabet{ 'a', 'b', 'c', 'd', 'e', 'f' };
+        Nft nft{ nft::strings::replace_reluctant_literal({'a', 'b', 'c' }, { 'f' }, &alphabet) };
+        Nft nft_applied_nfa{ nft.apply(nfa, 0) };
+        Nfa result{ project_to(nft_applied_nfa, 1).to_nfa_move() };
+        result.remove_epsilon();
+        result.trim();
+        Nfa expected{};
+        expected.initial.insert(0);
+        expected.delta.add(0, 'd', 1);
+        expected.delta.add(1, 'f', 2);
+        expected.delta.add(2, 'e', 3);
+        expected.final.insert(3);
+        CHECK(nfa::are_equivalent(result, expected));
+    }
+}