diff --git a/examples/nft-preimage.cc b/examples/nft-preimage.cc new file mode 100644 index 000000000..03713fa1b --- /dev/null +++ b/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"; +} diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index 7c2609379..2aa147cd1 100644 --- a/include/mata/nft/nft.hh +++ b/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& symbols, JumpMode jump_mode = JumpMode::RepeatSymbol); + Nft& insert_identity(State state, const std::vector& 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. * diff --git a/src/nft/nft.cc b/src/nft/nft.cc index 8bcabb42b..61d115104 100644 --- a/src/nft/nft.cc +++ b/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 ""; @@ -405,13 +405,17 @@ State Nft::add_transition(const State source, const std::vector& symbols return insert_word(source, symbols); } -void Nft::insert_identity(const State state, const std::vector &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 &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() { diff --git a/src/nft/operations.cc b/src/nft/operations.cc index c5b1b39ba..a9302e185 100644 --- a/src/nft/operations.cc +++ b/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(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);