Create Nft with inverted levels (tapes)

include/mata/nfa/delta.hh

@@ -135,6 +135,11 @@ public:
     ///returns an iterator to the smallest epsilon, or end() if there is no epsilon
     const_iterator first_epsilon_it(Symbol first_epsilon) const;
 
+    /**
+     * @brief Get the set of all target states in the @c StatePost.
+     * @return Set of all target states in the @c StatePost.
+     */
+    StateSet get_successors() const;
 
     /**
      * @brief Iterator over moves represented as @c Move instances.
@@ -166,7 +171,7 @@ public:
         StatePost::const_iterator symbol_post_it_{}; ///< Current symbol post iterator to iterate over.
         /// End symbol post iterator which is no longer iterated over (one after the last symbol post iterated over or
         ///  end()).
-        StatePost::const_iterator symbol_post_end_{}; 
+        StatePost::const_iterator symbol_post_end_{};
     }; // class Moves.
 
     /**
@@ -221,7 +226,7 @@ public:
     /// Const all moves iterator.
     const_iterator(const StatePost& state_post);
     /// Construct iterator from @p symbol_post_it (including) to @p symbol_post_it_end (excluding).
-    const_iterator(const StatePost& state_post, StatePost::const_iterator symbol_post_it, 
+    const_iterator(const StatePost& state_post, StatePost::const_iterator symbol_post_it,
                    StatePost::const_iterator symbol_post_it_end);
     const_iterator(const const_iterator& other) noexcept = default;
     const_iterator(const_iterator&&) = default;
@@ -457,6 +462,23 @@ public:
      */
     std::vector<Transition> get_transitions_to(State state_to) const;
 
+    /**
+     * Get transitions from @p state_from to @p state_to.
+     * @param state_from[in] Source state.
+     * @param state_from[in] Target state.
+     * @return Transitions from @p source to @p state_to.
+     *
+     * Operation is slow, traverses over all symbol posts.
+     */
+    std::vector<Transition> get_transitions_between(State state_from, State state_to) const;
+
+    /**
+     * Get the set of states that are successors of the given @p state.
+     * @param[in] state State from which successors are checked.
+     * @return Set of states that are successors of the given @p state.
+     */
+    StateSet get_successors(State state) const;
+
     /**
      * Iterate over @p epsilon symbol posts under the given @p state.
      * @param[in] state State from which epsilon transitions are checked.

include/mata/nft/nft.hh

@@ -67,6 +67,13 @@ public:
      * @param[in] levels_vector Vector of levels to be appended.
      */
     void append(const Levels& levels_vector) { for (const Level& level: levels_vector) { push_back(level); } }
+
+    /**
+     * @brief Count the number of occurrences of a level in @c this.
+     *
+     * @param[in] level Level to be counted.
+     */
+    size_t count(Level level) const { return static_cast<size_t>(std::count(begin(), end(), level)); }
 };
 
 /**
@@ -167,6 +174,12 @@ public:
      */
     State add_state_with_level(State state, Level level);
 
+    /**
+     * Get the number of states with level @p level.
+     * @return The number of states with level @p level.
+     */
+    size_t num_of_states_with_level(Level level) const;
+
     /**
      * Inserts a @p word into the NFT from a source state @p source to a target state @p target.
      * Creates new states along the path of the @p word.
@@ -759,6 +772,20 @@ Nft simple_revert(const Nft& aut);
 //  dense automata, where it is almost as slow as simple_revert. Candidate for removal.
 Nft somewhat_simple_revert(const Nft& aut);
 
+/**
+ * @brief Inverts the levels of the given transducer @p aut.
+ *
+ * The function inverts the levels of the transducer, i.e., the level 0 becomes the last level, level 1 becomes the
+ * second last level, and so on.
+ *
+ * @param[in] aut The transducer for inverting levels.
+ * @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 new transducer with inverted levels.
+ */
+Nft invert_levels(const Nft& aut, JumpMode jump_mode = JumpMode::RepeatSymbol);
+
 // Removing epsilon transitions
 Nft remove_epsilon(const Nft& aut, Symbol epsilon = EPSILON);
 

src/nfa/delta.cc

@@ -61,6 +61,18 @@ StatePost::const_iterator Delta::epsilon_symbol_posts(const StatePost& state_pos
     return state_post.end();
 }
 
+StateSet StatePost::get_successors() const {
+    StateSet successors;
+    for (const SymbolPost& symbol_post: *this) {
+        successors.insert(symbol_post.targets);
+    }
+    return successors;
+}
+
+StateSet Delta::get_successors(const State state) const {
+    return state_post(state).get_successors();
+}
+
 std::vector<Transition> Delta::get_transitions_to(const State state_to) const {
     std::vector<Transition> transitions_to_state{};
     const size_t num_of_states{ this->num_of_states() };
@@ -75,6 +87,17 @@ std::vector<Transition> Delta::get_transitions_to(const State state_to) const {
     return transitions_to_state;
 }
 
+std::vector<Transition> Delta::get_transitions_between(const State state_from, const State state_to) const {
+    std::vector<Transition> transitions_between{};
+    for (const SymbolPost& symbol_post: state_post(state_from)) {
+        const StateSet::const_iterator state_to_find_it = symbol_post.targets.find(state_to);
+        if (state_to_find_it != symbol_post.targets.end()) {
+            transitions_between.push_back({ state_from, symbol_post.symbol, state_to });
+        }
+    }
+    return transitions_between;
+}
+
 void Delta::add(const State source, Symbol symbol, const State target) {
     if (const State max_state{ std::max(source, target) }; max_state >= state_posts_.size()) {
         reserve_on_insert(state_posts_, max_state);

src/nft/nft.cc

@@ -23,6 +23,10 @@ using StateBoolArray = std::vector<bool>; ///< Bool array for states in the auto
 const std::string mata::nft::TYPE_NFT = "NFT";
 
 
+size_t Nft::num_of_states_with_level(const Level level) const {
+    return levels.count(level);
+}
+
 Nft& Nft::trim(StateRenaming* state_renaming) {
 
 #ifdef _STATIC_STRUCTURES_

src/nft/operations.cc

@@ -677,6 +677,136 @@ Nft mata::nft::revert(const Nft& aut) {
     //return somewhat_simple_revert(aut);
 }
 
+Nft mata::nft::invert_levels(const Nft& aut, const JumpMode jump_mode) {
+    const size_t num_of_states = aut.num_of_states();
+
+    // Find states with level zero and rename them.
+    std::vector<State> renaming(num_of_states, Limits::max_state);
+    size_t num_of_zerostates = 0;
+    for (State s = 0; s < num_of_states; ++s) {
+        if (aut.levels[s] == 0) {
+            renaming[s] = num_of_zerostates++;
+        }
+    }
+
+    // Rename initial states
+    SparseSet<State> new_initial;
+    for (const State s: aut.initial) {
+        new_initial.insert(renaming[s]);
+    }
+    // Rename final states
+    SparseSet<State> new_final;
+    for (const State s: aut.final) {
+        new_final.insert(renaming[s]);
+    }
+    // Create new automaton
+    Nft aut_inv = Nft(num_of_zerostates, std::move(new_initial), std::move(new_final), Levels(num_of_zerostates, 0), aut.num_of_levels, aut.alphabet);
+
+    // Creates new states with inverted levels for each inner state in the path.
+    auto create_states_with_inverted_levels = [&](const std::vector<State>& path_states) {
+        for (const State s: path_states) {
+            if (aut.levels[s] == 0) { continue; }
+            renaming[s] = aut_inv.add_state_with_level(static_cast<Level>(aut.num_of_levels - aut.levels[s]));
+        }
+    };
+
+    // Returns transitions of the path.
+    auto get_path_transitions = [&](const std::vector<State>& path_states) {
+        std::vector<Transition> path_transitions;
+        for (size_t i = 0; i < path_states.size() - 1; ++i) {
+            const State src = path_states[i];
+            const State trg = path_states[i + 1];
+            std::vector<Transition> transitions_between = aut.delta.get_transitions_between(src, trg);
+            path_transitions.insert(path_transitions.end(), transitions_between.begin(), transitions_between.end());
+        }
+
+        return path_transitions;
+    };
+
+    // Creates inverted transitions for each transition in the path.
+    // Can work with different jump modes.
+    auto map_inverted_transitions = [&](const std::vector<Transition>& path, const State head, const State tail) {
+        for (const auto &[src, symbol, trg]: path) {
+            const bool is_src_head = src == head;
+            const bool is_trg_tail = trg == tail;
+            if (is_src_head && is_trg_tail) {
+                // It is a direct transition between two zero-states (the head and the tail).
+                // Just copy it.
+                if (jump_mode == JumpMode::AppendDontCares && aut.num_of_levels > 1) {
+                    const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut.num_of_levels - 1));
+                    aut_inv.delta.add(renaming[src], DONT_CARE, aux_state);
+                    aut_inv.delta.add(aux_state, symbol, renaming[trg]);
+                } else {
+                    aut_inv.delta.add(renaming[src], symbol, renaming[trg]);
+                }
+            } else if (is_src_head) {
+                // It is a transition from a zero-state (head) to a nonzero-state (inner state).
+                // Map it as transition from that nonzero-state (inner state) to the tail (zero-states).
+                if (jump_mode == JumpMode::AppendDontCares && aut.levels[trg] > 1) {
+                    const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut.num_of_levels - 1));
+                    aut_inv.delta.add(renaming[trg], DONT_CARE, aux_state);
+                    aut_inv.delta.add(aux_state, symbol, renaming[tail]);
+                } else {
+                    aut_inv.delta.add(renaming[trg], symbol, renaming[tail]);
+                }
+
+            } else if (is_trg_tail) {
+                // It is a transition from a nonzero-state (inner state) to a zero-state (tail).
+                // Map it as transition from the zero-state (head) to that nonzero-state (inner state).
+                if (jump_mode == JumpMode::AppendDontCares && (aut.num_of_levels - aut.levels[src]) > 1) {
+                    const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut_inv.levels[renaming[src]] - 1));
+                    aut_inv.delta.add(renaming[head], DONT_CARE, aux_state);
+                    aut_inv.delta.add(aux_state, symbol, renaming[src]);
+                } else {
+                    aut_inv.delta.add(renaming[head], symbol, renaming[src]);
+                }
+            } else {
+                // It is a transition between two nonzero-states (inner states).
+                // Just swap the source and target.
+                if (jump_mode == JumpMode::AppendDontCares && (aut.levels[trg] - aut.levels[src]) > 1) {
+                    const State aux_state = aut_inv.add_state_with_level(static_cast<Level>(aut_inv.levels[renaming[src]] - 1));
+                    aut_inv.delta.add(renaming[trg], DONT_CARE, aux_state);
+                    aut_inv.delta.add(aux_state, symbol, renaming[src]);
+                } else {
+                    aut_inv.delta.add(renaming[trg], symbol, renaming[src]);
+                }
+            }
+        }
+    };
+
+    // Main loop of the algorithm.
+    for (State path_head = 0; path_head < num_of_states; ++path_head) {
+        // Test if the state is a head of some path.
+        if (aut.levels[path_head] != 0) {
+            continue;   // Not a head.
+        }
+        // Process all paths using dfs.
+        std::stack<std::pair<State, std::vector<State>>> stack;
+        stack.push({ path_head, { path_head } });
+        while (!stack.empty()) {
+            auto [src, path] = stack.top();
+            stack.pop();
+
+            if (aut.levels[src] == 0 && path.size() > 1) {
+                // A tail of the path (src) has been reached.
+                create_states_with_inverted_levels(path);
+                const std::vector<Transition> path_transitions = get_path_transitions(path);
+                map_inverted_transitions(path_transitions, path.front(), path.back());
+                continue;
+            }
+
+            for (const State trg: aut.delta[src].get_successors()) {
+                // Extend the path.
+                std::vector<State> new_path = path;
+                new_path.push_back(trg);
+                stack.push({ trg, std::move(new_path) });
+            }
+        }
+    }
+
+    return aut_inv;
+}
+
 std::pair<Run, bool> mata::nft::Nft::get_word_for_path(const Run& run) const {
     if (run.path.empty()) { return {{}, true}; }