Merge pull request #477 from VeriFIT/nft-utility-functions

Nft utility functions #patch

examples/nft-preimage.cc

@@ -0,0 +1,46 @@
+#include "mata/alphabet.hh"
+#include "mata/nfa/algorithms.hh"
+#include "mata/nft/builder.hh"
+#include "mata/nft/nft.hh"
+#include "mata/nfa/nfa.hh"
+#include "mata/nft/types.hh"
+#include "mata/parser/re2parser.hh"
+
+int main() {
+    using namespace mata;
+    using namespace mata::nft;
+    using namespace mata::nfa;
+    mata::EnumAlphabet alphabet{ 'a', 'b', 'c', 'd', 'e', 'f', 'g', 'A', 'B', 'C', 'D', 'E', 'F', 'G' };
+
+
+    Nft nft{}; // By default, has DEFAULT_NUM_OF_LEVELS tapes.
+    //Nft nft{ Nft::with_levels(3) };
+    State initial{ nft.add_state() }; // Add a new state with level 0.
+    nft.initial.insert(initial);
+    State final{ nft.add_state_with_level(0) }; // Add a new state with a manually specified level.
+    nft.final.insert(final);
+
+    // Transduce one symbol on each tape (= level).
+    State next_state{ nft.add_transition(initial, { 'a', 'A' }) };
+    // Then transduce a sequence of 'bc' to 'BC'.
+    next_state = nft.insert_word(next_state, { 'b', 'B', 'c', 'C' });
+    // Then transduce a sequence 'd' to 'DEF' (non-length-preserving operation).
+    nft.insert_word_by_parts(next_state, { { 'd' }, { 'D', 'E', 'F' } }, final);
+    // Finally, accept the same suffix on all tapes.
+    nft.insert_identity(final, &alphabet);
+    // NFT nft transduces a sequence of 'abcd' to 'ABCDEF', accepting the same suffix on all tapes.
+
+    // Create NFA from a regex, each character mapping to its UTF-8 value.
+    Nfa nfa{};
+    parser::create_nfa(&nfa, "ABCDEFggg");
+
+    // Compute the pre-image of an NFA as an NFT, identical to nft || Id(nfa).
+    Nft backward_applied_nft = nft.apply_backward(nfa);
+    // Extract a pre-image NFA for the tape 0.
+    Nfa nfa_pre_image{ project_to(backward_applied_nft, 0) };
+    // Minimize the result pre-image using hopcroft minimization.
+    nfa_pre_image = determinize(remove_epsilon(nfa_pre_image).trim());
+    assert(nfa_pre_image.is_deterministic());
+    nfa_pre_image = algorithms::minimize_hopcroft(nfa_pre_image);
+    std::cout << nfa_pre_image.print_to_dot(true) << "\n";
+}

include/mata/nft/nft.hh

@@ -264,8 +264,22 @@ public:
     * @param 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 Self with inserted identity.
     */
-    void insert_identity(State state, const std::vector<Symbol>& symbols, JumpMode jump_mode = JumpMode::RepeatSymbol);
+    Nft& insert_identity(State state, const std::vector<Symbol>& symbols, JumpMode jump_mode = JumpMode::RepeatSymbol);
+
+    /**
+    * Inserts identity transitions into the NFT.
+    *
+    * @param state The state where the identity transition will be inserted. @p state server as both the source and
+    *  target state.
+    * @param alpahbet The alphabet with symbols used for the identity transition. Identity will be created for each symbol in the @p alphabet.
+    * @param 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 Self with inserted identity.
+    */
+    Nft& insert_identity(State state, const Alphabet* alphabet, JumpMode jump_mode = JumpMode::RepeatSymbol);
 
     /**
     * Inserts an identity transition into the NFT.
@@ -276,8 +290,9 @@ public:
     * @param 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 Self with inserted identity.
     */
-    void insert_identity(State state, Symbol symbol, JumpMode jump_mode = JumpMode::RepeatSymbol);
+    Nft& insert_identity(State state, Symbol symbol, JumpMode jump_mode = JumpMode::RepeatSymbol);
 
     /**
      * @brief Clear the underlying NFT to a blank NFT.
@@ -368,13 +383,13 @@ public:
      * @param[in] ascii Whether to use ASCII characters for the output.
      * @return automaton in DOT format
      */
-    std::string print_to_DOT(bool ascii = false) const;
+    std::string print_to_dot(bool ascii = false) const;
     /**
      * @brief Prints the automaton to the output stream in DOT format
      *
      * @param[in] ascii Whether to use ASCII characters for the output.
      */
-    void print_to_DOT(std::ostream &output, bool ascii = false) const;
+    void print_to_dot(std::ostream &output, bool ascii = false) const;
     /**
      * @brief Prints the automaton in mata format
      *
@@ -441,6 +456,19 @@ public:
         const nfa::Nfa& nfa, Level level_to_apply_on = 0,
         JumpMode jump_mode = JumpMode::RepeatSymbol) const;
 
+    /**
+     * @brief Apply @p nfa to @c this backward.
+     *
+     * Identical to `this || Id(nfa)`.
+     * @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_backward(const nfa::Nfa& nfa, Level level_to_apply_on = 1, JumpMode jump_mode = JumpMode::RepeatSymbol) const;
+
     /**
      * @brief Copy NFT as NFA.
      *

src/nft/nft.cc

@@ -76,13 +76,13 @@ Nft& Nft::trim(StateRenaming* state_renaming) {
     return *this;
 }
 
-std::string Nft::print_to_DOT(const bool ascii) const {
+std::string Nft::print_to_dot(const bool ascii) const {
     std::stringstream output;
-    print_to_DOT(output, ascii);
+    print_to_dot(output, ascii);
     return output.str();
 }
 
-void Nft::print_to_DOT(std::ostream &output, const bool ascii) const {
+void Nft::print_to_dot(std::ostream &output, const bool ascii) const {
     auto translate_special_symbols = [&](const Symbol symbol) -> std::string {
         if (symbol == EPSILON) {
             return "<eps>";
@@ -405,13 +405,17 @@ State Nft::add_transition(const State source, const std::vector<Symbol>& symbols
     return insert_word(source, symbols);
 }
 
-void Nft::insert_identity(const State state, const std::vector<Symbol> &symbols, const JumpMode jump_mode) {
-    for (const Symbol symbol : symbols) {
-        insert_identity(state, symbol, jump_mode);
-    }
+Nft& Nft::insert_identity(const State state, const std::vector<Symbol> &symbols, const JumpMode jump_mode) {
+    for (const Symbol symbol: symbols) { insert_identity(state, symbol, jump_mode); }
+    return *this;
+}
+
+Nft& Nft::insert_identity(const State state, const Alphabet* alphabet, const JumpMode jump_mode) {
+    for (const Symbol symbol: alphabet->get_alphabet_symbols()) { insert_identity(state, symbol, jump_mode); }
+    return *this;
 }
 
-void Nft::insert_identity(const State state, const Symbol symbol, const JumpMode jump_mode) {
+Nft& 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?
@@ -421,6 +425,7 @@ void Nft::insert_identity(const State state, const Symbol symbol, const JumpMode
 //    } else {
         insert_word(state, Word(num_of_levels, symbol), state);
 //    }
+    return *this;
 }
 
 void Nft::clear() {

src/nft/operations.cc

@@ -352,6 +352,10 @@ Nft Nft::apply(const nfa::Nfa& nfa, Level level_to_apply_on, JumpMode jump_mode)
     return compose(nft_from_nfa, *this, static_cast<Level>(this->num_of_levels) - 1, level_to_apply_on, jump_mode);
 }
 
+Nft Nft::apply_backward(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(*this, nft_from_nfa, level_to_apply_on, 0, 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);